From 209e89a94cfcb72b0888b373f5d8a98e28f8a80f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Sep 2015 09:25:44 +0200 Subject: [PATCH] parseaut: swallow the dstarparser Note that the parser is still not able to reader multiple dstar automata. * src/dstarparse/: Delete. * configure.ac, src/Makefile.am, README: Adjust. * src/parseaut/parseaut.yy, src/parseaut/scanaut.ll: Merge in the dstarparser rules. * src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tests/ikwiad.cc: Adjust usage. * src/tests/parseaut.test: Adjust expected output. --- README | 3 +- configure.ac | 1 - src/Makefile.am | 5 +- src/bin/common_trans.cc | 40 +--- src/bin/common_trans.hh | 2 - src/bin/dstar2tgba.cc | 4 +- src/bin/ltlcross.cc | 104 ++++------ src/bin/ltldo.cc | 94 +++------ src/dstarparse/.gitignore | 7 - src/dstarparse/Makefile.am | 56 ----- src/dstarparse/dstarparse.yy | 392 ----------------------------------- src/dstarparse/dstarscan.ll | 152 -------------- src/dstarparse/parsedecl.hh | 37 ---- src/dstarparse/public.hh | 61 ------ src/parseaut/parseaut.yy | 245 +++++++++++++++++++--- src/parseaut/scanaut.ll | 18 ++ src/tests/ikwiad.cc | 61 ++---- src/tests/parseaut.test | 5 +- 18 files changed, 331 insertions(+), 956 deletions(-) delete mode 100644 src/dstarparse/.gitignore delete mode 100644 src/dstarparse/Makefile.am delete mode 100644 src/dstarparse/dstarparse.yy delete mode 100644 src/dstarparse/dstarscan.ll delete mode 100644 src/dstarparse/parsedecl.hh delete mode 100644 src/dstarparse/public.hh diff --git a/README b/README index b79eca2dc..039943851 100644 --- a/README +++ b/README @@ -137,7 +137,6 @@ Core directories src/ Sources for libspot. bin/ User tools built using the Spot library. man/ Man pages for the above tools. - dstarparse/ Parser for the output of ltl2dstar. graph/ Graph representations. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. @@ -146,7 +145,7 @@ src/ Sources for libspot. ltlparse/ Parser for LTL formulae. ltlvisit/ Visitors of LTL formulae. misc/ Miscellaneous support files. - parseaut/ Parser for HOA automata and Spin's never claims. + parseaut/ Parser for automata in multiple formats. priv/ Private algorithms, used internally but not exported. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. diff --git a/configure.ac b/configure.ac index aeed5e8b2..273a489f2 100644 --- a/configure.ac +++ b/configure.ac @@ -200,7 +200,6 @@ AC_CONFIG_FILES([ lib/Makefile src/bin/Makefile src/bin/man/Makefile - src/dstarparse/Makefile src/kripke/Makefile src/graph/Makefile src/parseaut/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index edfdcf75f..5a86005f6 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -26,14 +26,13 @@ AUTOMAKE_OPTIONS = subdir-objects # end, after building '.' (since the current directory contains # libspot.la needed by the tests) SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph twa \ - twaalgos ta taalgos kripke kripkeparse dstarparse parseaut \ - . bin tests sanity + twaalgos ta taalgos kripke kripkeparse parseaut . bin tests \ + sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ - dstarparse/libdstarparse.la \ parseaut/libparseaut.la \ kripke/libkripke.la \ kripkeparse/libkripkeparse.la \ diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc index 7cbc01d5b..2d01fea90 100644 --- a/src/bin/common_trans.cc +++ b/src/bin/common_trans.cc @@ -194,7 +194,6 @@ printable_result_filename::~printable_result_filename() void printable_result_filename::reset(unsigned n) { translator_num = n; - format = None; } void printable_result_filename::cleanup() @@ -204,33 +203,12 @@ void printable_result_filename::cleanup() } void -printable_result_filename::print(std::ostream& os, const char* pos) const +printable_result_filename::print(std::ostream& os, const char*) const { - output_format old_format = format; - // The HOA parser can read LBTT, neverclaims, and HOA. - if (*pos == 'N' || *pos == 'T' || *pos == 'H' || *pos == 'O') - format = Hoa; - else if (*pos == 'D') - format = Dstar; - else - SPOT_UNREACHABLE(); - - if (val_) - { - // It's OK to use a specifier multiple time, but it's not OK - // to mix the formats. - if (format != old_format) - error(2, 0, - "you may not mix different output specifiers: %s", - translators[translator_num].spec); - } - else - { - char prefix[30]; - snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num); - const_cast(this)->val_ - = spot::create_tmpfile(prefix); - } + char prefix[30]; + snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num); + const_cast(this)->val_ = + spot::create_tmpfile(prefix); quote_shell_string(os, val()->name()); } @@ -268,11 +246,11 @@ translator_runner::translator_runner(spot::bdd_dict_ptr dict, "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " "to pass the formula.", t.spec); if (!no_output_allowed - && !(has['O'] || has['D'] || + && !(has['O'] || // backward-compatibility - has['N'] || has['T'] || has['H'])) - error(2, 0, "no output %%-sequence in '%s'.\n Use one of " - "%%O or %%D to indicate where and how the automaton is saved.", + has['D'] || has['N'] || has['T'] || has['H'])) + error(2, 0, "no output %%-sequence in '%s'.\n Use " + "%%O to indicate where the automaton is output.", t.spec); // Remember the %-sequences used by all translators. prime(t.cmd); diff --git a/src/bin/common_trans.hh b/src/bin/common_trans.hh index 598e7cf09..d69905905 100644 --- a/src/bin/common_trans.hh +++ b/src/bin/common_trans.hh @@ -60,8 +60,6 @@ struct printable_result_filename final: public spot::printable_value { unsigned translator_num; - enum output_format { None, Dstar, Hoa }; - mutable output_format format; printable_result_filename(); ~printable_result_filename(); diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 5b28a2077..3395ea021 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -42,7 +42,7 @@ #include "twa/bddprint.hh" #include "misc/optionmap.hh" #include "misc/timer.hh" -#include "dstarparse/public.hh" +#include "parseaut/public.hh" #include "twaalgos/sccinfo.hh" static const char argp_program_doc[] ="\ @@ -148,7 +148,7 @@ namespace process_file(const char* filename) { spot::parse_aut_error_list pel; - auto daut = spot::dstar_parse(filename, pel, spot::make_bdd_dict()); + auto daut = spot::parse_aut(filename, pel, spot::make_bdd_dict()); if (spot::format_parse_aut_errors(std::cerr, filename, pel)) return 2; if (!daut) diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 60e9e243a..cb10aef3a 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -38,7 +38,6 @@ #include "common_trans.hh" #include "common_file.hh" #include "common_finput.hh" -#include "dstarparse/public.hh" #include "parseaut/public.hh" #include "ltlast/unop.hh" #include "ltlvisit/print.hh" @@ -493,8 +492,6 @@ namespace std::ostringstream command; format(command, translators[translator_num].cmd); - assert(output.format != printable_result_filename::None); - std::string cmd = command.str(); std::cerr << "Running [" << l << translator_num << "]: " << cmd << std::endl; @@ -548,73 +545,42 @@ namespace status_str = "ok"; problem = false; es = 0; - switch (output.format) + + spot::parse_aut_error_list pel; + std::string filename = output.val()->name(); + auto aut = spot::parse_aut(filename, pel, dict); + if (!pel.empty()) { - case printable_result_filename::Dstar: - { - spot::parse_aut_error_list pel; - std::string filename = output.val()->name(); - auto aut = spot::dstar_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 DSTAR" - " output.\n"; - spot::format_parse_aut_errors(err, filename, pel); - end_error(); - res = nullptr; - } - else - { - res = aut->aut; - } - break; - } - case printable_result_filename::Hoa: // Will also read neverclaims - { - spot::parse_aut_error_list pel; - std::string filename = output.val()->name(); - auto aut = spot::parse_aut(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 automaton.\n"; - spot::format_parse_aut_errors(err, filename, pel); - end_error(); - res = nullptr; - } - else if (!aut) - { - status_str = "empty output"; - problem = true; - es = -1; - global_error() << "error: empty output.\n"; - end_error(); - res = nullptr; - } - else if (aut->aborted) - { - status_str = "aborted"; - problem = true; - es = -1; - global_error() << "error: aborted HOA file.\n"; - end_error(); - res = nullptr; - } - else - { - res = aut->aut; - } - break; - } - case printable_result_filename::None: - SPOT_UNREACHABLE(); + status_str = "parse error"; + problem = true; + es = -1; + std::ostream& err = global_error(); + err << "error: failed to parse the produced automaton.\n"; + spot::format_parse_aut_errors(err, filename, pel); + end_error(); + res = nullptr; + } + else if (!aut) + { + status_str = "empty output"; + problem = true; + es = -1; + global_error() << "error: empty output.\n"; + end_error(); + res = nullptr; + } + else if (aut->aborted) + { + status_str = "aborted"; + problem = true; + es = -1; + global_error() << "error: aborted HOA file.\n"; + end_error(); + res = nullptr; + } + else + { + res = aut->aut; } } diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index d5d99ca85..3b2615528 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -42,7 +42,6 @@ #include "twaalgos/relabel.hh" #include "twaalgos/totgba.hh" #include "parseaut/public.hh" -#include "dstarparse/public.hh" const char argp_program_doc[] ="\ Run LTL/PSL formulas through another program, performing conversion\n\ @@ -134,8 +133,6 @@ namespace std::ostringstream command; format(command, translators[translator_num].cmd); - //assert(output.format != printable_result_filename::None); - std::string cmd = command.str(); //std::cerr << "Running [" << l << translator_num << "]: " // << cmd << std::endl; @@ -166,69 +163,44 @@ namespace std::cerr << "error: execution of command \"" << cmd << "\" returned exit code " << es << ".\n"; } - else + else if (output.val()) { problem = false; - switch (output.format) + + spot::parse_aut_error_list pel; + std::string filename = output.val()->name(); + auto aut = spot::parse_aut(filename, pel, dict); + if (!pel.empty()) { - case printable_result_filename::Dstar: - { - spot::parse_aut_error_list pel; - std::string filename = output.val()->name(); - auto aut = spot::dstar_parse(filename, pel, dict); - if (!pel.empty()) - { - problem = true; - std::cerr << "error: failed to parse the output of \"" - << cmd << "\" as a DSTAR automaton.\n"; - spot::format_parse_aut_errors(std::cerr, filename, pel); - res = nullptr; - } - else - { - res = aut->aut; - } - break; - } - case printable_result_filename::Hoa: - { - // Will also read neverclaims/LBTT - spot::parse_aut_error_list pel; - std::string filename = output.val()->name(); - auto aut = spot::parse_aut(filename, pel, dict); - if (!pel.empty()) - { - problem = true; - std::cerr << "error: failed to parse the automaton " - "produced by \"" << cmd << "\".\n"; - spot::format_parse_aut_errors(std::cerr, filename, pel); - res = nullptr; - } - else if (!aut) - { - problem = true; - std::cerr << "error: command \"" << cmd - << "\" produced an empty output.\n"; - res = nullptr; - } - else if (aut->aborted) - { - problem = true; - std::cerr << "error: command \"" << cmd - << "\" aborted its output.\n"; - res = nullptr; - } - else - { - res = aut->aut; - } - } - break; - case printable_result_filename::None: - problem = false; + problem = true; + std::cerr << "error: failed to parse the automaton " + "produced by \"" << cmd << "\".\n"; + spot::format_parse_aut_errors(std::cerr, filename, pel); res = nullptr; - break; } + else if (!aut) + { + problem = true; + std::cerr << "error: command \"" << cmd + << "\" produced an empty output.\n"; + res = nullptr; + } + else if (aut->aborted) + { + problem = true; + std::cerr << "error: command \"" << cmd + << "\" aborted its output.\n"; + res = nullptr; + } + else + { + res = aut->aut; + } + } + else // No automaton output + { + problem = false; + res = nullptr; } output.cleanup(); diff --git a/src/dstarparse/.gitignore b/src/dstarparse/.gitignore deleted file mode 100644 index 39850e7cd..000000000 --- a/src/dstarparse/.gitignore +++ /dev/null @@ -1,7 +0,0 @@ -position.hh -dstarparse.cc -dstarparse.output -dstarparse.hh -dstarscan.cc -stack.hh -location.hh diff --git a/src/dstarparse/Makefile.am b/src/dstarparse/Makefile.am deleted file mode 100644 index cf2ab30aa..000000000 --- a/src/dstarparse/Makefile.am +++ /dev/null @@ -1,56 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2013, 2015 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=) - -dstarparsedir = $(pkgincludedir)/dstarparse - -dstarparse_HEADERS = public.hh - -noinst_LTLIBRARIES = libdstarparse.la - -DSTARPARSE_YY = dstarparse.yy -FROM_DSTARPARSE_YY_MAIN = dstarparse.cc -FROM_DSTARPARSE_YY_OTHERS = \ - stack.hh \ - dstarparse.hh - -FROM_DSTARPARSE_YY = $(FROM_DSTARPARSE_YY_MAIN) $(FROM_DSTARPARSE_YY_OTHERS) - -BUILT_SOURCES = $(FROM_DSTARPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_DSTARPARSE_YY) - -$(FROM_DSTARPARSE_YY_MAIN): $(srcdir)/$(DSTARPARSE_YY) -## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(DSTARPARSE_YY), it will also use the value of $(srcdir)/ -## in the generated include statements. - cd $(srcdir) && \ - $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \ - $(DSTARPARSE_YY) -o $(FROM_DSTARPARSE_YY_MAIN) -$(FROM_DSTARPARSE_YY_OTHERS): $(DSTARPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_DSTARPARSE_YY_MAIN) - -EXTRA_DIST = $(DSTARPARSE_YY) - -libdstarparse_la_SOURCES = \ - $(FROM_DSTARPARSE_YY) \ - dstarscan.ll \ - parsedecl.hh diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy deleted file mode 100644 index 73016a4ab..000000000 --- a/src/dstarparse/dstarparse.yy +++ /dev/null @@ -1,392 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2013, 2014, 2015 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 "dstaryy" -%debug -%error-verbose -%lex-param { spot::parse_aut_error_list& error_list } -%define api.location.type "spot::location" - -%code requires -{ -#include -#include -#include "ltlast/constant.hh" -#include "public.hh" - - inline namespace dstaryy_support - { - typedef std::map map_t; - - struct result_ - { - spot::parsed_aut_ptr h; - spot::ltl::environment* env; - std::vector guards; - std::vector::const_iterator cur_guard; - map_t dest_map; - unsigned int cur_state; - int plus; - int minus; - - int states = -1; - unsigned start_state = 0U; - unsigned accpair_count = 0U; - std::vector ap; - std::set ap_set; - - bool accpair_count_seen:1; - bool start_state_seen:1; - bool ignore_more_ap:1; - - result_(): - accpair_count_seen(false), - start_state_seen(false), - ignore_more_ap(false) - { - } - }; - } -} - -%parse-param {spot::parse_aut_error_list& error_list} -%parse-param {result_& res} -%union -{ - std::string* str; - unsigned int num; - spot::acc_cond::mark_t mark; -} - -%code -{ -#include -/* dstarparse.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" - - static void fill_guards(result_& res); -} - -%token DRA "DRA" -%token DSA "DSA" -%token V2 "v2" -%token EXPLICIT "explicit" -%token ACCPAIRS "Acceptance-Pairs:" -%token AP "AP:"; -%token START "Start:"; -%token STATES "States:"; -%token STATE "State:"; -%token ACCSIG "Acc-Sig:"; -%token ENDOFHEADER "---"; -%token EOL "new line"; -%token STRING "string"; -%token NUMBER "number"; - -%type sign -%type dstar_accsigs dstar_state_accsig - -%destructor { delete $$; } -%printer { - if ($$) - debug_stream() << *$$; - else - debug_stream() << "\"\""; } -%printer { debug_stream() << $$; } - -%% -dstar: dstar_header ENDOFHEADER eols dstar_states - { res.h->loc = @$; } - -eols : EOL | eols EOL -opt_eols: | opt_eols EOL - -dstar_type: DRA - { - res.h->type = spot::parsed_aut_type::DRA; - res.plus = 1; - res.minus = 0; - } - | DSA - { - res.h->type = spot::parsed_aut_type::DSA; - res.plus = 0; - res.minus = 1; - } - -dstar_header: dstar_type opt_eols V2 opt_eols EXPLICIT opt_eols dstar_sizes - { - bool err = false; - if (res.states < 0) - { - error(@5, "missing state count"); - err = true; - } - if (!res.accpair_count_seen) - { - error(@5, "missing acceptance-pair count"); - err = true; - } - if (!res.start_state_seen) - { - error(@5, "missing start-state number"); - err = true; - } - if (!res.ignore_more_ap) - { - error(@5, "missing atomic proposition definition"); - err = true; - } - if (err) - { - res.h->aut = nullptr; - YYABORT; - } - res.h->aut->new_states(res.states);; - res.h->aut->set_init_state(res.start_state); - fill_guards(res); - res.cur_guard = res.guards.end(); - } - -aps: - | aps STRING opt_eols - { - if (!res.ignore_more_ap) - { - auto f = res.env->require(*$2); - auto d = res.h->aut->get_dict(); - int b = 0; - if (f == nullptr) - { - std::ostringstream out; - out << "unknown atomic proposition \"" << *$2 << "\""; - error(@1, out.str()); - f = spot::ltl::default_environment::instance() - .require("$unknown$"); - b = d->register_proposition(f, res.h->aut); - } - else - { - b = d->register_proposition(f, res.h->aut); - if (!res.ap_set.emplace(b).second) - { - std::ostringstream out; - out << "duplicate atomic proposition \"" << *$2 << "\""; - error(@1, out.str()); - } - } - f->destroy(); - res.ap.push_back(b); - } - delete $2; - } - -dstar_sizes: - | dstar_sizes error eols - { - error(@2, "unknown header ignored"); - } - | dstar_sizes ACCPAIRS opt_eols NUMBER opt_eols - { - res.accpair_count = $4; - res.accpair_count_seen = true; - res.h->aut->set_acceptance(2 * $4, - res.h->type == spot::parsed_aut_type::DRA - ? spot::acc_cond::acc_code::rabin($4) - : spot::acc_cond::acc_code::streett($4)); - } - | dstar_sizes STATES opt_eols NUMBER opt_eols - { - res.states = $4; - } - | dstar_sizes START opt_eols NUMBER opt_eols - { - res.start_state = $4; - res.start_state_seen = true; - } - | dstar_sizes AP opt_eols NUMBER { res.ap.reserve($4); } opt_eols aps - { - if (!res.ignore_more_ap) - { - int announced = $4; - int given = res.ap.size(); - if (given != announced) - { - std::ostringstream str; - str << announced << " atomic propositions announced but " - << given << " given"; - error(@$, str.str()); - } - if (given > 31) - { - error(@$, - "ltl2star does not support more than 31 " - "atomic propositions"); - } - res.ignore_more_ap = true; - } - else - { - error(@$, "additional declaration of APs"); - } - } - -opt_name: | STRING opt_eols - { - delete $1; - } - -dstar_state_id: STATE opt_eols NUMBER opt_eols opt_name - { - if (res.cur_guard != res.guards.end()) - error(@1, "not enough transitions for previous state"); - if (res.states < 0 || $3 >= (unsigned) res.states) - { - std::ostringstream o; - if (res.states > 0) - { - o << "state numbers should be in the range [0.." - << res.states - 1 << "]"; - } - else - { - o << "no states have been declared"; - } - error(@3, o.str()); - } - res.cur_guard = res.guards.begin(); - res.dest_map.clear(); - res.cur_state = $3; - } - -sign: '+' { $$ = res.plus; } - | '-' { $$ = res.minus; } - -// Membership to a pair is represented as (+NUM,-NUM) -dstar_accsigs: opt_eols - { - $$ = 0U; - } - | dstar_accsigs sign NUMBER opt_eols - { - if (res.states < 0 || res.cur_state >= (unsigned) res.states) - break; - if ($3 < res.accpair_count) - { - $$ = $1; - $$.set($3 * 2 + $2); - } - else - { - std::ostringstream o; - if (res.accpair_count > 0) - { - o << "acceptance pairs should be in the range [0.." - << res.accpair_count - 1 << "]"; - } - else - { - o << "no acceptance pairs have been declared"; - } - error(@3, o.str()); - } - } - -dstar_state_accsig: ACCSIG dstar_accsigs { $$ = $2; } - -dstar_transitions: - | dstar_transitions NUMBER opt_eols - { - std::pair i = - res.dest_map.emplace($2, *res.cur_guard); - if (!i.second) - i.first->second |= *res.cur_guard; - ++res.cur_guard; - } - -dstar_states: - | dstar_states dstar_state_id dstar_state_accsig dstar_transitions - { - for (auto i: res.dest_map) - res.h->aut->new_edge(res.cur_state, i.first, i.second, $3); - } -%% - -static void fill_guards(result_& r) -{ - spot::bdd_dict_ptr d = r.h->aut->get_dict(); - size_t nap = r.ap.size(); - - int* vars = new int[nap]; - for (unsigned i = 0; i < nap; ++i) - vars[i] = r.ap[nap - 1 - i]; - - // build the 2^nap possible guards - r.guards.reserve(1U << nap); - for (size_t i = 0; i < (1U << nap); ++i) - r.guards.push_back(bdd_ibuildcube(i, nap, vars)); - r.cur_guard = r.guards.begin(); - - delete[] vars; -} - -void -dstaryy::parser::error(const location_type& location, - const std::string& message) -{ - error_list.emplace_back(location, message); -} - -namespace spot -{ - parsed_aut_ptr - dstar_parse(const std::string& name, - parse_aut_error_list& error_list, - const bdd_dict_ptr& dict, - ltl::environment& env, - bool debug) - { - if (dstaryyopen(name)) - { - error_list.emplace_back(spot::location(), - std::string("Cannot open file ") + name); - return nullptr; - } - result_ r; - r.h = std::make_shared(); - r.h->aut = make_twa_graph(dict); - r.h->aut->prop_deterministic(true); - r.h->aut->prop_state_based_acc(true); - r.env = &env; - dstaryy::parser parser(error_list, r); - parser.set_debug_level(debug); - parser.parse(); - dstaryyclose(); - return r.h; - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/dstarparse/dstarscan.ll b/src/dstarparse/dstarscan.ll deleted file mode 100644 index d4a4a3063..000000000 --- a/src/dstarparse/dstarscan.ll +++ /dev/null @@ -1,152 +0,0 @@ -/* -*- coding: utf-8 -*- -** Copyright (C) 2013, 2014, 2015 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="dstaryy" -%option outfile="lex.yy.c" -/* %option debug */ - -%{ -#include -#include "dstarparse/parsedecl.hh" - -#define YY_USER_ACTION yylloc->columns(yyleng); -#define YY_NEVER_INTERACTIVE 1 - -typedef dstaryy::parser::token token; -%} - -eol \n+|\r+ -eol2 (\n\r)+|(\r\n)+ -%x in_COMMENT in_STRING - -%% - -%{ - std::string s; - yylloc->step(); -%} - -{eol} yylloc->lines(yyleng); return token::EOL; -{eol2} yylloc->lines(yyleng / 2); return token::EOL; - - /* skip blanks and comments */ -[ \t]+ yylloc->step(); -"/*" BEGIN(in_COMMENT); -"//".* continue; -"Comment:".* yylloc->step(); - -"DRA" return token::DRA; -"DSA" return token::DSA; -"v2" return token::V2; -"explicit" return token::EXPLICIT; - -"Acceptance-Pairs:" return token::ACCPAIRS; -"AP:" return token::AP; -"Start:" return token::START; -"States:" return token::STATES; -"State:" return token::STATE; -"Acc-Sig:" return token::ACCSIG; -"---" return token::ENDOFHEADER; - -[0-9]+ { - errno = 0; - unsigned long n = strtoul(yytext, 0, 10); - yylval->num = n; - if (errno || yylval->num != n) - { - error_list.push_back( - spot::parse_aut_error(*yylloc, - "value too large")); - yylval->num = 0; - } - return token::NUMBER; - } - -"\"" BEGIN(in_STRING); - -{ - [^*\n]* continue; - "*"+[^*/\n]* continue; - "\n"+ yylloc->end.column = 1; yylloc->lines(yyleng); - "*"+"/" BEGIN(INITIAL); - <> { - error_list.push_back( - spot::parse_aut_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::parse_aut_error(*yylloc, - "unclosed string")); - return 0; - } -} - -. return *yytext; - - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - -namespace spot -{ - int - dstaryyopen(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 - dstaryyclose() - { - fclose(yyin); - } -} diff --git a/src/dstarparse/parsedecl.hh b/src/dstarparse/parsedecl.hh deleted file mode 100644 index 3d4e04d6f..000000000 --- a/src/dstarparse/parsedecl.hh +++ /dev/null @@ -1,37 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015 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 . - -#pragma once - -#include -#include "dstarparse.hh" -#include "misc/location.hh" -#include "parseaut/public.hh" - -# define YY_DECL \ - int dstaryylex(dstaryy::parser::semantic_type *yylval, \ - spot::location *yylloc, \ - spot::parse_aut_error_list& error_list) -YY_DECL; - -namespace spot -{ - int dstaryyopen(const std::string& name); - void dstaryyclose(); -} diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh deleted file mode 100644 index 03f93a498..000000000 --- a/src/dstarparse/public.hh +++ /dev/null @@ -1,61 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 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 . - -#pragma once - -#include "twa/twagraph.hh" -#include "misc/location.hh" -#include "ltlenv/defaultenv.hh" -#include "parseaut/public.hh" -#include -#include -#include -#include - -namespace spot -{ - /// \addtogroup twa_io - /// @{ - - /// \brief Build a spot::twa_graph_ptr from ltl2dstar'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 parsed_aut_ptr - dstar_parse(const std::string& filename, - parse_aut_error_list& error_list, - const bdd_dict_ptr& dict, - ltl::environment& env = ltl::default_environment::instance(), - bool debug = false); - - /// @} -} diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index d7b4d61f5..bf817af2b 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -42,6 +42,8 @@ inline namespace hoayy_support { + typedef std::map map_t; + /* 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 @@ -76,6 +78,7 @@ std::vector ap; std::vector guards; std::vector::const_iterator cur_guard; + map_t dest_map; std::vector info_states; // States declared and used. std::vector> start; // Initial states; std::unordered_map alias; @@ -87,6 +90,8 @@ spot::acc_cond::mark_t acc_state; spot::acc_cond::mark_t neg_acc_sets = 0U; spot::acc_cond::mark_t pos_acc_sets = 0U; + int plus; + int minus; std::vector* state_names = nullptr; std::map states_map; std::set ap_set; @@ -179,13 +184,23 @@ %token INT "integer"; %token ENDOFFILE 0 "end of file" +%token DRA "DRA" +%token DSA "DSA" +%token V2 "v2" +%token EXPLICIT "explicit" +%token ACCPAIRS "Acceptance-Pairs:" +%token ACCSIG "Acc-Sig:"; +%token ENDOFHEADER "---"; + + %left '|' %left '&' %nonassoc '!' -%type checked-state-num state-num acc-set +%type checked-state-num state-num acc-set sign %type label-expr %type acc-sig acc-sets trans-acc_opt state-acc_opt + dstar_accsigs dstar_state_accsig %type string_opt /**** NEVERCLAIM tokens ****/ @@ -249,6 +264,7 @@ aut: aut-1 { res.h->loc = @$; YYACCEPT; } aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; } | never { res.h->type = spot::parsed_aut_type::NeverClaim; } | lbtt { res.h->type = spot::parsed_aut_type::LBTT; } + | dstar /* we will set type as DSA or DRA while parsing first line */ /**********************************************************************/ /* Rules for HOA */ @@ -408,6 +424,35 @@ format-version: "HOA:" { res.h->loc = @1; } version res.h->loc = @2; } version +aps: "AP:" INT { + if (res.ignore_more_ap) + { + error(@1, "ignoring this redeclaration of APs..."); + error(res.ap_loc, "... previously declared here."); + } + else + { + res.ap_count = $2; + res.ap.reserve($2); + } + } + ap-names + { + if (!res.ignore_more_ap) + { + 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()); + } + res.ignore_more_ap = true; + } + } + header-items: | header-items header-item header-item: "States:" INT { @@ -436,34 +481,7 @@ header-item: "States:" INT { res.start.emplace_back(@$, $2); } - | "AP:" INT { - if (res.ignore_more_ap) - { - error(@1, "ignoring this redeclaration of APs..."); - error(res.ap_loc, "... previously declared here."); - } - else - { - res.ap_count = $2; - res.ap.reserve($2); - } - } - ap-names - { - if (!res.ignore_more_ap) - { - 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()); - } - res.ignore_more_ap = true; - } - } + | aps | "Alias:" ANAME label-expr { if (!res.alias.emplace(*$2, bdd_from_int($3)).second) @@ -1078,6 +1096,175 @@ incorrectly-labeled-edge: trans-label unlabeled-edge " edge has no label"); } + +/**********************************************************************/ +/* Rules for LTL2DSTAR's format */ +/**********************************************************************/ + +dstar: dstar_header "---" dstar_states + +dstar_type: "DRA" + { + res.h->type = spot::parsed_aut_type::DRA; + res.plus = 1; + res.minus = 0; + } + | "DSA" + { + res.h->type = spot::parsed_aut_type::DSA; + res.plus = 0; + res.minus = 1; + } + +dstar_header: dstar_type "v2" "explicit" dstar_sizes + { + bool err = false; + if (res.states < 0) + { + error(@4, "missing state count"); + err = true; + } + if (!res.ignore_more_acc) + { + error(@4, "missing acceptance-pair count"); + err = true; + } + if (res.start.empty()) + { + error(@4, "missing start-state number"); + err = true; + } + if (!res.ignore_more_ap) + { + error(@4, "missing atomic proposition definition"); + err = true; + } + if (err) + { + res.h->aut = nullptr; + YYABORT; + } + res.h->aut->new_states(res.states);; + res.info_states.resize(res.states); + fill_guards(res); + res.cur_guard = res.guards.end(); + res.h->aut->prop_state_based_acc(); + res.h->aut->prop_deterministic(); + // res.h->aut->prop_complete(); + } + +dstar_sizes: +/* | dstar_sizes error eols + { + error(@2, "unknown header ignored"); + } +*/ + | dstar_sizes "Acceptance-Pairs:" INT + { + if (res.ignore_more_acc) + { + error(@1 + @2, "ignoring this redefinition of the " + "acceptance pairs..."); + error(res.accset_loc, "... previously defined here."); + } + else{ + res.accset = $3; + res.h->aut->set_acceptance(2 * $3, + res.h->type == spot::parsed_aut_type::DRA + ? spot::acc_cond::acc_code::rabin($3) + : spot::acc_cond::acc_code::streett($3)); + res.accset_loc = @3; + res.ignore_more_acc = true; + } + } + | dstar_sizes "States:" INT + { + res.states = $3; + } + | dstar_sizes "Start:" INT + { + res.start.emplace_back(@3, $3); + } + | dstar_sizes aps + +opt_name: | STRING { delete $1; } + +dstar_state_id: "State:" INT opt_name + { + if (res.cur_guard != res.guards.end()) + error(@1, "not enough transitions for previous state"); + if (res.states < 0 || $2 >= (unsigned) res.states) + { + std::ostringstream o; + if (res.states > 0) + { + o << "state numbers should be in the range [0.." + << res.states - 1 << "]"; + } + else + { + o << "no states have been declared"; + } + error(@2, o.str()); + } + res.cur_guard = res.guards.begin(); + res.dest_map.clear(); + res.cur_state = $2; + res.info_states[$2].declared = true; + } + +sign: '+' { $$ = res.plus; } + | '-' { $$ = res.minus; } + +// Membership to a pair is represented as (+NUM,-NUM) +dstar_accsigs: + { + $$ = 0U; + } + | dstar_accsigs sign INT + { + if (res.states < 0 || res.cur_state >= (unsigned) res.states) + break; + if (res.accset > 0 && $3 < (unsigned) res.accset) + { + $$ = $1; + $$.set($3 * 2 + $2); + } + else + { + std::ostringstream o; + if (res.accset > 0) + { + o << "acceptance pairs should be in the range [0.." + << res.accset - 1 << "]"; + } + else + { + o << "no acceptance pairs have been declared"; + } + error(@3, o.str()); + } + } + +dstar_state_accsig: "Acc-Sig:" dstar_accsigs { $$ = $2; } + +dstar_transitions: + | dstar_transitions INT + { + std::pair i = + res.dest_map.emplace($2, *res.cur_guard); + if (!i.second) + i.first->second |= *res.cur_guard; + ++res.cur_guard; + } + +dstar_states: + | dstar_states dstar_state_id dstar_state_accsig dstar_transitions + { + for (auto i: res.dest_map) + res.h->aut->new_edge(res.cur_state, i.first, i.second, $3); + } + /**********************************************************************/ /* Rules for neverclaims */ /**********************************************************************/ diff --git a/src/parseaut/scanaut.ll b/src/parseaut/scanaut.ll index 5d7695d93..324a5bcfe 100644 --- a/src/parseaut/scanaut.ll +++ b/src/parseaut/scanaut.ll @@ -49,6 +49,7 @@ identifier [[:alpha:]_][[:alnum:]_-]* %s in_HOA in_NEVER in_LBTT_HEADER %s in_LBTT_STATE in_LBTT_INIT in_LBTT_TRANS %s in_LBTT_T_ACC in_LBTT_S_ACC in_LBTT_GUARD +%s in_DSTAR %% %{ @@ -82,6 +83,8 @@ identifier [[:alpha:]_][[:alnum:]_-]* "HOA:" BEGIN(in_HOA); return token::HOA; "--ABORT--" BEGIN(INITIAL); throw spot::hoa_abort{*yylloc}; "never" BEGIN(in_NEVER); return token::NEVER; +"DSA" BEGIN(in_DSTAR); return token::DSA; +"DRA" BEGIN(in_DSTAR); return token::DRA; [0-9]+[ \t][0-9]+[ts]? { BEGIN(in_LBTT_HEADER); @@ -134,6 +137,21 @@ identifier [[:alpha:]_][[:alnum:]_-]* [0-9]+ parse_int(); return token::INT; } +{ + "States:" return token::STATES; + "State:" return token::STATE; + "Start:" return token::START; + "AP:" return token::AP; + "v2" return token::V2; + "explicit" return token::EXPLICIT; + "Comment:".* continue; + "//".* continue; + "Acceptance-Pairs:" return token::ACCPAIRS; + "Acc-Sig:" return token::ACCSIG; + "---" return token::ENDOFHEADER; + [0-9]+ parse_int(); return token::INT; +} + { "skip" return token::SKIP; "if" return token::IF; diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 199576abf..c0dbc61ff 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -39,7 +39,6 @@ #include "twaalgos/degen.hh" #include "twa/twaproduct.hh" #include "twaalgos/reducerun.hh" -#include "dstarparse/public.hh" #include "parseaut/public.hh" #include "twaalgos/dupexp.hh" #include "twaalgos/minimize.hh" @@ -118,8 +117,7 @@ syntax(char* prog) << std::endl << " -XD do not compute an automaton, read it from an" << " ltl2dstar file" << std::endl - << " -XDB read the from an ltl2dstar file and convert it to " - << "TGBA" << std::endl + << " -XDB like -XD, and convert it to TGBA\n" << " -XH do not compute an automaton, read it from a" << " HOA file\n" << " -XL do not compute an automaton, read it from an" @@ -341,7 +339,6 @@ checked_main(int argc, char** argv) bool accepting_run = false; bool accepting_run_replay = false; bool from_file = false; - enum { ReadDstar, ReadHoa } readformat = ReadHoa; bool nra2nba = false; bool scc_filter = false; bool simpltl = false; @@ -859,28 +856,23 @@ checked_main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-XD")) { from_file = true; - readformat = ReadDstar; } else if (!strcmp(argv[formula_index], "-XDB")) { from_file = true; - readformat = ReadDstar; nra2nba = true; } else if (!strcmp(argv[formula_index], "-XH")) { from_file = true; - readformat = ReadHoa; } else if (!strcmp(argv[formula_index], "-XL")) { from_file = true; - readformat = ReadHoa; } else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH { from_file = true; - readformat = ReadHoa; } else if (!strcmp(argv[formula_index], "-y")) { @@ -957,45 +949,18 @@ checked_main(int argc, char** argv) if (from_file) { - switch (readformat) - { - case ReadDstar: - { - spot::parse_aut_error_list pel; - tm.start("parsing dstar"); - auto daut = spot::dstar_parse(input, pel, dict, env, debug_opt); - tm.stop("parsing dstar"); - if (spot::format_parse_aut_errors(std::cerr, input, pel)) - return 2; - tm.start("dstar2tgba"); - if (nra2nba) - { - a = spot::to_generalized_buchi(daut->aut); - assume_sba = a->is_sba(); - } - else - { - a = daut->aut; - daut->aut = 0; - assume_sba = false; - } - tm.stop("dstar2tgba"); - } - break; - case ReadHoa: - { - spot::parse_aut_error_list pel; - tm.start("parsing hoa"); - auto daut = spot::parse_aut(input, pel, dict, env, debug_opt); - tm.stop("parsing hoa"); - if (spot::format_parse_aut_errors(std::cerr, input, pel)) - return 2; - daut->aut->merge_edges(); - a = daut->aut; - assume_sba = a->is_sba(); - } - break; - } + spot::parse_aut_error_list pel; + tm.start("parsing hoa"); + auto daut = spot::parse_aut(input, pel, dict, env, debug_opt); + tm.stop("parsing hoa"); + if (spot::format_parse_aut_errors(std::cerr, input, pel)) + return 2; + daut->aut->merge_edges(); + a = daut->aut; + + if (nra2nba) + a = spot::to_generalized_buchi(daut->aut); + assume_sba = a->is_sba(); } else { diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test index 8ee2e819e..754128cf0 100755 --- a/src/tests/parseaut.test +++ b/src/tests/parseaut.test @@ -965,18 +965,17 @@ and even more garbage EOF se='syntax error, unexpected' # this is just to keep lines short -end='end of file or HOA: or never or LBTT header' expecterr input <