diff --git a/README b/README index 0f9f965b4..671c2df9f 100644 --- a/README +++ b/README @@ -157,6 +157,7 @@ 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. eltlparse/ Parser for ELTL formulae. eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. kripke/ Kripke Structure interface. diff --git a/configure.ac b/configure.ac index d054f0fa8..59227c9e6 100644 --- a/configure.ac +++ b/configure.ac @@ -147,6 +147,7 @@ AC_CONFIG_FILES([ lib/Makefile src/bin/Makefile src/bin/man/Makefile + src/dstarparse/Makefile src/eltlparse/Makefile src/eltltest/defs src/eltltest/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 4ba2cf2b8..a7aba7799 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -26,14 +26,15 @@ 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 eltlparse tgba \ - tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \ - neverparse kripkeparse . bin ltltest eltltest tgbatest \ - sabatest sanity kripketest + tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \ + neverparse kripkeparse dstarparse . bin ltltest eltltest \ + tgbatest sabatest kripketest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined libspot_la_LIBADD = \ + dstarparse/libdstarparse.la \ eltlparse/libeltlparse.la \ kripke/libkripke.la \ kripkeparse/libkripkeparse.la \ diff --git a/src/dstarparse/.gitignore b/src/dstarparse/.gitignore new file mode 100644 index 000000000..39850e7cd --- /dev/null +++ b/src/dstarparse/.gitignore @@ -0,0 +1,7 @@ +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 new file mode 100644 index 000000000..4c8c18cf0 --- /dev/null +++ b/src/dstarparse/Makefile.am @@ -0,0 +1,59 @@ +## -*- coding: utf-8 -*- +## Copyright (C) 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=) + +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 \ + $(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 = \ + fmterror.cc \ + nra2nba.cc \ + nsa2tgba.cc \ + $(FROM_DSTARPARSE_YY) \ + dstarscan.ll \ + parsedecl.hh diff --git a/src/dstarparse/dstarparse.yy b/src/dstarparse/dstarparse.yy new file mode 100644 index 000000000..640344399 --- /dev/null +++ b/src/dstarparse/dstarparse.yy @@ -0,0 +1,352 @@ +/* -*- coding: utf-8 -*- +** Copyright (C) 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 . +*/ +%language "C++" +%locations +%defines +%expect 0 // No shift/reduce +%name-prefix "dstaryy" +%debug +%error-verbose +%lex-param { spot::dstar_parse_error_list& error_list } +%define api.location.type "spot::location" + +%code requires +{ +#include +#include +#include "ltlast/constant.hh" +#include "public.hh" + + typedef std::map map_t; + + struct result_ + { + spot::dstar_aut* d; + spot::ltl::environment* env; + std::vector guards; + std::vector::const_iterator cur_guard; + map_t dest_map; + int cur_state; + + unsigned state_count; + std::vector aps; + + bool state_count_seen:1; + bool accpair_count_seen:1; + bool start_state_seen:1; + bool aps_seen:1; + + result_() : + state_count_seen(false), + accpair_count_seen(false), + start_state_seen(false), + aps_seen(false) + { + } + }; +} + +%parse-param {spot::dstar_parse_error_list& error_list} +%parse-param {result_& result} +%union +{ + std::string* str; + unsigned int num; +} + +%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 + +%destructor { delete $$; } +%printer { + if ($$) + debug_stream() << *$$; + else + debug_stream() << "\"\""; } +%printer { debug_stream() << $$; } + +%% +dstar: header ENDOFHEADER eols states + +eols : EOL | eols EOL +opt_eols: | opt_eols EOL + +auttype: DRA { result.d->type = spot::Rabin; } + | DSA { result.d->type = spot::Streett; } + + +header: auttype opt_eols V2 opt_eols EXPLICIT opt_eols sizes + { + bool err = false; + if (!result.state_count_seen) + { + error(@5, "missing state count"); + err = true; + } + if (!result.accpair_count_seen) + { + error(@5, "missing acceptance-pair count"); + err = true; + } + if (!result.start_state_seen) + { + error(@5, "missing start-state number"); + err = true; + } + if (!result.aps_seen) + { + error(@5, "missing atomic proposition definition"); + err = true; + } + if (err) + { + delete result.d->aut; + result.d->aut = 0; + YYABORT; + } + fill_guards(result); + } + +aps: + | aps STRING opt_eols + { + result.aps.push_back(*$2); + delete $2; + } + +sizes: + | sizes error eols + { + error(@2, "unknown header ignored"); + } + | sizes ACCPAIRS opt_eols NUMBER opt_eols + { + result.d->accpair_count = $4; + result.accpair_count_seen = true; + } + | sizes STATES opt_eols NUMBER opt_eols + { + result.state_count = $4; + result.state_count_seen = true; + } + | sizes START opt_eols NUMBER opt_eols + { + result.d->aut->set_init_state($4); + result.start_state_seen = true; + } + | sizes AP opt_eols NUMBER opt_eols aps + { + int announced = $4; + int given = result.aps.size(); + if (given != announced) + { + std::ostringstream str; + str << announced << " atomic propositions announced but " + << given << " given"; + error(@4 + @6, str.str()); + } + if (given > 31) + { + error(@4 + @6, + "ltl2star does not support more than 31 atomic propositions"); + } + result.aps_seen = true; + } + +opt_name: | STRING opt_eols + { + delete $1; + } + +state_id: STATE opt_eols NUMBER opt_eols opt_name + { + if (result.cur_guard != result.guards.end()) + error(@1, "not enough transitions for previous state"); + if ($3 >= result.state_count) + { + std::ostringstream o; + if (result.state_count > 0) + { + o << "state numbers should be in the range [0.." + << result.state_count - 1<< "]"; + } + else + { + o << "no states have been declared"; + } + error(@3, o.str()); + } + result.cur_guard = result.guards.begin(); + result.dest_map.clear(); + result.cur_state = $3; + } + +sign: '+' { $$ = 0; } + | '-' { $$ = 1; } + +// Membership to a pair is represented as (+NUM,-NUM) +accsigs: opt_eols + | accsigs sign NUMBER opt_eols + { + if ((unsigned) result.cur_state >= result.state_count) + break; + assert(result.d->accsets); + if ($3 < result.d->accpair_count) + { + result.d->accsets->at(result.cur_state * 2 + $2).set($3); + } + else + { + std::ostringstream o; + if (result.d->accpair_count > 0) + { + o << "acceptance pairs should be in the range [0.." + << result.d->accpair_count - 1<< "]"; + } + else + { + o << "no acceptance pairs have been declared"; + } + error(@3, o.str()); + } + } + +state_accsig: ACCSIG accsigs + +transitions: + | transitions NUMBER opt_eols + { + std::pair i = + result.dest_map.insert(std::make_pair($2, *result.cur_guard)); + if (!i.second) + i.first->second |= *result.cur_guard; + ++result.cur_guard; + } + +states: + | states state_id state_accsig transitions + { + for (map_t::const_iterator i = result.dest_map.begin(); + i != result.dest_map.end(); ++i) + { + spot::tgba_explicit_number::transition* t = + result.d->aut->create_transition(result.cur_state, i->first); + t->condition = i->second; + } + } +%% + +static void fill_guards(result_& r) +{ + spot::bdd_dict* d = r.d->aut->get_dict(); + + size_t nap = r.aps.size(); + int* vars = new int[nap]; + + // Get a BDD variable for each atomic proposition + for (size_t i = 0; i < nap; ++i) + { + const spot::ltl::formula* f = r.env->require(r.aps[i]); + vars[nap - 1 - i] = d->register_proposition(f, r.d->aut); + f->destroy(); + } + + // 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)); + + delete[] vars; + r.cur_guard = r.guards.end(); + + r.d->accsets = spot::make_bitvect_array(r.d->accpair_count, + 2 * r.state_count); +} + +void +dstaryy::parser::error(const location_type& location, + const std::string& message) +{ + error_list.push_back(spot::dstar_parse_error(location, message)); +} + +namespace spot +{ + dstar_aut* + dstar_parse(const std::string& name, + dstar_parse_error_list& error_list, + bdd_dict* dict, + ltl::environment& env, + bool debug) + { + if (dstaryyopen(name)) + { + error_list.push_back + (dstar_parse_error(spot::location(), + std::string("Cannot open file ") + name)); + return 0; + } + result_ r; + r.d = new dstar_aut; + r.d->aut = new tgba_explicit_number(dict); + r.d->accsets = 0; + r.env = &env; + dstaryy::parser parser(error_list, r); + parser.set_debug_level(debug); + parser.parse(); + dstaryyclose(); + + if (!r.d->aut || !r.d->accsets) + { + delete r.d; + return 0; + } + return r.d; + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/dstarparse/dstarscan.ll b/src/dstarparse/dstarscan.ll new file mode 100644 index 000000000..431da852e --- /dev/null +++ b/src/dstarparse/dstarscan.ll @@ -0,0 +1,149 @@ +/* Copyright (C) 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 . +*/ +%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|\n\r|\r\n +%x in_COMMENT in_STRING + +%% + +%{ + std::string s; + yylloc->step(); +%} + +{eol} yylloc->lines(yyleng); 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::dstar_parse_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::dstar_parse_error(*yylloc, + "unclosed comment")); + return 0; + } +} + +{ + \" { + BEGIN(INITIAL); + yylval->str = new std::string(s); + return token::STRING; + } + \\\" s += '"'; + \\. s += yytext[1]; + [^\\\"]+ s.append(yytext, yyleng); + <> { + error_list.push_back( + spot::dstar_parse_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/fmterror.cc b/src/dstarparse/fmterror.cc new file mode 100644 index 000000000..67c468061 --- /dev/null +++ b/src/dstarparse/fmterror.cc @@ -0,0 +1,41 @@ +// Copyright (C) 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 . + +#include +#include "public.hh" + +namespace spot +{ + bool + format_dstar_parse_errors(std::ostream& os, + const std::string& filename, + dstar_parse_error_list& error_list) + { + bool printed = false; + spot::dstar_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/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc new file mode 100644 index 000000000..cfcec40a7 --- /dev/null +++ b/src/dstarparse/nra2nba.cc @@ -0,0 +1,128 @@ +// Copyright (C) 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 . + +#include "public.hh" +#include "tgbaalgos/reachiter.hh" +#include "tgbaalgos/sccfilter.hh" +#include "ltlast/constant.hh" + +namespace spot +{ + namespace + { + // Christof Löding's Diploma Thesis: Methods for the + // Transformation of ω-Automata: Complexity and Connection to + // Second Order Logic. Section 3.4.3: Rabin to Büchi. + // + // However beware that the {...,(Ei,Fi),...} pairs used by + // are the reversed compared to the {...,(Li,Ui),...} pairs + // used by several other people. We have Ei=Ui and Fi=Li. + class nra_to_nba_worker: public tgba_reachable_iterator_depth_first + { + public: + nra_to_nba_worker(const dstar_aut* a): + tgba_reachable_iterator_depth_first(a->aut), + out_(new tgba_explicit_number(a->aut->get_dict())), + d_(a), + num_states_(a->aut->num_states()) + { + bdd_dict* bd = out_->get_dict(); + bd->register_all_variables_of(a->aut, out_); + + // Invent a new acceptance set for the degeneralized automaton. + int accvar = + bd->register_acceptance_variable(ltl::constant::true_instance(), + out_); + acc_ = bdd_ithvar(accvar); + out_->set_acceptance_conditions(acc_); + } + + tgba_explicit_number* + result() + { + return out_; + } + + void + process_link(const state* sin, int, + const state* sout, int, + const tgba_succ_iterator* si) + { + int in = d_->aut->get_label(sin); + int out = d_->aut->get_label(sout); + + typedef state_explicit_number::transition trans; + trans* t = out_->create_transition(in, out); + bdd cond = t->condition = si->current_condition(); + + // Create one clone of the automaton per accepting pair, + // removing states from the Ui part of the (Li, Ui) pairs. + // (Or the Ei part of Löding's (Ei, Fi) pairs.) + bitvect& l = d_->accsets->at(2 * in); + bitvect& u = d_->accsets->at(2 * in + 1); + for (size_t i = 0; i < d_->accpair_count; ++i) + { + int shift = num_states_ * (i + 1); + // In the Ui set. (Löding's Ei set.) + if (!u.get(i)) + { + // Transition t1 is a non-deterministic jump + // from the original automaton to the i-th clone. + // + // Transition t2 constructs the clone. + // + // Löding creates transition t1 regardless of the + // acceptance set. We restrict it to the non-Li + // states. Both his definition and this + // implementation create more transitions than needed: + // we do not need more than one transition per + // accepting cycle. + trans* t1 = out_->create_transition(in, out + shift); + t1->condition = cond; + + trans* t2 = out_->create_transition(in + shift, out + shift); + t2->condition = cond; + // In the Li set. (Löding's Fi set.) + if (l.get(i)) + t2->acceptance_conditions = acc_; + } + } + } + + protected: + tgba_explicit_number* out_; + const dstar_aut* d_; + size_t num_states_; + bdd acc_; + }; + + } + + SPOT_API + tgba* nra_to_nba(const dstar_aut* nra) + { + assert(nra->type == Rabin); + nra_to_nba_worker w(nra); + w.run(); + tgba_explicit_number* aut = w.result(); + tgba* res = scc_filter_states(aut); + delete aut; + return res; + } + +} diff --git a/src/dstarparse/nsa2tgba.cc b/src/dstarparse/nsa2tgba.cc new file mode 100644 index 000000000..39a53efde --- /dev/null +++ b/src/dstarparse/nsa2tgba.cc @@ -0,0 +1,245 @@ +// Copyright (C) 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 . + +#include +#include +#include "public.hh" +#include "tgbaalgos/sccfilter.hh" +#include "ltlenv/defaultenv.hh" + +namespace spot +{ + // Christof Löding's Diploma Thesis: Methods for the + // Transformation of ω-Automata: Complexity and Connection to + // Second Order Logic. Section 3.4.3, gives a transition + // from Streett with |Q| states to BA with |Q|*(4^n-3^n+2) + // states, if n is the number of acceptance pairs. + // + // Duret-Lutz et al. (ATVA'2009): On-the-fly Emptiness Check of + // Transition-based Streett Automata. Section 3.3 contains a + // conversion from transition-based Streett Automata to TGBA using + // the generalized Büchi acceptance to limit the explosion. It goes + // from Streett with |Q| states to (T)GBA with |Q|*(2^n+1) states. + // However the definition of the number of acceptance sets in that + // paper is suboptimal: only n are needed, not 2^n. + // + // This implements this second version. + + namespace + { + // A state in the resulting automaton corresponds is either a + // state of the original automaton (in which case bv == 0) or a + // state of the original automaton associated to a set of pending + // acceptance represented by a bitvect. + + struct build_state + { + int s; + const bitvect* pend; + + build_state(int st, const bitvect* bv = 0): + s(st), + pend(bv) + { + } + }; + + typedef std::pair degen_state; + + struct build_state_hash + { + size_t + operator()(const build_state& s) const + { + if (!s.pend) + return s.s; + else + return s.s ^ s.pend->hash(); + } + }; + + struct build_state_equal + { + bool + operator()(const build_state& left, + const build_state& right) const + { + if (left.s != right.s) + return false; + if (left.pend == right.pend) + return true; + if (!right.pend || !left.pend) + return false; + return *left.pend == *right.pend; + } + }; + + // Associate the build state to its number. + typedef Sgi::hash_map bs2num_map; + + // Queue of state to be processed. + typedef std::deque queue_t; + + } + + int label(const tgba_explicit_number* aut, state* s) + { + int label = aut->get_label(s); + s->destroy(); + return label; + } + + SPOT_API + tgba* nsa_to_tgba(const dstar_aut* nsa) + { + assert(nsa->type == Streett); + tgba_explicit_number* a = nsa->aut; + bdd_dict* dict = a->get_dict(); + + tgba_explicit_number* res = new tgba_explicit_number(dict); + dict->register_all_variables_of(a, res); + + // Create accpair_count acceptance sets for tge TGBA. + size_t npairs = nsa->accpair_count; + std::vector acc_b(npairs); + { + ltl::environment& envacc = ltl::default_environment::instance(); + std::vector acc_f(npairs); + for (unsigned n = 0; n < npairs; ++n) + { + std::ostringstream s; + s << n; + const ltl::formula* af = acc_f[n] = envacc.require(s.str()); + res->declare_acceptance_condition(af->clone()); + } + bdd allacc = bddfalse; + for (unsigned n = 0; n < npairs; ++n) + { + const ltl::formula* af = acc_f[n]; + allacc |= acc_b[n] = res->get_acceptance_condition(af); + } + } + + // These maps make it possible to convert build_state to number + // and vice-versa. + bs2num_map bs2num; + + queue_t todo; + + build_state s(label(a, a->get_init_state())); + + bs2num[s] = 0; + todo.push_back(s); + + while (!todo.empty()) + { + s = todo.front(); + todo.pop_front(); + int src = bs2num[s]; + + tgba_succ_iterator* i = a->succ_iter(a->get_state(s.s)); + for (i->first(); !i->done(); i->next()) + { + int dlabel = label(a, i->current_state()); + + bitvect* pend = 0; + bdd acc = bddfalse; + if (s.pend) + { + pend = s.pend->clone(); + *pend |= nsa->accsets->at(2 * dlabel); // L + *pend -= nsa->accsets->at(2 * dlabel + 1); // U + + for (size_t i = 0; i < npairs; ++i) + if (!pend->get(i)) + acc |= acc_b[i]; + } + + + build_state d(dlabel, pend); + // Have we already seen this destination? + int dest; + std::pair dres = + bs2num.insert(bs2num_map::value_type(d, 0)); + if (!dres.second) + { + dest = dres.first->second; + delete d.pend; + } + else + { + dest = dres.first->second = bs2num.size() - 1; + todo.push_back(d); + } + state_explicit_number::transition* t = + res->create_transition(src, dest); + t->condition = i->current_condition(); + t->acceptance_conditions = acc; + + // Jump to level ∅ + if (s.pend == 0) + { + bitvect* pend = make_bitvect(npairs); + build_state d(label(a, i->current_state()), pend); + // Have we already seen this destination? + int dest; + std::pair dres = + bs2num.insert(bs2num_map::value_type(d, 0)); + if (!dres.second) + { + dest = dres.first->second; + delete d.pend; + } + else + { + dest = dres.first->second = bs2num.size() - 1; + todo.push_back(d); + } + state_explicit_number::transition* t = + res->create_transition(src, dest); + t->condition = i->current_condition(); + } + } + delete i; + } + + + // { + // bs2num_map::iterator i = bs2num.begin(); + // while (i != bs2num.end()) + // { + // std::cerr << i->second << ": (" << i->first.s << ","; + // if (i->first.pend) + // std::cerr << *i->first.pend << ")\n"; + // else + // std::cerr << "-)\n"; + // ++i; + // } + // } + + // Cleanup the bs2num map. + bs2num_map::iterator i = bs2num.begin(); + while (i != bs2num.end()) + delete (i++)->first.pend; + + return res; + } + +} + diff --git a/src/dstarparse/parsedecl.hh b/src/dstarparse/parsedecl.hh new file mode 100644 index 000000000..d69170eb8 --- /dev/null +++ b/src/dstarparse/parsedecl.hh @@ -0,0 +1,39 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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_DSTARPARSE_PARSEDECL_HH +# define SPOT_DSTARPARSE_PARSEDECL_HH + +#include +#include "dstarparse.hh" +#include "misc/location.hh" + +# define YY_DECL \ + int dstaryylex(dstaryy::parser::semantic_type *yylval, \ + spot::location *yylloc, \ + spot::dstar_parse_error_list& error_list) +YY_DECL; + +namespace spot +{ + int dstaryyopen(const std::string& name); + void dstaryyclose(); +} + +#endif // SPOT_DSTARPARSE_PARSEDECL_HH diff --git a/src/dstarparse/public.hh b/src/dstarparse/public.hh new file mode 100644 index 000000000..634d15e65 --- /dev/null +++ b/src/dstarparse/public.hh @@ -0,0 +1,120 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 . + +#ifndef SPOT_DSTARPARSE_PUBLIC_HH +# define SPOT_DSTARPARSE_PUBLIC_HH + +# include "tgba/tgbaexplicit.hh" +# include "misc/location.hh" +# include "ltlenv/defaultenv.hh" +# include +# include +# include +# include +# include + +namespace spot +{ + /// \addtogroup tgba_io + /// @{ + + /// \brief A parse diagnostic with its location. + typedef std::pair dstar_parse_error; + /// \brief A list of parser diagnostics, as filled by parse. + typedef std::list dstar_parse_error_list; + + enum dstar_type { Rabin, Streett }; + + /// \brief Temporary encoding of an omega automaton produced by + /// ltl2dstar. + struct SPOT_API dstar_aut + { + // Transition structure of the automaton. + // This is encoded as a TGBA without acceptance condition. + tgba_explicit_number* aut; + /// Type of the acceptance. + dstar_type type; + /// Number of acceptance pairs. + size_t accpair_count; + /// \brief acceptance sets encoded as 2*num_state bit-vectors of + /// num_pairs bits + /// + /// Assuming $F=\{(L_0,U_0),\ldots,(L_i,U_i),\ldots\}$, + /// $s\in L_i$ iff accsets->at(s * 2).get(i)$, + /// an $s\in $U_i$ iff accsets->at(s * 2 + 1).get(i). + bitvect_array* accsets; + + ~dstar_aut() + { + delete aut; + delete accsets; + } + }; + + + /// \brief Build a spot::tgba_explicit 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 dstar_aut* + dstar_parse(const std::string& filename, + dstar_parse_error_list& error_list, + bdd_dict* dict, + ltl::environment& env = ltl::default_environment::instance(), + bool debug = false); + + /// \brief Format diagnostics produced by spot::dstar_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_dstar_parse_errors(std::ostream& os, + const std::string& filename, + dstar_parse_error_list& error_list); + + + /// \brief Convert a non-deterministic Rabin automaton into a + /// non-deterministic Büchi automaton. + SPOT_API + tgba* nra_to_nba(const dstar_aut* nra); + + /// \brief Convert a non-deterministic Streett automaton into a + /// non-deterministic tgba. + SPOT_API + tgba* nsa_to_tgba(const dstar_aut* nra); + + /// @} +} + +#endif // SPOT_DSTARPARSE_PUBLIC_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index b6ab29824..1f87f14e1 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -80,6 +80,7 @@ TESTS = \ renault.test \ nondet.test \ neverclaimread.test \ + dstar.test \ readsave.test \ simdet.test \ sim.test \ diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test new file mode 100755 index 000000000..0d6c1863b --- /dev/null +++ b/src/tgbatest/dstar.test @@ -0,0 +1,131 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 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 . + +# Do some quick translations to make sure the neverclaims produced by +# spot actually look correct! We do that by parsing them via ltlcross. +# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed. + +. ./defs +set -e + +cat >dra.dstar <expected < 1 + 1 [label="0"] + 1 -> 1 [label="a & !b\n"] + 1 -> 2 [label="!a & !b\n"] + 1 -> 3 [label="b\n"] + 2 [label="1"] + 2 -> 2 [label="1\n"] + 3 [label="2"] + 3 -> 3 [label="1\n"] +} +EOF + +diff expected stdout + +cat >dsa.dstar <expected < 1 + 1 [label="0"] + 1 -> 2 [label="1\n"] + 1 -> 3 [label="1\n"] + 2 [label="1"] + 2 -> 2 [label="!a\n"] + 2 -> 3 [label="!a\n"] + 2 -> 4 [label="a\n"] + 2 -> 5 [label="a\n"] + 3 [label="2"] + 3 -> 6 [label="!a\n"] + 3 -> 5 [label="a\n{Acc[\"0\"]}"] + 4 [label="3"] + 4 -> 2 [label="!a\n"] + 4 -> 3 [label="!a\n"] + 4 -> 4 [label="a\n"] + 4 -> 5 [label="a\n"] + 5 [label="4"] + 5 -> 6 [label="!a\n"] + 5 -> 5 [label="a\n{Acc[\"0\"]}"] + 6 [label="5"] + 6 -> 6 [label="!a\n"] + 6 -> 7 [label="a\n"] + 7 [label="6"] + 7 -> 6 [label="!a\n"] + 7 -> 7 [label="a\n"] +} +EOF + +diff expected stdout diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 9e8ba524e..e450f5b6b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -45,6 +45,7 @@ #include "tgbaalgos/reducerun.hh" #include "tgbaparse/public.hh" #include "neverparse/public.hh" +#include "dstarparse/public.hh" #include "tgbaalgos/dupexp.hh" #include "tgbaalgos/minimize.hh" #include "taalgos/minimize.hh" @@ -119,6 +120,10 @@ syntax(char* prog) << std::endl << " -X do not compute an automaton, read it from a file" << 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 << " -XL do not compute an automaton, read it from an" << " LBTT file" << std::endl << " -XN do not compute an automaton, read it from a" @@ -361,8 +366,8 @@ main(int argc, char** argv) bool accepting_run = false; bool accepting_run_replay = false; bool from_file = false; - bool read_neverclaim = false; - bool read_lbtt = false; + enum { ReadSpot, ReadLbtt, ReadNeverclaim, ReadDstar } readformat = ReadSpot; + bool nra2nba = false; bool scc_filter = false; bool simpltl = false; spot::ltl::ltl_simplifier_options redopt(false, false, false, false, @@ -899,16 +904,28 @@ main(int argc, char** argv) else if (!strcmp(argv[formula_index], "-X")) { from_file = true; + readformat = ReadSpot; } - else if (!strcmp(argv[formula_index], "-XN")) + else if (!strcmp(argv[formula_index], "-XD")) { from_file = true; - read_neverclaim = true; + readformat = ReadDstar; + } + else if (!strcmp(argv[formula_index], "-XDB")) + { + from_file = true; + readformat = ReadDstar; + nra2nba = true; } else if (!strcmp(argv[formula_index], "-XL")) { from_file = true; - read_lbtt = true; + readformat = ReadLbtt; + } + else if (!strcmp(argv[formula_index], "-XN")) + { + from_file = true; + readformat = ReadNeverclaim; } else if (!strcmp(argv[formula_index], "-y")) { @@ -1018,59 +1035,102 @@ main(int argc, char** argv) if (from_file) { spot::tgba_explicit_string* e = 0; - if (!read_neverclaim && !read_lbtt) + switch (readformat) { - spot::tgba_parse_error_list pel; - tm.start("parsing automaton"); - to_free = a = e = spot::tgba_parse(input, pel, dict, - env, env, debug_opt); - tm.stop("parsing automaton"); - if (spot::format_tgba_parse_errors(std::cerr, input, pel)) + case ReadSpot: { - delete to_free; - delete dict; - return 2; - } - } - else if (read_neverclaim) - { - spot::neverclaim_parse_error_list pel; - tm.start("parsing neverclaim"); - to_free = 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)) - { - delete to_free; - delete dict; - return 2; - } - assume_sba = true; - } - else - { - std::string error; - std::fstream f(input.c_str()); - if (!f) - { - std::cerr << "cannot open " << input << std::endl; - delete dict; - return 2; - } - tm.start("parsing lbtt"); - to_free = a = - const_cast(spot::lbtt_parse(f, error, dict, - env, env)); - tm.stop("parsing lbtt"); - if (!to_free) - { - std::cerr << error << std::endl; - delete dict; - return 2; + spot::tgba_parse_error_list pel; + tm.start("parsing automaton"); + to_free = a = e = spot::tgba_parse(input, pel, dict, + env, env, debug_opt); + tm.stop("parsing automaton"); + if (spot::format_tgba_parse_errors(std::cerr, input, pel)) + { + delete to_free; + delete dict; + return 2; + } } + break; + case ReadNeverclaim: + { + spot::neverclaim_parse_error_list pel; + tm.start("parsing neverclaim"); + to_free = 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)) + { + delete to_free; + delete dict; + return 2; + } + assume_sba = true; + } + break; + case ReadLbtt: + { + std::string error; + std::fstream f(input.c_str()); + if (!f) + { + std::cerr << "cannot open " << input << std::endl; + delete dict; + return 2; + } + tm.start("parsing lbtt"); + to_free = a = + const_cast(spot::lbtt_parse(f, error, dict, + env, env)); + tm.stop("parsing lbtt"); + if (!to_free) + { + std::cerr << error << std::endl; + delete dict; + return 2; + } + } + break; + case ReadDstar: + { + spot::dstar_parse_error_list pel; + tm.start("parsing dstar"); + spot::dstar_aut* daut; + daut = spot::dstar_parse(input, pel, dict, + env, debug_opt); + if (nra2nba) + { + if (daut->type == spot::Rabin) + { + to_free = a = spot::nra_to_nba(daut); + assume_sba = true; + } + else + { + to_free = a = spot::nsa_to_tgba(daut); + assume_sba = false; + } + } + else + { + to_free = a = daut->aut; + daut->aut = 0; + assume_sba = false; + } + delete daut; + tm.stop("parsing dstar"); + if (spot::format_dstar_parse_errors(std::cerr, input, pel)) + { + delete to_free; + delete dict; + return 2; + } + } + break; } if (e) e->merge_transitions(); + } else {