From d3607a7ce3fd47df9a79c19cb33e45590927ef73 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 31 Jul 2017 21:03:49 +0200 Subject: [PATCH] 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. --- NEWS | 9 +++ spot/parseaut/parseaut.yy | 91 +++++++++++++++++++++++------ spot/twaalgos/hoa.cc | 83 +++++++++++++++++---------- tests/core/alternating.test | 40 ++++++------- tests/core/complete.test | 16 +++--- tests/core/det.test | 8 +-- tests/core/explsum.test | 6 +- tests/core/parseaut.test | 110 +++++++++++++++++++++++++++++++++--- tests/core/readsave.test | 4 +- tests/core/sbacc.test | 2 +- tests/core/tgbagraph.test | 4 +- tests/python/alternating.py | 8 +-- tests/python/dualize.py | 16 +++--- 13 files changed, 291 insertions(+), 106 deletions(-) diff --git a/NEWS b/NEWS index 70319502c..214682f11 100644 --- a/NEWS +++ b/NEWS @@ -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., 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: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 5e9e37a0e..613dcb0cb 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -146,7 +146,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); bool accept_all_seen = 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(); bool trans_acc_seen = false; @@ -346,6 +347,7 @@ BOOLEAN: 't' | 'f' header: format-version header-items { + bool v1plus = strverscmp("v1", res.format_version.c_str()) < 0; // Preallocate the states if we know their number. if (res.states >= 0) { @@ -457,14 +459,15 @@ header: format-version header-items res.acc_style = State_Acc; } - auto univ_branch = res.prop_is_true("univ-branch"); - if (res.opts.want_kripke && univ_branch) - error(univ_branch.loc, - "Kripke structures may not use 'properties: univ-branch'"); + if (auto univ_branch = res.prop_is_true("univ-branch")) + if (res.opts.want_kripke) + error(univ_branch.loc, + "Kripke structures may not use 'properties: univ-branch'"); } { unsigned ss = res.start.size(); auto det = res.prop_is_true("deterministic"); + auto no_exist = res.prop_is_false("exist-branch"); if (ss > 1) { if (det) @@ -472,16 +475,46 @@ header: format-version header-items error(det.loc, "deterministic automata should have at most " "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 { // Assume the automaton is deterministic until proven // wrong, or unless we are building a Kripke structure. 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"); if (ss < 1) { @@ -1069,14 +1102,29 @@ body: states error(@1, "automaton is 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")) { error(@1, "automaton is 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 { if (((int) $1) < 0) @@ -1132,7 +1180,7 @@ checked-state-num: state-num states: | states state { - if ((res.deterministic.is_true() || res.complete.is_true())) + if ((res.universal.is_true() || res.complete.is_true())) { bdd available = bddtrue; bool det = true; @@ -1142,15 +1190,21 @@ states: | states state det = false; 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")) { error(@2, "automaton is not deterministic..."); error(p.loc, "... 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) { @@ -1192,7 +1246,8 @@ state: state-name labeled-edges { // Assume the worse. This skips the tests about determinism // 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(); } @@ -1402,6 +1457,7 @@ state-conj-checked: state-conj-2 " previous declaration..."); error(ub.loc, "... here"); } + res.existential = false; } /* Block of unlabeled edge, with occasional (incorrect) labeled @@ -1531,7 +1587,8 @@ dstar_header: dstar_sizes res.info_states.resize(res.states); } res.acc_style = State_Acc; - res.deterministic = true; + res.universal = true; + res.existential = true; res.complete = true; fill_guards(res); res.cur_guard = res.guards.end(); @@ -2339,9 +2396,7 @@ static void fix_initial_state(result_& r) static void fix_properties(result_& r) { - r.aut_or_ks->prop_universal(r.deterministic); - // std::cerr << "fix det: " << r.deterministic << '\n'; - // std::cerr << "fix complete: " << r.complete << '\n'; + r.aut_or_ks->prop_universal(r.universal); r.aut_or_ks->prop_complete(r.complete); if (r.acc_style == State_Acc || (r.acc_style == Mixed_Acc && !r.trans_acc_seen)) @@ -2373,7 +2428,7 @@ static void check_version(const result_& r) std::ostringstream s; s << "we can read HOA v" << supported << " 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()); return; } diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index 061776328..51d45e6a7 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -50,7 +50,7 @@ namespace spot std::vector common_acc; bool has_state_acc; bool is_complete; - bool is_deterministic; + bool is_universal; bool is_colored; bool use_implicit_labels; bool use_state_labels = true; @@ -65,7 +65,7 @@ namespace spot bool state_labels) { 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; number_all_ap(aut); } @@ -95,7 +95,7 @@ namespace spot std::string empty; unsigned ns = aut->num_states(); - bool deterministic = true; + bool universal = true; bool complete = true; bool state_acc = true; bool nodeadend = true; @@ -117,10 +117,10 @@ namespace spot lastcond = t.cond; if (complete) sum |= t.cond; - if (deterministic) + if (universal) { if (!bdd_implies(t.cond, available)) - deterministic = false; + universal = false; else available -= t.cond; } @@ -151,7 +151,7 @@ namespace spot common_acc.push_back(st_acc); state_acc &= st_acc; } - is_deterministic = deterministic; + is_universal = universal; is_complete = complete; has_state_acc = state_acc; // If the automaton has state-based acceptance and contain @@ -160,10 +160,10 @@ namespace spot is_colored = colored && (!has_state_acc || nodeadend); // If the automaton declares that it is universal or // 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" " 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" " despite prop_universal()==false"); if (aut->prop_complete().is_true() && !complete) @@ -455,21 +455,6 @@ namespace spot } 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; state_labels = md.use_state_labels; if (implicit_labels) @@ -490,20 +475,60 @@ namespace spot prop(" complete"); else if (v1_1) prop(" !complete"); - if (md.is_deterministic) - prop(" deterministic"); - else if (v1_1) - prop(" !deterministic"); + // The definition of "deterministic" was changed between HOA v1 + // (were it meant "universal") and HOA v1.1 were it means + // ("universal" and "existential"). + 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 // properties seems redundant. People working on unambiguous // automata are usually concerned about non-deterministic // unambiguous automata. So do not mention "unambiguous" // in the case of deterministic automata. - if (aut->prop_unambiguous() && (verbose || !md.is_deterministic)) + if (aut->prop_unambiguous() && (verbose || !md.is_universal)) prop(" unambiguous"); else if (v1_1 && !aut->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"); else if (v1_1 && !aut->prop_semi_deterministic()) prop(" !semi-deterministic"); diff --git a/tests/core/alternating.test b/tests/core/alternating.test index a0878c310..614faacc3 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -129,7 +129,7 @@ diff expect.dot alt.dot autfilt --trust=no --check=strength alt.hoa | grep properties: >output cat >expected <