parseaut: preliminary support for reading alternating automata

Currently this only reads universal branches.  The parser (and the
automaton code) do not support universal initial states.

* spot/parseaut/parseaut.yy: Read universal branches.  Deal with
the no-univ-branch/!univ-branch change in HOA 1.1.
* tests/python/alternating.py: Read the output of print_hoa.
* tests/core/parseaut.test: Adjust test output, and add more tests.

spot/parseaut/parseaut.yy

@@ -157,6 +157,14 @@ extern "C" int strverscmp(const char *s1, const char *s2);
 	return i->second;
       }
 
+      prop_info prop_is_false(const std::string& p)
+      {
+	auto i = props.find(p);
+	if (i == props.end())
+	  return prop_info{spot::location(), false};
+	return prop_info{i->second.loc, !i->second.val};
+      }
+
       ~result_()
       {
 	delete namer;
@@ -180,6 +188,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
   pair* p;
   std::list<pair>* list;
   spot::acc_cond::acc_code* code;
+  std::vector<unsigned>* states;
 }
 
 %code
@@ -230,6 +239,7 @@ extern "C" int strverscmp(const char *s1, const char *s2);
 %left '&'
 %nonassoc '!'
 
+%type <states> state-conj-2 state-conj-checked
 %type <num> checked-state-num state-num acc-set sign
 %type <b> label-expr
 %type <mark> acc-sig acc-sets trans-acc_opt state-acc_opt
@@ -274,9 +284,23 @@ extern "C" int strverscmp(const char *s1, const char *s2);
 %destructor { bdd_delref($$); } <b>
 %destructor { bdd_delref($$->first); delete $$->second; delete $$; } <p>
 %destructor { delete $$; } <code>
+%destructor { delete $$; } <states>
+%printer {
+  auto& os = debug_stream();
+  os << '{';
+  bool notfirst = false;
+  for (auto i: *$$)
+  {
+    if (notfirst)
+      os << ", ";
+    else
+      notfirst = true;
+    os << i;
+  }
+  os << '}';
+} <states>
 %destructor {
-  for (std::list<pair>::iterator i = $$->begin();
+  for (auto i = $$->begin(); i != $$->end(); ++i)
-       i != $$->end(); ++i)
   {
     bdd_delref(i->first);
     delete i->second;
@@ -374,7 +398,7 @@ header: format-version header-items
 	      {
 		if (res.opts.want_kripke)
 		  error(trans_labels.loc,
-			"Kripke structure may not use transition labels");
+			"Kripke structures may not use transition labels");
 
 		if (state_labels)
 		  {
@@ -406,7 +430,7 @@ header: format-version header-items
 
 	    if (res.opts.want_kripke && res.label_style != State_Labels)
 	      error(@$,
-		    "Kripke structure should use 'properties: state-labels'");
+		    "Kripke structures should use 'properties: state-labels'");
 
 	    auto state_acc = res.prop_is_true("state-acc");
 	    auto trans_acc = res.prop_is_true("trans-acc");
@@ -428,7 +452,12 @@ 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'");
+          }
 	  {
 	    unsigned ss = res.start.size();
 	    auto det = res.prop_is_true("deterministic");
@@ -602,7 +631,7 @@ header-item: "States:" INT
 	   }
            | "Start:" init-state-conj-2
 	     {
-	       error(@2, "alternation is not yet supported");
+	       error(@2, "alternation is not yet supported for initial states");
 	       YYABORT;
 	     }
            | "Start:" state-num
@@ -723,14 +752,22 @@ acc-spec: | acc-spec BOOLEAN
 	    }
 properties: | properties IDENTIFIER
 	      {
-		auto pos = res.props.emplace(*$2, result_::prop_info{@2, true});
+                bool val = true;
-		if (!pos.first->second.val)
+                // no-univ-branch was replaced by !univ-branch in HOA 1.1
+                if (*$2 == "no-univ-branch")
+                  {
+                    *$2 = "univ-branch";
+                    val = false;
+                  }
+		auto pos = res.props.emplace(*$2, result_::prop_info{@2, val});
+		if (pos.first->second.val != val)
 		  {
 		    std::ostringstream out(std::ios_base::ate);
 		    error(@2, std::string("'properties: ")
-			  + *$2 + "' contradicts...");
+			  + (val ? "" : "!") + *$2 + "' contradicts...");
 		    error(pos.first->second.loc,
-			  std::string("... 'properties: !") + *$2
+			  std::string("... 'properties: ")
+                          + (val ? "!" : "") + *$2
 			  + "' previously given here.");
 		  }
 		delete $2;
@@ -773,10 +810,17 @@ header-spec: | header-spec BOOLEAN
 	       }
 
 state-conj-2: checked-state-num '&' checked-state-num
+            {
+              $$ = new std::vector<unsigned>{$1, $3};
+            }
             | state-conj-2 '&' checked-state-num
+            {
+              $$ = $1;
+              $$->emplace_back($3);
+            }
 
 	      // Currently we do not check the number of these states
-	      // since we do not support alternation.
+	      // since we do not support alternation for initial states.
 init-state-conj-2: state-num '&' state-num
             | init-state-conj-2 '&' state-num
 
@@ -1262,12 +1306,30 @@ labeled-edge: trans-label checked-state-num trans-acc_opt
 					   res.cur_label, $3 | res.acc_state);
 		  }
 	      }
-	    | trans-label state-conj-2 trans-acc_opt
+	    | trans-label state-conj-checked trans-acc_opt
 	      {
-		error(@2, "alternation is not yet supported");
+                if (res.cur_label != bddfalse)
-		YYABORT;
+                  {
+                    assert(!res.opts.want_kripke);
+                    res.h->aut->new_univ_edge(res.cur_state,
+                                              $2->begin(), $2->end(),
+                                              res.cur_label,
+                                              $3 | res.acc_state);
+                  }
+                delete $2;
 	      }
 
+state-conj-checked: state-conj-2
+              {
+                $$ = $1;
+                if (auto ub = res.prop_is_false("univ-branch"))
+                  {
+                    error(@1, "universal branch used despite"
+                          " previous declaration...");
+                    error(ub.loc, "... here");
+                  }
+              }
+
 /* Block of unlabeled edge, with occasional (incorrect) labeled
    edge. We never have zero unlabeled edges, these are considered as
    zero labeled edges. */
@@ -1305,10 +1367,36 @@ unlabeled-edge: checked-state-num trans-acc_opt
 					     cond, $2 | res.acc_state);
 		    }
 		}
-	      | state-conj-2 trans-acc_opt
+	      | state-conj-checked trans-acc_opt
 		{
-		  error(@1, "alternation is not yet supported");
+		  bdd cond;
-		  YYABORT;
+		  if (res.has_state_label)
+		    {
+		      cond = res.state_label;
+		    }
+		  else
+		    {
+		      if (res.guards.empty())
+			fill_guards(res);
+		      if (res.cur_guard == res.guards.end())
+			{
+			  error(@$, "too many transitions for this state, "
+				"ignoring this one");
+			  cond = bddfalse;
+			}
+		      else
+			{
+			  cond = *res.cur_guard++;
+			}
+		    }
+		  if (cond != bddfalse)
+		    {
+		      assert(!res.opts.want_kripke);
+                      res.h->aut->new_univ_edge(res.cur_state,
+                                                $1->begin(), $1->end(),
+                                                cond, $2 | res.acc_state);
+		    }
+                  delete $1;
 		}
 incorrectly-labeled-edge: trans-label unlabeled-edge
                           {

tests/core/parseaut.test

@@ -1921,10 +1921,61 @@ State: 11 "t"
 EOF
 
 expecterr input <<EOF
-input:4.8-12: alternation is not yet supported
+input:4.8-12: alternation is not yet supported for initial states
 autfilt: failed to read automaton from input
 EOF
 
+# Some alternation errors
+cat >input <<EOF
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: no-univ-branch trans-labels explicit-labels state-acc
+properties: complete deterministic
+--BODY--
+State: 0
+[!0&!1] 0&1
+[0&!1] 1
+[!0&1] 2
+[0&1] 0&1
+--END--
+HOA: v1.1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: !univ-branch trans-labels explicit-labels state-acc
+properties: complete deterministic
+--BODY--
+State: 0
+[!0&!1] 0&1
+[0&!1] 1
+[!0&1] 2
+[0&1] 0&1
+--END--
+EOF
+
+err1="this might cause the following errors"
+expecterr input<<EOF
+input:11.9-11: universal branch used despite previous declaration...
+input:7.13-26: ... here
+input:14.7-9: universal branch used despite previous declaration...
+input:7.13-26: ... here
+input:11.11: state 1 has no definition
+input:13.8: state 2 has no definition
+input:16.6-9: we can read HOA v1 but this file uses v1.1; $err1
+input:26.9-11: universal branch used despite previous declaration...
+input:22.13-24: ... here
+input:29.7-9: universal branch used despite previous declaration...
+input:22.13-24: ... here
+input:26.11: state 1 has no definition
+input:28.8: state 2 has no definition
+EOF
+
 
 cat >input <<EOF
 HOA: v1
@@ -2056,6 +2107,50 @@ State: 0
 [!0&1] 0 {2}
 [0&1] 0 {}
 --END--
+HOA: v1
+tool: "ltl3ba" "1.1.3"
+name: "VWAA for (a U b) && G(F(b)) && F(G(a))"
+States: 7
+Start: 0
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+AP: 2 "b" "a"
+properties: trans-labels explicit-labels state-acc univ-branch very-weak
+--BODY--
+State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
+ [(0)] 3&1
+ [(!0 & 1)] 5&3&1
+State: 1 "FG(a)" {0}
+ [(1)] 2
+ [t] 1
+State: 2 "G(a)"
+ [(1)] 2
+State: 3 "GF(b)"
+ [(0)] 3
+ [(!0)] 4&3
+State: 4 "F(b)" {0}
+ [(0)] 6
+ [(!0)] 4
+State: 5 "((a) U (b))" {0}
+ [(0)] 6
+ [(!0 & 1)] 5
+State: 6 "t"
+ [t] 6
+--END--
+HOA: v1
+States: 3
+Start: 0
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+AP: 2 "a" "b"
+--BODY--
+State: 0
+0&1 1 0&   2&1 0&1  /* weird spacing on purpose  */
+State: 2
+0 & 1 2 & 1 2 0 & 2 & 1
+State: 1
+0&1 2&1 2 1&1 /* should we warn about duplicate destinations for univ edges? */
+--END--
 EOF
 
 expectok input <<EOF
@@ -2209,6 +2304,60 @@ State: 0
 [!0&1] 0 {2}
 [0&1] 0
 --END--
+HOA: v1
+name: "VWAA for (a U b) && G(F(b)) && F(G(a))"
+States: 7
+Start: 0
+AP: 2 "b" "a"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels state-acc
+--BODY--
+State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
+[0] 3&1
+[!0&1] 5&3&1
+State: 1 "FG(a)" {0}
+[1] 2
+[t] 1
+State: 2 "G(a)"
+[1] 2
+State: 3 "GF(b)"
+[0] 3
+[!0] 4&3
+State: 4 "F(b)" {0}
+[0] 6
+[!0] 4
+State: 5 "((a) U (b))" {0}
+[0] 6
+[!0&1] 5
+State: 6 "t"
+[t] 6
+--END--
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: co-Buchi
+Acceptance: 1 Fin(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!0&!1] 0&1
+[0&!1] 1
+[!0&1] 0&2&1
+[0&1] 0&1
+State: 1
+[!0&!1] 0&1
+[0&!1] 2&1
+[!0&1] 2
+[0&1] 1&1
+State: 2
+[!0&!1] 0&1
+[0&!1] 2&1
+[!0&1] 2
+[0&1] 0&2&1
+--END--
 EOF
 
 # The complements are Streett and Rabin, but the acceptance set are
@@ -2360,6 +2509,60 @@ State: 0
 [!0&1] 0 {2}
 [0&1] 0
 --END--
+HOA: v1
+name: "VWAA for (a U b) && G(F(b)) && F(G(a))"
+States: 7
+Start: 0
+AP: 2 "b" "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: univ-branch trans-labels explicit-labels state-acc
+--BODY--
+State: 0 "((((a) U (b)) && GF(b)) && FG(a))"
+[0] 3&1
+[!0&1] 5&3&1
+State: 1 "FG(a)" {0}
+[1] 2
+[t] 1
+State: 2 "G(a)"
+[1] 2
+State: 3 "GF(b)"
+[0] 3
+[!0] 4&3
+State: 4 "F(b)" {0}
+[0] 6
+[!0] 4
+State: 5 "((a) U (b))" {0}
+[0] 6
+[!0&1] 5
+State: 6 "t"
+[t] 6
+--END--
+HOA: v1
+States: 3
+Start: 0
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: univ-branch trans-labels explicit-labels state-acc complete
+properties: deterministic
+--BODY--
+State: 0
+[!0&!1] 0&1
+[0&!1] 1
+[!0&1] 0&2&1
+[0&1] 0&1
+State: 1
+[!0&!1] 0&1
+[0&!1] 2&1
+[!0&1] 2
+[0&1] 1&1
+State: 2
+[!0&!1] 0&1
+[0&!1] 2&1
+[!0&1] 2
+[0&1] 0&2&1
+--END--
 EOF
 
 cat >input <<EOF

tests/python/alternating.py

@@ -69,3 +69,8 @@ State: 1
 State: 2
 [0 | 1] 2
 --END--"""
+
+aut2 = spot.automaton(h)
+h2 = aut2.to_str('hoa')
+print(h2)
+assert h == h2