diff --git a/NEWS b/NEWS index a080fe084..ff522766e 100644 --- a/NEWS +++ b/NEWS @@ -74,14 +74,18 @@ New in spot 1.99.6a (not yet released) acc_cond::is_ff() -> acc_cond::is_f() parse_acc_code() -> acc_cond::acc_code(...) - * Automata property bits (those that tell whether the automaton is deterministic, weak, stutter-invariant, etc.) are now stored using three-valued logic: in addition to "maybe"/"yes" they can now also represent "no". This is some preparation for the upcomming - support of the HOA v1.1 format, but it also saves some time in - some algorithms (e.g, is_deterministic() can now return - immediately on automata marked as not deterministic). + support of the HOA v1.1 format, but it also saves time in some + algorithms (e.g, is_deterministic() can now return immediately on + automata marked as not deterministic). + + * The automaton parser now accept negated properties as they will be + introduced in HOA v1.1, and will check for some inconsistencies. + These properties are stored and used when appropriate, but they + are not yet output by the HOA printer. Python: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 899d073f4..1675b37a6 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -97,7 +97,16 @@ extern "C" int strverscmp(const char *s1, const char *s2); std::vector info_states; // States declared and used. std::vector> start; // Initial states; std::unordered_map alias; - std::unordered_map props; + struct prop_info + { + spot::location loc; + bool val; + operator bool() const + { + return val; + }; + }; + std::unordered_map props; spot::location states_loc; spot::location ap_loc; spot::location state_label_loc; @@ -138,6 +147,14 @@ extern "C" int strverscmp(const char *s1, const char *s2); std::map labels; + prop_info prop_is_true(const std::string& p) + { + auto i = props.find(p); + if (i == props.end()) + return prop_info{spot::location(), false}; + return i->second; + } + ~result_() { delete namer; @@ -323,52 +340,52 @@ header: format-version header-items } // Process properties. { - auto explicit_labels = res.props.find("explicit-labels"); - auto implicit_labels = res.props.find("implicit-labels"); + auto explicit_labels = res.prop_is_true("explicit-labels"); + auto implicit_labels = res.prop_is_true("implicit-labels"); - if (implicit_labels != res.props.end() && res.opts.want_kripke) - error(implicit_labels->second, - "Kripke structure may not use implicit labels"); - - if (implicit_labels != res.props.end()) + if (implicit_labels) { - if (explicit_labels == res.props.end()) + if (res.opts.want_kripke) + error(implicit_labels.loc, + "Kripke structure may not use implicit labels"); + + if (explicit_labels) { - res.label_style = Implicit_Labels; + error(implicit_labels.loc, + "'properties: implicit-labels' is incompatible " + "with..."); + error(explicit_labels.loc, + "... 'properties: explicit-labels'."); } else { - error(implicit_labels->second, - "'properties: implicit-labels' is incompatible " - "with..."); - error(explicit_labels->second, - "... 'properties: explicit-labels'."); + res.label_style = Implicit_Labels; } } - auto trans_labels = res.props.find("trans-labels"); - auto state_labels = res.props.find("state-labels"); + auto trans_labels = res.prop_is_true("trans-labels"); + auto state_labels = res.prop_is_true("state-labels"); - if (trans_labels != res.props.end() && res.opts.want_kripke) - error(trans_labels->second, - "Kripke structure may not use transition labels"); - - if (trans_labels != res.props.end()) + if (trans_labels) { - if (state_labels == res.props.end()) + if (res.opts.want_kripke) + error(trans_labels.loc, + "Kripke structure may not use transition labels"); + + if (state_labels) + { + error(trans_labels.loc, + "'properties: trans-labels' is incompatible with..."); + error(state_labels.loc, + "... 'properties: state-labels'."); + } + else { if (res.label_style != Implicit_Labels) res.label_style = Trans_Labels; } - else - { - error(trans_labels->second, - "'properties: trans-labels' is incompatible with..."); - error(state_labels->second, - "... 'properties: state-labels'."); - } } - else if (state_labels != res.props.end()) + else if (state_labels) { if (res.label_style != Implicit_Labels) { @@ -376,9 +393,9 @@ header: format-version header-items } else { - error(state_labels->second, + error(state_labels.loc, "'properties: state-labels' is incompatible with..."); - error(implicit_labels->second, + error(implicit_labels.loc, "... 'properties: implicit-labels'."); } } @@ -387,35 +404,35 @@ header: format-version header-items error(@$, "Kripke structure should use 'properties: state-labels'"); - auto state_acc = res.props.find("state-acc"); - auto trans_acc = res.props.find("trans-acc"); - if (trans_acc != res.props.end()) + auto state_acc = res.prop_is_true("state-acc"); + auto trans_acc = res.prop_is_true("trans-acc"); + if (trans_acc) { - if (state_acc == res.props.end()) + if (state_acc) { - res.acc_style = Trans_Acc; + error(trans_acc.loc, + "'properties: trans-acc' is incompatible with..."); + error(state_acc.loc, + "... 'properties: state-acc'."); } else { - error(trans_acc->second, - "'properties: trans-acc' is incompatible with..."); - error(state_acc->second, - "... 'properties: state-acc'."); + res.acc_style = Trans_Acc; } } - else if (state_acc != res.props.end()) + else if (state_acc) { res.acc_style = State_Acc; } } { unsigned ss = res.start.size(); - auto det = res.props.find("deterministic"); + auto det = res.prop_is_true("deterministic"); if (ss > 1) { - if (det != res.props.end()) + if (det) { - error(det->second, + error(det.loc, "deterministic automata should have at most " "one initial state"); } @@ -427,12 +444,12 @@ header: format-version header-items // wrong, or unless we are building a Kripke structure. res.deterministic = !res.opts.want_kripke; } - auto complete = res.props.find("complete"); + auto complete = res.prop_is_true("complete"); if (ss < 1) { - if (complete != res.props.end()) + if (complete) { - error(complete->second, + error(complete.loc, "complete automata should have at least " "one initial state"); } @@ -447,9 +464,8 @@ header: format-version header-items // if ap_count == 0, then a Kripke structure could be // declared complete, although that probably doesn't // matter. - if (res.opts.want_kripke && complete != res.props.end() - && res.ap_count > 0) - error(complete->second, + if (res.opts.want_kripke && complete && res.ap_count > 0) + error(complete.loc, "Kripke structure may not be complete"); } if (res.opts.trust_hoa) @@ -457,25 +473,68 @@ header: format-version header-items auto& a = res.aut_or_ks; auto& p = res.props; auto e = p.end(); - if (p.find("stutter-invariant") != e) + auto si = p.find("stutter-invariant"); + if (si != e) { - a->prop_stutter_invariant(true); + a->prop_stutter_invariant(si->second.val); auto i = p.find("stutter-sensitive"); - if (i != e) - error(i->second, + if (i != e && si->second.val == i->second.val) + error(i->second.loc, "automaton cannot be both stutter-invariant" "and stutter-sensitive"); } - if (p.find("stutter-sensitive") != e) - a->prop_stutter_invariant(false); - if (p.find("inherently-weak") != e) - a->prop_inherently_weak(true); - if (p.find("weak") != e) - a->prop_weak(true); - if (p.find("terminal") != e) - a->prop_terminal(true); - if (p.find("unambiguous") != e) - a->prop_unambiguous(true); + else + { + auto ss = p.find("stutter-sensitive"); + if (ss != e) + a->prop_stutter_invariant(!ss->second.val); + } + auto iw = p.find("inherently-weak"); + auto w = p.find("weak"); + auto t = p.find("terminal"); + if (iw != e) + { + a->prop_inherently_weak(iw->second.val); + if (w != e && !iw->second.val && w->second.val) + { + error(w->second.loc, "'properties: weak' contradicts..."); + error(iw->second.loc, + "... 'properties: !inherently-weak' given here"); + } + if (t != e && !iw->second.val && t->second.val) + { + error(t->second.loc, + "'properties: terminal' contradicts..."); + error(iw->second.loc, + "... 'properties: !inherently-weak' given here"); + } + } + if (w != e) + { + a->prop_weak(w->second.val); + if (t != e && !w->second.val && t->second.val) + { + error(t->second.loc, + "'properties: terminal' contradicts..."); + error(w->second.loc, + "... 'properties: !weak' given here"); + } + } + if (t != e) + a->prop_terminal(t->second.val); + auto u = p.find("unambiguous"); + if (u != e) + { + a->prop_unambiguous(u->second.val); + auto d = p.find("deterministic"); + if (d != e && !u->second.val && d->second.val) + { + error(d->second.loc, + "'properties: deterministic' contradicts..."); + error(u->second.loc, + "... 'properties: !unambiguous' given here"); + } + } } } @@ -654,9 +713,34 @@ acc-spec: | acc-spec BOOLEAN } properties: | properties IDENTIFIER { - res.props.emplace(*$2, @2); + auto pos = res.props.emplace(*$2, result_::prop_info{@2, true}); + if (!pos.first->second.val) + { + std::ostringstream out(std::ios_base::ate); + error(@2, std::string("'properties: ") + + *$2 + "' contradicts..."); + error(pos.first->second.loc, + std::string("... 'properties: !") + *$2 + + "' previously given here."); + } delete $2; } + | properties '!' IDENTIFIER + { + auto loc = @2 + @3; + auto pos = + res.props.emplace(*$3, result_::prop_info{loc, false}); + if (pos.first->second.val) + { + std::ostringstream out(std::ios_base::ate); + error(loc, std::string("'properties: !") + + *$3 + "' contradicts..."); + error(pos.first->second.loc, + std::string("... 'properties: ") + *$3 + + "' previously given here."); + } + delete $3; + } header-spec: | header-spec BOOLEAN | header-spec INT | header-spec STRING @@ -918,22 +1002,20 @@ states: | states state if (res.deterministic && !det) { res.deterministic = false; - auto p = res.props.find("deterministic"); - if (p != res.props.end()) + if (auto p = res.prop_is_true("deterministic")) { error(@2, "automaton is not deterministic..."); - error(p->second, + error(p.loc, "... despite 'properties: deterministic'"); } } if (res.complete && available != bddfalse) { res.complete = false; - auto p = res.props.find("complete"); - if (p != res.props.end()) + if (auto p = res.prop_is_true("complete")) { error(@2, "automaton is not complete..."); - error(p->second, "... despite 'properties: complete'"); + error(p.loc, "... despite 'properties: complete'"); } } } @@ -950,7 +1032,7 @@ state: state-name labeled-edges { error(@2, "these transitions have implicit labels but the" " automaton is..."); - error(res.props["state-labels"], "... declared with " + error(res.props["state-labels"].loc, "... declared with " "'properties: state-labels'"); // Do not repeat this message. res.label_style = Mixed_Labels; @@ -1019,11 +1101,11 @@ state-label_opt: { res.has_state_label = false; } error(@$, "state label used although the automaton was..."); if (res.label_style == Trans_Labels) - error(res.props["trans-labels"], + error(res.props["trans-labels"].loc, "... declared with 'properties: trans-labels'" " here"); else - error(res.props["implicit-labels"], + error(res.props["implicit-labels"].loc, "... declared with 'properties: implicit-labels'" " here"); // Do not show this error anymore. @@ -1045,11 +1127,11 @@ trans-label: label error(@$, "transition label used although the " "automaton was..."); if (res.label_style == State_Labels) - error(res.props["state-labels"], + error(res.props["state-labels"].loc, "... declared with 'properties: state-labels' " "here"); else - error(res.props["implicit-labels"], + error(res.props["implicit-labels"].loc, "... declared with 'properties: implicit-labels'" " here"); // Do not show this error anymore. @@ -1094,7 +1176,7 @@ state-acc_opt: if (res.acc_style == Trans_Acc) { error(@$, "state-based acceptance used despite..."); - error(res.props["trans-acc"], + error(res.props["trans-acc"].loc, "... declaration of transition-based acceptance."); res.acc_style = Mixed_Acc; } @@ -1110,7 +1192,7 @@ trans-acc_opt: if (res.acc_style == State_Acc) { error(@$, "trans-based acceptance used despite..."); - error(res.props["state-acc"], + error(res.props["state-acc"].loc, "... declaration of state-based acceptance."); res.acc_style = Mixed_Acc; } diff --git a/tests/core/parseaut.test b/tests/core/parseaut.test index 48a3ed959..c859adb41 100755 --- a/tests/core/parseaut.test +++ b/tests/core/parseaut.test @@ -374,8 +374,8 @@ cat >input<input<input<