diff --git a/README b/README
index fcd48be58..f6d98e0e4 100644
--- a/README
+++ b/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.
diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 03c7f1cc2..84bd066b0 100644
--- a/buddy/src/bddx.h
+++ b/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)
diff --git a/configure.ac b/configure.ac
index 582f06632..5ae5b4725 100644
--- a/configure.ac
+++ b/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
diff --git a/src/Makefile.am b/src/Makefile.am
index 25cc70fc9..3567c05d4 100644
--- a/src/Makefile.am
+++ b/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 \
diff --git a/src/hoaparse/.gitignore b/src/hoaparse/.gitignore
new file mode 100644
index 000000000..2ed9b3c24
--- /dev/null
+++ b/src/hoaparse/.gitignore
@@ -0,0 +1,7 @@
+position.hh
+hoaparse.cc
+hoaparse.output
+hoaparse.hh
+hoascan.cc
+stack.hh
+location.hh
diff --git a/src/hoaparse/Makefile.am b/src/hoaparse/Makefile.am
new file mode 100644
index 000000000..dddc38fbc
--- /dev/null
+++ b/src/hoaparse/Makefile.am
@@ -0,0 +1,57 @@
+## -*- 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 .
+
+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
diff --git a/src/hoaparse/fmterror.cc b/src/hoaparse/fmterror.cc
new file mode 100644
index 000000000..decad775b
--- /dev/null
+++ b/src/hoaparse/fmterror.cc
@@ -0,0 +1,42 @@
+// -*- 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 .
+
+#include
+#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;
+ }
+}
diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
new file mode 100644
index 000000000..5708f6efa
--- /dev/null
+++ b/src/hoaparse/hoaparse.yy
@@ -0,0 +1,506 @@
+/* -*- 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 .
+*/
+%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
+#include
+#include
+#include "ltlast/constant.hh"
+#include "public.hh"
+
+ struct result_
+ {
+ spot::hoa_aut_ptr h;
+ spot::ltl::environment* env;
+ std::vector 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
+/* 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 IDENTIFIER "identifier";
+%token HEADERNAME "header name";
+%token ANAME "alias name";
+%token STRING "string";
+%token INT "integer";
+
+%left '|'
+%left '&'
+%nonassoc '!'
+
+%type state-num acc-set
+%type label-expr
+%type acc-sig_opt acc-sets
+
+%destructor { delete $$; }
+%destructor { bdd_delref($$); }
+%printer {
+ if ($$)
+ debug_stream() << *$$;
+ else
+ debug_stream() << "\"\""; }
+%printer { debug_stream() << $$; }
+
+%%
+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();
+ r.h->aut = make_tgba_digraph(dict);
+ r.env = &env;
+ hoayy::parser parser(error_list, r);
+ parser.set_debug_level(debug);
+ if (parser.parse())
+ r.h->aut = nullptr;
+ hoayyclose();
+ if (!r.h->aut)
+ return nullptr;
+
+ if (r.start != -1)
+ r.h->aut->set_init_state(r.start);
+ else
+ {
+ // If no initial state has been declared, add one, because
+ // Spot will not work without one.
+ r.h->aut->set_init_state(r.h->aut->new_state());
+ }
+ return r.h;
+ }
+}
+
+// Local Variables:
+// mode: c++
+// End:
diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll
new file mode 100644
index 000000000..9d43fc17e
--- /dev/null
+++ b/src/hoaparse/hoascan.ll
@@ -0,0 +1,165 @@
+/* -*- 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 .
+*/
+%option noyywrap
+%option prefix="hoayy"
+%option outfile="lex.yy.c"
+/* %option debug */
+
+%{
+#include
+#include "hoaparse/parsedecl.hh"
+
+#define YY_USER_ACTION yylloc->columns(yyleng);
+#define YY_NEVER_INTERACTIVE 1
+
+typedef hoayy::parser::token token;
+%}
+
+eol \n+|\r+
+eol2 (\n\r)+|(\r\n)+
+identifier [[:alpha:]_][[:alnum:]_-]*
+
+%x in_COMMENT in_STRING
+
+%%
+
+%{
+ std::string s;
+ yylloc->step();
+%}
+
+
+ /* skip blanks and comments */
+{eol} yylloc->lines(yyleng); yylloc->step();
+{eol2} yylloc->lines(yyleng / 2); yylloc->step();
+[ \t\v\f]+ yylloc->step();
+"/*" BEGIN(in_COMMENT);
+"//".* continue;
+"\"" BEGIN(in_STRING);
+
+"HOA:" return token::HOA;
+"States:" return token::STATES;
+"Start:" return token::START;
+"AP:" return token::AP;
+"Alias:" return token::ALIAS;
+"Acceptance:" return token::ACCEPTANCE;
+"acc-name:" return token::ACCNAME;
+"tool:" return token::TOOL;
+"name:" return token::NAME;
+"properties:" return token::PROPERTIES;
+"--BODY--" return token::BODY;
+"--END--" return token::END;
+"State:" return token::STATE;
+[tf{}()\[\]&|!] return *yytext;
+
+{identifier} {
+ yylval->str = new std::string(yytext, yyleng);
+ return token::IDENTIFIER;
+ }
+{identifier}":" {
+ yylval->str = new std::string(yytext, yyleng - 1);
+ return token::HEADERNAME;
+ }
+"@"[[:alnum:]_-]+ {
+ yylval->str = new std::string(yytext + 1, yyleng - 1);
+ return token::ANAME;
+ }
+[0-9]+ {
+ errno = 0;
+ unsigned long n = strtoul(yytext, 0, 10);
+ yylval->num = n;
+ if (errno || yylval->num != n)
+ {
+ error_list.push_back(
+ spot::hoa_parse_error(*yylloc,
+ "value too large"));
+ yylval->num = 0;
+ }
+ return token::INT;
+ }
+
+{
+ [^*\n]* continue;
+ "*"+[^*/\n]* continue;
+ "\n"+ yylloc->end.column = 1; yylloc->lines(yyleng);
+ "*"+"/" BEGIN(INITIAL);
+ <> {
+ error_list.push_back(
+ spot::hoa_parse_error(*yylloc,
+ "unclosed comment"));
+ return 0;
+ }
+}
+
+{
+ \" {
+ BEGIN(INITIAL);
+ yylval->str = new std::string(s);
+ return token::STRING;
+ }
+ \\\" s += '"';
+ \\. s += yytext[1];
+ [^\\\"]+ s.append(yytext, yyleng);
+ <> {
+ error_list.push_back(
+ spot::hoa_parse_error(*yylloc,
+ "unclosed string"));
+ return 0;
+ }
+}
+
+. return *yytext;
+
+%{
+ /* Dummy use of yyunput to shut up a gcc warning. */
+ (void) &yyunput;
+%}
+
+%%
+
+namespace spot
+{
+ int
+ hoayyopen(const std::string &name)
+ {
+ // yy_flex_debug = 1;
+ if (name == "-")
+ {
+ yyin = stdin;
+ }
+ else
+ {
+ yyin = fopen(name.c_str(), "r");
+ if (!yyin)
+ return 1;
+ }
+ // Reset the lexer in case a previous parse
+ // ended badly.
+ YY_NEW_FILE;
+ BEGIN(INITIAL);
+ return 0;
+ }
+
+ void
+ hoayyclose()
+ {
+ fclose(yyin);
+ }
+}
diff --git a/src/hoaparse/parsedecl.hh b/src/hoaparse/parsedecl.hh
new file mode 100644
index 000000000..8eecc8410
--- /dev/null
+++ b/src/hoaparse/parsedecl.hh
@@ -0,0 +1,39 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et Développement
+// de l'EPITA.
+//
+// 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 .
+
+#ifndef SPOT_HOAPARSE_PARSEDECL_HH
+# define SPOT_HOAPARSE_PARSEDECL_HH
+
+#include
+#include "hoaparse.hh"
+#include "misc/location.hh"
+
+# define YY_DECL \
+ int hoayylex(hoayy::parser::semantic_type *yylval, \
+ spot::location *yylloc, \
+ spot::hoa_parse_error_list& error_list)
+YY_DECL;
+
+namespace spot
+{
+ int hoayyopen(const std::string& name);
+ void hoayyclose();
+}
+
+#endif // SPOT_HOAPARSE_PARSEDECL_HH
diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh
new file mode 100644
index 000000000..02fbee6dd
--- /dev/null
+++ b/src/hoaparse/public.hh
@@ -0,0 +1,92 @@
+// -*- 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 .
+
+#ifndef SPOT_HOAPARSE_PUBLIC_HH
+# define SPOT_HOAPARSE_PUBLIC_HH
+
+# include "tgba/tgbagraph.hh"
+# include "misc/location.hh"
+# include "ltlenv/defaultenv.hh"
+# include
+# include
+# include
+# include
+# include
+
+namespace spot
+{
+ /// \addtogroup tgba_io
+ /// @{
+
+ /// \brief A parse diagnostic with its location.
+ typedef std::pair hoa_parse_error;
+ /// \brief A list of parser diagnostics, as filled by parse.
+ typedef std::list hoa_parse_error_list;
+
+ /// \brief Temporary encoding of an omega automaton produced by
+ /// ltl2hoa.
+ struct SPOT_API hoa_aut
+ {
+ // Transition structure of the automaton.
+ // This is encoded as a TGBA without acceptance condition.
+ tgba_digraph_ptr aut;
+ };
+
+ typedef std::shared_ptr hoa_aut_ptr;
+ typedef std::shared_ptr const_hoa_aut_ptr;
+
+ /// \brief Build a spot::tgba_digraph from ltl2hoa's output.
+ /// \param filename The name of the file to parse.
+ /// \param error_list A list that will be filled with
+ /// parse errors that occured during parsing.
+ /// \param dict The BDD dictionary where to use.
+ /// \param env The environment of atomic proposition into which parsing
+ /// should take place.
+ /// \param debug When true, causes the parser to trace its execution.
+ /// \return A pointer to the tgba built from \a filename, or
+ /// 0 if the file could not be opened.
+ ///
+ /// Note that the parser usually tries to recover from errors. It can
+ /// return an non zero value even if it encountered error during the
+ /// parsing of \a filename. If you want to make sure \a filename
+ /// was parsed succesfully, check \a error_list for emptiness.
+ ///
+ /// \warning This function is not reentrant.
+ SPOT_API hoa_aut_ptr
+ hoa_parse(const std::string& filename,
+ hoa_parse_error_list& error_list,
+ const bdd_dict_ptr& dict,
+ ltl::environment& env = ltl::default_environment::instance(),
+ bool debug = false);
+
+ /// \brief Format diagnostics produced by spot::hoa_parse.
+ /// \param os Where diagnostics should be output.
+ /// \param filename The filename that should appear in the diagnostics.
+ /// \param error_list The error list filled by spot::ltl::parse while
+ /// parsing \a ltl_string.
+ /// \return \c true iff any diagnostic was output.
+ SPOT_API bool
+ format_hoa_parse_errors(std::ostream& os,
+ const std::string& filename,
+ hoa_parse_error_list& error_list);
+
+ /// @}
+}
+
+#endif // SPOT_HOAPARSE_PUBLIC_HH
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 13cf35a0a..7f2283a3c 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -84,6 +84,7 @@ TESTS = \
nondet.test \
det.test \
neverclaimread.test \
+ hoaparse.test \
dstar.test \
readsave.test \
maskacc.test \
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
new file mode 100755
index 000000000..e28a374ee
--- /dev/null
+++ b/src/tgbatest/hoaparse.test
@@ -0,0 +1,198 @@
+#!/bin/sh
+# -*- 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 .
+
+
+. ./defs
+
+set -e
+
+expecterr()
+{
+ cat >$1.exp
+ ../ltl2tgba -XH $1 2>$1.err && exit 1
+ test $? = 2
+ cat $1.err
+ diff $1.err $1.exp
+}
+
+
+cat >input <input <input <input <input <input <input <input <input <input <aut;
+ assume_sba = false;
+ }
+ break;
}
}
else