Commit 8568c3b4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

postproc: integrate tgba_determinize()

* spot/twa/acc.hh: Add a smaller version of is_parity().
* spot/twaalgos/postproc.cc: Call tgba_determinize() if asked for
Generic acceptance and Deterministic output.
* bin/common_post.cc: Add 'G' as a shorthand for --generic.
* doc/org/ltl2tgba.org: Illustrate =ltl2tgba -G -D=.
parent 03d9a751
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -32,8 +32,7 @@ bool level_set = false;
bool pref_set = false;
enum {
OPT_GENERIC = 1,
OPT_HIGH,
OPT_HIGH = 1,
OPT_LOW,
OPT_MEDIUM,
OPT_SMALL,
......@@ -44,6 +43,8 @@ static const argp_option options[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output automaton type:", 2 },
{ "generic", 'G', nullptr, 0,
"any acceptance condition is allowed", 0 },
{ "tgba", OPT_TGBA, nullptr, 0,
"Transition-based Generalized Büchi Automaton (default)", 0 },
{ "ba", 'B', nullptr, 0,
......@@ -57,7 +58,9 @@ static const argp_option options[] =
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 },
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata "
"(combine with --generic to be sure to obtain a deterministic "
"automaton)", 0 },
{ "any", 'a', nullptr, 0, "no preference, do not bother making it small "
"or deterministic", 0 },
/**************************************************/
......@@ -73,7 +76,7 @@ static const argp_option options_disabled[] =
{
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output automaton type:", 2 },
{ "generic", OPT_GENERIC, nullptr, 0,
{ "generic", 'G', nullptr, 0,
"any acceptance is allowed (default)", 0 },
{ "tgba", OPT_TGBA, nullptr, 0,
"Transition-based Generalized Büchi Automaton", 0 },
......@@ -88,7 +91,9 @@ static const argp_option options_disabled[] =
/**************************************************/
{ nullptr, 0, nullptr, 0, "Simplification goal:", 20 },
{ "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 },
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 },
{ "deterministic", 'D', nullptr, 0, "prefer deterministic automata "
"(combine with --generic to be sure to obtain a deterministic "
"automaton)", 0 },
{ "any", 'a', nullptr, 0, "no preference, do not bother making it small "
"or deterministic", 0 },
/**************************************************/
......@@ -120,15 +125,15 @@ parse_opt_post(int key, char*, struct argp_state*)
pref = spot::postprocessor::Deterministic;
pref_set = true;
break;
case 'G':
type = spot::postprocessor::Generic;
break;
case 'M':
type = spot::postprocessor::Monitor;
break;
case 'S':
sbacc = spot::postprocessor::SBAcc;
break;
case OPT_GENERIC:
type = spot::postprocessor::Generic;
break;
case OPT_HIGH:
level = spot::postprocessor::High;
simplification_level = 3;
......
......@@ -3,11 +3,22 @@
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool translates LTL or PSL formulas into two kinds of Büchi
automata, or to monitors. The default is to output Transition-based
Generalized Büchi Automata (hereinafter abbreviated TGBA), but more
traditional Büchi automata (BA) may be requested using the =-B=
option.
This tool translates LTL or PSL formulas into different types of
automata.
The inner algorithm produces Transition-based Generalized Büchi
Automata, hence the name of the tools, but =ltl2tgba= has grown and
now offers several options to adjust the type of automaton output.
Those options will be covered in more detail below, but here is
a quick summary:
- =--tgba= (the default) outputs Transition-based Generalized
Büchi Automata
- =--ba= (or =-B=) outputs state-based Büchi automata
- =--monitor= (or =-M=) outputs Monitors
- =--generic --deterministic= (or =-GD=) will do whatever it takes to
produce a deterministic automaton, and may output generalized Büchi,
or parity acceptance.
* TGBA and BA
......@@ -448,6 +459,13 @@ Note that options =--deterministic= and =--small= express
/preferences/. They certainly do /not/ guarantee that the output will
be deterministic, or will be the smallest automaton possible.
In particular, for properties more complex than obligations, it is
possible that no deterministic TGBA exist, and even if it exists,
=ltl2tgba= might not find it: so a non-deterministic automaton can be
returned in this case. If you absolutely want a deterministic
automaton, [[#generic][read on about the =--generic= option below]].
An example formula where the difference between =-D= and =--small= is
flagrant is =Ga|Gb|Gc=:
......@@ -697,6 +715,49 @@ to experiment with the different settings on a small version of the
pattern, and select the lowest setting that satisfies your
expectations.
* Deterministic automata with =--generic=
:PROPERTIES:
:CUSTOM_ID: generic
:END:
The =--generic= (or =-G=) option allows =ltl2tgba= to use more
complex acceptance. Combined with =--deterministic= (or =-D=) this
allows the use of a determinization algorithm that produce automata
with parity acceptance.
For instance =FGa= is the typical formula for which not
deterministic TGBA exists.
#+NAME: ltl2tgba-fga
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba "FGa" -D -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fga.png :cmdline -Tpng :var txt=ltl2tgba-fga :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-fga.png]]
But with =--generic=, =ltl2tgba= will output the following Rabin automaton:
#+NAME: ltl2tgba-fga-D
#+BEGIN_SRC sh :results verbatim :exports none
ltl2tgba "FGa" -G -D -d.a
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fga-D.png :cmdline -Tpng :var txt=ltl2tgba-fga-D :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:ltl2tgba-fga-D.png]]
Note that determinization algorithm implemented actually outputs
parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as
=Rabin 1= or =parity min odd 2=.
* Translating multiple formulas for statistics
If multiple formulas are given to =ltl2tgba=, the corresponding
......
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
// l'Epita.
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
// Développement de l'Epita.
//
// This file is part of Spot, a model checking library.
//
......@@ -1040,6 +1040,12 @@ namespace spot
// check whether the condition is logically equivalent to some
// parity acceptance condition.
bool is_parity(bool& max, bool& odd, bool equiv = false) const;
bool is_parity() const
{
bool max;
bool min;
return is_parity(max, min);
}
// Return (true, m) if there exist some acceptance mark m that
// does not satisfy the acceptance condition. Return (false, 0U)
......
......@@ -33,6 +33,7 @@
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sepsets.hh>
#include <spot/twaalgos/determinize.hh>
namespace spot
{
......@@ -175,27 +176,25 @@ namespace spot
if (type_ == BA || SBACC_)
state_based_ = true;
bool tgb_used = false;
if (type_ != Generic && !a->acc().is_generalized_buchi())
{
a = to_generalized_buchi(a);
tgb_used = true;
if (PREF_ == Any && level_ == Low)
a = do_scc_filter(a, true);
}
if (PREF_ == Any && level_ == Low)
if (type_ == Generic
|| type_ == TGBA
|| (type_ == BA && a->is_sba())
|| (type_ == Monitor && a->num_sets() == 0))
{
if (tgb_used)
a = do_scc_filter(a, true);
if (COMP_)
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
}
if (PREF_ == Any && level_ == Low
&& (type_ == Generic
|| type_ == TGBA
|| (type_ == BA && a->is_sba())
|| (type_ == Monitor && a->num_sets() == 0)))
{
if (COMP_)
a = complete(a);
if (SBACC_)
a = sbacc(a);
return a;
}
int original_acc = a->num_sets();
......@@ -365,14 +364,26 @@ namespace spot
}
}
if (PREF_ == Deterministic && type_ == Generic && !dba)
{
dba = tgba_determinize(to_generalized_buchi(sim));
if (level_ != Low)
dba = simulation(dba);
sim = nullptr;
}
// Now dba contains either the result of WDBA-minimization (in
// that case dba_is_wdba=true), or some deterministic automaton
// that is either the result of the simulation or of the
// TBA-determinization (dba_is_wdba=false in both cases). If the
// dba is a WDBA, we do not have to run SAT-minimization. A
// negative value in sat_minimize_ can for its use for debugging.
// TBA-determinization (dba_is_wdba=false in both cases), or a
// parity automaton coming from tgba_determinize(). If the dba is
// a WDBA, we do not have to run SAT-minimization. A negative
// value in sat_minimize_ can force its use for debugging.
if (sat_minimize_ && dba && (!dba_is_wdba || sat_minimize_ < 0))
{
if (type_ == Generic)
throw std::runtime_error
("postproc() no yet updated to mix sat-minimize and Generic");
unsigned target_acc;
if (type_ == BA)
target_acc = 1;
......@@ -393,10 +404,8 @@ namespace spot
// because the input TBA might be smaller.
if (state_based_)
in = degeneralize(dba);
else if (dba->num_sets() != 1)
in = degeneralize_tba(dba);
else
in = dba;
in = degeneralize_tba(dba);
}
else
{
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment