Commit 1ab46b08 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

postproc: Add option to output Complete automata.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Tweak set_pref()
to also accept Any|Complete, Small|Complete, or Deterministic|Complete.
* src/bin/common_post.hh, src/bin/common_post.cc: Add option --complete
and set comp.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Pass
comp to set_pref().
* src/tgbaalgos/complete.cc: Preserve state-based acceptance.
* src/tgbatest/dstar.test, src/tgbatest/ltlcross2.test,
src/tgbatest/nondet.test: Augment tests.
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, NEWS: Document.
parent b31facff
...@@ -58,14 +58,18 @@ New in spot 1.1.4a (not relased) ...@@ -58,14 +58,18 @@ New in spot 1.1.4a (not relased)
number of seconds spent building the output automaton (excluding number of seconds spent building the output automaton (excluding
the time spent parsing the input). the time spent parsing the input).
- ltl2tgba and dstar2tgba can use a SAT-solver to minimize - ltl2tgba, ltl2tgta, and dstar2tgba have a --complete option
deterministic automata. Doing so is only needed on properties to output complete automata.
that are stronger than obligations (for which our
- ltl2tgba, ltl2tgta, and dstar2tgba can use a SAT-solver to
minimize deterministic automata. Doing so is only needed on
properties that are stronger than obligations (for which our
WDBA-minimization procedure will return a minimimal WDBA-minimization procedure will return a minimimal
deterministic automaton more efficiently) and is disabled by deterministic automaton more efficiently) and is disabled by
default. See the spot-x(7) man page for documentation about the default. See the spot-x(7) man page for documentation about the
related options: sat-minimize, sat-states, sat-acc, state-based. related options: sat-minimize, sat-states, sat-acc, state-based.
* New functions and classes in the library: * New functions and classes in the library:
- dtba_sat_synthetize(): Use a SAT-solver to build an equivalent - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent
...@@ -138,6 +142,10 @@ New in spot 1.1.4a (not relased) ...@@ -138,6 +142,10 @@ New in spot 1.1.4a (not relased)
effectively perform a DFS. As a consequence, it does not effectively perform a DFS. As a consequence, it does not
inherit anymore from tgba_reachable_iterator. inherit anymore from tgba_reachable_iterator.
- postproc::set_pref() was used to accept an argument among Any,
Small or Deterministic. These can now be combined with Complete
as Any|Complete, Small|Complete, or Deterministic|Complete.
- All the parsers implemented in Spot now use the same type to - All the parsers implemented in Spot now use the same type to
store locations. store locations.
......
...@@ -274,6 +274,8 @@ dstar2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' ...@@ -274,6 +274,8 @@ dstar2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: -a, --any no preference : -a, --any no preference
: -C, --complete output a complete automaton (combine with other
: intents)
: -D, --deterministic prefer deterministic automata : -D, --deterministic prefer deterministic automata
: --small prefer small automata (default) : --small prefer small automata (default)
...@@ -327,8 +329,8 @@ For instance here is a complex command that will ...@@ -327,8 +329,8 @@ For instance here is a complex command that will
The statistics displayed in this case are: =%S=, the number of states The statistics displayed in this case are: =%S=, the number of states
of the input (Rabin) automaton, =%s=, the number of states of the of the input (Rabin) automaton, =%s=, the number of states of the
output (Büchi) automaton, and =%d=, whether the output automaton is output (Büchi) automaton, =%d=, whether the output automaton is
deterministic or not. deterministic, and =%p= whether the automaton is complete.
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 --tree-size=10..15 a b c | randltl -n -1 --tree-size=10..15 a b c |
...@@ -338,40 +340,42 @@ while read f; do ...@@ -338,40 +340,42 @@ while read f; do
echo "$f" echo "$f"
ltlfilt -l -f "$f" | ltlfilt -l -f "$f" |
ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - - | ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-sD - - |
dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d' dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
done done
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
F(a | !b) F(a | !b)
DRA: 2st.; BA: 2st.; det.? 1 DRA: 2st.; BA: 2st.; det.? 1; complete? 1
Fa | (Xc U (c & Xc)) Fa | (Xc U (c & Xc))
DRA: 5st.; BA: 5st.; det.? 1 DRA: 5st.; BA: 5st.; det.? 1; complete? 1
X(((!b & XGc) | (b & XF!c)) U (!a & ((!b & XGc) | (b & XF!c)))) X(((!b & XGc) | (b & XF!c)) U (!a & ((!b & XGc) | (b & XF!c))))
DRA: 8st.; BA: 7st.; det.? 1 DRA: 8st.; BA: 7st.; det.? 1; complete? 0
!b | !a !b | !a
DRA: 3st.; BA: 2st.; det.? 1 DRA: 3st.; BA: 2st.; det.? 1; complete? 0
F!a F!a
DRA: 2st.; BA: 2st.; det.? 1 DRA: 2st.; BA: 2st.; det.? 1; complete? 1
F(Ga R (b | Ga)) F(Ga R (b | Ga))
DRA: 10st.; BA: 10st.; det.? 0 DRA: 10st.; BA: 10st.; det.? 0; complete? 0
!c U (!c & !a) !c U (!c & !a)
DRA: 3st.; BA: 2st.; det.? 1 DRA: 3st.; BA: 2st.; det.? 1; complete? 0
!c | FGb !c | FGb
DRA: 4st.; BA: 5st.; det.? 0 DRA: 4st.; BA: 5st.; det.? 0; complete? 0
G(c U a) G(c U a)
DRA: 4st.; BA: 3st.; det.? 1 DRA: 4st.; BA: 3st.; det.? 1; complete? 0
c & Gb c & Gb
DRA: 3st.; BA: 2st.; det.? 1 DRA: 3st.; BA: 2st.; det.? 1; complete? 0
#+end_example #+end_example
An important point you should be aware of when comparing these numbers An important point you should be aware of when comparing these numbers
of states is that the deterministic automata produced by =ltl2dstar= of states is that the deterministic automata produced by =ltl2dstar=
are complete, while the automata produced by =dstar2tgba= are complete, while the automata produced by =dstar2tgba=
(deterministic or not) are not complete. This can explain a (deterministic or not) are not complete by default. This can explain
difference of one state (the "sink" state, which is not output by a difference of one state (the so called "sink" state).
=dstar2tgba=).
You can instruct =dstar2tgba= to output a complete automaton using the
=--complete= option (or =-C= for short).
** Conversion from Rabin and Streett to TGBA ** Conversion from Rabin and Streett to TGBA
......
...@@ -319,6 +319,8 @@ ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' ...@@ -319,6 +319,8 @@ ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d'
#+END_SRC #+END_SRC
#+RESULTS: #+RESULTS:
: -a, --any no preference : -a, --any no preference
: -C, --complete output a complete automaton (combine with other
: intents)
: -D, --deterministic prefer deterministic automata : -D, --deterministic prefer deterministic automata
: --small prefer small automata (default) : --small prefer small automata (default)
...@@ -473,6 +475,11 @@ You can augment the number of terms in the disjunction to magnify the ...@@ -473,6 +475,11 @@ You can augment the number of terms in the disjunction to magnify the
difference. For N terms, the =--small= automaton has N+1 states, difference. For N terms, the =--small= automaton has N+1 states,
while the =--deterministic= automaton needs 2^N-1 states. while the =--deterministic= automaton needs 2^N-1 states.
Add the =--complete= option if you want to obtain a complete
automaton, with a sink state capturing that rejected words that would
not otherwise have a run in the output automaton.
A last parameter that can be used to tune the translation is the amount A last parameter that can be used to tune the translation is the amount
of pre- and post-processing performed. These two steps can be adjusted of pre- and post-processing performed. These two steps can be adjusted
via a common set of switches: via a common set of switches:
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de // Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -23,6 +23,7 @@ ...@@ -23,6 +23,7 @@
spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_type type = spot::postprocessor::TGBA;
spot::postprocessor::output_pref pref = spot::postprocessor::Small; spot::postprocessor::output_pref pref = spot::postprocessor::Small;
spot::postprocessor::output_pref comp = spot::postprocessor::Any;
spot::postprocessor::optimization_level level = spot::postprocessor::High; spot::postprocessor::optimization_level level = spot::postprocessor::High;
#define OPT_SMALL 1 #define OPT_SMALL 1
...@@ -37,6 +38,8 @@ static const argp_option options[] = ...@@ -37,6 +38,8 @@ static const argp_option options[] =
{ "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 },
{ "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 }, { "deterministic", 'D', 0, 0, "prefer deterministic automata", 0 },
{ "any", 'a', 0, 0, "no preference", 0 }, { "any", 'a', 0, 0, "no preference", 0 },
{ "complete", 'C', 0, 0, "output a complete automaton (combine "
"with other intents)", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "Optimization level:", 21 }, { 0, 0, 0, 0, "Optimization level:", 21 },
{ "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 },
...@@ -55,6 +58,9 @@ parse_opt_post(int key, char*, struct argp_state*) ...@@ -55,6 +58,9 @@ parse_opt_post(int key, char*, struct argp_state*)
case 'a': case 'a':
pref = spot::postprocessor::Any; pref = spot::postprocessor::Any;
break; break;
case 'C':
comp = spot::postprocessor::Complete;
break;
case 'D': case 'D':
pref = spot::postprocessor::Deterministic; pref = spot::postprocessor::Deterministic;
break; break;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement de // Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -28,6 +28,7 @@ extern const struct argp post_argp; ...@@ -28,6 +28,7 @@ extern const struct argp post_argp;
extern spot::postprocessor::output_type type; extern spot::postprocessor::output_type type;
extern spot::postprocessor::output_pref pref; extern spot::postprocessor::output_pref pref;
extern spot::postprocessor::output_pref comp;
extern spot::postprocessor::optimization_level level; extern spot::postprocessor::optimization_level level;
#endif // SPOT_BIN_COMMON_FINPUT_HH #endif // SPOT_BIN_COMMON_FINPUT_HH
...@@ -373,7 +373,7 @@ main(int argc, char** argv) ...@@ -373,7 +373,7 @@ main(int argc, char** argv)
jobs.push_back(job("-", true)); jobs.push_back(job("-", true));
spot::postprocessor post(&extra_options); spot::postprocessor post(&extra_options);
post.set_pref(pref); post.set_pref(pref | comp);
post.set_type(type); post.set_type(type);
post.set_level(level); post.set_level(level);
......
...@@ -283,7 +283,7 @@ main(int argc, char** argv) ...@@ -283,7 +283,7 @@ main(int argc, char** argv)
program_name); program_name);
spot::translator trans(&extra_options); spot::translator trans(&extra_options);
trans.set_pref(pref); trans.set_pref(pref | comp);
trans.set_type(type); trans.set_type(type);
trans.set_level(level); trans.set_level(level);
......
...@@ -267,7 +267,7 @@ main(int argc, char** argv) ...@@ -267,7 +267,7 @@ main(int argc, char** argv)
spot::ltl::ltl_simplifier simpl(simplifier_options()); spot::ltl::ltl_simplifier simpl(simplifier_options());
spot::postprocessor postproc(&extra_options); spot::postprocessor postproc(&extra_options);
postproc.set_pref(pref); postproc.set_pref(pref | comp);
postproc.set_type(type); postproc.set_type(type);
postproc.set_level(level); postproc.set_level(level);
......
...@@ -80,12 +80,19 @@ namespace spot ...@@ -80,12 +80,19 @@ namespace spot
{ {
// add a transition to a sink state if the state is not complete. // add a transition to a sink state if the state is not complete.
bdd all = bddtrue; bdd all = bddtrue;
for (i->first(); !i->done(); i->next()) bdd acc = bddfalse;
i->first();
// In case the automaton use state-based acceptance, propagate
// the acceptance of the first transition to the one we add.
if (!i->done())
acc = i->current_acceptance_conditions();
for (; !i->done(); i->next())
all -= i->current_condition(); all -= i->current_condition();
if (all != bddfalse) if (all != bddfalse)
{ {
trans* t = out_->create_transition(n, 0); trans* t = out_->create_transition(n, 0);
t->condition = all; t->condition = all;
t->acceptance_conditions = acc | addacc_;
} }
} }
......
...@@ -126,9 +126,12 @@ namespace spot ...@@ -126,9 +126,12 @@ namespace spot
return s; return s;
} }
#define PREF_ (pref_ & (Small | Deterministic))
#define COMP_ (pref_ & Complete)
const tgba* postprocessor::run(const tgba* a, const ltl::formula* f) const tgba* postprocessor::run(const tgba* a, const ltl::formula* f)
{ {
if (type_ == TGBA && pref_ == Any && level_ == Low) if (type_ == TGBA && PREF_ == Any && level_ == Low)
return a; return a;
if (simul_ < 0) if (simul_ < 0)
...@@ -143,7 +146,7 @@ namespace spot ...@@ -143,7 +146,7 @@ namespace spot
// Remove useless SCCs. // Remove useless SCCs.
if (type_ == Monitor) if (type_ == Monitor)
{ {
// Do not bother about acceptance conditions, they we be // Do not bother about acceptance conditions, they will be
// ignored. // ignored.
const tgba* s = scc_filter_states(a); const tgba* s = scc_filter_states(a);
delete a; delete a;
...@@ -158,7 +161,7 @@ namespace spot ...@@ -158,7 +161,7 @@ namespace spot
if (type_ == Monitor) if (type_ == Monitor)
{ {
if (pref_ == Deterministic) if (PREF_ == Deterministic)
{ {
const tgba* m = minimize_monitor(a); const tgba* m = minimize_monitor(a);
delete a; delete a;
...@@ -170,7 +173,7 @@ namespace spot ...@@ -170,7 +173,7 @@ namespace spot
delete a; delete a;
a = m; a = m;
} }
if (pref_ == Any) if (PREF_ == Any)
return a; return a;
const tgba* sim = do_simul(a, simul_); const tgba* sim = do_simul(a, simul_);
...@@ -189,16 +192,22 @@ namespace spot ...@@ -189,16 +192,22 @@ namespace spot
if (count_states(m) > count_states(sim)) if (count_states(m) > count_states(sim))
{ {
delete m; delete m;
return sim;
} }
else else
{ {
delete sim; delete sim;
return m; sim = m;
}
if (COMP_ == Complete)
{
const tgba* s = tgba_complete(sim);
delete sim;
sim = s;
} }
return sim;
} }
if (pref_ == Any) if (PREF_ == Any)
{ {
if (type_ == BA) if (type_ == BA)
a = do_degen(a); a = do_degen(a);
...@@ -213,9 +222,9 @@ namespace spot ...@@ -213,9 +222,9 @@ namespace spot
// (Small,Low) is the only configuration where we do not run // (Small,Low) is the only configuration where we do not run
// WDBA-minimization. // WDBA-minimization.
if ((pref_ != Small || level_ != Low) && wdba_minimize_) if ((PREF_ != Small || level_ != Low) && wdba_minimize_)
{ {
bool reject_bigger = (pref_ == Small) && (level_ == Medium); bool reject_bigger = (PREF_ == Small) && (level_ == Medium);
dba = minimize_obligation(a, f, 0, reject_bigger); dba = minimize_obligation(a, f, 0, reject_bigger);
if (dba == a) // Minimization failed. if (dba == a) // Minimization failed.
dba = 0; dba = 0;
...@@ -226,7 +235,7 @@ namespace spot ...@@ -226,7 +235,7 @@ namespace spot
// Run a simulation when wdba failed (or was not run), or // Run a simulation when wdba failed (or was not run), or
// at hard levels if we want a small output. // at hard levels if we want a small output.
if (!dba || (level_ == High && pref_ == Small)) if (!dba || (level_ == High && PREF_ == Small))
{ {
sim = do_simul(a, simul_); sim = do_simul(a, simul_);
...@@ -254,7 +263,7 @@ namespace spot ...@@ -254,7 +263,7 @@ namespace spot
if (tba_determinisation_ && !dba) if (tba_determinisation_ && !dba)
{ {
const tgba* tmpd = 0; const tgba* tmpd = 0;
if (pref_ == Deterministic if (PREF_ == Deterministic
&& f && f
&& f->is_syntactic_recurrence() && f->is_syntactic_recurrence()
&& sim->number_of_acceptance_conditions() > 1) && sim->number_of_acceptance_conditions() > 1)
...@@ -275,8 +284,8 @@ namespace spot ...@@ -275,8 +284,8 @@ namespace spot
// may up it if you want to try producing larger automata. // may up it if you want to try producing larger automata.
const tgba* tmp = const tgba* tmp =
tba_determinize_check(in, tba_determinize_check(in,
(pref_ == Small) ? 2 : 8, (PREF_ == Small) ? 2 : 8,
1 << ((pref_ == Small) ? 13 : 15), 1 << ((PREF_ == Small) ? 13 : 15),
f); f);
if (tmp != 0 && tmp != in) if (tmp != 0 && tmp != in)
{ {
...@@ -287,7 +296,7 @@ namespace spot ...@@ -287,7 +296,7 @@ namespace spot
delete tmp; delete tmp;
} }
delete tmpd; delete tmpd;
if (dba && pref_ == Deterministic) if (dba && PREF_ == Deterministic)
{ {
// disregard the result of the simulation. // disregard the result of the simulation.
delete sim; delete sim;
...@@ -401,15 +410,26 @@ namespace spot ...@@ -401,15 +410,26 @@ namespace spot
{ {
const tgba* s = scc_filter(dba, true); const tgba* s = scc_filter(dba, true);
delete dba; delete dba;
return s; assert(!sim);
dba = s;
} }
else if (sim) else if (sim)
{ {
const tgba* s = scc_filter(sim, true); const tgba* s = scc_filter(sim, true);
delete sim; delete sim;
return s; assert(!dba);
sim = s;
} }
} }
return dba ? dba : sim;
sim = dba ? dba : sim;
if (COMP_ == Complete)
{
const tgba* s = tgba_complete(sim);
delete sim;
sim = s;
}
return sim;
} }
} }
...@@ -72,7 +72,17 @@ namespace spot ...@@ -72,7 +72,17 @@ namespace spot
type_ = type; type_ = type;
} }
enum output_pref { Any, Small, Deterministic }; enum
{
Any = 0,
Small = 1,
Deterministic = 2,
// 3 reserved for unambiguous
// Combine Complete as 'Small | Complete' or 'Deterministic | Complete'
Complete = 4
};
typedef int output_pref;
void void
set_pref(output_pref pref) set_pref(output_pref pref)
{ {
...@@ -95,7 +105,7 @@ namespace spot ...@@ -95,7 +105,7 @@ namespace spot
const tgba* do_degen(const tgba* input); const tgba* do_degen(const tgba* input);
output_type type_; output_type type_;
output_pref pref_; int pref_;
optimization_level level_; optimization_level level_;
// Fine-tuning options fetched from the option_map. // Fine-tuning options fetched from the option_map.
bool degen_reset_; bool degen_reset_;
......
...@@ -155,6 +155,8 @@ EOF ...@@ -155,6 +155,8 @@ EOF
diff expected stdout diff expected stdout
test "`../../bin/dstar2tgba -D dsa.dstar --stats '%s %t %p %d'`" = "2 5 0 0"
test "`../../bin/dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "3 8 1 0"
...@@ -233,3 +235,5 @@ digraph G { ...@@ -233,3 +235,5 @@ digraph G {
EOF EOF
diff expected stdout diff expected stdout
test "`../../bin/dstar2tgba -D dra.dstar --stats '%s %t %p %d'`" = "3 12 1 1"
...@@ -38,4 +38,6 @@ ltl2tgba=../../bin/ltl2tgba ...@@ -38,4 +38,6 @@ ltl2tgba=../../bin/ltl2tgba
"$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
"$ltl2tgba --lbtt --ba --high %f > %T" \ "$ltl2tgba --lbtt --ba --high %f > %T" \
"$ltl2tgba --lbtt -BDC %f > %T" \
"$ltl2tgba --lbtt -BC %f > %T" \
--json=output.json --csv=output.csv --json=output.json --csv=output.csv
...@@ -30,13 +30,34 @@ EOF ...@@ -30,13 +30,34 @@ EOF
cut -d, -f1 expected.1 | cut -d, -f1 expected.1 |
../../bin/ltl2tgba -F- --stats='%f, %d %p' >out.1 ../../bin/ltl2tgba -F- --stats='%f, %d %p' >out.1
diff out.1 expected.1 diff out.1 expected.1
../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s' >out.2
cat >expected.2<<EOF cat >expected.2<<EOF
FGa 0 1 2 FGa, 0 1
GFa 1 0 1 GFa, 1 1
a U b, 1 1
G(Fa | !r) | Fx, 0 1
EOF