From 0c5f87b442398ae0612d88c949d829d328c8270a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 7 Nov 2015 13:36:31 +0100 Subject: [PATCH] add support for the "terminal" property * src/twa/twa.hh: Store the terminal property. * src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O for "terminal". * src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/minimize.cc: Set terminal as apropriate. * src/twaalgos/safety.cc: Use it. * doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it. * src/tests/complement.test, src/tests/monitor.test, wrap/python/tests/automata-io.ipynb: Adjust. --- NEWS | 18 +++++++++--------- doc/org/hoa.org | 3 ++- doc/org/tut21.org | 3 +++ src/parseaut/parseaut.yy | 20 +++++++++----------- src/tests/complement.test | 2 +- src/tests/monitor.test | 2 +- src/twa/twa.hh | 16 ++++++++++++++++ src/twaalgos/hoa.cc | 4 +++- src/twaalgos/ltl2tgba_fm.cc | 13 ++++++++++--- src/twaalgos/minimize.cc | 10 ++++++++++ src/twaalgos/safety.cc | 2 ++ wrap/python/tests/automata-io.ipynb | 4 ++-- 12 files changed, 68 insertions(+), 29 deletions(-) diff --git a/NEWS b/NEWS index 951c177f6..9a13a567f 100644 --- a/NEWS +++ b/NEWS @@ -22,16 +22,16 @@ New in spot 1.99.5a (not yet released) Boolean argument. This argument used to be optionnal (defaulting to True), but it no longer is. - * Automata now support the "weak" property in addition to the - previously supported "inherently-weak". + * Automata now support the "weak" and "terminal" properties in + addition to the previously supported "inherently-weak". - * By default the HOA printer tries to not bloat the output with - properties that are probably useless. The HOA printer now has a - new option "v" (use "-Hv" from the command line) to output more - verbose "properties:". This currently includes outputing - "no-univ-branch", outputting "unambiguous" even for automata - already tagged as "deterministic", and "inherently-weak" even - for automata tagged as "weak". + * By default the HOA printer tries not to bloat the output with + properties that are redundant and probably useless. The HOA + printer now has a new option "v" (use "-Hv" from the command line) + to output more verbose "properties:". This currently includes + outputing "no-univ-branch", outputting "unambiguous" even for + automata already tagged as "deterministic", and "inherently-weak" + or "weak" even for automata tagged "weak" or "terminal". Python: * Add bindings for is_unambiguous(). diff --git a/doc/org/hoa.org b/doc/org/hoa.org index a0779f417..92e3891b8 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -591,7 +591,8 @@ particular: | =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= | | =stutter-invariant= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | | =stutter-sensitive= | trusted | yes | as stored | can be re-checked with =--check=stuttering= | -| =weak= | trusted | yes | as stored | | +| =terminal= | trusted | yes | as stored | | +| =weak= | trusted | yes | as stored if (=-Hv= or not =terminal=) | | | =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | | | =colored= | ignored | no | checked | | diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 3080e4d9a..991ae360f 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -119,6 +119,8 @@ corresponding BDD variable number, and then use for instance << (aut->prop_unambiguous() ? "yes\n" : "maybe\n"); out << "State-Based Acc: " << (aut->prop_state_acc() ? "yes\n" : "maybe\n"); + out << "Terminal: " + << (aut->prop_terminal() ? "yes\n" : "maybe\n"); out << "Weak: " << (aut->prop_weak() ? "yes\n" : "maybe\n"); out << "Inherently Weak: " @@ -160,6 +162,7 @@ Name: Fa | G(Fb & Fc) Deterministic: maybe Unambiguous: yes State-Based Acc: maybe +Terminal: maybe Weak: maybe Inherently Weak: maybe Stutter Invariant: yes diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index b32b77720..31275046e 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -429,17 +429,15 @@ header: format-version header-items } if (res.opts.trust_hoa) { - auto e = res.props.end(); - bool si = res.props.find("stutter-invariant") != e; - res.h->aut->prop_stutter_invariant(si); - bool ss = res.props.find("stutter-sensitive") != e; - res.h->aut->prop_stutter_sensitive(ss); - bool iw = res.props.find("inherently-weak") != e; - res.h->aut->prop_inherently_weak(iw); - bool wk = res.props.find("weak") != e; - res.h->aut->prop_weak(wk); - bool un = res.props.find("unambiguous") != e; - res.h->aut->prop_unambiguous(un); + auto& a = res.h->aut; + auto& p = res.props; + auto e = p.end(); + a->prop_stutter_invariant(p.find("stutter-invariant") != e); + a->prop_stutter_sensitive(p.find("stutter-sensitive") != e); + a->prop_inherently_weak(p.find("inherently-weak") != e); + a->prop_weak(p.find("weak") != e); + a->prop_terminal(p.find("terminal") != e); + a->prop_unambiguous(p.find("unambiguous") != e); } } diff --git a/src/tests/complement.test b/src/tests/complement.test index 67205ca5b..ef968a697 100755 --- a/src/tests/complement.test +++ b/src/tests/complement.test @@ -78,7 +78,7 @@ AP: 1 "a" acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic weak +properties: deterministic terminal --BODY-- State: 0 [0] 2 diff --git a/src/tests/monitor.test b/src/tests/monitor.test index b832b469b..8a5c79cfa 100755 --- a/src/tests/monitor.test +++ b/src/tests/monitor.test @@ -53,7 +53,7 @@ AP: 1 "a" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic -properties: stutter-invariant inherently-weak +properties: stutter-invariant terminal --BODY-- State: 0 [t] 0 diff --git a/src/twa/twa.hh b/src/twa/twa.hh index 289e05ab1..0407fa4c6 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -757,6 +757,7 @@ namespace spot bool state_based_acc:1; // State-based acceptance. bool inherently_weak:1; // Inherently Weak automaton. bool weak:1; // Weak automaton. + bool terminal:1; // Terminal automaton. bool deterministic:1; // Deterministic automaton. bool unambiguous:1; // Unambiguous automaton. bool stutter_invariant:1; // Stutter invariant language. @@ -831,6 +832,19 @@ namespace spot is.inherently_weak = val; } + bool prop_terminal() const + { + return is.terminal; + } + + void prop_terminal(bool val) + { + if (val) + is.inherently_weak = is.weak = is.terminal = true; + else + is.terminal = false; + } + bool prop_weak() const { return is.weak; @@ -914,6 +928,7 @@ namespace spot prop_state_acc(other->prop_state_acc()); if (p.inherently_weak) { + prop_terminal(other->prop_terminal()); prop_weak(other->prop_weak()); prop_inherently_weak(other->prop_inherently_weak()); } @@ -935,6 +950,7 @@ namespace spot prop_state_acc(false); if (!p.inherently_weak) { + prop_terminal(false); prop_weak(false); prop_inherently_weak(false); } diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 44a279288..24968733f 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -425,7 +425,9 @@ namespace spot prop(" stutter-invariant"); if (aut->prop_stutter_sensitive()) prop(" stutter-sensitive"); - if (aut->prop_weak()) + if (aut->prop_terminal()) + prop(" terminal"); + if (aut->prop_weak() && (verbose || !aut->prop_terminal())) prop(" weak"); if (aut->prop_inherently_weak() && (verbose || !aut->prop_weak())) prop(" inherently-weak"); diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc index d86721677..54691b654 100644 --- a/src/twaalgos/ltl2tgba_fm.cc +++ b/src/twaalgos/ltl2tgba_fm.cc @@ -1972,6 +1972,8 @@ namespace spot } bdd all_events = observable_events | unobservable_events; + auto orig_f = f2; + // This is in case the initial state is equivalent to true... if (symb_merge) f2 = fc.canonize(f2); @@ -2172,9 +2174,6 @@ namespace spot } } - // Set the following to true to preserve state names. - a->release_formula_namer(namer, false); - auto& acc = a->acc(); unsigned ns = a->num_states(); for (unsigned s = 0; s < ns; ++s) @@ -2185,10 +2184,18 @@ namespace spot a->prop_inherently_weak(f2.is_syntactic_persistence()); a->prop_stutter_invariant(f2.is_syntactic_stutter_invariant()); + if (orig_f.is_syntactic_guarantee()) + { + a->prop_terminal(true); + assert(a->num_sets() <= 1); + } // Currently the unambiguous option work only with LTL. a->prop_unambiguous(f2.is_ltl_formula() && unambiguous); + // Set the following to true to preserve state names. + a->release_formula_namer(namer, false); + if (!simplifier) // This should not be deleted before we have registered all propositions. delete s; diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index e0835a097..1dc6c2c6f 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -584,6 +584,16 @@ namespace spot res->prop_copy(a, { false, false, false, true }); res->prop_deterministic(true); res->prop_weak(true); + // If the input was terminal, then the output is also terminal. + // FIXME: + // (1) We should have a specialized version of this function for + // the case where the input is terminal. See issue #120. + // (2) It would be nice to have a more precise detection of + // terminal automata in the output. Calling + // is_guarantee_automaton() seems overkill here. But maybe we can + // add a quick check inside minimize_dfa. + if (a->prop_terminal()) + res->prop_terminal(true); return res; } diff --git a/src/twaalgos/safety.cc b/src/twaalgos/safety.cc index 3ee1b020b..8c142110e 100644 --- a/src/twaalgos/safety.cc +++ b/src/twaalgos/safety.cc @@ -27,6 +27,8 @@ namespace spot is_guarantee_automaton(const const_twa_graph_ptr& aut, scc_info* si) { + if (aut->prop_terminal()) + return true; // Create an scc_info if the user did not give one to us. bool need_si = !si; if (need_si) diff --git a/wrap/python/tests/automata-io.ipynb b/wrap/python/tests/automata-io.ipynb index 8dabfc9de..19f1aa7c6 100644 --- a/wrap/python/tests/automata-io.ipynb +++ b/wrap/python/tests/automata-io.ipynb @@ -60,7 +60,7 @@ "acc-name: Buchi\n", "Acceptance: 1 Inf(0)\n", "properties: trans-labels explicit-labels state-acc deterministic\n", - "properties: stutter-invariant weak\n", + "properties: stutter-invariant terminal\n", "--BODY--\n", "State: 0 {0}\n", "[t] 0\n", @@ -198,7 +198,7 @@ "acc-name: Buchi\r\n", "Acceptance: 1 Inf(0)\r\n", "properties: trans-labels explicit-labels state-acc deterministic\r\n", - "properties: stutter-invariant weak\r\n", + "properties: stutter-invariant terminal\r\n", "--BODY--\r\n", "State: 0 {0}\r\n", "[t] 0\r\n",