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

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.
parent 65488871
...@@ -22,16 +22,16 @@ New in spot 1.99.5a (not yet released) ...@@ -22,16 +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 * Automata now support the "weak" and "terminal" properties in
previously supported "inherently-weak". 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 not to bloat the output with
properties that are probably useless. The HOA printer now has a properties that are redundant and probably useless. The HOA
new option "v" (use "-Hv" from the command line) to output more printer now has a new option "v" (use "-Hv" from the command line)
verbose "properties:". This currently includes outputing to output more verbose "properties:". This currently includes
"no-univ-branch", outputting "unambiguous" even for automata outputing "no-univ-branch", outputting "unambiguous" even for
already tagged as "deterministic", and "inherently-weak" even automata already tagged as "deterministic", and "inherently-weak"
for automata tagged as "weak". or "weak" even for automata tagged "weak" or "terminal".
Python: Python:
* Add bindings for is_unambiguous(). * Add bindings for is_unambiguous().
......
...@@ -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= |
| =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=) | | | =inherently-weak= | trusted | yes | as stored if (=-Hv= or not =weak=) | |
| =colored= | ignored | no | checked | | | =colored= | ignored | no | checked | |
......
...@@ -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 << "Terminal: "
<< (aut->prop_terminal() ? "yes\n" : "maybe\n");
out << "Weak: " out << "Weak: "
<< (aut->prop_weak() ? "yes\n" : "maybe\n"); << (aut->prop_weak() ? "yes\n" : "maybe\n");
out << "Inherently Weak: " out << "Inherently Weak: "
...@@ -160,6 +162,7 @@ Name: Fa | G(Fb & Fc) ...@@ -160,6 +162,7 @@ Name: Fa | G(Fb & Fc)
Deterministic: maybe Deterministic: maybe
Unambiguous: yes Unambiguous: yes
State-Based Acc: maybe State-Based Acc: maybe
Terminal: maybe
Weak: maybe Weak: maybe
Inherently Weak: maybe Inherently Weak: maybe
Stutter Invariant: yes Stutter Invariant: yes
......
...@@ -429,17 +429,15 @@ header: format-version header-items ...@@ -429,17 +429,15 @@ header: format-version header-items
} }
if (res.opts.trust_hoa) if (res.opts.trust_hoa)
{ {
auto e = res.props.end(); auto& a = res.h->aut;
bool si = res.props.find("stutter-invariant") != e; auto& p = res.props;
res.h->aut->prop_stutter_invariant(si); auto e = p.end();
bool ss = res.props.find("stutter-sensitive") != e; a->prop_stutter_invariant(p.find("stutter-invariant") != e);
res.h->aut->prop_stutter_sensitive(ss); a->prop_stutter_sensitive(p.find("stutter-sensitive") != e);
bool iw = res.props.find("inherently-weak") != e; a->prop_inherently_weak(p.find("inherently-weak") != e);
res.h->aut->prop_inherently_weak(iw); a->prop_weak(p.find("weak") != e);
bool wk = res.props.find("weak") != e; a->prop_terminal(p.find("terminal") != e);
res.h->aut->prop_weak(wk); a->prop_unambiguous(p.find("unambiguous") != e);
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 weak properties: deterministic terminal
--BODY-- --BODY--
State: 0 State: 0
[0] 2 [0] 2
......
...@@ -53,7 +53,7 @@ AP: 1 "a" ...@@ -53,7 +53,7 @@ AP: 1 "a"
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 terminal
--BODY-- --BODY--
State: 0 State: 0
[t] 0 [t] 0
......
...@@ -757,6 +757,7 @@ namespace spot ...@@ -757,6 +757,7 @@ namespace spot
bool state_based_acc:1; // State-based acceptance. bool state_based_acc:1; // State-based acceptance.
bool inherently_weak:1; // Inherently Weak automaton. bool inherently_weak:1; // Inherently Weak automaton.
bool weak:1; // Weak automaton. bool weak:1; // Weak automaton.
bool terminal:1; // Terminal 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.
...@@ -831,6 +832,19 @@ namespace spot ...@@ -831,6 +832,19 @@ namespace spot
is.inherently_weak = val; 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 bool prop_weak() const
{ {
return is.weak; return is.weak;
...@@ -914,6 +928,7 @@ namespace spot ...@@ -914,6 +928,7 @@ namespace spot
prop_state_acc(other->prop_state_acc()); prop_state_acc(other->prop_state_acc());
if (p.inherently_weak) if (p.inherently_weak)
{ {
prop_terminal(other->prop_terminal());
prop_weak(other->prop_weak()); prop_weak(other->prop_weak());
prop_inherently_weak(other->prop_inherently_weak()); prop_inherently_weak(other->prop_inherently_weak());
} }
...@@ -935,6 +950,7 @@ namespace spot ...@@ -935,6 +950,7 @@ namespace spot
prop_state_acc(false); prop_state_acc(false);
if (!p.inherently_weak) if (!p.inherently_weak)
{ {
prop_terminal(false);
prop_weak(false); prop_weak(false);
prop_inherently_weak(false); prop_inherently_weak(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_weak()) if (aut->prop_terminal())
prop(" terminal");
if (aut->prop_weak() && (verbose || !aut->prop_terminal()))
prop(" weak"); prop(" weak");
if (aut->prop_inherently_weak() && (verbose || !aut->prop_weak())) if (aut->prop_inherently_weak() && (verbose || !aut->prop_weak()))
prop(" inherently-weak"); prop(" inherently-weak");
......
...@@ -1972,6 +1972,8 @@ namespace spot ...@@ -1972,6 +1972,8 @@ namespace spot
} }
bdd all_events = observable_events | unobservable_events; bdd all_events = observable_events | unobservable_events;
auto orig_f = f2;
// This is in case the initial state is equivalent to true... // This is in case the initial state is equivalent to true...
if (symb_merge) if (symb_merge)
f2 = fc.canonize(f2); f2 = fc.canonize(f2);
...@@ -2172,9 +2174,6 @@ namespace spot ...@@ -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(); auto& acc = a->acc();
unsigned ns = a->num_states(); unsigned ns = a->num_states();
for (unsigned s = 0; s < ns; ++s) for (unsigned s = 0; s < ns; ++s)
...@@ -2185,10 +2184,18 @@ namespace spot ...@@ -2185,10 +2184,18 @@ namespace spot
a->prop_inherently_weak(f2.is_syntactic_persistence()); a->prop_inherently_weak(f2.is_syntactic_persistence());
a->prop_stutter_invariant(f2.is_syntactic_stutter_invariant()); 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. // Currently the unambiguous option work only with LTL.
a->prop_unambiguous(f2.is_ltl_formula() && unambiguous); 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) if (!simplifier)
// This should not be deleted before we have registered all propositions. // This should not be deleted before we have registered all propositions.
delete s; delete s;
......
...@@ -584,6 +584,16 @@ namespace spot ...@@ -584,6 +584,16 @@ namespace spot
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_weak(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; return res;
} }
......
...@@ -27,6 +27,8 @@ namespace spot ...@@ -27,6 +27,8 @@ namespace spot
is_guarantee_automaton(const const_twa_graph_ptr& aut, is_guarantee_automaton(const const_twa_graph_ptr& aut,
scc_info* si) scc_info* si)
{ {
if (aut->prop_terminal())
return true;
// Create an scc_info if the user did not give one to us. // Create an scc_info if the user did not give one to us.
bool need_si = !si; bool need_si = !si;
if (need_si) if (need_si)
......
...@@ -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 weak\n", "properties: stutter-invariant terminal\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 weak\r\n", "properties: stutter-invariant terminal\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",
......
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