From 7a03228880ae2b1fcd66f80f6474512e8564319d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 21 Nov 2014 11:05:24 +0100
Subject: [PATCH] hoa: add alias support

* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: Test it.
---
 src/hoaparse/hoaparse.yy   | 22 +++++++++++--
 src/tgbatest/hoaparse.test | 64 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+), 3 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index c45340bba..19b97cd69 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -32,6 +32,7 @@
 #include <string>
 #include <cstring>
 #include <sstream>
+#include <unordered_map>
 #include "ltlast/constant.hh"
 #include "public.hh"
 
@@ -48,6 +49,7 @@
     std::vector<bdd> guards;
     std::vector<bdd>::const_iterator cur_guard;
     std::vector<bool> declared_states; // States that have been declared.
+    std::unordered_map<std::string, bdd> alias;
     spot::location states_loc;
     spot::location ap_loc;
     spot::location state_label_loc;
@@ -238,6 +240,12 @@ header-item: "States:" INT
 	     }
            | "Alias:" ANAME label-expr
              {
+	       if (!res.alias.emplace(*$2, bdd_from_int($3)).second)
+		 {
+		   std::ostringstream o;
+		   o << "ignoring redefinition of alias @" << *$2;
+		   error(@$, o.str());
+		 }
 	       delete $2;
 	       bdd_delref($3);
 	     }
@@ -352,10 +360,18 @@ label-expr: 't'
 	    }
           | ANAME
 	    {
+	      auto i = res.alias.find(*$1);
+	      if (i == res.alias.end())
+		{
+		  error(@$, "unknown alias @" + *$1);
+		  $$ = 1;
+		}
+	      else
+		{
+		  $$ = i->second.id();
+		  bdd_addref($$);
+		}
 	      delete $1;
-              error(@1, "aliases are not yet supported");
-              YYABORT;
-              $$ = 0;
 	    }
           | '!' label-expr
 	    {
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index df3cc96f3..a263dde06 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -322,3 +322,67 @@ EOF
 expecterr input <<EOF
 input:13.7: too many transition for this state, ignoring this one
 EOF
+
+
+cat >input <<EOF
+    HOA: v1
+    name: "GFa & GF(b & c)"
+    States: 1
+    Start: 0
+    acc-name: generalized-Buchi 2
+    Acceptance: 2 (Inf(0) & Inf(1))
+    AP: 3 "a" "b" "c"
+    Alias: @a 0
+    Alias: @a 1 & 2 /* should be @bc */
+    --BODY--
+    State: 0
+    [!@a & !@bc] 0
+    [@a & !@bc]  0 {0}
+    [!@a & @bc]  0 {1}
+    [@a & @bc]   0 {0 1}
+    --END--
+EOF
+
+expecterr input <<EOF
+input:9.5-19: ignoring redefinition of alias @a
+input:12.13-15: unknown alias @bc
+input:13.12-14: unknown alias @bc
+input:14.12-14: unknown alias @bc
+input:15.11-13: unknown alias @bc
+EOF
+
+cat >input <<EOF
+    HOA: v1
+    name: "GFa & GF(b & c)"
+    States: 1
+    Start: 0
+    acc-name: generalized-Buchi 2
+    Acceptance: 2 (Inf(0) & Inf(1))
+    AP: 3 "a" "b" "c"
+    Alias: @a 0
+    Alias: @bc 1 & 2
+    --BODY--
+    State: 0
+    [!@a & !@bc] 0
+    [@a & !@bc]  0 {0}
+    [!@a & @bc]  0 {1}
+    [@a & @bc]   0 {0 1}
+    --END--
+EOF
+
+expectok input <<EOF
+HOA: v1
+States: 1
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: generalized-Buchi 2
+Acceptance: 2 Inf(0)&Inf(1)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[!0&!1 | !0&!2] 0
+[0&!1 | 0&!2] 0 {0}
+[!0&1&2] 0 {1}
+[0&1&2] 0 {0 1}
+--END--
+EOF