diff --git a/NEWS b/NEWS index d5bc2371d..021548c09 100644 --- a/NEWS +++ b/NEWS @@ -49,6 +49,10 @@ New in spot 2.11.6.dev (not yet released) supports only one): it now reuse the edges leaving initial states without incoming transitions. + - The automaton parser has a new option "drop_false_edges" to + specify where edges labeled by "false" should be ignored during + parsing. It is enabled by default for backward compatibility. + - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula() that converts a BDD into a CNF instead of a DNF. @@ -104,6 +108,12 @@ New in spot 2.11.6.dev (not yet released) removal of superfluous APs that is now performed by ltlsynt (search for --polarity and --global-equivalence above). + Python: + + - The spot.automata() and spot.automaton() functions now accept a + drop_false_edges=False argument to disable the historical behavior + of ignoring edges labeled by False. + Bugs fixed: - tgba_determinize()'s use_simulation option would cause it to diff --git a/python/spot/__init__.py b/python/spot/__init__.py index 02bdcb1f6..cefb59b77 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -564,7 +564,7 @@ function acd{num}_node(node, acc){{ def automata(*sources, timeout=None, ignore_abort=True, trust_hoa=True, no_sid=False, debug=False, - want_kripke=False): + want_kripke=False, drop_false_edges=True): """Read automata from a list of sources. Parameters @@ -587,6 +587,9 @@ def automata(*sources, timeout=None, ignore_abort=True, If True, the input is expected to discribe Kripke structures, in the HOA format, and the returned type will be of type kripke_graph_ptr. + drop_false_edges : bool, optional + If True (the default), edges labeled by false will + be ignored during parsing. no_sid : bool, optional When an automaton is obtained from a subprocess, this subprocess is started from a shell with its own session @@ -647,6 +650,7 @@ def automata(*sources, timeout=None, ignore_abort=True, o.trust_hoa = trust_hoa o.raise_errors = True o.want_kripke = want_kripke + o.drop_false_edges = drop_false_edges for filename in sources: try: diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 05e404474..8de9d9fab 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -1649,7 +1649,7 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt "(previous edge is labeled)"); else cond = res.state_label; - if (cond != bddfalse) + if (cond != bddfalse || !res.opts.drop_false_edges) { unsigned e; if (res.opts.want_kripke) @@ -1665,12 +1665,13 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt labeled-edge: trans-label checked-state-num trans-acc_opt { unsigned e = 0; - if (res.cur_label != bddfalse || + if (res.cur_label != bddfalse + || !res.opts.drop_false_edges // As a hack to allow states to be accepting // even if they do not have transitions, we // do not ignore false-labeled self-loops if they // have some colors) - ($2 == res.cur_state && !!($3 | res.acc_state))) + || ($2 == res.cur_state && !!($3 | res.acc_state))) { if (res.opts.want_kripke) e = res.h->ks->new_edge(res.cur_state, $2); @@ -1684,7 +1685,7 @@ labeled-edge: trans-label checked-state-num trans-acc_opt | trans-label state-conj-checked trans-acc_opt { unsigned e = 0; - if (res.cur_label != bddfalse) + if (res.cur_label != bddfalse || !res.opts.drop_false_edges) { assert(!res.opts.want_kripke); e = res.h->aut->new_univ_edge(res.cur_state, @@ -1737,7 +1738,7 @@ unlabeled-edge: checked-state-num trans-acc_opt } } unsigned e = 0; - if (cond != bddfalse) + if (cond != bddfalse || !res.opts.drop_false_edges) { if (res.opts.want_kripke) e = res.h->ks->new_edge(res.cur_state, $1); @@ -1770,7 +1771,7 @@ unlabeled-edge: checked-state-num trans-acc_opt } } unsigned e = 0; - if (cond != bddfalse) + if (cond != bddfalse || !res.opts.drop_false_edges) { assert(!res.opts.want_kripke); e = res.h->aut->new_univ_edge(res.cur_state, diff --git a/spot/parseaut/public.hh b/spot/parseaut/public.hh index ec16b3ad7..2a5cfff76 100644 --- a/spot/parseaut/public.hh +++ b/spot/parseaut/public.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2022 Laboratoire de Recherche et +// Copyright (C) 2013-2017, 2022-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -103,6 +103,7 @@ namespace spot bool trust_hoa = true; ///< Trust properties in HOA files bool raise_errors = false; ///< Raise errors as exceptions. bool want_kripke = false; ///< Parse as a Kripke structure. + bool drop_false_edges = true; ///< Drop edges with false labels. }; /// \brief Parse a stream of automata @@ -193,12 +194,12 @@ namespace spot /// \param opts Additional options to pass to the parser. /// \return A pointer to a \c parsed_aut structure. /// - /// This is a wrapper around spot::automaton_stream_parser that returns - /// the first automaton of the file. Empty inputs are reported as - /// syntax errors, so the \c aut field of the result is guaranteed not - /// to be null if \c errors is empty. (This is unlike - /// automaton_stream_parser::parse() where a null \c aut denots the - /// end of a stream.) + /// This is a wrapper around spot::automaton_stream_parser that + /// returns the first automaton of the file. Empty inputs are + /// reported as syntax errors, so the \c aut field of the result is + /// guaranteed not to be null if \c errors is empty. (This is + /// unlike automaton_stream_parser::parse() where a null \c aut + /// denotes the end of a stream.) /// /// \warning This function is not reentrant. SPOT_API parsed_aut_ptr diff --git a/tests/python/parsetgba.py b/tests/python/parsetgba.py index 038b33a19..a91b702fb 100755 --- a/tests/python/parsetgba.py +++ b/tests/python/parsetgba.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2012, 2014, 2015, 2022 Laboratoire de Recherche et +# Copyright (C) 2012, 2014, 2015, 2022, 2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -35,11 +35,60 @@ out.write(contents) out.close() a = spot.parse_aut(filename, spot.make_bdd_dict()) - tc.assertFalse(a.errors) - spot.print_dot(spot.get_cout(), a.aut) - del a - os.unlink(filename) + + +autstr = """ +HOA: v1 +States: 2 +Start: 0 +AP: 0 +Acceptance: 0 t +spot.highlight.edges: 1 1 2 2 3 3 4 4 +--BODY-- +State: 0 +[t] 1 +[f] 0 +State: 1 +[f] 0 +[t] 0 +--END-- +""" + +a1 = spot.automaton(autstr) +tc.assertEqual(a1.to_str("hoa", "1.1"), """HOA: v1.1 +States: 2 +Start: 0 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic weak +spot.highlight.edges: 1 1 2 4 +--BODY-- +State: 0 +[t] 1 +State: 1 +[t] 0 +--END--""") +a2 = spot.automaton(autstr, drop_false_edges=False) +tc.assertEqual(a2.to_str("hoa", "1.1"), """HOA: v1.1 +States: 2 +Start: 0 +AP: 0 +acc-name: all +Acceptance: 0 t +properties: trans-labels explicit-labels state-acc complete +properties: deterministic weak +spot.highlight.edges: 1 1 2 2 3 3 4 4 +--BODY-- +State: 0 +[t] 1 +[f] 0 +State: 1 +[f] 0 +[t] 0 +--END--""")