parseaut: allow false edges to not be dropped

This is a followup to issue #548, which was caused by edges being
dropped.  In that context dropping edge was not really desirable, so
let's make this behavior configurable.

* spot/parseaut/public.hh: Add a new option.
* python/spot/__init__.py: Likewise.
* spot/parseaut/parseaut.yy: Honor that option.
* tests/python/parsetgba.py: Add a short test for it.
* NEWS: Mention it.

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

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:

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,

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
+  /// This is a wrapper around spot::automaton_stream_parser that
-  /// the first automaton of the file.  Empty inputs are reported as
+  /// returns the first automaton of the file.  Empty inputs are
-  /// syntax errors, so the \c aut field of the result is guaranteed not
+  /// reported as syntax errors, so the \c aut field of the result is
-  /// to be null if \c errors is empty.  (This is unlike
+  /// guaranteed not to be null if \c errors is empty.  (This is
-  /// automaton_stream_parser::parse() where a null \c aut denots the
+  /// unlike automaton_stream_parser::parse() where a null \c aut
-  /// end of a stream.)
+  /// denotes the end of a stream.)
   ///
   /// \warning This function is not reentrant.
   SPOT_API parsed_aut_ptr

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--""")