From 654888718c818f96ae7ca8036e40e9bf66ad8c42 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Nov 2015 18:31:05 +0100 Subject: [PATCH] add support for the weak property This fixes #119. * doc/org/tut21.org, doc/org/hoa.org, NEWS: Document it. * src/twa/twa.hh: Support it in automata. * src/twaalgos/hoa.cc, src/parseaut/parseaut.yy: Add I/O support. * src/twaalgos/minimize.cc, src/twaalgos/totgba.cc: Set weak automata on output. * src/tests/complement.test, src/tests/parseaut.test, src/tests/readsave.test, src/tests/remfin.test, src/tests/sccsimpl.test, src/tests/wdba2.test, wrap/python/tests/automata-io.ipynb: Adjust. --- NEWS | 8 ++++++-- doc/org/hoa.org | 5 +++-- doc/org/tut21.org | 5 ++++- src/parseaut/parseaut.yy | 6 ++++-- src/tests/complement.test | 2 +- src/tests/parseaut.test | 3 +-- src/tests/readsave.test | 5 ++--- src/tests/remfin.test | 2 +- src/tests/sccsimpl.test | 4 ++-- src/tests/wdba2.test | 3 +-- src/twa/twa.hh | 32 +++++++++++++++++++++++------ src/twaalgos/hoa.cc | 4 +++- src/twaalgos/minimize.cc | 8 ++++---- src/twaalgos/totgba.cc | 2 +- wrap/python/tests/automata-io.ipynb | 6 +++--- 15 files changed, 62 insertions(+), 33 deletions(-) diff --git a/NEWS b/NEWS index 5d61462ee..951c177f6 100644 --- a/NEWS +++ b/NEWS @@ -22,12 +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". + * 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", and outputting "unambiguous" even for automata - already tagged as "deterministic". + "no-univ-branch", outputting "unambiguous" even for automata + already tagged as "deterministic", and "inherently-weak" even + for automata tagged as "weak". Python: * Add bindings for is_unambiguous(). diff --git a/doc/org/hoa.org b/doc/org/hoa.org index a5858e751..a0779f417 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -527,7 +527,7 @@ is parsed; this is for instance the case of =deterministic=, body of the file, and then return and error if what has been declared does not correspond to the reality. -Some supported properties (like =inherently-weak=, =unambiguous=, or +Some supported properties (like =weak=, =unambiguous=, or =stutter-invariant=) are not double-checked, because that would require too much additional operations. Command-line tools that read HOA files all take a =--trust-hoa=no= option to ignore properties that @@ -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= | -| =inherently-weak= | trusted | yes | as stored | | +| =weak= | trusted | yes | as stored | | +| =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | | | =colored= | ignored | no | checked | | ** Named properties diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 9f167a40f..3080e4d9a 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -85,7 +85,7 @@ corresponding BDD variable number, and then use for instance void custom_print(std::ostream& out, spot::twa_graph_ptr& aut) { - // We need the dictionary to print the BDD that labels the edge + // We need the dictionary to print the BDDs that label the edges const auto& dict = aut->get_dict(); // Some meta-data... @@ -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 << "Weak: " + << (aut->prop_weak() ? "yes\n" : "maybe\n"); out << "Inherently Weak: " << (aut->prop_inherently_weak() ? "yes\n" : "maybe\n"); out << "Stutter Invariant: " @@ -158,6 +160,7 @@ Name: Fa | G(Fb & Fc) Deterministic: maybe Unambiguous: yes State-Based Acc: maybe +Weak: maybe Inherently Weak: maybe Stutter Invariant: yes State 0: diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 885d4ac8b..b32b77720 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -436,8 +436,10 @@ header: format-version header-items res.h->aut->prop_stutter_sensitive(ss); bool iw = res.props.find("inherently-weak") != e; res.h->aut->prop_inherently_weak(iw); - bool iu = res.props.find("unambiguous") != e; - res.h->aut->prop_unambiguous(iu); + 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); } } diff --git a/src/tests/complement.test b/src/tests/complement.test index c5adc3f21..67205ca5b 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 inherently-weak +properties: deterministic weak --BODY-- State: 0 [0] 2 diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test index 1b866fa50..7402bc9a0 100755 --- a/src/tests/parseaut.test +++ b/src/tests/parseaut.test @@ -1189,8 +1189,7 @@ run 2 ../ikwiad -XH foob 2>output.err grep 'foob:1.1: Cannot open file foob' output.err # Make sure we can read multiple automata from stdin -../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' | - sed 's/ stutter-invariant//;s/ inherently-weak//;/properties:$/d' > input +../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input ../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output diff input output diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 34769e03f..082bb9866 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -726,8 +726,7 @@ Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc deterministic -properties: inherently-weak +properties: trans-labels explicit-labels state-acc deterministic weak --BODY-- State: 0 [1] 2 @@ -752,7 +751,7 @@ AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: no-univ-branch trans-labels explicit-labels state-acc -properties: deterministic unambiguous inherently-weak +properties: deterministic unambiguous weak inherently-weak --BODY-- State: 0 [1] 2 diff --git a/src/tests/remfin.test b/src/tests/remfin.test index 12b93b9a7..98e33b84e 100755 --- a/src/tests/remfin.test +++ b/src/tests/remfin.test @@ -602,7 +602,7 @@ AP: 0 acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic -properties: stutter-invariant inherently-weak +properties: stutter-invariant weak --BODY-- State: 0 --END-- diff --git a/src/tests/sccsimpl.test b/src/tests/sccsimpl.test index 6ecf2f317..221b3315a 100755 --- a/src/tests/sccsimpl.test +++ b/src/tests/sccsimpl.test @@ -316,7 +316,7 @@ AP: 1 "p0" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic inherently-weak +properties: deterministic weak --BODY-- State: 0 {0} [t] 0 @@ -331,7 +331,7 @@ AP: 1 "p0" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels state-acc complete -properties: deterministic inherently-weak +properties: deterministic weak --BODY-- State: 0 {0} [t] 0 diff --git a/src/tests/wdba2.test b/src/tests/wdba2.test index 526076767..a9d3230bf 100755 --- a/src/tests/wdba2.test +++ b/src/tests/wdba2.test @@ -67,8 +67,7 @@ Start: 2 AP: 1 "p1" acc-name: Buchi Acceptance: 1 Inf(0) -properties: implicit-labels state-acc complete deterministic -properties: inherently-weak +properties: implicit-labels state-acc complete deterministic weak --BODY-- State: 0 {0} 0 0 diff --git a/src/twa/twa.hh b/src/twa/twa.hh index bc9dc6034..289e05ab1 100644 --- a/src/twa/twa.hh +++ b/src/twa/twa.hh @@ -755,7 +755,8 @@ namespace spot struct bprop { bool state_based_acc:1; // State-based acceptance. - bool inherently_weak:1; // Weak automaton. + bool inherently_weak:1; // Inherently Weak automaton. + bool weak:1; // Weak automaton. bool deterministic:1; // Deterministic automaton. bool unambiguous:1; // Unambiguous automaton. bool stutter_invariant:1; // Stutter invariant language. @@ -830,6 +831,19 @@ namespace spot is.inherently_weak = val; } + bool prop_weak() const + { + return is.weak; + } + + void prop_weak(bool val) + { + if (val) + is.inherently_weak = is.weak = true; + else + is.weak = false; + } + bool prop_deterministic() const { return is.deterministic; @@ -882,9 +896,9 @@ namespace spot struct prop_set { bool state_based; - bool inherently_weak; - bool deterministic; - bool stutter_inv; + bool inherently_weak; // and weak + bool deterministic; // and unambiguous + bool stutter_inv; // and stutter_sensitive static prop_set all() { @@ -899,7 +913,10 @@ namespace spot if (p.state_based) prop_state_acc(other->prop_state_acc()); if (p.inherently_weak) - prop_inherently_weak(other->prop_inherently_weak()); + { + prop_weak(other->prop_weak()); + prop_inherently_weak(other->prop_inherently_weak()); + } if (p.deterministic) { prop_deterministic(other->prop_deterministic()); @@ -917,7 +934,10 @@ namespace spot if (!p.state_based) prop_state_acc(false); if (!p.inherently_weak) - prop_inherently_weak(false); + { + prop_weak(false); + prop_inherently_weak(false); + } if (!p.deterministic) { prop_deterministic(false); diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 7fcb5b7c5..44a279288 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_inherently_weak()) + if (aut->prop_weak()) + prop(" weak"); + if (aut->prop_inherently_weak() && (verbose || !aut->prop_weak())) prop(" inherently-weak"); os << nl; diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc index c82cdc121..e0835a097 100644 --- a/src/twaalgos/minimize.cc +++ b/src/twaalgos/minimize.cc @@ -482,7 +482,7 @@ namespace spot auto res = minimize_dfa(det_a, final, non_final); res->prop_copy(a, { false, false, false, true }); res->prop_deterministic(true); - res->prop_inherently_weak(true); + res->prop_weak(true); res->prop_state_acc(true); return res; } @@ -583,7 +583,7 @@ namespace spot auto res = minimize_dfa(det_a, final, non_final); res->prop_copy(a, { false, false, false, true }); res->prop_deterministic(true); - res->prop_inherently_weak(true); + res->prop_weak(true); return res; } @@ -605,7 +605,7 @@ namespace spot // If the input automaton was already weak and deterministic, the // output is necessary correct. - if (aut_f->prop_inherently_weak() && aut_f->prop_deterministic()) + if (aut_f->prop_weak() && aut_f->prop_deterministic()) return min_aut_f; // if f is a syntactic obligation formula, the WDBA minimization @@ -654,7 +654,7 @@ namespace spot if (product(min_aut_f, aut_neg_f)->is_empty()) { // Complement the minimized WDBA. - assert(min_aut_f->prop_inherently_weak()); + assert(min_aut_f->prop_weak()); auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f)); if (product(aut_f, neg_min_aut_f)->is_empty()) // Finally, we are now sure that it was safe diff --git a/src/twaalgos/totgba.cc b/src/twaalgos/totgba.cc index 83405f6f7..dfe5ad7dd 100644 --- a/src/twaalgos/totgba.cc +++ b/src/twaalgos/totgba.cc @@ -335,7 +335,7 @@ namespace spot res = make_twa_graph(aut->get_dict()); res->set_init_state(res->new_state()); res->prop_state_acc(true); - res->prop_inherently_weak(true); + res->prop_weak(true); res->prop_deterministic(true); res->prop_stutter_invariant(true); return res; diff --git a/wrap/python/tests/automata-io.ipynb b/wrap/python/tests/automata-io.ipynb index 9ac2fd57d..8dabfc9de 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 inherently-weak\n", + "properties: stutter-invariant weak\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 inherently-weak\r\n", + "properties: stutter-invariant weak\r\n", "--BODY--\r\n", "State: 0 {0}\r\n", "[t] 0\r\n", @@ -859,4 +859,4 @@ "metadata": {} } ] -} \ No newline at end of file +}