From e55bcd95aa770264b5d4b8efda3b79c9fb5de884 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Nov 2014 18:48:36 +0100 Subject: [PATCH] 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 | 1 + buddy/src/bddx.h | 4 + configure.ac | 1 + src/Makefile.am | 5 +- src/hoaparse/.gitignore | 7 + src/hoaparse/Makefile.am | 57 +++++ src/hoaparse/fmterror.cc | 42 +++ src/hoaparse/hoaparse.yy | 506 +++++++++++++++++++++++++++++++++++++ src/hoaparse/hoascan.ll | 165 ++++++++++++ src/hoaparse/parsedecl.hh | 39 +++ src/hoaparse/public.hh | 92 +++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/hoaparse.test | 198 +++++++++++++++ src/tgbatest/ltl2tgba.cc | 23 +- 14 files changed, 1138 insertions(+), 3 deletions(-) create mode 100644 src/hoaparse/.gitignore create mode 100644 src/hoaparse/Makefile.am create mode 100644 src/hoaparse/fmterror.cc create mode 100644 src/hoaparse/hoaparse.yy create mode 100644 src/hoaparse/hoascan.ll create mode 100644 src/hoaparse/parsedecl.hh create mode 100644 src/hoaparse/public.hh create mode 100755 src/tgbatest/hoaparse.test 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