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

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.
parent eecd2012
...@@ -22,12 +22,16 @@ New in spot 1.99.5a (not yet released) ...@@ -22,12 +22,16 @@ New in spot 1.99.5a (not yet released)
Boolean argument. This argument used to be optionnal (defaulting Boolean argument. This argument used to be optionnal (defaulting
to True), but it no longer is. 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 * By default the HOA printer tries to not bloat the output with
properties that are probably useless. The HOA printer now has a properties that are probably useless. The HOA printer now has a
new option "v" (use "-Hv" from the command line) to output more new option "v" (use "-Hv" from the command line) to output more
verbose "properties:". This currently includes outputing verbose "properties:". This currently includes outputing
"no-univ-branch", and outputting "unambiguous" even for automata "no-univ-branch", outputting "unambiguous" even for automata
already tagged as "deterministic". already tagged as "deterministic", and "inherently-weak" even
for automata tagged as "weak".
Python: Python:
* Add bindings for is_unambiguous(). * Add bindings for is_unambiguous().
......
...@@ -527,7 +527,7 @@ is parsed; this is for instance the case of =deterministic=, ...@@ -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 body of the file, and then return and error if what has been declared
does not correspond to the reality. 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 =stutter-invariant=) are not double-checked, because that would
require too much additional operations. Command-line tools that read require too much additional operations. Command-line tools that read
HOA files all take a =--trust-hoa=no= option to ignore properties that HOA files all take a =--trust-hoa=no= option to ignore properties that
...@@ -591,7 +591,8 @@ particular: ...@@ -591,7 +591,8 @@ particular:
| =unambiguous= | trusted | yes | as stored if (=-Hv= or not =deterministic=) | can be re-checked with =--check=unambiguous= | | =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-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= | | =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 | | | =colored= | ignored | no | checked | |
** Named properties ** Named properties
......
...@@ -85,7 +85,7 @@ corresponding BDD variable number, and then use for instance ...@@ -85,7 +85,7 @@ corresponding BDD variable number, and then use for instance
void custom_print(std::ostream& out, spot::twa_graph_ptr& aut) 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(); const auto& dict = aut->get_dict();
// Some meta-data... // Some meta-data...
...@@ -119,6 +119,8 @@ corresponding BDD variable number, and then use for instance ...@@ -119,6 +119,8 @@ corresponding BDD variable number, and then use for instance
<< (aut->prop_unambiguous() ? "yes\n" : "maybe\n"); << (aut->prop_unambiguous() ? "yes\n" : "maybe\n");
out << "State-Based Acc: " out << "State-Based Acc: "
<< (aut->prop_state_acc() ? "yes\n" : "maybe\n"); << (aut->prop_state_acc() ? "yes\n" : "maybe\n");
out << "Weak: "
<< (aut->prop_weak() ? "yes\n" : "maybe\n");
out << "Inherently Weak: " out << "Inherently Weak: "
<< (aut->prop_inherently_weak() ? "yes\n" : "maybe\n"); << (aut->prop_inherently_weak() ? "yes\n" : "maybe\n");
out << "Stutter Invariant: " out << "Stutter Invariant: "
...@@ -158,6 +160,7 @@ Name: Fa | G(Fb & Fc) ...@@ -158,6 +160,7 @@ Name: Fa | G(Fb & Fc)
Deterministic: maybe Deterministic: maybe
Unambiguous: yes Unambiguous: yes
State-Based Acc: maybe State-Based Acc: maybe
Weak: maybe
Inherently Weak: maybe Inherently Weak: maybe
Stutter Invariant: yes Stutter Invariant: yes
State 0: State 0:
......
...@@ -436,8 +436,10 @@ header: format-version header-items ...@@ -436,8 +436,10 @@ header: format-version header-items
res.h->aut->prop_stutter_sensitive(ss); res.h->aut->prop_stutter_sensitive(ss);
bool iw = res.props.find("inherently-weak") != e; bool iw = res.props.find("inherently-weak") != e;
res.h->aut->prop_inherently_weak(iw); res.h->aut->prop_inherently_weak(iw);
bool iu = res.props.find("unambiguous") != e; bool wk = res.props.find("weak") != e;
res.h->aut->prop_unambiguous(iu); res.h->aut->prop_weak(wk);
bool un = res.props.find("unambiguous") != e;
res.h->aut->prop_unambiguous(un);
} }
} }
......
...@@ -78,7 +78,7 @@ AP: 1 "a" ...@@ -78,7 +78,7 @@ AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak properties: deterministic weak
--BODY-- --BODY--
State: 0 State: 0
[0] 2 [0] 2
......
...@@ -1189,8 +1189,7 @@ run 2 ../ikwiad -XH foob 2>output.err ...@@ -1189,8 +1189,7 @@ run 2 ../ikwiad -XH foob 2>output.err
grep 'foob:1.1: Cannot open file foob' output.err grep 'foob:1.1: Cannot open file foob' output.err
# Make sure we can read multiple automata from stdin # Make sure we can read multiple automata from stdin
../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' | ../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input
sed 's/ stutter-invariant//;s/ inherently-weak//;/properties:$/d' > input
../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output ../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output
diff input output diff input output
......
...@@ -726,8 +726,7 @@ Start: 1 ...@@ -726,8 +726,7 @@ Start: 1
AP: 2 "a" "b" AP: 2 "a" "b"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic weak
properties: inherently-weak
--BODY-- --BODY--
State: 0 State: 0
[1] 2 [1] 2
...@@ -752,7 +751,7 @@ AP: 2 "a" "b" ...@@ -752,7 +751,7 @@ AP: 2 "a" "b"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: no-univ-branch trans-labels explicit-labels state-acc properties: no-univ-branch trans-labels explicit-labels state-acc
properties: deterministic unambiguous inherently-weak properties: deterministic unambiguous weak inherently-weak
--BODY-- --BODY--
State: 0 State: 0
[1] 2 [1] 2
......
...@@ -602,7 +602,7 @@ AP: 0 ...@@ -602,7 +602,7 @@ AP: 0
acc-name: all acc-name: all
Acceptance: 0 t Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant inherently-weak properties: stutter-invariant weak
--BODY-- --BODY--
State: 0 State: 0
--END-- --END--
......
...@@ -316,7 +316,7 @@ AP: 1 "p0" ...@@ -316,7 +316,7 @@ AP: 1 "p0"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak properties: deterministic weak
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[t] 0 [t] 0
...@@ -331,7 +331,7 @@ AP: 1 "p0" ...@@ -331,7 +331,7 @@ AP: 1 "p0"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete
properties: deterministic inherently-weak properties: deterministic weak
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[t] 0 [t] 0
......
...@@ -67,8 +67,7 @@ Start: 2 ...@@ -67,8 +67,7 @@ Start: 2
AP: 1 "p1" AP: 1 "p1"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: implicit-labels state-acc complete deterministic properties: implicit-labels state-acc complete deterministic weak
properties: inherently-weak
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
0 0 0 0
......
...@@ -755,7 +755,8 @@ namespace spot ...@@ -755,7 +755,8 @@ namespace spot
struct bprop struct bprop
{ {
bool state_based_acc:1; // State-based acceptance. 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 deterministic:1; // Deterministic automaton.
bool unambiguous:1; // Unambiguous automaton. bool unambiguous:1; // Unambiguous automaton.
bool stutter_invariant:1; // Stutter invariant language. bool stutter_invariant:1; // Stutter invariant language.
...@@ -830,6 +831,19 @@ namespace spot ...@@ -830,6 +831,19 @@ namespace spot
is.inherently_weak = val; 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 bool prop_deterministic() const
{ {
return is.deterministic; return is.deterministic;
...@@ -882,9 +896,9 @@ namespace spot ...@@ -882,9 +896,9 @@ namespace spot
struct prop_set struct prop_set
{ {
bool state_based; bool state_based;
bool inherently_weak; bool inherently_weak; // and weak
bool deterministic; bool deterministic; // and unambiguous
bool stutter_inv; bool stutter_inv; // and stutter_sensitive
static prop_set all() static prop_set all()
{ {
...@@ -899,7 +913,10 @@ namespace spot ...@@ -899,7 +913,10 @@ namespace spot
if (p.state_based) if (p.state_based)
prop_state_acc(other->prop_state_acc()); prop_state_acc(other->prop_state_acc());
if (p.inherently_weak) 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) if (p.deterministic)
{ {
prop_deterministic(other->prop_deterministic()); prop_deterministic(other->prop_deterministic());
...@@ -917,7 +934,10 @@ namespace spot ...@@ -917,7 +934,10 @@ namespace spot
if (!p.state_based) if (!p.state_based)
prop_state_acc(false); prop_state_acc(false);
if (!p.inherently_weak) if (!p.inherently_weak)
prop_inherently_weak(false); {
prop_weak(false);
prop_inherently_weak(false);
}
if (!p.deterministic) if (!p.deterministic)
{ {
prop_deterministic(false); prop_deterministic(false);
......
...@@ -425,7 +425,9 @@ namespace spot ...@@ -425,7 +425,9 @@ namespace spot
prop(" stutter-invariant"); prop(" stutter-invariant");
if (aut->prop_stutter_sensitive()) if (aut->prop_stutter_sensitive())
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"); prop(" inherently-weak");
os << nl; os << nl;
......
...@@ -482,7 +482,7 @@ namespace spot ...@@ -482,7 +482,7 @@ namespace spot
auto res = minimize_dfa(det_a, final, non_final); auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, true }); res->prop_copy(a, { false, false, false, true });
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_inherently_weak(true); res->prop_weak(true);
res->prop_state_acc(true); res->prop_state_acc(true);
return res; return res;
} }
...@@ -583,7 +583,7 @@ namespace spot ...@@ -583,7 +583,7 @@ namespace spot
auto res = minimize_dfa(det_a, final, non_final); auto res = minimize_dfa(det_a, final, non_final);
res->prop_copy(a, { false, false, false, true }); res->prop_copy(a, { false, false, false, true });
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_inherently_weak(true); res->prop_weak(true);
return res; return res;
} }
...@@ -605,7 +605,7 @@ namespace spot ...@@ -605,7 +605,7 @@ namespace spot
// If the input automaton was already weak and deterministic, the // If the input automaton was already weak and deterministic, the
// output is necessary correct. // 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; return min_aut_f;
// if f is a syntactic obligation formula, the WDBA minimization // if f is a syntactic obligation formula, the WDBA minimization
...@@ -654,7 +654,7 @@ namespace spot ...@@ -654,7 +654,7 @@ namespace spot
if (product(min_aut_f, aut_neg_f)->is_empty()) if (product(min_aut_f, aut_neg_f)->is_empty())
{ {
// Complement the minimized WDBA. // 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)); auto neg_min_aut_f = remove_fin(dtwa_complement(min_aut_f));
if (product(aut_f, neg_min_aut_f)->is_empty()) if (product(aut_f, neg_min_aut_f)->is_empty())
// Finally, we are now sure that it was safe // Finally, we are now sure that it was safe
......
...@@ -335,7 +335,7 @@ namespace spot ...@@ -335,7 +335,7 @@ namespace spot
res = make_twa_graph(aut->get_dict()); res = make_twa_graph(aut->get_dict());
res->set_init_state(res->new_state()); res->set_init_state(res->new_state());
res->prop_state_acc(true); res->prop_state_acc(true);
res->prop_inherently_weak(true); res->prop_weak(true);
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_stutter_invariant(true); res->prop_stutter_invariant(true);
return res; return res;
......
...@@ -60,7 +60,7 @@ ...@@ -60,7 +60,7 @@
"acc-name: Buchi\n", "acc-name: Buchi\n",
"Acceptance: 1 Inf(0)\n", "Acceptance: 1 Inf(0)\n",
"properties: trans-labels explicit-labels state-acc deterministic\n", "properties: trans-labels explicit-labels state-acc deterministic\n",
"properties: stutter-invariant inherently-weak\n", "properties: stutter-invariant weak\n",
"--BODY--\n", "--BODY--\n",
"State: 0 {0}\n", "State: 0 {0}\n",
"[t] 0\n", "[t] 0\n",
...@@ -198,7 +198,7 @@ ...@@ -198,7 +198,7 @@
"acc-name: Buchi\r\n", "acc-name: Buchi\r\n",
"Acceptance: 1 Inf(0)\r\n", "Acceptance: 1 Inf(0)\r\n",
"properties: trans-labels explicit-labels state-acc deterministic\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", "--BODY--\r\n",
"State: 0 {0}\r\n", "State: 0 {0}\r\n",
"[t] 0\r\n", "[t] 0\r\n",
...@@ -859,4 +859,4 @@ ...@@ -859,4 +859,4 @@
"metadata": {} "metadata": {}
} }
] ]
} }
\ No newline at end of file
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