diff --git a/src/neverparse/neverclaimparse.yy b/src/neverparse/neverclaimparse.yy index f0f9d7747..d5ec008b8 100644 --- a/src/neverparse/neverclaimparse.yy +++ b/src/neverparse/neverclaimparse.yy @@ -33,18 +33,29 @@ #include #include "ltlast/constant.hh" #include "public.hh" +#include "tgba/formula2bdd.hh" - typedef std::pair pair; +/* 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_explicit_string*& result} +%parse-param {spot::tgba_digraph*& 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 @@ -74,24 +85,24 @@ static bool accept_all_seen = false; %token ASSERT "assert" %token FORMULA "boolean formula" %token IDENT "identifier" -%type formula opt_dest +%type formula +%type opt_dest %type

transition src_dest %type transitions transition_block %type ident_list %destructor { delete $$; } -%destructor { $$->first->destroy(); delete $$->second; delete $$; }

+%destructor { delete $$->second; delete $$; }

%destructor { for (std::list::iterator i = $$->begin(); i != $$->end(); ++i) { - i->first->destroy(); delete i->second; } delete $$; } - %printer { +%printer { if ($$) debug_stream() << *$$; else @@ -111,11 +122,12 @@ states: ident_list: IDENT ':' { + namer->new_state(*$1); $$ = $1; } | ident_list IDENT ':' { - result->add_state_alias(*$2, *$1); + namer->alias_state(namer->get_state(*$1), *$2); // Keep any identifier that starts with accept. if (strncmp("accept", $1->c_str(), 6)) { @@ -146,11 +158,10 @@ state: if (*$1 == "accept_all") accept_all_seen = true; - spot::state_explicit_string::transition* t = result->create_transition(*$1, *$1); - bool acc = !strncmp("accept", $1->c_str(), 6); - if (acc) - result->add_acceptance_condition(t, - spot::ltl::constant::true_instance()); + namer->new_transition(*$1, *$1, bddtrue, + !strncmp("accept", $1->c_str(), 6) ? + result->all_acceptance_conditions() : + static_cast(bddfalse)); delete $1; } | ident_list { delete $1; } @@ -158,22 +169,15 @@ state: | ident_list transition_block { std::list::iterator it; - bool acc = !strncmp("accept", $1->c_str(), 6); - for (it = $2->begin(); it != $2->end(); ++it) - { - spot::state_explicit_string::transition* t = - result->create_transition(*$1, *it->second); - - result->add_condition(t, it->first); - if (acc) - result - ->add_acceptance_condition(t, spot::ltl::constant::true_instance()); - } + bdd acc = !strncmp("accept", $1->c_str(), 6) ? + result->all_acceptance_conditions() : + static_cast(bddfalse); + for (auto& p: *$2) + namer->new_transition(*$1, *p.second, *p.first, acc); // Free the list delete $1; - for (std::list::iterator it = $2->begin(); - it != $2->end(); ++it) - delete it->second; + for (auto& p: *$2) + delete p.second; delete $2; } @@ -191,7 +195,43 @@ transitions: } -formula: FORMULA | "false" { $$ = new std::string("0"); } +formula: FORMULA + { + 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 */ @@ -218,28 +258,12 @@ src_dest: formula opt_dest // fi if (!$2) { - delete $1; $$ = 0; } else { - spot::ltl::parse_error_list pel; - const spot::ltl::formula* f = - spot::ltl::parse_boolean(*$1, pel, parse_environment, - debug_level(), true); - delete $1; - for(spot::ltl::parse_error_list::const_iterator i = pel.begin(); - i != pel.end(); ++i) - { - // Adjust the diagnostic to the current position. - spot::location here = @1; - here.end.line = here.begin.line + i->first.end.line - 1; - here.end.column = here.begin.column + i->first.end.column -1; - here.begin.line += i->first.begin.line - 1; - here.begin.column += i->first.begin.column - 1; - error(here, i->second); - } - $$ = new pair(f, $2); + $$ = new pair($1, $2); + namer->new_state(*$2); } } @@ -264,7 +288,7 @@ neverclaimyy::parser::error(const location_type& location, namespace spot { - tgba_explicit_string* + tgba_digraph* neverclaim_parse(const std::string& name, neverclaim_parse_error_list& error_list, bdd_dict* dict, @@ -277,23 +301,28 @@ namespace spot std::string("Cannot open file ") + name); return 0; } - tgba_explicit_string* result = new tgba_explicit_string(dict); - result->declare_acceptance_condition(spot::ltl::constant::true_instance()); - neverclaimyy::parser parser(error_list, env, result); + formula_cache fcache; + tgba_digraph* result = new tgba_digraph(dict); + auto namer = result->create_namer(); + + const ltl::formula* t = ltl::constant::true_instance(); + bdd acc = bdd_ithvar(dict->register_acceptance_variable(t, result)); + result->set_acceptance_conditions(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) { - spot::state_explicit_string::transition* t = - result->create_transition("accept_all", "accept_all"); - result->add_acceptance_condition - (t, spot::ltl::constant::true_instance()); + unsigned n = namer->new_state("accept_all"); + result->new_transition(n, n, bddtrue, acc); } accept_all_needed = false; accept_all_seen = false; + delete namer; return result; } } diff --git a/src/neverparse/public.hh b/src/neverparse/public.hh index 15477e5e6..63f65c8ed 100644 --- a/src/neverparse/public.hh +++ b/src/neverparse/public.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// 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. // @@ -20,7 +20,7 @@ #ifndef SPOT_NEVERPARSE_PUBLIC_HH # define SPOT_NEVERPARSE_PUBLIC_HH -# include "tgba/tgbaexplicit.hh" +# include "tgba/tgbagraph.hh" # include "misc/location.hh" # include "ltlenv/defaultenv.hh" # include @@ -55,7 +55,7 @@ namespace spot /// was parsed succesfully, check \a error_list for emptiness. /// /// \warning This function is not reentrant. - SPOT_API tgba_explicit_string* + SPOT_API tgba_digraph* neverclaim_parse(const std::string& filename, neverclaim_parse_error_list& error_list, diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e1ddcd8ac..f5b1144c1 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1025,6 +1025,7 @@ main(int argc, char** argv) break; case ReadNeverclaim: { + spot::tgba_digraph* e; spot::neverclaim_parse_error_list pel; tm.start("parsing neverclaim"); to_free = a = e = spot::neverclaim_parse(input, pel, dict, @@ -1037,6 +1038,7 @@ main(int argc, char** argv) return 2; } assume_sba = true; + e->merge_transitions(); } break; case ReadLbtt: diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index 3e75a715e..fc6cb3f67 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et +# 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. @@ -47,14 +47,14 @@ cat >expected < 1 - 1 [label="T2_init"] + 1 [label="0"] 1 -> 1 [label="1\n"] 1 -> 2 [label="p0 & p1\n"] - 2 [label="T1"] + 2 [label="1"] 2 -> 3 [label="p1 & !p0\n"] 2 -> 2 [label="!p1\n"] 2 -> 1 [label="!p1\n"] - 3 [label="accept_all", peripheries=2] + 3 [label="2", peripheries=2] 3 -> 3 [label="1\n{Acc[1]}"] } EOF @@ -91,14 +91,14 @@ cat >expected < 1 - 1 [label="T2_init"] + 1 [label="0"] 1 -> 1 [label="1\n"] 1 -> 2 [label="p0 & p1\n"] - 2 [label="T1"] + 2 [label="1"] 2 -> 3 [label="p1 & !p0\n"] 2 -> 2 [label="!p1\n"] 2 -> 1 [label="!p1\n"] - 3 [label="accept_all", peripheries=2] + 3 [label="2", peripheries=2] 3 -> 3 [label="1\n{Acc[1]}"] } EOF @@ -130,9 +130,9 @@ cat >expected < 1 - 1 [label="accept_init", peripheries=2] + 1 [label="0", peripheries=2] 1 -> 2 [label="p1\n{Acc[1]}"] - 2 [label="accept_all", peripheries=2] + 2 [label="1", peripheries=2] 2 -> 2 [label="1\n{Acc[1]}"] } EOF