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

hoa: fix I/O of determinism

Fixes #212.

* spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Recognize
exist-branch, and adjust printer to the 1.1 semantics.
* tests/core/alternating.test, tests/core/complete.test,
tests/core/det.test, tests/core/explsum.test,
tests/core/parseaut.test, tests/core/readsave.test,
tests/core/sbacc.test, tests/core/tgbagraph.test,
tests/python/alternating.py, tests/python/dualize.py: Adjust test
cases.
* NEWS: Mention the change.
parent 0cf250d8
...@@ -172,6 +172,15 @@ New in spot 2.3.5.dev (not yet released) ...@@ -172,6 +172,15 @@ New in spot 2.3.5.dev (not yet released)
process automata from different streams at the same time (i.e., process automata from different streams at the same time (i.e.,
using multiple spot::automaton_stream_parser instances at once). using multiple spot::automaton_stream_parser instances at once).
- The print_hoa() and parse_automaton() functions have been updated
to recognize the "exist-branch" property of the non-released HOA
v1.1, as well as the new meaning of property "deterministic". (In
HOA v1 "properties: deterministic" means that the automaton has no
existential branching; in HOA v1.1 it disallows universal
branching as well.) The meaning of "deterministic" in Spot has
been adjusted to these new semantics, see "Backward-incompatible
changes" below.
Python: Python:
- The 'spot.gen' package exports the functions from libspotgen. - The 'spot.gen' package exports the functions from libspotgen.
......
...@@ -146,7 +146,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); ...@@ -146,7 +146,8 @@ extern "C" int strverscmp(const char *s1, const char *s2);
bool accept_all_seen = false; bool accept_all_seen = false;
bool aliased_states = false; bool aliased_states = false;
spot::trival deterministic = spot::trival::maybe(); spot::trival universal = spot::trival::maybe();
spot::trival existential = spot::trival::maybe();
spot::trival complete = spot::trival::maybe(); spot::trival complete = spot::trival::maybe();
bool trans_acc_seen = false; bool trans_acc_seen = false;
...@@ -346,6 +347,7 @@ BOOLEAN: 't' | 'f' ...@@ -346,6 +347,7 @@ BOOLEAN: 't' | 'f'
header: format-version header-items header: format-version header-items
{ {
bool v1plus = strverscmp("v1", res.format_version.c_str()) < 0;
// Preallocate the states if we know their number. // Preallocate the states if we know their number.
if (res.states >= 0) if (res.states >= 0)
{ {
...@@ -457,14 +459,15 @@ header: format-version header-items ...@@ -457,14 +459,15 @@ header: format-version header-items
res.acc_style = State_Acc; res.acc_style = State_Acc;
} }
auto univ_branch = res.prop_is_true("univ-branch"); if (auto univ_branch = res.prop_is_true("univ-branch"))
if (res.opts.want_kripke && univ_branch) if (res.opts.want_kripke)
error(univ_branch.loc, error(univ_branch.loc,
"Kripke structures may not use 'properties: univ-branch'"); "Kripke structures may not use 'properties: univ-branch'");
} }
{ {
unsigned ss = res.start.size(); unsigned ss = res.start.size();
auto det = res.prop_is_true("deterministic"); auto det = res.prop_is_true("deterministic");
auto no_exist = res.prop_is_false("exist-branch");
if (ss > 1) if (ss > 1)
{ {
if (det) if (det)
...@@ -472,16 +475,46 @@ header: format-version header-items ...@@ -472,16 +475,46 @@ header: format-version header-items
error(det.loc, error(det.loc,
"deterministic automata should have at most " "deterministic automata should have at most "
"one initial state"); "one initial state");
res.deterministic = spot::trival::maybe(); res.universal = spot::trival::maybe();
} }
else if (no_exist)
{
error(no_exist.loc,
"universal automata should have at most "
"one initial state");
res.universal = spot::trival::maybe();
}
} }
else else
{ {
// Assume the automaton is deterministic until proven // Assume the automaton is deterministic until proven
// wrong, or unless we are building a Kripke structure. // wrong, or unless we are building a Kripke structure.
if (!res.opts.want_kripke) if (!res.opts.want_kripke)
res.deterministic = true; {
res.universal = true;
res.existential = true;
}
} }
for (auto& ss: res.start)
{
if (ss.second.size() > 1)
{
if (auto no_univ = res.prop_is_false("univ-branch"))
{
error(ss.first,
"conjunct initial state despite...");
error(no_univ.loc, "... property: !univ-branch");
}
else if (v1plus)
if (auto det = res.prop_is_true("deterministic"))
{
error(ss.first,
"conjunct initial state despite...");
error(det.loc, "... property: deterministic");
}
res.existential = false;
}
}
auto complete = res.prop_is_true("complete"); auto complete = res.prop_is_true("complete");
if (ss < 1) if (ss < 1)
{ {
...@@ -1069,14 +1102,29 @@ body: states ...@@ -1069,14 +1102,29 @@ body: states
error(@1, "automaton is complete..."); error(@1, "automaton is complete...");
error(p.loc, "... despite 'properties: !complete'"); error(p.loc, "... despite 'properties: !complete'");
} }
if (res.deterministic) bool det_warned = false;
if (res.universal && res.existential)
if (auto p = res.prop_is_false("deterministic")) if (auto p = res.prop_is_false("deterministic"))
{ {
error(@1, "automaton is deterministic..."); error(@1, "automaton is deterministic...");
error(p.loc, "... despite 'properties: !deterministic'"); error(p.loc, "... despite 'properties: !deterministic'");
det_warned = true;
}
if (res.universal.is_true() && !det_warned)
if (auto p = res.prop_is_true("exist-branch"))
{
error(@1, "automaton has no existential branching...");
error(p.loc, "... despite 'properties: exist-branch'");
det_warned = true;
}
if (res.existential.is_true() && !det_warned)
if (auto p = res.prop_is_true("univ-branch"))
{
error(@1, "automaton is has no universal branching...");
error(p.loc, "... despite 'properties: univ-branch'");
det_warned = true;
} }
} }
state-num: INT state-num: INT
{ {
if (((int) $1) < 0) if (((int) $1) < 0)
...@@ -1132,7 +1180,7 @@ checked-state-num: state-num ...@@ -1132,7 +1180,7 @@ checked-state-num: state-num
states: | states state states: | states state
{ {
if ((res.deterministic.is_true() || res.complete.is_true())) if ((res.universal.is_true() || res.complete.is_true()))
{ {
bdd available = bddtrue; bdd available = bddtrue;
bool det = true; bool det = true;
...@@ -1142,15 +1190,21 @@ states: | states state ...@@ -1142,15 +1190,21 @@ states: | states state
det = false; det = false;
available -= t.cond; available -= t.cond;
} }
if (res.deterministic.is_true() && !det) if (res.universal.is_true() && !det)
{ {
res.deterministic = false; res.universal = false;
if (auto p = res.prop_is_true("deterministic")) if (auto p = res.prop_is_true("deterministic"))
{ {
error(@2, "automaton is not deterministic..."); error(@2, "automaton is not deterministic...");
error(p.loc, error(p.loc,
"... despite 'properties: deterministic'"); "... despite 'properties: deterministic'");
} }
else if (auto p = res.prop_is_false("exist-branch"))
{
error(@2, "automaton has existential branching...");
error(p.loc,
"... despite 'properties: !exist-branch'");
}
} }
if (res.complete.is_true() && available != bddfalse) if (res.complete.is_true() && available != bddfalse)
{ {
...@@ -1192,7 +1246,8 @@ state: state-name labeled-edges ...@@ -1192,7 +1246,8 @@ state: state-name labeled-edges
{ {
// Assume the worse. This skips the tests about determinism // Assume the worse. This skips the tests about determinism
// we might perform on the state. // we might perform on the state.
res.deterministic = spot::trival::maybe(); res.universal = spot::trival::maybe();
res.existential = spot::trival::maybe();
res.complete = spot::trival::maybe(); res.complete = spot::trival::maybe();
} }
...@@ -1402,6 +1457,7 @@ state-conj-checked: state-conj-2 ...@@ -1402,6 +1457,7 @@ state-conj-checked: state-conj-2
" previous declaration..."); " previous declaration...");
error(ub.loc, "... here"); error(ub.loc, "... here");
} }
res.existential = false;
} }
/* Block of unlabeled edge, with occasional (incorrect) labeled /* Block of unlabeled edge, with occasional (incorrect) labeled
...@@ -1531,7 +1587,8 @@ dstar_header: dstar_sizes ...@@ -1531,7 +1587,8 @@ dstar_header: dstar_sizes
res.info_states.resize(res.states); res.info_states.resize(res.states);
} }
res.acc_style = State_Acc; res.acc_style = State_Acc;
res.deterministic = true; res.universal = true;
res.existential = true;
res.complete = true; res.complete = true;
fill_guards(res); fill_guards(res);
res.cur_guard = res.guards.end(); res.cur_guard = res.guards.end();
...@@ -2339,9 +2396,7 @@ static void fix_initial_state(result_& r) ...@@ -2339,9 +2396,7 @@ static void fix_initial_state(result_& r)
static void fix_properties(result_& r) static void fix_properties(result_& r)
{ {
r.aut_or_ks->prop_universal(r.deterministic); r.aut_or_ks->prop_universal(r.universal);
// std::cerr << "fix det: " << r.deterministic << '\n';
// std::cerr << "fix complete: " << r.complete << '\n';
r.aut_or_ks->prop_complete(r.complete); r.aut_or_ks->prop_complete(r.complete);
if (r.acc_style == State_Acc || if (r.acc_style == State_Acc ||
(r.acc_style == Mixed_Acc && !r.trans_acc_seen)) (r.acc_style == Mixed_Acc && !r.trans_acc_seen))
...@@ -2373,7 +2428,7 @@ static void check_version(const result_& r) ...@@ -2373,7 +2428,7 @@ static void check_version(const result_& r)
std::ostringstream s; std::ostringstream s;
s << "we can read HOA v" << supported s << "we can read HOA v" << supported
<< " but this file uses " << v << "; this might " << " but this file uses " << v << "; this might "
<< "cause the following errors"; "cause the following errors";
r.h->errors.emplace_front(r.format_version_loc, s.str()); r.h->errors.emplace_front(r.format_version_loc, s.str());
return; return;
} }
......
...@@ -50,7 +50,7 @@ namespace spot ...@@ -50,7 +50,7 @@ namespace spot
std::vector<bool> common_acc; std::vector<bool> common_acc;
bool has_state_acc; bool has_state_acc;
bool is_complete; bool is_complete;
bool is_deterministic; bool is_universal;
bool is_colored; bool is_colored;
bool use_implicit_labels; bool use_implicit_labels;
bool use_state_labels = true; bool use_state_labels = true;
...@@ -65,7 +65,7 @@ namespace spot ...@@ -65,7 +65,7 @@ namespace spot
bool state_labels) bool state_labels)
{ {
check_det_and_comp(aut); check_det_and_comp(aut);
use_implicit_labels = implicit && is_deterministic && is_complete; use_implicit_labels = implicit && is_universal && is_complete;
use_state_labels &= state_labels; use_state_labels &= state_labels;
number_all_ap(aut); number_all_ap(aut);
} }
...@@ -95,7 +95,7 @@ namespace spot ...@@ -95,7 +95,7 @@ namespace spot
std::string empty; std::string empty;
unsigned ns = aut->num_states(); unsigned ns = aut->num_states();
bool deterministic = true; bool universal = true;
bool complete = true; bool complete = true;
bool state_acc = true; bool state_acc = true;
bool nodeadend = true; bool nodeadend = true;
...@@ -117,10 +117,10 @@ namespace spot ...@@ -117,10 +117,10 @@ namespace spot
lastcond = t.cond; lastcond = t.cond;
if (complete) if (complete)
sum |= t.cond; sum |= t.cond;
if (deterministic) if (universal)
{ {
if (!bdd_implies(t.cond, available)) if (!bdd_implies(t.cond, available))
deterministic = false; universal = false;
else else
available -= t.cond; available -= t.cond;
} }
...@@ -151,7 +151,7 @@ namespace spot ...@@ -151,7 +151,7 @@ namespace spot
common_acc.push_back(st_acc); common_acc.push_back(st_acc);
state_acc &= st_acc; state_acc &= st_acc;
} }
is_deterministic = deterministic; is_universal = universal;
is_complete = complete; is_complete = complete;
has_state_acc = state_acc; has_state_acc = state_acc;
// If the automaton has state-based acceptance and contain // If the automaton has state-based acceptance and contain
...@@ -160,10 +160,10 @@ namespace spot ...@@ -160,10 +160,10 @@ namespace spot
is_colored = colored && (!has_state_acc || nodeadend); is_colored = colored && (!has_state_acc || nodeadend);
// If the automaton declares that it is universal or // If the automaton declares that it is universal or
// state-based, make sure that it really is. // state-based, make sure that it really is.
if (aut->prop_universal().is_true() && !deterministic) if (aut->prop_universal().is_true() && !universal)
throw std::runtime_error("print_hoa(): automaton is not universal" throw std::runtime_error("print_hoa(): automaton is not universal"
" but prop_universal()==true"); " but prop_universal()==true");
if (aut->prop_universal().is_false() && deterministic) if (aut->prop_universal().is_false() && universal)
throw std::runtime_error("print_hoa(): automaton is universal" throw std::runtime_error("print_hoa(): automaton is universal"
" despite prop_universal()==false"); " despite prop_universal()==false");
if (aut->prop_complete().is_true() && !complete) if (aut->prop_complete().is_true() && !complete)
...@@ -455,21 +455,6 @@ namespace spot ...@@ -455,21 +455,6 @@ namespace spot
} }
os << str; os << str;
}; };
// It's probable that nobody cares about the "no-univ-branch"
// property. The "univ-branch" property seems more important to
// announce that the automaton might not be parsable by tools that
// do not support alternating automata.
if (!aut->is_existential())
{
prop(" univ-branch");
}
else if (verbose)
{
if (v1_1)
prop(" !univ-branch");
else
prop(" no-univ-branch");
}
implicit_labels = md.use_implicit_labels; implicit_labels = md.use_implicit_labels;
state_labels = md.use_state_labels; state_labels = md.use_state_labels;
if (implicit_labels) if (implicit_labels)
...@@ -490,20 +475,60 @@ namespace spot ...@@ -490,20 +475,60 @@ namespace spot
prop(" complete"); prop(" complete");
else if (v1_1) else if (v1_1)
prop(" !complete"); prop(" !complete");
if (md.is_deterministic) // The definition of "deterministic" was changed between HOA v1
prop(" deterministic"); // (were it meant "universal") and HOA v1.1 were it means
else if (v1_1) // ("universal" and "existential").
prop(" !deterministic"); if (!v1_1)
{
if (md.is_universal)
prop(" deterministic");
// It's probable that nobody cares about the "no-univ-branch"
// property. The "univ-branch" property seems more important to
// announce that the automaton might not be parsable by tools that
// do not support alternating automata.
if (!aut->is_existential())
{
prop(" univ-branch");
}
else if (verbose)
{
if (v1_1)
prop(" !univ-branch");
else
prop(" no-univ-branch");
}
}
else
{
if (md.is_universal && aut->is_existential())
{
prop(" deterministic");
if (verbose)
prop(" !univ-branch !exist-branch");
}
else
{
prop(" !deterministic");
if (!aut->is_existential())
prop(" univ-branch");
else if (verbose)
prop(" !univ-branch");
if (!md.is_universal)
prop(" exist-branch");
else if (verbose)
prop(" !exist-branch");
}
}
// Deterministic automata are also unambiguous, so writing both // Deterministic automata are also unambiguous, so writing both
// properties seems redundant. People working on unambiguous // properties seems redundant. People working on unambiguous
// automata are usually concerned about non-deterministic // automata are usually concerned about non-deterministic
// unambiguous automata. So do not mention "unambiguous" // unambiguous automata. So do not mention "unambiguous"
// in the case of deterministic automata. // in the case of deterministic automata.
if (aut->prop_unambiguous() && (verbose || !md.is_deterministic)) if (aut->prop_unambiguous() && (verbose || !md.is_universal))
prop(" unambiguous"); prop(" unambiguous");
else if (v1_1 && !aut->prop_unambiguous()) else if (v1_1 && !aut->prop_unambiguous())
prop(" !unambiguous"); prop(" !unambiguous");
if (aut->prop_semi_deterministic() && (verbose || !md.is_deterministic)) if (aut->prop_semi_deterministic() && (verbose || !md.is_universal))
prop(" semi-deterministic"); prop(" semi-deterministic");
else if (v1_1 && !aut->prop_semi_deterministic()) else if (v1_1 && !aut->prop_semi_deterministic())
prop(" !semi-deterministic"); prop(" !semi-deterministic");
......
...@@ -129,7 +129,7 @@ diff expect.dot alt.dot ...@@ -129,7 +129,7 @@ diff expect.dot alt.dot
autfilt --trust=no --check=strength alt.hoa | grep properties: >output autfilt --trust=no --check=strength alt.hoa | grep properties: >output
cat >expected <<EOF cat >expected <<EOF
properties: univ-branch trans-labels explicit-labels state-acc properties: trans-labels explicit-labels state-acc univ-branch
properties: very-weak properties: very-weak
EOF EOF
diff output expected diff output expected
...@@ -168,7 +168,7 @@ Start: 0 ...@@ -168,7 +168,7 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: Buchi acc-name: Buchi
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
properties: univ-branch trans-labels explicit-labels state-acc complete properties: trans-labels explicit-labels state-acc complete univ-branch
properties: very-weak properties: very-weak
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
...@@ -211,8 +211,8 @@ Start: 0 ...@@ -211,8 +211,8 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -232,8 +232,8 @@ Start: 0&1 ...@@ -232,8 +232,8 @@ Start: 0&1
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -253,8 +253,8 @@ Start: 0 ...@@ -253,8 +253,8 @@ Start: 0
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 1 [0] 1
...@@ -280,8 +280,8 @@ Start: 0&2 ...@@ -280,8 +280,8 @@ Start: 0&2
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc properties: trans-labels explicit-labels trans-acc deterministic
properties: deterministic properties: univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -301,8 +301,8 @@ Start: 0&2&4 ...@@ -301,8 +301,8 @@ Start: 0&2&4
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc properties: trans-labels explicit-labels trans-acc deterministic
properties: deterministic properties: univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -325,8 +325,8 @@ Start: 0&1 ...@@ -325,8 +325,8 @@ Start: 0&1
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -343,8 +343,8 @@ Start: 0&1&3 ...@@ -343,8 +343,8 @@ Start: 0&1&3
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc properties: trans-labels explicit-labels trans-acc deterministic
properties: deterministic properties: univ-branch
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [0] 0
...@@ -365,8 +365,8 @@ Start: 0&1 ...@@ -365,8 +365,8 @@ Start: 0&1
AP: 1 "a" AP: 1 "a"
acc-name: co-Buchi acc-name: co-Buchi
Acceptance: 1 Fin(0) Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic univ-