diff --git a/NEWS b/NEWS index af001f7ed..920313354 100644 --- a/NEWS +++ b/NEWS @@ -58,14 +58,18 @@ New in spot 1.1.4a (not relased) number of seconds spent building the output automaton (excluding the time spent parsing the input). - - ltl2tgba 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 + - ltl2tgba, ltl2tgta, and dstar2tgba have a --complete option + to output complete automata. + + - 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 deterministic automaton more efficiently) and is disabled by default. See the spot-x(7) man page for documentation about the related options: sat-minimize, sat-states, sat-acc, state-based. + * New functions and classes in the library: - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent @@ -138,6 +142,10 @@ New in spot 1.1.4a (not relased) effectively perform a DFS. As a consequence, it does not 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 store locations. diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 4153fccb6..925a019aa 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -274,6 +274,8 @@ dstar2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference +: -C, --complete output a complete automaton (combine with other +: intents) : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) @@ -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 of the input (Rabin) automaton, =%s=, the number of states of the -output (Büchi) automaton, and =%d=, whether the output automaton is -deterministic or not. +output (Büchi) automaton, =%d=, whether the output automaton is +deterministic, and =%p= whether the automaton is complete. #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 --tree-size=10..15 a b c | @@ -338,40 +340,42 @@ while read f; do echo "$f" ltlfilt -l -f "$f" | 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 #+END_SRC #+RESULTS: #+begin_example F(a | !b) - DRA: 2st.; BA: 2st.; det.? 1 + DRA: 2st.; BA: 2st.; det.? 1; complete? 1 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)))) - DRA: 8st.; BA: 7st.; det.? 1 + DRA: 8st.; BA: 7st.; det.? 1; complete? 0 !b | !a - DRA: 3st.; BA: 2st.; det.? 1 + DRA: 3st.; BA: 2st.; det.? 1; complete? 0 F!a - DRA: 2st.; BA: 2st.; det.? 1 + DRA: 2st.; BA: 2st.; det.? 1; complete? 1 F(Ga R (b | Ga)) - DRA: 10st.; BA: 10st.; det.? 0 + DRA: 10st.; BA: 10st.; det.? 0; complete? 0 !c U (!c & !a) - DRA: 3st.; BA: 2st.; det.? 1 + DRA: 3st.; BA: 2st.; det.? 1; complete? 0 !c | FGb - DRA: 4st.; BA: 5st.; det.? 0 + DRA: 4st.; BA: 5st.; det.? 0; complete? 0 G(c U a) - DRA: 4st.; BA: 3st.; det.? 1 + DRA: 4st.; BA: 3st.; det.? 1; complete? 0 c & Gb - DRA: 3st.; BA: 2st.; det.? 1 + DRA: 3st.; BA: 2st.; det.? 1; complete? 0 #+end_example An important point you should be aware of when comparing these numbers of states is that the deterministic automata produced by =ltl2dstar= are complete, while the automata produced by =dstar2tgba= -(deterministic or not) are not complete. This can explain a -difference of one state (the "sink" state, which is not output by -=dstar2tgba=). +(deterministic or not) are not complete by default. This can explain +a difference of one state (the so called "sink" state). + +You can instruct =dstar2tgba= to output a complete automaton using the +=--complete= option (or =-C= for short). ** Conversion from Rabin and Streett to TGBA diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 904c7e9b1..0eaf7aaae 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -319,6 +319,8 @@ ltl2tgba --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -a, --any no preference +: -C, --complete output a complete automaton (combine with other +: intents) : -D, --deterministic prefer deterministic automata : --small prefer small automata (default) @@ -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, 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 of pre- and post-processing performed. These two steps can be adjusted via a common set of switches: diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 83021535e..fa9e06a45 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,6 +23,7 @@ spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_pref pref = spot::postprocessor::Small; +spot::postprocessor::output_pref comp = spot::postprocessor::Any; spot::postprocessor::optimization_level level = spot::postprocessor::High; #define OPT_SMALL 1 @@ -37,6 +38,8 @@ static const argp_option options[] = { "small", OPT_SMALL, 0, 0, "prefer small automata (default)", 0 }, { "deterministic", 'D', 0, 0, "prefer deterministic automata", 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 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, @@ -55,6 +58,9 @@ parse_opt_post(int key, char*, struct argp_state*) case 'a': pref = spot::postprocessor::Any; break; + case 'C': + comp = spot::postprocessor::Complete; + break; case 'D': pref = spot::postprocessor::Deterministic; break; diff --git a/src/bin/common_post.hh b/src/bin/common_post.hh index b68998239..f2fcc0cb1 100644 --- a/src/bin/common_post.hh +++ b/src/bin/common_post.hh @@ -1,5 +1,5 @@ // -*- 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). // // This file is part of Spot, a model checking library. @@ -28,6 +28,7 @@ extern const struct argp post_argp; extern spot::postprocessor::output_type type; extern spot::postprocessor::output_pref pref; +extern spot::postprocessor::output_pref comp; extern spot::postprocessor::optimization_level level; #endif // SPOT_BIN_COMMON_FINPUT_HH diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 08b5451ed..1b4b92038 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -373,7 +373,7 @@ main(int argc, char** argv) jobs.push_back(job("-", true)); spot::postprocessor post(&extra_options); - post.set_pref(pref); + post.set_pref(pref | comp); post.set_type(type); post.set_level(level); diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index d17ee4d85..133843b8f 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -283,7 +283,7 @@ main(int argc, char** argv) program_name); spot::translator trans(&extra_options); - trans.set_pref(pref); + trans.set_pref(pref | comp); trans.set_type(type); trans.set_level(level); diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index c7cbf6939..1e0ce9aea 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -267,7 +267,7 @@ main(int argc, char** argv) spot::ltl::ltl_simplifier simpl(simplifier_options()); spot::postprocessor postproc(&extra_options); - postproc.set_pref(pref); + postproc.set_pref(pref | comp); postproc.set_type(type); postproc.set_level(level); diff --git a/src/tgbaalgos/complete.cc b/src/tgbaalgos/complete.cc index 8de040498..ffee42406 100644 --- a/src/tgbaalgos/complete.cc +++ b/src/tgbaalgos/complete.cc @@ -80,12 +80,19 @@ namespace spot { // add a transition to a sink state if the state is not complete. 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(); if (all != bddfalse) { trans* t = out_->create_transition(n, 0); t->condition = all; + t->acceptance_conditions = acc | addacc_; } } diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 17254bb1a..add6f3f3e 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -126,9 +126,12 @@ namespace spot return s; } +#define PREF_ (pref_ & (Small | Deterministic)) +#define COMP_ (pref_ & Complete) + 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; if (simul_ < 0) @@ -143,7 +146,7 @@ namespace spot // Remove useless SCCs. if (type_ == Monitor) { - // Do not bother about acceptance conditions, they we be + // Do not bother about acceptance conditions, they will be // ignored. const tgba* s = scc_filter_states(a); delete a; @@ -158,7 +161,7 @@ namespace spot if (type_ == Monitor) { - if (pref_ == Deterministic) + if (PREF_ == Deterministic) { const tgba* m = minimize_monitor(a); delete a; @@ -170,7 +173,7 @@ namespace spot delete a; a = m; } - if (pref_ == Any) + if (PREF_ == Any) return a; const tgba* sim = do_simul(a, simul_); @@ -189,16 +192,22 @@ namespace spot if (count_states(m) > count_states(sim)) { delete m; - return sim; } else { 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) a = do_degen(a); @@ -213,9 +222,9 @@ namespace spot // (Small,Low) is the only configuration where we do not run // 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); if (dba == a) // Minimization failed. dba = 0; @@ -226,7 +235,7 @@ namespace spot // Run a simulation when wdba failed (or was not run), or // 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_); @@ -254,7 +263,7 @@ namespace spot if (tba_determinisation_ && !dba) { const tgba* tmpd = 0; - if (pref_ == Deterministic + if (PREF_ == Deterministic && f && f->is_syntactic_recurrence() && sim->number_of_acceptance_conditions() > 1) @@ -275,8 +284,8 @@ namespace spot // may up it if you want to try producing larger automata. const tgba* tmp = tba_determinize_check(in, - (pref_ == Small) ? 2 : 8, - 1 << ((pref_ == Small) ? 13 : 15), + (PREF_ == Small) ? 2 : 8, + 1 << ((PREF_ == Small) ? 13 : 15), f); if (tmp != 0 && tmp != in) { @@ -287,7 +296,7 @@ namespace spot delete tmp; } delete tmpd; - if (dba && pref_ == Deterministic) + if (dba && PREF_ == Deterministic) { // disregard the result of the simulation. delete sim; @@ -401,15 +410,26 @@ namespace spot { const tgba* s = scc_filter(dba, true); delete dba; - return s; + assert(!sim); + dba = s; } else if (sim) { const tgba* s = scc_filter(sim, true); 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; } } diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh index 947a4761b..693089b42 100644 --- a/src/tgbaalgos/postproc.hh +++ b/src/tgbaalgos/postproc.hh @@ -72,7 +72,17 @@ namespace spot 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 set_pref(output_pref pref) { @@ -95,7 +105,7 @@ namespace spot const tgba* do_degen(const tgba* input); output_type type_; - output_pref pref_; + int pref_; optimization_level level_; // Fine-tuning options fetched from the option_map. bool degen_reset_; diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index a904e0032..8dde21c58 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -155,6 +155,8 @@ EOF 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 { EOF diff expected stdout + +test "`../../bin/dstar2tgba -D dra.dstar --stats '%s %t %p %d'`" = "3 12 1 1" diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test index 00e484613..367ed9e1f 100755 --- a/src/tgbatest/ltlcross2.test +++ b/src/tgbatest/ltlcross2.test @@ -38,4 +38,6 @@ ltl2tgba=../../bin/ltl2tgba "$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 --ba --high %f > %T" \ +"$ltl2tgba --lbtt -BDC %f > %T" \ +"$ltl2tgba --lbtt -BC %f > %T" \ --json=output.json --csv=output.csv diff --git a/src/tgbatest/nondet.test b/src/tgbatest/nondet.test index fa868824f..170e13721 100755 --- a/src/tgbatest/nondet.test +++ b/src/tgbatest/nondet.test @@ -30,13 +30,34 @@ EOF cut -d, -f1 expected.1 | ../../bin/ltl2tgba -F- --stats='%f, %d %p' >out.1 - diff out.1 expected.1 -../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s' >out.2 cat >expected.2<out.2 diff out.2 expected.2 + + +../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s %p' >out.3 +cat >expected.3<out.4 +cat >expected.4<