From e1bba50047d14b76f75c0dd7467dcceeb3c2edef Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 3 Dec 2014 18:20:35 +0100 Subject: [PATCH] hoa: swallow the neverclaim parser This way we can easily parse a stream of HOAs intermixed with neverclaims. * src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll: Add rules for neverclaims, adjusted from src/neverparse/neverclaimparse.yy and src/neverparse/neverclaimparse.ll. * src/hoaparse/public.hh, NEWS: Update documentation. * src/neverparse/: Remove this directory. * README, configure.ac, src/Makefile.am: Adjust accordingly. * src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc: Use HOA parser to read neverclaims. * src/tgbatest/hoaparse.test, src/tgbatest/neverclaimread.test: Adjust. --- NEWS | 6 + README | 3 +- configure.ac | 1 - src/Makefile.am | 9 +- src/bin/ltlcross.cc | 33 +-- src/hoaparse/hoaparse.yy | 281 ++++++++++++++++++++++-- src/hoaparse/hoascan.ll | 126 ++++++++--- src/hoaparse/public.hh | 12 +- src/neverparse/.gitignore | 7 - src/neverparse/Makefile.am | 57 ----- src/neverparse/fmterror.cc | 42 ---- src/neverparse/neverclaimparse.yy | 340 ------------------------------ src/neverparse/neverclaimscan.ll | 151 ------------- src/neverparse/parsedecl.hh | 39 ---- src/neverparse/public.hh | 79 ------- src/tgbatest/hoaparse.test | 57 ++++- src/tgbatest/ltl2tgba.cc | 25 +-- src/tgbatest/neverclaimread.test | 2 +- 18 files changed, 453 insertions(+), 817 deletions(-) delete mode 100644 src/neverparse/.gitignore delete mode 100644 src/neverparse/Makefile.am delete mode 100644 src/neverparse/fmterror.cc delete mode 100644 src/neverparse/neverclaimparse.yy delete mode 100644 src/neverparse/neverclaimscan.ll delete mode 100644 src/neverparse/parsedecl.hh delete mode 100644 src/neverparse/public.hh diff --git a/NEWS b/NEWS index b856aac5c..213e5421b 100644 --- a/NEWS +++ b/NEWS @@ -43,6 +43,12 @@ New in spot 1.99a (not yet released) used in a stream. The parser currently ignore all optional headers (starting with a lowercase letter). + - The above HOA parser can also parse neverclaims, so the + neverclaim parser has been removed. This implies that + autfilt can input a mix of HOA and neverclaims, and that + ltlcross' %N and %H specifiers (used to indicate whether + a tool produces neverclaims or HOA) are now synonyms. + - randomize() is a new algorithm that reorder the states and transition of an automaton at random. It can be used from the command-line using "autfilt --randomize". diff --git a/README b/README index f6d98e0e4..98cfb407c 100644 --- a/README +++ b/README @@ -142,7 +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. + hoaparse/ Parser for HOA automata and Spin's never claims. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. kripketest/ Tests for kripke explicit. @@ -152,7 +152,6 @@ src/ Sources for libspot. ltlvisit/ Visitors of LTL formulae. ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. misc/ Miscellaneous support files. - neverparse/ Parser for SPIN never claims. priv/ Private algorithms, used internally but not exported. tgba/ TGBA objects and cousins. tgbaalgos/ Algorithms on TGBA. diff --git a/configure.ac b/configure.ac index 5ae5b4725..fb70d3f1c 100644 --- a/configure.ac +++ b/configure.ac @@ -192,7 +192,6 @@ AC_CONFIG_FILES([ src/ltlvisit/Makefile src/Makefile src/misc/Makefile - src/neverparse/Makefile src/priv/Makefile src/sanity/Makefile src/tgbaalgos/gtec/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 3567c05d4..e2da5094e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -25,10 +25,10 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. Keep tests at the # end, after building '.' (since the current directory contains # libspot.la needed by the tests) -SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ - tgbaalgos tgbaparse ta taalgos kripke neverparse \ - kripkeparse dstarparse hoaparse . bin ltltest graphtest \ - tgbatest kripketest sanity +SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph tgba \ + tgbaalgos tgbaparse ta taalgos kripke kripkeparse \ + dstarparse hoaparse . bin ltltest graphtest tgbatest \ + kripketest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -43,7 +43,6 @@ libspot_la_LIBADD = \ ltlparse/libltlparse.la \ ltlvisit/libltlvisit.la \ misc/libmisc.la \ - neverparse/libneverparse.la \ priv/libpriv.la \ taalgos/libtaalgos.la \ ta/libta.la \ diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 1e3216c58..4cf875149 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -36,7 +36,6 @@ #include "common_setup.hh" #include "common_cout.hh" #include "common_finput.hh" -#include "neverparse/public.hh" #include "dstarparse/public.hh" #include "hoaparse/public.hh" #include "ltlast/unop.hh" @@ -115,9 +114,9 @@ static const argp_option options[] = 0 }, { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, - { "%N,%T,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the output automaton as a Never claim, in LBTT's or in LTL2DSTAR's " - "format", 0 }, + { "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's," + "or in the HOA format", 0 }, { 0, 0, 0, 0, "If either %l, %L, or %T are used, any input formula that does " "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " @@ -710,7 +709,7 @@ namespace public spot::printable_value { unsigned translator_num; - enum output_format { None, Spin, Lbtt, Dstar, Hoa }; + enum output_format { None, Lbtt, Dstar, Hoa }; mutable output_format format; printable_result_filename() @@ -740,7 +739,7 @@ namespace { output_format old_format = format; if (*pos == 'N') - format = Spin; + format = Hoa; // The HOA parse also reads neverclaims else if (*pos == 'T') format = Lbtt; else if (*pos == 'D') @@ -939,24 +938,6 @@ namespace es = 0; switch (output.format) { - case printable_result_filename::Spin: - { - spot::neverclaim_parse_error_list pel; - std::string filename = output.val()->name(); - res = spot::neverclaim_parse(filename, pel, dict); - if (!pel.empty()) - { - status_str = "parse error"; - problem = true; - es = -1; - std::ostream& err = global_error(); - err << "error: failed to parse the produced neverclaim.\n"; - spot::format_neverclaim_parse_errors(err, filename, pel); - end_error(); - res = nullptr; - } - break; - } case printable_result_filename::Lbtt: { std::string error; @@ -1039,7 +1020,7 @@ namespace } break; } - case printable_result_filename::Hoa: + case printable_result_filename::Hoa: // Will also read neverclaims { spot::hoa_parse_error_list pel; std::string filename = output.val()->name(); @@ -1050,7 +1031,7 @@ namespace problem = true; es = -1; std::ostream& err = global_error(); - err << "error: failed to parse the produced HOA file.\n"; + err << "error: failed to parse the produced automaton.\n"; spot::format_hoa_parse_errors(err, filename, pel); end_error(); res = nullptr; diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 4ae1eb40c..6ce680731 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -35,8 +35,18 @@ #include #include #include "ltlast/constant.hh" +#include "tgba/formula2bdd.hh" #include "public.hh" + /* Cache parsed formulae. Labels on arcs are frequently identical + and it would be a waste of time to parse them to formula* over and + over, and to register all their atomic_propositions in the + bdd_dict. Keep the bdd result around so we can reuse it. */ + typedef std::map formula_cache; + + typedef std::pair pair; + typedef typename spot::tgba_digraph::namer::type named_tgba_t; + // Note: because this parser is meant to be used on a stream of // automata, it tries hard to recover from errors, so that we get a // chance to reach the end of the current automaton in order to @@ -46,6 +56,8 @@ { spot::hoa_aut_ptr h; spot::ltl::environment* env; + formula_cache fcache; + named_tgba_t* namer = nullptr; std::vector ap; std::vector guards; std::vector::const_iterator cur_guard; @@ -73,6 +85,15 @@ bool ignore_acc_silent = false; bool ignore_more_acc = false; // Set to true after the first // "Acceptance:" line has been read. + + bool accept_all_needed = false; + bool accept_all_seen = false; + std::map labels; + + ~result_() + { + delete namer; + } }; } @@ -88,12 +109,17 @@ unsigned int num; int b; spot::acc_cond::mark_t mark; + pair* p; + std::list* list; } %code { #include -/* hoaparse.hh and parsedecl.hh include each other recursively. +#include "ltlast/constant.hh" +#include "ltlparse/public.hh" + + /* 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" @@ -101,6 +127,7 @@ static void fill_guards(result_& res); } +/**** HOA tokens ****/ %token HOA "HOA:" %token STATES "States:" %token START "Start:" @@ -114,7 +141,7 @@ %token BODY "--BODY--" %token END "--END--" %token STATE "State:"; -%token IDENTIFIER "identifier"; +%token IDENTIFIER "identifier"; // also used by neverclaim %token HEADERNAME "header name"; %token ANAME "alias name"; %token STRING "string"; @@ -129,8 +156,42 @@ %type label-expr %type acc-sig_opt acc-sets +/**** NEVERCLAIM tokens ****/ + +%token NEVER "never" +%token SKIP "skip" +%token IF "if" +%token FI "fi" +%token DO "do" +%token OD "od" +%token ARROW "->" +%token GOTO "goto" +%token FALSE "false" +%token ATOMIC "atomic" +%token ASSERT "assert" +%token FORMULA "boolean formula" + +%type nc-formula +%type nc-opt-dest nc-formula-or-ident +%type

nc-transition nc-src-dest +%type nc-transitions nc-transition-block +%type nc-one-ident nc-ident-list + + + + %destructor { delete $$; } %destructor { bdd_delref($$); } +%destructor { bdd_delref($$->first); delete $$->second; delete $$; }

+%destructor { + for (std::list::iterator i = $$->begin(); + i != $$->end(); ++i) + { + bdd_delref(i->first); + delete i->second; + } + delete $$; + } %printer { if ($$) debug_stream() << *$$; @@ -139,22 +200,18 @@ %printer { debug_stream() << $$; } %% +aut: aut-1 { res.h->loc = @$; YYACCEPT; } + | ENDOFFILE { YYABORT; } + +aut-1: hoa | never + +/**********************************************************************/ +/* Rules for HOA */ +/**********************************************************************/ + hoa: header "--BODY--" body "--END--" - { - res.h->loc = @$; - YYACCEPT; - } hoa: error "--END--" - { - res.h->loc = @$; - YYACCEPT; - } hoa: error ENDOFFILE - { - res.h->loc = @$; - YYACCEPT; - } -hoa: ENDOFFILE { YYABORT; } string_opt: | STRING BOOLEAN: 't' | 'f' @@ -660,6 +717,200 @@ incorrectly-labeled-edge: trans-label unlabeled-edge " edge has no label"); } +/**********************************************************************/ +/* Rules for neverclaims */ +/**********************************************************************/ + +never: "never" { res.namer = res.h->aut->create_namer(); + res.h->aut->set_single_acceptance_set(); + res.h->aut->prop_state_based_acc(); } + '{' nc-states '}' + { + // Add an accept_all state if needed. + if (res.accept_all_needed && !res.accept_all_seen) + { + unsigned n = res.namer->new_state("accept_all"); + res.h->aut->new_acc_transition(n, n, bddtrue); + } + } + +nc-states: + /* empty */ + | nc-state + | nc-states ';' nc-state + | nc-states ';' + +nc-one-ident: IDENTIFIER ':' + { + unsigned n = res.namer->new_state(*$1); + if (res.labels.empty()) + { + // The first state is initial. + res.start.emplace_back(@$, n); + } + auto r = res.labels.insert(std::make_pair(*$1, @1)); + if (!r.second) + { + error(@1, std::string("redefinition of ") + *$1 + "..."); + error(r.first->second, std::string("... ") + *$1 + + " previously defined here"); + } + $$ = $1; + } + +nc-ident-list: nc-one-ident + | nc-ident-list nc-one-ident + { + res.namer->alias_state(res.namer->get_state(*$1), *$2); + // Keep any identifier that starts with accept. + if (strncmp("accept", $1->c_str(), 6)) + { + delete $1; + $$ = $2; + } + else + { + delete $2; + $$ = $1; + } + } + +nc-transition-block: + "if" nc-transitions "fi" + { + $$ = $2; + } + | "do" nc-transitions "od" + { + $$ = $2; + } + +nc-state: + nc-ident-list "skip" + { + if (*$1 == "accept_all") + res.accept_all_seen = true; + + res.namer->new_transition(*$1, *$1, bddtrue, + !strncmp("accept", $1->c_str(), 6) ? + res.h->aut->acc().all_sets() : + spot::acc_cond::mark_t(0U)); + delete $1; + } + | nc-ident-list { delete $1; } + | nc-ident-list "false" { delete $1; } + | nc-ident-list nc-transition-block + { + auto acc = !strncmp("accept", $1->c_str(), 6) ? + res.h->aut->acc().all_sets() : spot::acc_cond::mark_t(0U); + for (auto& p: *$2) + { + bdd c = bdd_from_int(p.first); + bdd_delref(p.first); + res.namer->new_transition(*$1, *p.second, c, acc); + delete p.second; + } + delete $1; + delete $2; + } + +nc-transitions: + /* empty */ { $$ = new std::list; } + | nc-transitions nc-transition + { + if ($2) + { + $1->push_back(*$2); + delete $2; + } + $$ = $1; + } + +nc-formula-or-ident: FORMULA | IDENTIFIER + +nc-formula: nc-formula-or-ident + { + auto i = res.fcache.find(*$1); + if (i == res.fcache.end()) + { + spot::ltl::parse_error_list pel; + auto f = spot::ltl::parse_boolean(*$1, pel, *res.env, + debug_level(), true); + for (auto& j: pel) + { + // Adjust the diagnostic to the current position. + spot::location here = @1; + here.end.line = here.begin.line + j.first.end.line - 1; + here.end.column = here.begin.column + j.first.end.column; + here.begin.line += j.first.begin.line - 1; + here.begin.column += j.first.begin.column; + error_list.emplace_back(here, j.second); + } + bdd cond = bddfalse; + if (f) + { + cond = spot::formula_to_bdd(f, res.h->aut->get_dict(), + res.h->aut); + f->destroy(); + } + $$ = (res.fcache[*$1] = cond).id(); + } + else + { + $$ = i->second.id(); + } + bdd_addref($$); + delete $1; + } + | "false" + { + $$ = 0; + } + +nc-opt-dest: + /* empty */ + { + $$ = 0; + } + | "->" "goto" IDENTIFIER + { + $$ = $3; + } + | "->" "assert" FORMULA + { + delete $3; + $$ = new std::string("accept_all"); + res.accept_all_needed = true; + } + +nc-src-dest: nc-formula nc-opt-dest + { + // If there is no destination, do ignore the transition. + // This happens for instance with + // if + // :: false + // fi + if (!$2) + { + $$ = 0; + } + else + { + $$ = new pair($1, $2); + res.namer->new_state(*$2); + } + } + +nc-transition: + ':' ':' "atomic" '{' nc-src-dest '}' + { + $$ = $5; + } + | ':' ':' nc-src-dest + { + $$ = $3; + } + %% static void fill_guards(result_& r) diff --git a/src/hoaparse/hoascan.ll b/src/hoaparse/hoascan.ll index a87734f46..20cbefd6b 100644 --- a/src/hoaparse/hoascan.ll +++ b/src/hoaparse/hoascan.ll @@ -25,12 +25,16 @@ %{ #include #include "hoaparse/parsedecl.hh" +#include "misc/escape.hh" #define YY_USER_ACTION yylloc->columns(yyleng); #define YY_NEVER_INTERACTIVE 1 typedef hoayy::parser::token token; static unsigned comment_level = 0; +static unsigned parent_level = 0; +static int orig_cond = 0; +static bool missing_parent = false; %} @@ -38,7 +42,8 @@ eol \n+|\r+ eol2 (\n\r)+|(\r\n)+ identifier [[:alpha:]_][[:alnum:]_-]* -%x in_COMMENT in_STRING +%x in_COMMENT in_STRING in_NEVER_PAR +%s in_HOA in_NEVER %% @@ -52,38 +57,48 @@ identifier [[:alpha:]_][[:alnum:]_-]* {eol} yylloc->lines(yyleng); yylloc->step(); {eol2} yylloc->lines(yyleng / 2); yylloc->step(); [ \t\v\f]+ yylloc->step(); -"/""*"+ BEGIN(in_COMMENT); comment_level = 1; -"\"" BEGIN(in_STRING); +"/""*"+ { + orig_cond = YY_START; + BEGIN(in_COMMENT); + comment_level = 1; + } +"\"" { + orig_cond = YY_START; + BEGIN(in_STRING); + comment_level = 1; + } +"HOA:" BEGIN(in_HOA); return token::HOA; +"--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc}; +"never" BEGIN(in_NEVER); return token::NEVER; -"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; -"--ABORT--" throw spot::hoa_abort{*yylloc}; -"--END--" return token::END; -"State:" return token::STATE; -[tf{}()\[\]&|!] return *yytext; +{ + "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--" BEGIN(INITIAL); return token::END; + "State:" return token::STATE; + [tf{}()\[\]&|!] return *yytext; -{identifier} { + {identifier} { yylval->str = new std::string(yytext, yyleng); return token::IDENTIFIER; } -{identifier}":" { + {identifier}":" { yylval->str = new std::string(yytext, yyleng - 1); return token::HEADERNAME; } -"@"[[:alnum:]_-]+ { + "@"[[:alnum:]_-]+ { yylval->str = new std::string(yytext + 1, yyleng - 1); return token::ANAME; } -[0-9]+ { + [0-9]+ { errno = 0; unsigned long n = strtoul(yytext, 0, 10); yylval->num = n; @@ -96,6 +111,38 @@ identifier [[:alpha:]_][[:alnum:]_-]* } return token::INT; } +} + +{ + "skip" return token::SKIP; + "if" return token::IF; + "fi" return token::FI; + "do" return token::DO; + "od" return token::OD; + "->" return token::ARROW; + "goto" return token::GOTO; + "false"|"0" return token::FALSE; + "atomic" return token::ATOMIC; + "assert" return token::ASSERT; + + ("!"[ \t]*)?"(" { + parent_level = 1; + BEGIN(in_NEVER_PAR); + yylval->str = new std::string(yytext, yyleng); + } + + "true"|"1" { + yylval->str = new std::string(yytext, yyleng); + return token::FORMULA; + } + + [a-zA-Z][a-zA-Z0-9_]* { + yylval->str = new std::string(yytext, yyleng); + return token::IDENTIFIER; + } + +} + { "/""*"+ ++comment_level; @@ -103,7 +150,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* "/"[^*\n]* continue; "*"+[^*/\n]* continue; "\n"+ yylloc->end.column = 1; yylloc->lines(yyleng); - "*"+"/" if (--comment_level == 0) BEGIN(INITIAL); + "*"+"/" if (--comment_level == 0) BEGIN(orig_cond); <> { error_list.push_back( spot::hoa_parse_error(*yylloc, @@ -114,7 +161,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* { \" { - BEGIN(INITIAL); + BEGIN(orig_cond); yylval->str = new std::string(s); return token::STRING; } @@ -128,6 +175,35 @@ identifier [[:alpha:]_][[:alnum:]_-]* } } +{ + "(" { + ++parent_level; + yylval->str->append(yytext, yyleng); + } + /* if we match ")&&(" or ")||(", stay in mode */ + ")"[ \t]*("&&"|"||")[ \t!]*"(" { + yylval->str->append(yytext, yyleng); + } + ")" { + yylval->str->append(yytext, yyleng); + if (!--parent_level) + { + BEGIN(in_NEVER); + spot::trim(*yylval->str); + return token::FORMULA; + } + } + [^()]+ yylval->str->append(yytext, yyleng); + <> { + unput(')'); + if (!missing_parent) + error_list.push_back( + spot::hoa_parse_error(*yylloc, + "missing closing parenthese")); + missing_parent = true; + } +} + . return *yytext; %{ @@ -158,6 +234,8 @@ namespace spot YY_NEW_FILE; BEGIN(INITIAL); comment_level = 0; + parent_level = 0; + missing_parent = false; return 0; } diff --git a/src/hoaparse/public.hh b/src/hoaparse/public.hh index 19097d026..2a7a92922 100644 --- a/src/hoaparse/public.hh +++ b/src/hoaparse/public.hh @@ -66,7 +66,7 @@ namespace spot bool debug = false); }; - /// \brief Build a spot::tgba_digraph from a HOA file. + /// \brief Build a spot::tgba_digraph from a HOA file or a neverclaim. /// \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. @@ -82,6 +82,16 @@ namespace spot /// parsing of \a filename. If you want to make sure \a filename /// was parsed succesfully, check \a error_list for emptiness. /// + /// The specification of the HOA format can be found at + /// http://adl.github.io/hoaf/ + /// + /// The grammar of neverclaim will not accept every possible + /// neverclaim output. It has been tuned to accept the output of + /// spin -f, ltl2ba, ltl3ba, and modella. If you know of some other + /// tool that produce Büchi automata in the form of a neverclaim, + /// but is not understood by this parse, please report it to + /// spot@lrde.epita.fr. + /// /// \warning This function is not reentrant. inline hoa_aut_ptr hoa_parse(const std::string& filename, diff --git a/src/neverparse/.gitignore b/src/neverparse/.gitignore deleted file mode 100644 index 8b61948f3..000000000 --- a/src/neverparse/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -position.hh -neverclaimparse.cc -neverclaimparse.output -neverclaimparse.hh -neverclaimscan.cc -stack.hh -location.hh diff --git a/src/neverparse/Makefile.am b/src/neverparse/Makefile.am deleted file mode 100644 index d82eb71e8..000000000 --- a/src/neverparse/Makefile.am +++ /dev/null @@ -1,57 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2011, 2013 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=) - -neverparsedir = $(pkgincludedir)/neverparse - -neverparse_HEADERS = public.hh - -noinst_LTLIBRARIES = libneverparse.la - -NEVERCLAIMPARSE_YY = neverclaimparse.yy -FROM_NEVERCLAIMPARSE_YY_MAIN = neverclaimparse.cc -FROM_NEVERCLAIMPARSE_YY_OTHERS = \ - stack.hh \ - neverclaimparse.hh - -FROM_NEVERCLAIMPARSE_YY = $(FROM_NEVERCLAIMPARSE_YY_MAIN) $(FROM_NEVERCLAIMPARSE_YY_OTHERS) - -BUILT_SOURCES = $(FROM_NEVERCLAIMPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_NEVERCLAIMPARSE_YY) - -$(FROM_NEVERCLAIMPARSE_YY_MAIN): $(srcdir)/$(NEVERCLAIMPARSE_YY) -## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(NEVERCLAIMPARSE_YY), it will also use the value of $(srcdir)/ -## in the generated include statements. - cd $(srcdir) && \ - $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \ - $(NEVERCLAIMPARSE_YY) -o $(FROM_NEVERCLAIMPARSE_YY_MAIN) -$(FROM_NEVERCLAIMPARSE_YY_OTHERS): $(NEVERCLAIMPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_NEVERCLAIMPARSE_YY_MAIN) - -EXTRA_DIST = $(NEVERCLAIMPARSE_YY) - -libneverparse_la_SOURCES = \ - fmterror.cc \ - $(FROM_NEVERCLAIMPARSE_YY) \ - neverclaimscan.ll \ - parsedecl.hh diff --git a/src/neverparse/fmterror.cc b/src/neverparse/fmterror.cc deleted file mode 100644 index 092763153..000000000 --- a/src/neverparse/fmterror.cc +++ /dev/null @@ -1,42 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 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_neverclaim_parse_errors(std::ostream& os, - const std::string& filename, - neverclaim_parse_error_list& error_list) - { - bool printed = false; - spot::neverclaim_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/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy deleted file mode 100644 index 11725244e..000000000 --- a/src/neverparse/neverclaimparse.yy +++ /dev/null @@ -1,340 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 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 . -*/ -%language "C++" -%locations -%defines -%expect 0 // No shift/reduce -%name-prefix "neverclaimyy" -%debug -%error-verbose -%lex-param { spot::neverclaim_parse_error_list& error_list } -%define api.location.type "spot::location" - -%code requires -{ -#include -#include -#include "public.hh" -#include "tgba/formula2bdd.hh" - -/* Cache parsed formulae. Labels on arcs are frequently identical and - it would be a waste of time to parse them to formula* over and - over, and to register all their atomic_propositions in the - bdd_dict. Keep the bdd result around so we can reuse it. */ - typedef std::map formula_cache; - - typedef std::pair pair; - typedef typename spot::tgba_digraph::namer::type named_tgba_t; -} - -%parse-param {spot::neverclaim_parse_error_list& error_list} -%parse-param {spot::ltl::environment& parse_environment} -%parse-param {spot::tgba_digraph_ptr& result} -%parse-param {named_tgba_t*& namer} -%parse-param {formula_cache& fcache} -%union -{ - std::string* str; - pair* p; - std::list* list; - const bdd* b; -} - -%code -{ -#include "ltlast/constant.hh" -#include "ltlparse/public.hh" - -/* neverclaimparse.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" -using namespace spot::ltl; -static bool accept_all_needed = false; -static bool accept_all_seen = false; -static std::map labels; -} - -%token NEVER "never" -%token SKIP "skip" -%token IF "if" -%token FI "fi" -%token DO "do" -%token OD "od" -%token ARROW "->" -%token GOTO "goto" -%token FALSE "false" -%token ATOMIC "atomic" -%token ASSERT "assert" -%token FORMULA "boolean formula" -%token IDENT "identifier" -%type formula -%type opt_dest formula_or_ident -%type

transition src_dest -%type transitions transition_block -%type one_ident ident_list - - -%destructor { delete $$; } -%destructor { delete $$->second; delete $$; }

-%destructor { - for (std::list::iterator i = $$->begin(); - i != $$->end(); ++i) - { - delete i->second; - } - delete $$; - } -%printer { - if ($$) - debug_stream() << *$$; - else - debug_stream() << "\"\""; } - -%% -neverclaim: - "never" '{' states '}' - - -states: - /* empty */ - | state - | states ';' state - | states ';' - -one_ident: IDENT ':' - { - namer->new_state(*$1); - std::pair::const_iterator, bool> - res = labels.insert(std::make_pair(*$1, @1)); - if (!res.second) - { - error(@1, std::string("redefinition of ") + *$1 + "..."); - error(res.first->second, std::string("... ") + *$1 + " previously defined here"); - } - $$ = $1; - } - - -ident_list: one_ident - | ident_list one_ident - { - namer->alias_state(namer->get_state(*$1), *$2); - // Keep any identifier that starts with accept. - if (strncmp("accept", $1->c_str(), 6)) - { - delete $1; - $$ = $2; - } - else - { - delete $2; - $$ = $1; - } - } - - -transition_block: - "if" transitions "fi" - { - $$ = $2; - } - | "do" transitions "od" - { - $$ = $2; - } - -state: - ident_list "skip" - { - if (*$1 == "accept_all") - accept_all_seen = true; - - namer->new_transition(*$1, *$1, bddtrue, - !strncmp("accept", $1->c_str(), 6) ? - result->acc().all_sets() : - spot::acc_cond::mark_t(0U)); - delete $1; - } - | ident_list { delete $1; } - | ident_list "false" { delete $1; } - | ident_list transition_block - { - auto acc = !strncmp("accept", $1->c_str(), 6) ? - result->acc().all_sets() : spot::acc_cond::mark_t(0U); - for (auto& p: *$2) - namer->new_transition(*$1, *p.second, *p.first, acc); - // Free the list - delete $1; - for (auto& p: *$2) - delete p.second; - delete $2; - } - - -transitions: - /* empty */ { $$ = new std::list; } - | transitions transition - { - if ($2) - { - $1->push_back(*$2); - delete $2; - } - $$ = $1; - } - - -formula_or_ident: FORMULA | IDENT - -formula: formula_or_ident - { - formula_cache::const_iterator i = fcache.find(*$1); - if (i == fcache.end()) - { - parse_error_list pel; - const formula* f = - spot::ltl::parse_boolean(*$1, pel, parse_environment, - debug_level(), true); - for (auto& j: pel) - { - // Adjust the diagnostic to the current position. - spot::location here = @1; - here.end.line = here.begin.line + j.first.end.line - 1; - here.end.column = here.begin.column + j.first.end.column; - here.begin.line += j.first.begin.line - 1; - here.begin.column += j.first.begin.column; - error_list.emplace_back(here, j.second); - } - bdd cond = bddfalse; - if (f) - { - cond = formula_to_bdd(f, result->get_dict(), result); - f->destroy(); - } - $$ = &(fcache[*$1] = cond); - } - else - { - $$ = &i->second; - } - delete $1; - } - | "false" - { - $$ = &bddfalse; - } - -opt_dest: - /* empty */ - { - $$ = 0; - } - | "->" "goto" IDENT - { - $$ = $3; - } - | "->" "assert" FORMULA - { - delete $3; - $$ = new std::string("accept_all"); - accept_all_needed = true; - } - -src_dest: formula opt_dest - { - // If there is no destination, do ignore the transition. - // This happens for instance with - // if - // :: false - // fi - if (!$2) - { - $$ = 0; - } - else - { - $$ = new pair($1, $2); - namer->new_state(*$2); - } - } - - -transition: - ':' ':' "atomic" '{' src_dest '}' - { - $$ = $5; - } - | ':' ':' src_dest - { - $$ = $3; - } -%% - -void -neverclaimyy::parser::error(const location_type& location, - const std::string& message) -{ - error_list.emplace_back(location, message); -} - -namespace spot -{ - tgba_digraph_ptr - neverclaim_parse(const std::string& name, - neverclaim_parse_error_list& error_list, - bdd_dict_ptr dict, - environment& env, - bool debug) - { - if (neverclaimyyopen(name)) - { - error_list.emplace_back(spot::location(), - std::string("Cannot open file ") + name); - return 0; - } - formula_cache fcache; - tgba_digraph_ptr result = make_tgba_digraph(dict); - auto namer = result->create_namer(); - result->set_single_acceptance_set(); - result->prop_state_based_acc(); - - neverclaimyy::parser parser(error_list, env, result, namer, fcache); - parser.set_debug_level(debug); - parser.parse(); - neverclaimyyclose(); - - if (accept_all_needed && !accept_all_seen) - { - unsigned n = namer->new_state("accept_all"); - result->new_acc_transition(n, n, bddtrue); - } - accept_all_needed = false; - accept_all_seen = false; - labels.clear(); - - delete namer; - return result; - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/neverparse/neverclaimscan.ll b/src/neverparse/neverclaimscan.ll deleted file mode 100644 index 50ad283f3..000000000 --- a/src/neverparse/neverclaimscan.ll +++ /dev/null @@ -1,151 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 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 . -*/ -%option noyywrap -%option prefix="neverclaimyy" -%option outfile="lex.yy.c" - -%{ -#include -#include "neverparse/parsedecl.hh" -#include "misc/escape.hh" - -#define YY_USER_ACTION \ - yylloc->columns(yyleng); - -#define YY_NEVER_INTERACTIVE 1 - -typedef neverclaimyy::parser::token token; -static int parent_level = 0; -static bool missing_parent = false; - -%} - -%x in_par - -eol \n+|\r+ -eol2 (\n\r)+|(\r\n)+ - -%% - -%{ - yylloc->step(); -%} - - /* skip blanks */ -{eol} yylloc->lines(yyleng); yylloc->step(); -{eol2} yylloc->lines(yyleng / 2); yylloc->step(); -[ \t]+ yylloc->step(); -"/*".*"*/" yylloc->step(); - -"never" return token::NEVER; -"skip" return token::SKIP; -"if" return token::IF; -"fi" return token::FI; -"do" return token::DO; -"od" return token::OD; -"->" return token::ARROW; -"goto" return token::GOTO; -"false"|"0" return token::FALSE; -"atomic" return token::ATOMIC; -"assert" return token::ASSERT; - -("!"[ \t]*)?"(" { - parent_level = 1; - BEGIN(in_par); - yylval->str = new std::string(yytext,yyleng); - } - -{ - "(" { - ++parent_level; - yylval->str->append(yytext, yyleng); - } - /* if we match ")&&(" or ")||(", stay in mode */ - ")"[ \t]*("&&"|"||")[ \t!]*"(" { - yylval->str->append(yytext, yyleng); - } - ")" { - yylval->str->append(yytext, yyleng); - if (!--parent_level) - { - BEGIN(0); - spot::trim(*yylval->str); - return token::FORMULA; - } - } - [^()]+ yylval->str->append(yytext, yyleng); - <> { - unput(')'); - if (!missing_parent) - error_list.push_back( - spot::neverclaim_parse_error(*yylloc, - "missing closing parenthese")); - missing_parent = true; - } -} - -"true"|"1" { - yylval->str = new std::string(yytext, yyleng); - return token::FORMULA; - } - -[a-zA-Z][a-zA-Z0-9_]* { - yylval->str = new std::string(yytext, yyleng); - return token::IDENT; - } - -. return *yytext; - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - -namespace spot -{ - int - neverclaimyyopen(const std::string &name) - { - 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. - BEGIN(0); - YY_NEW_FILE; - return 0; - } - - void - neverclaimyyclose() - { - fclose(yyin); - missing_parent = false; - } -} diff --git a/src/neverparse/parsedecl.hh b/src/neverparse/parsedecl.hh deleted file mode 100644 index 6724c0828..000000000 --- a/src/neverparse/parsedecl.hh +++ /dev/null @@ -1,39 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 2013 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_NEVERPARSE_PARSEDECL_HH -# define SPOT_NEVERPARSE_PARSEDECL_HH - -#include -#include "neverclaimparse.hh" -#include "misc/location.hh" - -# define YY_DECL \ - int neverclaimyylex(neverclaimyy::parser::semantic_type *yylval, \ - spot::location *yylloc, \ - spot::neverclaim_parse_error_list& error_list) -YY_DECL; - -namespace spot -{ - int neverclaimyyopen(const std::string& name); - void neverclaimyyclose(); -} - -#endif // SPOT_NEVERCLAIMPARSE_PARSEDECL_HH diff --git a/src/neverparse/public.hh b/src/neverparse/public.hh deleted file mode 100644 index ae79ffc65..000000000 --- a/src/neverparse/public.hh +++ /dev/null @@ -1,79 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2010, 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_NEVERPARSE_PUBLIC_HH -# define SPOT_NEVERPARSE_PUBLIC_HH - -# include "tgba/tgbagraph.hh" -# include "misc/location.hh" -# include "ltlenv/defaultenv.hh" -# include -# include -# include -# include - -namespace spot -{ - /// \addtogroup tgba_io - /// @{ - - /// \brief A parse diagnostic with its location. - typedef std::pair neverclaim_parse_error; - /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list neverclaim_parse_error_list; - - /// \brief Build a spot::tgba_digraph from a Spin never claim file. - /// \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 tgba_digraph_ptr - neverclaim_parse(const std::string& filename, - neverclaim_parse_error_list& - error_list, - bdd_dict_ptr dict, - ltl::environment& env = ltl::default_environment::instance(), - bool debug = false); - - /// \brief Format diagnostics produced by spot::neverclaim_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_neverclaim_parse_errors(std::ostream& os, - const std::string& filename, - neverclaim_parse_error_list& error_list); - /// @} -} - -#endif // SPOT_NEVERCLAIMPARSE_PUBLIC_HH diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test index 082e68fb4..0632fd0b0 100755 --- a/src/tgbatest/hoaparse.test +++ b/src/tgbatest/hoaparse.test @@ -480,6 +480,7 @@ EOF diff expected input.out +# Mix HOA with neverclaims cat >input < goto accept_all + :: ((a)) -> goto T0_init + fi; +accept_all: + skip +} + + +never { + start: if :: false -> goto T0 fi; + T0: false +} EOF expectok input <input <merge_transitions(); } break; - case ReadNeverclaim: - { - spot::tgba_digraph_ptr e; - spot::neverclaim_parse_error_list pel; - tm.start("parsing neverclaim"); - a = e = spot::neverclaim_parse(input, pel, dict, - env, debug_opt); - tm.stop("parsing neverclaim"); - if (spot::format_neverclaim_parse_errors(std::cerr, input, pel)) - return 2; - assume_sba = true; - e->merge_transitions(); - } - break; case ReadLbtt: { std::string error; @@ -1113,8 +1097,9 @@ checked_main(int argc, char** argv) tm.stop("parsing hoa"); if (spot::format_hoa_parse_errors(std::cerr, input, pel)) return 2; + daut->aut->merge_transitions(); a = daut->aut; - assume_sba = false; + assume_sba = a->is_sba(); } break; } diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index d615afa6b..94cdf78c2 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -169,7 +169,7 @@ EOF run 2 ../ltl2tgba -XN input > stdout 2>stderr cat >expected <<\EOF -input:9.16: syntax error, unexpected $undefined, expecting fi or ':' +input:9.16: syntax error, unexpected ')', expecting fi or ':' EOF grep input: stderr > stderrfilt diff stderrfilt expected