From 355461ae996fe88efa5ea925edfbfa553983520b Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Sat, 4 Apr 2009 21:54:01 +0200 Subject: [PATCH] Extend the ELTL parser to support basic aliases of automaton operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix notation for binary automaton operators. * README: Document the ELTL directories. * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add support for aliases and infix notation. * src/eltlparse/public.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh: Clean them. * src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Add tests for the ELTL parser's extensions. * src/tgbatest/eltl2tgba.cc: Adjust. --- ChangeLog | 15 ++ README | 4 +- src/eltlparse/eltlparse.yy | 325 ++++++++++++++++++++++++++++-------- src/eltlparse/eltlscan.ll | 82 ++++----- src/eltlparse/public.hh | 8 +- src/eltltest/acc.test | 17 ++ src/ltlast/nfa.cc | 2 +- src/ltlast/nfa.hh | 2 +- src/tgbatest/eltl2tgba.cc | 4 +- src/tgbatest/eltl2tgba.test | 26 ++- 10 files changed, 370 insertions(+), 115 deletions(-) diff --git a/ChangeLog b/ChangeLog index 368946824..a5e6015c5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,18 @@ +2009-04-04 Damien Lefortier + + Extend the ELTL parser to support basic aliases of automaton + operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix + notation for binary automaton operators. + + * README: Document the ELTL directories. + * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add + support for aliases and infix notation. + * src/eltlparse/public.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh: + Clean them. + * src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Add tests + for the ELTL parser's extensions. + * src/tgbatest/eltl2tgba.cc: Adjust. + 2009-03-26 Damien Lefortier Add support for ELTL (AST & parser), and an adaptation of LaCIM diff --git a/README b/README index 537864a49..d66c960c1 100644 --- a/README +++ b/README @@ -93,7 +93,7 @@ Core directories ---------------- src/ Sources for libspot. - ltlast/ LTL abstract syntax tree. + ltlast/ LTL abstract syntax tree (including nodes for ELTL). ltlenv/ LTL environments. ltlparse/ Parser for LTL formulae. ltlvisit/ Visitors of LTL formulae. @@ -105,6 +105,8 @@ src/ Sources for libspot. tgbaparse/ Parser for explicit TGBA. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. evtgba*/ Ignore these for now. + eltlparse/ Parser for ELTL formulae. + eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. doc/ Documentation for libspot. spot.html/ HTML reference manual. spot.latex/ Sources for the PDF manual. (Not distributed, can be rebuilt.) diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index d3e1db6eb..6b9e524a4 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -32,29 +32,144 @@ #include #include #include +#include +#include #include "public.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/destroy.hh" -// Implementation details for error handling. namespace spot { namespace eltl { + /// The following parser allows one to define aliases of automaton + /// operators such as: F=U(true,$0). Internally it's handled by + /// creating a small AST associated with each alias in order to + /// instanciate the right automatop after: U(constant(1), AP(f)) + /// for the formula F(f). + /// + struct alias + { + virtual ~alias() {}; + }; + /// We use boost::shared_ptr to easily handle deletion. + typedef boost::shared_ptr alias_ptr; + + struct alias_not : alias + { + alias_ptr s; + }; + enum type { Xor, Implies, Equiv, Or, And }; + struct alias_binary : alias + { + type ty; + alias_ptr lhs; + alias_ptr rhs; + }; + struct alias_nfa : alias + { + nfa::ptr nfa; + std::list s; + }; + struct alias_arg : alias + { + int i; + }; + + typedef std::map nfamap; + typedef std::map aliasmap; + + /// Implementation details for error handling. struct parse_error_list_t { parse_error_list list_; std::string file_; }; + + /// Instanciate the formula corresponding to the given alias. + static formula* + alias2formula(alias_ptr ap, spot::ltl::automatop::vec* v) + { + if (alias_not* a = dynamic_cast(ap.get())) + return unop::instance(unop::Not, alias2formula(a->s, v)); + if (alias_arg* a = dynamic_cast(ap.get())) + return a->i == -1 ? constant::true_instance() : v->at(a->i); + if (alias_nfa* a = dynamic_cast(ap.get())) + { + automatop::vec* va = new automatop::vec; + std::list::const_iterator i = a->s.begin(); + while (i != a->s.end()) + va->push_back(alias2formula(*i++, v)); + return automatop::instance(a->nfa, va); + } + /// TODO. + assert(0); + } + + /// Get the arity of a given alias. + static size_t + arity(alias_ptr ap) + { + if (alias_not* a = dynamic_cast(ap.get())) + return arity(a->s); + if (alias_arg* a = dynamic_cast(ap.get())) + return a->i + 1; + if (alias_nfa* a = dynamic_cast(ap.get())) + { + size_t res = 0; + std::list::const_iterator i = a->s.begin(); + while (i != a->s.end()) + res = std::max(arity(*i++), res); + return res; + } + /// TODO. + assert(0); + } } } -#define PARSE_ERROR(Loc, Msg) \ - pe.list_.push_back \ +#define PARSE_ERROR(Loc, Msg) \ + pe.list_.push_back \ (parse_error(Loc, spair(pe.file_, Msg))) + +#define CHECK_EXISTING_NMAP(Loc, Ident) \ + { \ + nfamap::iterator i = nmap.find(*Ident); \ + if (i == nmap.end()) \ + { \ + std::string s = "unknown automaton operator `"; \ + s += *Ident; \ + s += "'"; \ + PARSE_ERROR(Loc, s); \ + delete Ident; \ + YYERROR; \ + } \ + } + +#define CHECK_ARITY(Loc, Ident, A1, A2) \ + { \ + if (A1 != A2) \ + { \ + std::ostringstream oss1; \ + oss1 << A1; \ + std::ostringstream oss2; \ + oss2 << A2; \ + \ + std::string s(*Ident); \ + s += " is used with "; \ + s += oss1.str(); \ + s += " arguments, but has an arity of "; \ + s += oss2.str(); \ + PARSE_ERROR(Loc, s); \ + delete Ident; \ + YYERROR; \ + } \ + } + } %parse-param {spot::eltl::nfamap& nmap} +%parse-param {spot::eltl::aliasmap& amap} %parse-param {spot::eltl::parse_error_list_t &pe} %parse-param {spot::ltl::environment &parse_environment} %parse-param {spot::ltl::formula* &result} @@ -68,6 +183,10 @@ namespace spot spot::ltl::nfa* nval; spot::ltl::automatop::vec* aval; spot::ltl::formula* fval; + + /// To handle aliases. + spot::eltl::alias* pval; + spot::eltl::alias_nfa* bval; } %code { @@ -81,40 +200,45 @@ using namespace spot::ltl; /* All tokens. */ -%token ATOMIC_PROP "atomic proposition" - IDENT "identifier" +%token ATOMIC_PROP "atomic proposition" + IDENT "identifier" -%token ARG "argument" - STATE "state" - OP_OR "or operator" - OP_XOR "xor operator" - OP_AND "and operator" - OP_IMPLIES "implication operator" - OP_EQUIV "equivalent operator" - OP_NOT "not operator" +%token ARG "argument" + STATE "state" + OP_OR "or operator" + OP_XOR "xor operator" + OP_AND "and operator" + OP_IMPLIES "implication operator" + OP_EQUIV "equivalent operator" + OP_NOT "not operator" -%token ACC "accept" - EQ "=" - LPAREN "(" - RPAREN ")" - COMMA "," - END_OF_FILE "end of file" - CONST_TRUE "constant true" - CONST_FALSE "constant false" +%token ACC "accept" + EQ "=" + LPAREN "(" + RPAREN ")" + COMMA "," + END_OF_FILE "end of file" + CONST_TRUE "constant true" + CONST_FALSE "constant false" /* Priorities. */ -/* Logical operators. */ %left OP_OR %left OP_XOR %left OP_AND %left OP_IMPLIES OP_EQUIV +%left ATOMIC_PROP + %nonassoc OP_NOT %type nfa_def %type subformula %type arg_list +%type nfa_arg +%type nfa_alias +%type nfa_alias_arg +%type nfa_alias_arg_list %destructor { delete $$; } "atomic proposition" %destructor { spot::ltl::destroy($$); } subformula @@ -132,7 +256,7 @@ result: nfa_list subformula /* NFA definitions. */ -nfa_list: /* empty. */ +nfa_list: /* empty */ | nfa_list nfa ; @@ -142,28 +266,22 @@ nfa: IDENT "=" "(" nfa_def ")" nmap[*$1] = nfa::ptr($4); delete $1; } + | IDENT "=" nfa_alias + { + amap[*$1] = alias_ptr($3); + delete $1; + } ; -nfa_def: /* empty. */ +nfa_def: /* empty */ { $$ = new nfa(); } - | nfa_def STATE STATE ARG + | nfa_def STATE STATE nfa_arg { - if ($4 == -1 || $3 == -1 || $2 == -1) - { - std::string s = "out of range integer"; - PARSE_ERROR(@1, s); - YYERROR; - } $1->add_transition($2, $3, $4); $$ = $1; } - | nfa_def STATE STATE CONST_TRUE - { - $1->add_transition($2, $3, -1); - $$ = $1; - } | nfa_def ACC STATE { $1->set_final($3); @@ -171,6 +289,71 @@ nfa_def: /* empty. */ } ; +nfa_alias: IDENT "(" nfa_alias_arg_list ")" + { + aliasmap::iterator i = amap.find(*$1); + if (i != amap.end()) + assert(0); // FIXME + else + { + CHECK_EXISTING_NMAP(@1, $1); + nfa::ptr np = nmap[*$1]; + + CHECK_ARITY(@1, $1, $3->s.size(), np->arity()); + $3->nfa = np; + $$ = $3; + } + delete $1; + } + | OP_NOT nfa_alias + { + alias_not* a = new alias_not; + a->s = alias_ptr($2); + $$ = a; + } + // TODO: more complicated aliases like | IDENT "(" nfa_alias ")" + +nfa_alias_arg_list: nfa_alias_arg + { + $$ = new alias_nfa; + $$->s.push_back(alias_ptr($1)); + } + | nfa_alias_arg_list "," nfa_alias_arg + { + $1->s.push_back(alias_ptr($3)); + $$ = $1; + } +; + +nfa_alias_arg: nfa_arg + { + alias_arg* a = new alias_arg; + a->i = $1; + $$ = a; + } + | OP_NOT nfa_alias_arg + { + alias_not* a = new alias_not; + a->s = alias_ptr($2); + $$ = a; + } + // TODO + +nfa_arg: ARG + { + if ($1 == -1) + { + std::string s = "out of range integer"; + PARSE_ERROR(@1, s); + YYERROR; + } + $$ = $1; + } + | CONST_TRUE + { $$ = -1; } +; + + /* Formulae. */ subformula: ATOMIC_PROP @@ -189,40 +372,50 @@ subformula: ATOMIC_PROP } else delete $1; + } + | subformula ATOMIC_PROP subformula + { + aliasmap::iterator i = amap.find(*$2); + if (i != amap.end()) + { + CHECK_ARITY(@1, $2, 2, arity(i->second)); + automatop::vec* v = new automatop::vec; + v->push_back($1); + v->push_back($3); + $$ = alias2formula(i->second, v); + delete v; + } + else + { + CHECK_EXISTING_NMAP(@1, $2); + nfa::ptr np = nmap[*$2]; + + CHECK_ARITY(@1, $2, 2, np->arity()); + automatop::vec* v = new automatop::vec; + v->push_back($1); + v->push_back($3); + $$ = automatop::instance(np, v); + } + delete $2; } | ATOMIC_PROP "(" arg_list ")" { - nfamap::iterator i = nmap.find(*$1); - if (i == nmap.end()) + aliasmap::iterator i = amap.find(*$1); + if (i != amap.end()) { - std::string s = "unknown automaton operator `"; - s += *$1; - s += "'"; - PARSE_ERROR(@1, s); - delete $1; - YYERROR; - } - - automatop* res = automatop::instance(i->second, $3); - if (res->size() != i->second->arity()) - { - std::ostringstream oss1; - oss1 << res->size(); - std::ostringstream oss2; - oss2 << i->second->arity(); - - std::string s(*$1); - s += " is used with "; - s += oss1.str(); - s += " arguments, but has an arity of "; - s += oss2.str(); - PARSE_ERROR(@1, s); - delete $1; + CHECK_ARITY(@1, $1, $3->size(), arity(i->second)); + $$ = alias2formula(i->second, $3); delete $3; - YYERROR; + } + else + { + CHECK_EXISTING_NMAP(@1, $1); + nfa::ptr np = nmap[*$1]; + + CHECK_ARITY(@1, $1, $3->size(), np->arity()); + $$ = automatop::instance(np, $3); } delete $1; - $$ = res; } | CONST_TRUE { $$ = constant::true_instance(); } @@ -284,9 +477,10 @@ namespace spot } formula* result = 0; nfamap nmap; + aliasmap amap; parse_error_list_t pe; pe.file_ = name; - eltlyy::parser parser(nmap, pe, env, result); + eltlyy::parser parser(nmap, amap, pe, env, result); parser.set_debug_level(debug); parser.parse(); error_list = pe.list_; @@ -303,8 +497,9 @@ namespace spot flex_scan_string(eltl_string.c_str()); formula* result = 0; nfamap nmap; + aliasmap amap; parse_error_list_t pe; - eltlyy::parser parser(nmap, pe, env, result); + eltlyy::parser parser(nmap, amap, pe, env, result); parser.set_debug_level(debug); parser.parse(); error_list = pe.list_; diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll index 92ed586c6..47b0abfc0 100644 --- a/src/eltlparse/eltlscan.ll +++ b/src/eltlparse/eltlscan.ll @@ -58,18 +58,53 @@ eol \n|\r|\n\r|\r\n yylloc->step(); %} + /* Rules for the include part. */ + +[ \t]* +[^ \t\n]+ { + FILE* tmp = fopen(yytext, "r"); + if (!tmp) + ERROR(std::string("cannot open file ") + yytext); + else + { + include.push(make_pair(YY_CURRENT_BUFFER, pe.file_)); + pe.file_ = std::string(yytext); + yy_switch_to_buffer(yy_create_buffer(tmp, YY_BUF_SIZE)); + } + BEGIN(INITIAL); + } + + /* Global rules (1). */ + +"(" return token::LPAREN; +"," return token::COMMA; +")" return token::RPAREN; +"!" return token::OP_NOT; + + /* & and | come from Spin. && and || from LTL2BA. + /\, \/, and xor are from LBTT. + */ +"||"|"|"|"+"|"\\/" { + return token::OP_OR; + } +"&&"|"&"|"."|"*"|"/\\" { + return token::OP_AND; + } +"^"|"xor" return token::OP_XOR; +"=>"|"->" return token::OP_IMPLIES; +"<=>"|"<->" return token::OP_EQUIV; + /* Rules for the automaton definitions part. */ +"include" BEGIN(incl); +"%" BEGIN(formula); + "=" return token::EQ; "accept" return token::ACC; + [tT][rR][uU][eE] { return token::CONST_TRUE; } -"(" return token::LPAREN; -")" return token::RPAREN; -"%" BEGIN(formula); - -"include" BEGIN(incl); [a-zA-Z][a-zA-Z0-9_]* { yylval->sval = new std::string(yytext, yyleng); @@ -99,30 +134,8 @@ eol \n|\r|\n\r|\r\n yy_switch_to_buffer(s.first); } - /* Rules for the include part. */ - -[ \t]* -[^ \t\n]+ { - FILE* tmp = fopen(yytext, "r"); - if (!tmp) - ERROR(std::string("cannot open file ") + yytext); - else - { - include.push(make_pair(YY_CURRENT_BUFFER, pe.file_)); - pe.file_ = std::string(yytext); - yy_switch_to_buffer(yy_create_buffer(tmp, YY_BUF_SIZE)); - } - BEGIN(INITIAL); - } - /* Rules for the formula part. */ -"(" return token::LPAREN; -")" return token::RPAREN; -"!" return token::OP_NOT; -"," return token::COMMA; - - "1"|[tT][rR][uU][eE] { return token::CONST_TRUE; } @@ -130,25 +143,12 @@ eol \n|\r|\n\r|\r\n return token::CONST_FALSE; } - /* & and | come from Spin. && and || from LTL2BA. - /\, \/, and xor are from LBTT. - */ -"||"|"|"|"+"|"\\/" { - return token::OP_OR; - } -"&&"|"&"|"."|"*"|"/\\" { - return token::OP_AND; - } -"^"|"xor" return token::OP_XOR; -"=>"|"->" return token::OP_IMPLIES; -"<=>"|"<->" return token::OP_EQUIV; - [a-zA-Z][a-zA-Z0-9_]* { yylval->sval = new std::string(yytext, yyleng); return token::ATOMIC_PROP; } - /* Global rules. */ + /* Global rules (2). */ /* discard whitespace */ {eol} yylloc->lines(yyleng); yylloc->step(); diff --git a/src/eltlparse/public.hh b/src/eltlparse/public.hh index f965ed64b..01615507c 100644 --- a/src/eltlparse/public.hh +++ b/src/eltlparse/public.hh @@ -35,6 +35,11 @@ # include # include +// namespace +// { +// typedef std::map nfamap; +// } + namespace spot { using namespace ltl; @@ -50,9 +55,6 @@ namespace spot /// \brief A list of parser diagnostics, as filled by parse. typedef std::list parse_error_list; - /// - typedef std::map nfamap; - /// \brief Build a formula from a text file. /// \param name The name of the file to parse. /// \param error_list A list that will be filled with diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test index b07f5bb2e..ab9b9b939 100755 --- a/src/eltltest/acc.test +++ b/src/eltltest/acc.test @@ -33,7 +33,24 @@ U=( 0 1 \$1 accept 1 ) +F=U(true, \$0) +R=!U(!\$0, !\$1) +% +a U b | a R b | F(true) | U(a,b) -> R(a,b) EOF +run 0 ./acc input || exit 1 + +cat >input <input < finals_; diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc index 14eb276dd..17482c133 100644 --- a/src/tgbatest/eltl2tgba.cc +++ b/src/tgbatest/eltl2tgba.cc @@ -51,7 +51,9 @@ X=(0 1 true \ U=(0 0 $0 \ 0 1 $1 \ accept 1) \ -G=(0 0 $0)"; +G=(0 0 $0) \ +F=U(true, $0) \ +R=!U(!$0, !$1)"; return s; } diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test index 53c9dbcda..9bd3e8272 100755 --- a/src/tgbatest/eltl2tgba.test +++ b/src/tgbatest/eltl2tgba.test @@ -36,6 +36,8 @@ U=( G=( 0 0 \$0 ) +F=U(true, \$0) +R=!U(!\$0, !\$1) EOF cat >input <input <input <input <input <input <