hoa: preliminary implementation of a parser

* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
* src/Makefile.am, configure.ac, README: Adjust.
* src/tgbatest/ltl2tgba.cc: Add a -XH option.
* src/tgbatest/hoaparse.test: New file.
* src/tgbatest/Makefile.am: Adjust.
* buddy/src/bddx.h: Add a bdd_from_int() function.

README

@@ -142,6 +142,7 @@ src/              Sources for libspot.
    dstarparse/    Parser for the output of ltl2dstar.
    graph/         Graph representations.
    graphtest/     Graph representations.
+   hoaparse/      Parser for the HOA format.
    kripke/        Kripke Structure interface.
    kripkeparse/   Parser for explicit Kripke.
    kripketest/    Tests for kripke explicit.

buddy/src/bddx.h

@@ -573,6 +573,7 @@ protected:
    friend bdd      bdd_makesetpp(int *, int);
    friend int      bdd_setbddpair(bddPair*, int, const bdd &);
    friend int      bdd_setbddpairs(bddPair*, int*, const bdd *, int);
+   friend bdd      bdd_from_int(int i);
    friend bdd      bdd_buildcube(int, int, const bdd *);
    friend bdd      bdd_ibuildcubepp(int, int, int *);
    friend bdd      bdd_not(const bdd &);
@@ -715,6 +716,9 @@ inline bdd bdd_makesetpp(int *v, int n)
 inline int bdd_setbddpair(bddPair *p, int ov, const bdd &nv)
 { return bdd_setbddpair(p,ov,nv.root); }
 
+inline bdd bdd_from_int(int i)
+{ return i; }
+
    /* In bddop.c */
 
 inline bdd bdd_replace(const bdd &r, bddPair *p)

configure.ac

@@ -180,6 +180,7 @@ AC_CONFIG_FILES([
   src/graph/Makefile
   src/graphtest/Makefile
   src/graphtest/defs
+  src/hoaparse/Makefile
   src/ltlast/Makefile
   src/ltlenv/Makefile
   src/ltlparse/Makefile

src/Makefile.am

@@ -27,14 +27,15 @@ AUTOMAKE_OPTIONS = subdir-objects
 # libspot.la needed by the tests)
 SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba		\
           tgbaalgos tgbaparse ta taalgos kripke neverparse		\
-          kripkeparse dstarparse . bin ltltest graphtest tgbatest	\
-          kripketest sanity
+          kripkeparse dstarparse hoaparse . bin ltltest graphtest	\
+          tgbatest kripketest sanity
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
 libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined
 libspot_la_LIBADD =  \
   dstarparse/libdstarparse.la \
+  hoaparse/libhoaparse.la \
   kripke/libkripke.la \
   kripkeparse/libkripkeparse.la \
   ltlast/libltlast.la \

src/hoaparse/.gitignore

+position.hh
+hoaparse.cc
+hoaparse.output
+hoaparse.hh
+hoascan.cc
+stack.hh
+location.hh

src/hoaparse/Makefile.am

+## -*- coding: utf-8 -*-
+## Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
+## l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 3 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT
+# Disable -Werror because too many versions of flex yield warnings.
+AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
+
+hoaparsedir = $(pkgincludedir)/hoaparse
+
+hoaparse_HEADERS = public.hh
+
+noinst_LTLIBRARIES = libhoaparse.la
+
+HOAPARSE_YY = hoaparse.yy
+FROM_HOAPARSE_YY_MAIN = hoaparse.cc
+FROM_HOAPARSE_YY_OTHERS = \
+  stack.hh \
+  hoaparse.hh
+
+FROM_HOAPARSE_YY = $(FROM_HOAPARSE_YY_MAIN) $(FROM_HOAPARSE_YY_OTHERS)
+
+BUILT_SOURCES = $(FROM_HOAPARSE_YY)
+MAINTAINERCLEANFILES = $(FROM_HOAPARSE_YY)
+
+$(FROM_HOAPARSE_YY_MAIN): $(srcdir)/$(HOAPARSE_YY)
+## We must cd into $(srcdir) first because if we tell bison to read
+## $(srcdir)/$(HOAPARSE_YY), it will also use the value of $(srcdir)/
+## in the generated include statements.
+	cd $(srcdir) && \
+	  $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \
+	  $(HOAPARSE_YY) -o $(FROM_HOAPARSE_YY_MAIN)
+$(FROM_HOAPARSE_YY_OTHERS): $(HOAPARSE_YY)
+	@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_HOAPARSE_YY_MAIN)
+
+EXTRA_DIST = $(HOAPARSE_YY)
+
+libhoaparse_la_SOURCES = \
+  fmterror.cc \
+  $(FROM_HOAPARSE_YY) \
+  hoascan.ll \
+  parsedecl.hh

src/hoaparse/fmterror.cc

+// -*- coding: utf-8 -*-
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include <ostream>
+#include "public.hh"
+
+namespace spot
+{
+  bool
+  format_hoa_parse_errors(std::ostream& os,
+			    const std::string& filename,
+			    hoa_parse_error_list& error_list)
+  {
+    bool printed = false;
+    spot::hoa_parse_error_list::iterator it;
+    for (it = error_list.begin(); it != error_list.end(); ++it)
+      {
+	if (filename != "-")
+	  os << filename << ':';
+	os << it->first << ": ";
+	os << it->second << std::endl;
+	printed = true;
+      }
+    return printed;
+  }
+}

src/hoaparse/hoaparse.yy

+/* -*- coding: utf-8 -*-
+** Copyright (C) 2014 Laboratoire de Recherche et Développement
+** de l'Epita (LRDE).
+**
+** This file is part of Spot, a model checking library.
+**
+** Spot is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by
+** the Free Software Foundation; either version 3 of the License, or
+** (at your option) any later version.
+**
+** Spot is distributed in the hope that it will be useful, but WITHOUT
+** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+** or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+** License for more details.
+**
+** You should have received a copy of the GNU General Public License
+** along with this program.  If not, see <http://www.gnu.org/licenses/>.
+*/
+%language "C++"
+%locations
+%defines
+%expect 0 // No shift/reduce
+%name-prefix "hoayy"
+%debug
+%error-verbose
+%lex-param { spot::hoa_parse_error_list& error_list }
+%define api.location.type "spot::location"
+
+%code requires
+{
+#include <string>
+#include <cstring>
+#include <sstream>
+#include "ltlast/constant.hh"
+#include "public.hh"
+
+  struct result_
+  {
+    spot::hoa_aut_ptr h;
+    spot::ltl::environment* env;
+    std::vector<int> ap;
+    spot::location states_loc;
+    spot::location ap_loc;
+    spot::location state_label_loc;
+    spot::location start_loc;
+    spot::location accset_loc;
+    unsigned cur_state;
+    int start = -1;
+    int states = -1;
+    int ap_count = -1;
+    int accset = -1;
+    bdd state_label;
+    bdd cur_label;
+    bool has_state_label = false;
+    bool has_trans_label = false;
+    spot::acc_cond::mark_t acc_state;
+  };
+}
+
+%parse-param {spot::hoa_parse_error_list& error_list}
+%parse-param {result_& res}
+%union
+{
+  std::string* str;
+  unsigned int num;
+  int b;
+  spot::acc_cond::mark_t mark;
+}
+
+%code
+{
+#include <sstream>
+/* hoaparse.hh and parsedecl.hh include each other recursively.
+   We must ensure that YYSTYPE is declared (by the above %union)
+   before parsedecl.hh uses it. */
+#include "parsedecl.hh"
+}
+
+%token HOA "HOA:"
+%token STATES "States:"
+%token START "Start:"
+%token AP "AP:"
+%token ALIAS "Alias:"
+%token ACCEPTANCE "Acceptance:"
+%token ACCNAME "acc-name:"
+%token TOOL "tool:"
+%token NAME "name:"
+%token PROPERTIES "properties:"
+%token BODY "--BODY--"
+%token END "--END--"
+%token STATE "State:";
+%token <str> IDENTIFIER "identifier";
+%token <str> HEADERNAME "header name";
+%token <str> ANAME "alias name";
+%token <str> STRING "string";
+%token <num> INT "integer";
+
+%left '|'
+%left '&'
+%nonassoc '!'
+
+%type <num> state-num acc-set
+%type <b> label-expr
+%type <mark> acc-sig_opt acc-sets
+
+%destructor { delete $$; } <str>
+%destructor { bdd_delref($$); } <b>
+%printer {
+    if ($$)
+      debug_stream() << *$$;
+    else
+      debug_stream() << "\"\""; } <str>
+%printer { debug_stream() << $$; } <num>
+
+%%
+hoa: header "--BODY--" body "--END--"
+
+string_opt: | STRING
+BOOLEAN: 't' | 'f'
+
+header: format-version header-items
+        {
+	  if (res.accset < 0)
+	    {
+	      error(@$, "missing 'Acceptance:' header");
+	      YYABORT;
+	    }
+	}
+
+format-version: "HOA:" IDENTIFIER
+		{
+		  if (*$2 != "v1")
+		    error(@$, "unsupported version of the HOA format");
+		  delete $2;
+		}
+
+header-items: | header-items header-item
+header-item: "States:" INT
+           {
+	     if (res.states >= 0)
+	       {
+		 error(@$, "redefinition of the number of states...");
+		 error(res.states_loc, "... previously defined here.");
+	       }
+	     else
+	       {
+		 res.states_loc = @$;
+	       }
+	     if (((int) $2) < 0)
+	       {
+		 error(@$, "too many states for this implementation");
+		 YYABORT;
+	       }
+	     res.states = std::max(res.states, (int) $2);
+	     if (res.states <= res.start)
+	       {
+		 error(res.start_loc,
+		       "initial state number is larger than state count...");
+		 error(@$, "... declared here.");
+		 YYABORT;
+	       }
+	     int missing = res.states - res.h->aut->num_states();
+	     assert(missing >= 0);
+	     res.h->aut->new_states(missing);
+	   }
+           | "Start:" state-conj-2
+	     {
+	       res.start_loc = @$;
+	       error(@2, "alternation is not yet supported");
+	       YYABORT;
+	     }
+           | "Start:" state-num
+	     {
+	       if (res.start >= 0)
+		 {
+		   error(@$, "multiple initial states are not yet supported");
+		   YYABORT;
+		 }
+	       res.start = $2;
+	       res.start_loc = @$;
+	     }
+           | "AP:" INT {
+	                 if (res.ap_count != -1)
+		         {
+                           error(@1, "redeclaration of APs...");
+                           error(res.ap_loc, "... previously defined here.");
+			   YYABORT;
+                         }
+                         res.ap_count = $2; res.ap.reserve($2);
+	               }
+                   ap-names
+	     {
+	       res.ap_loc = @1 + @2;
+	       if ((int) res.ap.size() != res.ap_count)
+		 {
+		   std::ostringstream out;
+		   out << "found " << res.ap.size()
+		       << " atomic propositions instead of the "
+		       << res.ap_count << " announced";
+		   error(@$, out.str());
+		 }
+	     }
+           | "Alias:" ANAME label-expr
+             {
+	       delete $2;
+	       bdd_delref($3);
+	     }
+           | "Acceptance:" INT
+	      {
+	       if (res.accset >= 0)
+		 {
+		   error(@1 + @2, "redefinition of the acceptance condition...");
+		   error(res.accset_loc, "... previously defined here.");
+		   YYABORT;
+		 }
+	       else if ($2 > 8 * sizeof(spot::acc_cond::mark_t::value_t))
+		 {
+		   error(@1 + @2,
+			 "this implementation cannot support such a large "
+			 "number of acceptance sets");
+		   YYABORT;
+		 }
+	       else
+		 {
+		   res.h->aut->acc().add_sets($2);
+		   res.accset = $2;
+		   res.accset_loc = @1 + @2;
+		 }
+	     }
+             acceptance-cond
+           | "acc-name:" IDENTIFIER acc-spec
+             {
+	       delete $2;
+	     }
+           | "tool:" STRING string_opt
+             {
+	       delete $2;
+	     }
+           | "name:" STRING
+             {
+	       delete $2;
+	     }
+           | "properties:" properties
+           | HEADERNAME header-spec
+
+ap-names: | ap-names ap-name
+ap-name: STRING
+	 {
+	   auto f = res.env->require(*$1);
+	   if (f == nullptr)
+	     {
+	       std::ostringstream out;
+	       out << "unknown atomic proposition \"" << *$1 << "\"";
+	       delete $1;
+	       error(@1, out.str());
+	       YYABORT;
+	     }
+	   delete $1;
+	   auto b =
+	     res.h->aut->get_dict()->register_proposition(f, res.h->aut);
+	   f->destroy();
+	   res.ap.push_back(b);
+	 }
+
+acc-spec: | acc-spec BOOLEAN
+	  | acc-spec INT
+	  | acc-spec IDENTIFIER
+            {
+	      delete $2;
+	    }
+properties: | properties IDENTIFIER
+	      {
+		delete $2;
+	      }
+header-spec: | header-spec BOOLEAN
+             | header-spec INT
+             | header-spec STRING
+	       {
+		 delete $2;
+	       }
+             | header-spec IDENTIFIER
+	       {
+		 delete $2;
+	       }
+
+state-conj-2: state-num '&' state-num | state-conj-2 '&' state-num
+
+label-expr: 't'
+	    {
+	      $$ = bddtrue.id();
+	    }
+          | 'f'
+	    {
+	      $$ = bddfalse.id();
+	    }
+	  | INT
+	    {
+	      if ($1 >= res.ap.size())
+		{
+		  error(@1, "AP number is larger than the number of APs...");
+		  error(res.ap_loc, "... declared here");
+		  $$ = bddtrue.id();
+		}
+	      else
+		{
+		  $$ = bdd_ithvar(res.ap[$1]).id();
+		  bdd_addref($$);
+		}
+	    }
+          | ANAME
+	    {
+	      delete $1;
+              error(@1, "aliases are not yet supported");
+              YYABORT;
+              $$ = 0;
+	    }
+          | '!' label-expr
+	    {
+              $$ = bdd_not($2);
+              bdd_delref($2);
+              bdd_addref($$);
+            }
+          | label-expr '&' label-expr
+	    {
+              $$ = bdd_and($1, $3);
+              bdd_delref($1);
+              bdd_delref($3);
+              bdd_addref($$);
+            }
+          | label-expr '|' label-expr
+	    {
+              $$ = bdd_or($1, $3);
+              bdd_delref($1);
+              bdd_delref($3);
+              bdd_addref($$);
+            }
+
+
+acc-set: INT
+            {
+	      if ((int) $1 >= res.accset)
+		{
+		  error(@1, "number is larger than the count "
+			"of acceptance sets...");
+		  error(res.accset_loc, "... declared here.");
+		  YYABORT;
+		}
+	      $$ = $1;
+	    }
+
+acceptance-cond: IDENTIFIER '(' acc-set ')'
+		 {
+		   if (*$1 != "Inf")
+		     error(@1, "this implementation only supports "
+			   "'Inf' acceptance");
+		   delete $1;
+		 }
+               | IDENTIFIER '(' '!' acc-set ')'
+		 {
+		   error(@1, "this implementation does not support "
+			 "negated sets");
+		   delete $1;
+		 }
+               | '(' acceptance-cond ')'
+               | acceptance-cond '&' acceptance-cond
+               | acceptance-cond '|' acceptance-cond
+	         {
+		   error(@1, "this implementation does not support "
+			 "disjunction in acceptance conditions");
+		 }
+               | BOOLEAN
+
+
+body: states
+
+state-num: INT
+	   {
+	     if (((int) $1) < 0)
+	       {
+		 error(@1, "state number is too large for this implementation");
+		 YYABORT;
+	       }
+	     if ((int) $1 >= res.states)
+	       {
+		 if (res.states >= 0)
+		   {
+		     error(@1, "state number is larger than state count...");
+		     error(res.states_loc, "... declared here.");
+		   }
+		 int missing = ((int) $1) - res.h->aut->num_states() + 1;
+		 if (missing >= 0)
+		   res.h->aut->new_states(missing);
+	       }
+	     $$ = $1;
+	   }
+
+states: | states state
+state: state-name edges
+state-name: "State:" state-label_opt state-num string_opt acc-sig_opt
+	  {
+	    res.cur_state = $3;
+	    res.acc_state = $5;
+	  }
+label: '[' label-expr ']'
+	   {
+             res.cur_label = bdd_from_int($2);
+             bdd_delref($2);
+	   }
+state-label_opt:       { res.has_state_label = false; }
+               | label { res.has_state_label = true;
+                         res.state_label_loc = @1;
+		         res.state_label = res.cur_label; }
+trans-label_opt:       { res.has_trans_label = false; }
+               | label
+	         {
+		   if (res.has_state_label)
+		     {
+		       error(@1, "cannot label this transition because...");
+		       error(res.state_label_loc,
+			     "... the state is already labeled.");
+		       res.has_trans_label = false;
+		     }
+		   else
+		     {
+		       res.has_trans_label = true;
+		     }
+		 }
+
+acc-sig_opt:                   { $$ = spot::acc_cond::mark_t(0U); }
+           | '{' acc-sets '}'  { $$ = $2; }
+acc-sets:                      { $$ = spot::acc_cond::mark_t(0U); }
+        | acc-sets acc-set
+	  {
+	    $$ = $1 | res.h->aut->acc().mark($2);
+	  }
+edges: | edges edge
+edge: trans-label_opt state-num acc-sig_opt
+      {
+	bdd cond = bddfalse;
+	if (res.has_state_label)
+	  cond = res.state_label;
+	else if (res.has_trans_label)
+	  cond = res.cur_label;
+	else
+	  error(@$, "unlabeled transitions are not yet supported");
+	res.h->aut->new_transition(res.cur_state, $2, cond,
+				   $3 | res.acc_state);
+      }
+    | trans-label_opt state-conj-2 acc-sig_opt
+      {
+	error(@2, "alternation is not yet supported");
+	YYABORT;
+      }
+
+%%
+
+void
+hoayy::parser::error(const location_type& location,
+		       const std::string& message)
+{
+  error_list.emplace_back(location, message);
+}
+
+namespace spot
+{
+  hoa_aut_ptr
+  hoa_parse(const std::string& name,
+	      hoa_parse_error_list& error_list,
+	      const bdd_dict_ptr& dict,
+	      ltl::environment& env,
+	      bool debug)
+  {
+    if (hoayyopen(name))
+      {
+	error_list.emplace_back(spot::location(),
+				std::string("Cannot open file ") + name);
+	return 0;
+      }
+    result_ r;
+    r.h = std::make_shared<spot::hoa_aut>();
+    r.h->aut = make_tgba_digraph(dict);
+    r.env = &env;
+    hoayy::parser parser(error_list, r);
+    parser.set_debug_level(debug);