diff --git a/NEWS b/NEWS index 1b279245e..cb241cbff 100644 --- a/NEWS +++ b/NEWS @@ -70,6 +70,14 @@ New in spot 1.99.5a (not yet released) to syntethise larged automata with different acceptance conditions. + * Explicit Kripke structure (i.e., stored as explciti graphs) have + been rewritten above the graph class, using an interface similar + to the twa class. The new class is called kripke_graph. The + custom Kripke parser and printer have been removed, because we can + now use print_hoa() with the "k" option to print Kripke structure + in the HOA format, and furthermore the parse_aut() function now + has an option to read HOA file and produce them as kripke_graph. + * Renamings: is_guarantee_automaton() -> is_terminal_automaton() tgba_run -> twa_run diff --git a/README b/README index 2832c0f51..00e04aed5 100644 --- a/README +++ b/README @@ -139,7 +139,6 @@ src/ Sources for libspot. man/ Man pages for the above tools. graph/ Graph representations. kripke/ Kripke Structure interface. - kripkeparse/ Parser for explicit Kripke. tl/ Temporal Logic formulas and algorithms. misc/ Miscellaneous support files. parseaut/ Parser for automata in multiple formats. @@ -147,7 +146,7 @@ src/ Sources for libspot. priv/ Private algorithms, used internally but not exported. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. - tests/ Tests for the whole library. + tests/ Tests for the whole library. twa/ TωA objects and cousins (Transition-based ω-Automata). twaalgos/ Algorithms on TωA. gtec/ Couvreur's Emptiness-Check. diff --git a/configure.ac b/configure.ac index 73ba3811c..2c28f8851 100644 --- a/configure.ac +++ b/configure.ac @@ -206,7 +206,6 @@ AC_CONFIG_FILES([ src/bin/man/Makefile src/graph/Makefile src/kripke/Makefile - src/kripkeparse/Makefile src/Makefile src/misc/Makefile src/parseaut/Makefile diff --git a/iface/ltsmin/modelcheck.cc b/iface/ltsmin/modelcheck.cc index 3c003912f..382894785 100644 --- a/iface/ltsmin/modelcheck.cc +++ b/iface/ltsmin/modelcheck.cc @@ -28,8 +28,8 @@ #include "misc/timer.hh" #include "misc/memusage.hh" #include -#include "kripke/kripkeexplicit.hh" -#include "kripke/kripkeprint.hh" +#include "kripke/kripkegraph.hh" +#include "twaalgos/hoa.hh" static void syntax(char* prog) @@ -236,7 +236,7 @@ checked_main(int argc, char **argv) if (output == Kripke) { tm.start("kripke output"); - spot::kripke_save_reachable_renumbered(std::cout, model); + spot::print_hoa(std::cout, model, "k"); tm.stop("kripke output"); goto safe_exit; } diff --git a/src/Makefile.am b/src/Makefile.am index 0e1fe606e..863e7a512 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 tl graph twa twaalgos ta taalgos kripke \ - kripkeparse parseaut parsetl . bin tests sanity + parseaut parsetl . bin tests sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined $(SYMBOLIC_LDFLAGS) libspot_la_LIBADD = \ kripke/libkripke.la \ - kripkeparse/libkripkeparse.la \ misc/libmisc.la \ parseaut/libparseaut.la \ parsetl/libparsetl.la \ diff --git a/src/kripke/Makefile.am b/src/kripke/Makefile.am index b26448f12..6945dd8af 100644 --- a/src/kripke/Makefile.am +++ b/src/kripke/Makefile.am @@ -26,12 +26,9 @@ kripke_HEADERS = \ fairkripke.hh \ fwd.hh \ kripke.hh \ - kripkeexplicit.hh \ - kripkeprint.hh + kripkegraph.hh noinst_LTLIBRARIES = libkripke.la libkripke_la_SOURCES = \ fairkripke.cc \ - kripke.cc \ - kripkeexplicit.cc \ - kripkeprint.cc + kripke.cc diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc deleted file mode 100644 index 7b726b464..000000000 --- a/src/kripke/kripkeexplicit.cc +++ /dev/null @@ -1,269 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Developpement 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 "kripkeexplicit.hh" -#include "twa/bddprint.hh" -#include "twa/formula2bdd.hh" -#include - -namespace spot -{ - - state_kripke::state_kripke() - : bdd_ (bddtrue) - { - } - - void state_kripke::add_conditions(bdd f) - { - bdd_ &= f; - } - - void state_kripke::add_succ(state_kripke* add_me) - { - // This method must add only state_kripke for now. - state_kripke* to_add = down_cast(add_me); - assert(to_add); - succ_.push_back(to_add); - } - - int state_kripke::compare(const state* other) const - { - // This method should not be called to compare states from different - // automata, and all states from the same automaton will use the same - // state class. - const state_kripke* s = down_cast(other); - assert(s); - return s - this; - } - - size_t - state_kripke::hash() const - { - return - reinterpret_cast(this) - static_cast(nullptr); - } - - state_kripke* - state_kripke::clone() const - { - return const_cast(this); - } - - //////////////////////////// - // Support for succ_iterator - - const std::list& - state_kripke::get_succ() const - { - return succ_; - } - - - - - - - - - - ///////////////////////////////////// - // kripke_explicit_succ_iterator - - kripke_explicit_succ_iterator::kripke_explicit_succ_iterator - (const state_kripke* s, bdd cond) - : kripke_succ_iterator(cond), - s_(s) - { - } - - - kripke_explicit_succ_iterator::~kripke_explicit_succ_iterator() - { - } - - bool kripke_explicit_succ_iterator::first() - { - it_ = s_->get_succ().begin(); - return it_ != s_->get_succ().end(); - } - - bool kripke_explicit_succ_iterator::next() - { - ++it_; - return it_ != s_->get_succ().end(); - } - - bool kripke_explicit_succ_iterator::done() const - { - return it_ == s_->get_succ().end(); - } - - state_kripke* kripke_explicit_succ_iterator::dst() const - { - assert(!done()); - return *it_; - } - - ///////////////////////////////////// - // kripke_explicit - - - kripke_explicit::kripke_explicit(const bdd_dict_ptr& dict, - state_kripke* init) - : kripke(dict), - init_(init) - { - } - - - std::string - kripke_explicit::format_state(const spot::state* s) const - { - assert(s); - const state_kripke* se = down_cast(s); - assert(se); - std::map::const_iterator it = - sn_nodes_.find (se); - assert(it != sn_nodes_.end()); - return it->second; - } - - kripke_explicit::~kripke_explicit() - { - get_dict()->unregister_all_my_variables(this); - std::map::iterator it; - for (it = ns_nodes_.begin(); it != ns_nodes_.end(); ++it) - { - state_kripke* del_me = it->second; - delete del_me; - } - } - - state_kripke* - kripke_explicit::get_init_state() const - { - return init_; - } - - // FIXME: Change the bddtrue. - kripke_explicit_succ_iterator* - kripke_explicit::succ_iter(const spot::state* st) const - { - const state_kripke* s = down_cast(st); - assert(s); - state_kripke* it = const_cast(s); - return new kripke_explicit_succ_iterator(it, bddtrue); - } - - bdd - kripke_explicit::state_condition(const state* s) const - { - const state_kripke* f = down_cast(s); - assert(f); - return (f->as_bdd()); - } - - bdd - kripke_explicit::state_condition(const std::string& name) const - { - std::map::const_iterator it; - it = ns_nodes_.find(name); - assert(it != ns_nodes_.end()); - return state_condition(it->second); - } - - const std::map& - kripke_explicit::sn_get() const - { - return sn_nodes_; - } - - - void kripke_explicit::add_state(std::string name, - state_kripke* state) - { - if (ns_nodes_.find(name) == ns_nodes_.end()) - { - ns_nodes_[name] = state; - sn_nodes_[state] = name; - if (!init_) - init_ = state; - } - } - - void kripke_explicit::add_state(std::string name) - { - if (ns_nodes_.find(name) == ns_nodes_.end()) - { - state_kripke* state = new state_kripke; - add_state(name, state); - } - } - - void kripke_explicit::add_transition(state_kripke* source, - const state_kripke* dest) - { - state_kripke* Dest = const_cast(dest); - source->add_succ(Dest); - } - - void kripke_explicit::add_transition(std::string source, - const state_kripke* dest) - { - add_transition(ns_nodes_[source], dest); - } - - void kripke_explicit::add_transition(std::string source, - std::string dest) - { - auto destination = ns_nodes_.find(dest); - if (destination == ns_nodes_.end()) - { - state_kripke* neo = new state_kripke; - add_state(dest, neo); - add_transition(source, neo); - } - else - { - add_transition(source, destination->second); - } - } - - void kripke_explicit::add_conditions(bdd add, - state_kripke* on_me) - { - on_me->add_conditions(add); - } - - void kripke_explicit::add_conditions(bdd add, - std::string on_me) - { - add_conditions(add, ns_nodes_[on_me]); - } - - - void kripke_explicit::add_condition(formula f, std::string on_me) - { - add_conditions(formula_to_bdd(f, get_dict(), this), on_me); - } - - -} // End namespace spot. diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh deleted file mode 100644 index 220dee06c..000000000 --- a/src/kripke/kripkeexplicit.hh +++ /dev/null @@ -1,184 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 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 -#include "kripke.hh" -#include "tl/formula.hh" -#include "kripkeprint.hh" - -namespace spot -{ - /// \brief Concrete class for kripke states. - class SPOT_API state_kripke : public state - { - friend class kripke_explicit; - friend class kripke_explicit_succ_iterator; - private: - state_kripke(); - - /// \brief Compare two states. - /// - /// This method returns an integer less than, equal to, or greater - /// than zero if \a this is found, respectively, to be less than, equal - /// to, or greater than \a other according to some implicit total order. - /// - /// For moment, this method only compare the adress on the heap of the - /// twice pointers. - virtual int compare (const state* other) const; - - /// \brief Hash a state - virtual size_t hash() const; - - /// \brief Duplicate a state. - virtual state_kripke* clone() const; - - /// \brief Add a condition to the conditions already in the state. - /// \param f The condition to add. - void add_conditions(bdd f); - - /// \brief Add a new successor in the list. - /// \param succ The successor state to add. - void add_succ(state_kripke* succ); - - virtual bdd - as_bdd() const - { - return bdd_; - } - - /// \brief Release a state. - /// - virtual void - destroy() const - { - } - - virtual - ~state_kripke () - { - } - - //////////////////////////////// - // Management for succ_iterator - - const std::list& get_succ() const; - - bdd bdd_; - std::list succ_; - }; - - - /// \class kripke_explicit_succ_iterator - /// \brief Implement iterator pattern on successor of a state_kripke. - class SPOT_API kripke_explicit_succ_iterator : public kripke_succ_iterator - { - public: - kripke_explicit_succ_iterator(const state_kripke*, bdd); - - ~kripke_explicit_succ_iterator(); - - virtual bool first(); - virtual bool next(); - virtual bool done() const; - - virtual state_kripke* dst() const; - - private: - const state_kripke* s_; - std::list::const_iterator it_; - }; - - - /// \class kripke_explicit - /// \brief Kripke Structure. - class SPOT_API kripke_explicit : public kripke - { - public: - kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr); - ~kripke_explicit(); - - state_kripke* get_init_state() const; - - /// \brief Allow to get an iterator on the state we passed in - /// parameter. - kripke_explicit_succ_iterator* - succ_iter(const spot::state* state) const; - - /// \brief Get the condition on the state - bdd state_condition(const state* s) const; - /// \brief Get the condition on the state - bdd state_condition(const std::string&) const; - - /// \brief Return the name of the state. - std::string format_state(const state*) const; - - - /// \brief Create state, if it does not already exists. - /// - /// Used by the parser. - void add_state(std::string); - - /// \brief Add a transition between two states. - void add_transition(std::string source, - std::string dest); - - /// \brief Add a BDD condition to the state - /// - /// \param add the condition. - /// \param on_me where add the condition. - void add_conditions(bdd add, - std::string on_me); - - /// \brief Add a formula to the state corresponding to the name. - /// - /// \param f the formula to add. - /// \param on_me the state where to add. - void add_condition(formula f, std::string on_me); - - /// \brief Return map between states and their names. - const std::map& - sn_get() const; - - private: - /// \brief Add a state in the two maps. - void add_state(std::string, state_kripke*); - - void add_conditions(bdd add, - state_kripke* on_me); - - void add_transition(std::string source, - const state_kripke* dest); - - void add_transition(state_kripke* source, - const state_kripke* dest); - - state_kripke* init_; - std::map ns_nodes_; - std::map sn_nodes_; - }; - - inline kripke_explicit_ptr - make_kripke_explicit(const bdd_dict_ptr& d, - state_kripke* init = nullptr) - { - return std::make_shared(d, init); - } -} diff --git a/src/kripke/kripkegraph.hh b/src/kripke/kripkegraph.hh new file mode 100644 index 000000000..d145848fd --- /dev/null +++ b/src/kripke/kripkegraph.hh @@ -0,0 +1,283 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012, 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 +#include "kripke.hh" +#include "graph/graph.hh" +#include "tl/formula.hh" + +namespace spot +{ + /// \brief Concrete class for kripke_graph states. + struct SPOT_API kripke_graph_state: public spot::state + { + public: + kripke_graph_state(bdd cond = bddfalse) noexcept + : cond_(cond) + { + } + + virtual ~kripke_graph_state() noexcept + { + } + + virtual int compare(const spot::state* other) const + { + auto o = down_cast(other); + assert(o); + + // Do not simply return "other - this", it might not fit in an int. + if (o < this) + return -1; + if (o > this) + return 1; + return 0; + } + + virtual size_t hash() const + { + return + reinterpret_cast(this) - static_cast(nullptr); + } + + virtual kripke_graph_state* + clone() const + { + return const_cast(this); + } + + virtual void destroy() const + { + } + + bdd cond() const + { + return cond_; + } + + void cond(bdd c) + { + cond_ = c; + } + + private: + bdd cond_; + }; + + template + class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator + { + private: + typedef typename Graph::edge edge; + typedef typename Graph::state_data_t state; + const Graph* g_; + edge t_; + edge p_; + public: + kripke_graph_succ_iterator(const Graph* g, + const typename Graph::state_storage_t* s): + kripke_succ_iterator(s->cond()), + g_(g), + t_(s->succ) + { + } + + ~kripke_graph_succ_iterator() + { + } + + virtual void recycle(const typename Graph::state_storage_t* s) + { + cond_ = s->cond(); + t_ = s->succ; + } + + virtual bool first() + { + p_ = t_; + return p_; + } + + virtual bool next() + { + p_ = g_->edge_storage(p_).next_succ; + return p_; + } + + virtual bool done() const + { + return !p_; + } + + virtual kripke_graph_state* dst() const + { + assert(!done()); + return const_cast + (&g_->state_data(g_->edge_storage(p_).dst)); + } + }; + + + /// \class kripke_graph + /// \brief Kripke Structure. + class SPOT_API kripke_graph : public kripke + { + public: + typedef digraph graph_t; + typedef graph_t::edge_storage_t edge_storage_t; + protected: + graph_t g_; + mutable unsigned init_number_; + public: + kripke_graph(const bdd_dict_ptr& d) + : kripke(d), init_number_(0) + { + } + + virtual ~kripke_graph() + { + get_dict()->unregister_all_my_variables(this); + } + + unsigned num_states() const + { + return g_.num_states(); + } + + unsigned num_edges() const + { + return g_.num_edges(); + } + + void set_init_state(graph_t::state s) + { + assert(s < num_states()); + init_number_ = s; + } + + graph_t::state get_init_state_number() const + { + if (num_states() == 0) + const_cast(g_).new_state(); + return init_number_; + } + + // FIXME: The return type ought to be const. + virtual kripke_graph_state* get_init_state() const + { + if (num_states() == 0) + const_cast(g_).new_state(); + return const_cast(state_from_number(init_number_)); + } + + /// \brief Allow to get an iterator on the state we passed in + /// parameter. + virtual kripke_graph_succ_iterator* + succ_iter(const spot::state* st) const + { + auto s = down_cast(st); + assert(s); + assert(!s->succ || g_.valid_trans(s->succ)); + + if (this->iter_cache_) + { + auto it = + down_cast*>(this->iter_cache_); + it->recycle(s); + this->iter_cache_ = nullptr; + return it; + } + return new kripke_graph_succ_iterator(&g_, s); + + } + + graph_t::state + state_number(const state* st) const + { + auto s = down_cast(st); + assert(s); + return s - &g_.state_storage(0); + } + + const kripke_graph_state* + state_from_number(graph_t::state n) const + { + return &g_.state_data(n); + } + + kripke_graph_state* + state_from_number(graph_t::state n) + { + return &g_.state_data(n); + } + + std::string format_state(unsigned n) const + { + std::stringstream ss; + ss << n; + return ss.str(); + } + + virtual std::string format_state(const state* st) const + { + return format_state(state_number(st)); + } + + /// \brief Get the condition on the state + virtual bdd state_condition(const state* s) const + { + return down_cast(s)->cond(); + } + + edge_storage_t& edge_storage(unsigned t) + { + return g_.edge_storage(t); + } + + const edge_storage_t edge_storage(unsigned t) const + { + return g_.edge_storage(t); + } + + unsigned new_state(bdd cond) + { + return g_.new_state(cond); + } + + unsigned new_states(unsigned n, bdd cond) + { + return g_.new_states(n, cond); + } + + unsigned new_edge(unsigned src, unsigned dst) + { + return g_.new_edge(src, dst); + } + }; + + typedef std::shared_ptr kripke_graph_ptr; + + inline kripke_graph_ptr + make_kripke_graph(const bdd_dict_ptr& d) + { + return std::make_shared(d); + } +} diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc deleted file mode 100644 index a069be7d8..000000000 --- a/src/kripke/kripkeprint.cc +++ /dev/null @@ -1,137 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et -// Developpement 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 "kripkeprint.hh" -#include "kripkeexplicit.hh" -#include "twa/bddprint.hh" -#include "misc/escape.hh" -#include "twaalgos/reachiter.hh" -#include -#include - -namespace spot -{ - namespace - { - - class kripke_printer : public tgba_reachable_iterator_breadth_first - { - public: - kripke_printer(const const_kripke_ptr& a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os) - { - } - - void process_state(const state* s, int, twa_succ_iterator* si) - { - const bdd_dict_ptr d = aut_->get_dict(); - os_ << '"'; - escape_str(os_, aut_->format_state(s)); - os_ << "\", \""; - auto aut = std::static_pointer_cast (aut_); - assert(aut); - escape_str(os_, bdd_format_formula(d, aut->state_condition(s))); - - os_ << "\","; - for (si->first(); !si->done(); si->next()) - { - state* dest = si->dst(); - os_ << " \""; - escape_str(os_, aut_->format_state(dest)); - os_ << '"'; - } - os_ << ";\n"; - } - - private: - std::ostream& os_; - }; - - class kripke_printer_renumbered : - public tgba_reachable_iterator_breadth_first - { - public: - kripke_printer_renumbered(const const_kripke_ptr& a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os), - notfirst(false) - { - } - - void finish_state() - { - os_ << lastsuccs.str() << ";\n"; - lastsuccs.str(""); - } - - void process_state(const state* s, int in_s, twa_succ_iterator*) - { - if (notfirst) - finish_state(); - else - notfirst = true; - - const bdd_dict_ptr d = aut_->get_dict(); - os_ << 'S' << in_s << ", \""; - auto aut = std::static_pointer_cast(aut_); - assert(aut); - escape_str(os_, bdd_format_formula(d, - aut->state_condition(s))); - os_ << "\","; - } - - void - process_link(const state*, int, const state*, int d, - const twa_succ_iterator*) - { - lastsuccs << " S" << d; - } - - void - end() - { - finish_state(); - } - - private: - std::ostream& os_; - std::ostringstream lastsuccs; - bool notfirst; - }; - - } - - std::ostream& - kripke_save_reachable(std::ostream& os, const const_kripke_ptr& k) - { - kripke_printer p(k, os); - p.run(); - return os; - } - - std::ostream& - kripke_save_reachable_renumbered(std::ostream& os, const const_kripke_ptr& k) - { - kripke_printer_renumbered p(k, os); - p.run(); - return os; - } - - -} // End namespace Spot diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh deleted file mode 100644 index 733192944..000000000 --- a/src/kripke/kripkeprint.hh +++ /dev/null @@ -1,52 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement -// 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 "misc/common.hh" -#include -#include "kripke.hh" - -namespace spot -{ - - /// \ingroup twa_io - /// \brief Save the reachable part of Kripke structure in text format. - /// - /// The states will be named with the value returned by the - /// kripke::format_state() method. Such a string can be large, so - /// the output will not be I/O efficient. We recommend using this - /// function only for debugging. Use - /// kripke_save_reachable_renumbered() for large output. - /// - SPOT_API std::ostream& - kripke_save_reachable(std::ostream& os, const const_kripke_ptr& k); - - /// \ingroup twa_io - /// \brief Save the reachable part of Kripke structure in text format. - /// - /// States will be renumbered with sequential number. This is much - /// more I/O efficient when dumping large Kripke structures with big - /// state names. The drawback is that any information carried by - /// the state name is lost. - /// - SPOT_API std::ostream& - kripke_save_reachable_renumbered(std::ostream& os, const const_kripke_ptr& k); - -} // End namespace spot diff --git a/src/kripkeparse/.gitignore b/src/kripkeparse/.gitignore deleted file mode 100644 index 0bb28fc07..000000000 --- a/src/kripkeparse/.gitignore +++ /dev/null @@ -1,11 +0,0 @@ -Makefile -Makefile.in -location.hh -kripkeparse.hh -kripkeparse.cc -kripkeparse.output -kripkescan.cc -position.hh -stack.hh -*.lo -*.la diff --git a/src/kripkeparse/Makefile.am b/src/kripkeparse/Makefile.am deleted file mode 100644 index 9d347b134..000000000 --- a/src/kripkeparse/Makefile.am +++ /dev/null @@ -1,58 +0,0 @@ -## Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). -## -## This file is part of Spot, a model checking library. -## -## Spot is free software; you can redistribute it and/or modify it -## under the terms of the GNU General Public License as published by -## the Free Software Foundation; either version 3 of the License, or -## (at your option) any later version. -## -## Spot is distributed in the hope that it will be useful, but WITHOUT -## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -## License for more details. -## -## You should have received a copy of the GNU General Public License -## along with this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT -# Disable -Werror because too many versions of flex yield warnings. -AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) - -kripkeparsedir = $(pkgincludedir)/kripkeparse - -kripkeparse_HEADERS = public.hh - -noinst_LTLIBRARIES = libkripkeparse.la - -KRIPKEPARSE_YY = kripkeparse.yy -FROM_KRIPKEPARSE_YY_MAIN = kripkeparse.cc -FROM_KRIPKEPARSE_YY_OTHERS = \ - stack.hh \ - kripkeparse.hh - -FROM_KRIPKEPARSE_YY = \ - $(FROM_KRIPKEPARSE_YY_MAIN) \ - $(FROM_KRIPKEPARSE_YY_OTHERS) - -BUILT_SOURCES = $(FROM_KRIPKEPARSE_YY) -MAINTAINERCLEANFILES = $(FROM_KRIPKEPARSE_YY) - -$(FROM_KRIPKEPARSE_YY_MAIN): $(srcdir)/$(KRIPKEPARSE_YY) -## We must cd into $(srcdir) first because if we tell bison to read -## $(srcdir)/$(KRIPKEPARSE_YY), it will also use the value of $(srcdir)/ -## in the generated include statements. - cd $(srcdir) && \ - $(BISON) -Wall -Werror --report=all $(BISON_EXTRA_FLAGS) \ - $(KRIPKEPARSE_YY) -o $(FROM_KRIPKEPARSE_YY_MAIN) -$(FROM_KRIPKEPARSE_YY_OTHERS): $(KRIPKEPARSE_YY) - @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_KRIPKEPARSE_YY_MAIN) - -EXTRA_DIST = $(KRIPKEPARSE_YY) - -libkripkeparse_la_SOURCES = \ - $(FROM_KRIPKEPARSE_YY) \ - kripkescan.ll \ - parsedecl.hh \ - fmterror.cc diff --git a/src/kripkeparse/fmterror.cc b/src/kripkeparse/fmterror.cc deleted file mode 100644 index 1142a2658..000000000 --- a/src/kripkeparse/fmterror.cc +++ /dev/null @@ -1,42 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include "public.hh" - -namespace spot -{ - bool - format_kripke_parse_errors(std::ostream& os, - const std::string& filename, - kripke_parse_error_list& error_list) - { - bool printed = false; - spot::kripke_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/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy deleted file mode 100644 index 53ec57634..000000000 --- a/src/kripkeparse/kripkeparse.yy +++ /dev/null @@ -1,225 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 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 -%name-prefix "kripkeyy" -%debug -%error-verbose -%define api.location.type "spot::location" - -%code requires -{ -#include -#include -#include "public.hh" - -/* Cache parsed formulae. Labels on arcs are frequently identical and - it would be a waste of time to parse them to formula* over and - over, and to register all their atomic_propositions in the - bdd_dict. Keep the bdd result around so we can reuse it. */ -typedef std::map formula_cache; -} - -%parse-param {spot::kripke_parse_error_list& error_list} -%parse-param {spot::environment& parse_environment} -%parse-param {spot::kripke_explicit_ptr& result} -%parse-param {formula_cache& fcache} - -%union -{ - int token; - std::string* str; - std::list* list; -} - -%code -{ -#include "kripke/kripkeexplicit.hh" -#include "tl/parse.hh" -#include - -/* twaparse.hh and parsedecl.hh include each other recursively. - We must ensure that YYSTYPE is declared (by the above %union) - before parsedecl.hh uses it. */ -#include "parsedecl.hh" - -using namespace spot; -#include - //typedef std::pair pair; -} - -%token STRING UNTERMINATED_STRING IDENT -%token COMA "," -%token SEMICOL ";" -%type strident string -%type condition -%type follow_list - -%destructor { delete $$; } -%destructor { - std::cout << $$->size() << std::endl; - for (std::list::iterator i = $$->begin(); - i != $$->end(); ++i) - delete (*i); - delete $$; - } - -%printer { debug_stream() << *$$; } - -%% - -kripke: -lines { - } -| { -} -; - -/* At least one line. */ -lines: line { } -| lines line { } - ; - -line: -strident "," condition "," follow_list ";" -{ - result->add_state(*$1); - if ($3) - { - formula_cache::const_iterator i = fcache.find(*$3); - if (i == fcache.end()) - { - parse_error_list pel; - formula f = spot::parse_infix_boolean(*$3, pel, - parse_environment); - for (parse_error_list::iterator i = pel.begin(); - i != pel.end(); ++i) - { - //Adjust the diagnostic to the current position. - spot::location here = @3; - here.end.line = here.begin.line + i->first.end.line - 1; - here.end.column = - here.begin.column + i->first.end.column; - here.begin.line += i->first.begin.line - 1; - here.begin.column += i->first.begin.column; - error_list.emplace_back(here, i->second); - } - if (f) - result->add_condition(f, *$1); - else - result->add_conditions(bddfalse, *$1); - fcache[*$3] = result->state_condition(*$1); - } - else - { - result->add_conditions(i->second, *$1); - } - delete $3; - } - std::list::iterator i; - for (i = $5->begin(); i != $5->end(); ++i) - { - result->add_transition(*$1, **i); - delete *i; - } - - delete $1; - delete $5; -} -; - - -string: STRING - { $$ = $1; } - | UNTERMINATED_STRING - { - $$ = $1; - error_list.emplace_back(@1, "unterminated string"); - } -; - -strident: string -{ $$ = $1; } -| IDENT -{ $$ = $1; } -; - -follow_list: -follow_list strident -{ - $$ = $1; - $$->push_back($2); -} -| { - $$ = new std::list; - } -; - -condition: - { - $$ = 0; - } - | string - { - $$ = $1; - } - ; - -%% - -void -kripkeyy::parser::error(const location_type& location, - const std::string& message) -{ - error_list.emplace_back(location, message); -} - -namespace spot -{ - kripke_explicit_ptr - kripke_parse(const std::string& name, - kripke_parse_error_list& error_list, - const bdd_dict_ptr& dict, - environment& env, - bool debug) - { - if (kripkeyyopen(name)) - { - error_list.push_back - (kripke_parse_error(spot::location(), - std::string("Cannot open file ") + name)); - return nullptr; - } - formula_cache fcache; - auto result = make_kripke_explicit(dict); - kripkeyy::parser parser(error_list, env, result, fcache); - parser.set_debug_level(debug); - parser.parse(); - kripkeyyclose(); - - return result; - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/kripkeparse/kripkescan.ll b/src/kripkeparse/kripkescan.ll deleted file mode 100644 index fff7e65ad..000000000 --- a/src/kripkeparse/kripkescan.ll +++ /dev/null @@ -1,115 +0,0 @@ -/* Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement -* 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="kripkeyy" -%option outfile="lex.yy.c" -%x STATE_STRING - -%{ -#include -#include "kripkeparse/parsedecl.hh" - - -#define YY_USER_ACTION \ - yylloc->columns(yyleng); - -#define YY_NEVER_INTERACTIVE 1 - - typedef kripkeyy::parser::token token; - - -%} - -eol \n+|\r+ -eol2 (\n\r)+|(\r\n)+ - -%% - -%{ - yylloc->step (); -%} - -[a-zA-Z][a-zA-Z0-9_]* { - yylval->str = new std::string(yytext, yyleng); - return token::IDENT; - } - - /* discard whitespace */ -{eol} yylloc->lines(yyleng); yylloc->step(); -{eol2} yylloc->lines(yyleng / 2); yylloc->step(); -[ \t]+ yylloc->step(); - -\" { - yylval->str = new std::string; - BEGIN(STATE_STRING); - } - -"," { - return token::COMA; - } - -";" return token::SEMICOL; - -. return *yytext; - - /* Handle \" and \\ in strings. */ -{ - \" { - BEGIN(INITIAL); - return token::STRING; - } - \\["\\] yylval->str->append(1, yytext[1]); - [^"\\]+ yylval->str->append(yytext, yyleng); - <> { - BEGIN(INITIAL); - return token::UNTERMINATED_STRING; - } -} - -%{ - /* Dummy use of yyunput to shut up a gcc warning. */ - (void) &yyunput; -%} - -%% - -namespace spot -{ - int - kripkeyyopen(const std::string &name) - { - if (name == "-") - { - yyin = stdin; - } - else - { - yyin = fopen(name.c_str(), "r"); - if (!yyin) - return 1; - } - return 0; - } - - void - kripkeyyclose() - { - fclose(yyin); - } -} diff --git a/src/kripkeparse/parsedecl.hh b/src/kripkeparse/parsedecl.hh deleted file mode 100644 index c609359c2..000000000 --- a/src/kripkeparse/parsedecl.hh +++ /dev/null @@ -1,37 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement -// 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 -#include "kripkeparse.hh" -#include "misc/location.hh" - -# define YY_DECL \ - int kripkeyylex (kripkeyy::parser::semantic_type *yylval, \ - spot::location *yylloc) - -YY_DECL; - -namespace spot -{ - int kripkeyyopen(const std::string& name); - void kripkeyyclose(); -} diff --git a/src/kripkeparse/public.hh b/src/kripkeparse/public.hh deleted file mode 100644 index 457825eb4..000000000 --- a/src/kripkeparse/public.hh +++ /dev/null @@ -1,59 +0,0 @@ -// -*- coding: utf-8 -*_ -// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et -// Developpement 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 "kripke/kripkeexplicit.hh" -#include "misc/location.hh" -#include "tl/defaultenv.hh" -#include -#include -#include -#include - -namespace spot -{ - - /// \brief A parse diagnostic with its location. - typedef std::pair kripke_parse_error; - /// \brief A list of parser diagnostics, as filled by parse. - typedef std::list kripke_parse_error_list; - - - - SPOT_API kripke_explicit_ptr - kripke_parse(const std::string& name, - kripke_parse_error_list& error_list, - const bdd_dict_ptr& dict, - environment& env - = default_environment::instance(), - bool debug = false); - - - /// \brief Format diagnostics produced by spot::kripke_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::parse while - /// parsing \a ltl_string. - /// \return \c true if any diagnostic was output. - SPOT_API - bool format_kripke_parse_errors(std::ostream& os, - const std::string& filename, - kripke_parse_error_list& error_list); -} diff --git a/src/parseaut/parseaut.yy b/src/parseaut/parseaut.yy index 31275046e..c9fe646db 100644 --- a/src/parseaut/parseaut.yy +++ b/src/parseaut/parseaut.yy @@ -82,6 +82,7 @@ extern "C" int strverscmp(const char *s1, const char *s2); spot::location used_loc; }; spot::parsed_aut_ptr h; + spot::twa_ptr aut_or_ks; spot::automaton_parser_options opts; std::string format_version; spot::location format_version_loc; @@ -309,7 +310,10 @@ header: format-version header-items error(res.states_loc, "... declared here."); states = std::max(states, p.second + 1); } - res.h->aut->new_states(states); + if (res.opts.want_kripke) + res.h->ks->new_states(states, bddfalse); + else + res.h->aut->new_states(states); res.info_states.resize(states); } if (res.accset < 0) @@ -321,6 +325,11 @@ header: format-version header-items { auto explicit_labels = res.props.find("explicit-labels"); auto implicit_labels = res.props.find("implicit-labels"); + + if (implicit_labels != res.props.end() && res.opts.want_kripke) + error(implicit_labels->second, + "Kripke structure may not use implicit labels"); + if (implicit_labels != res.props.end()) { if (explicit_labels == res.props.end()) @@ -330,15 +339,20 @@ header: format-version header-items else { error(implicit_labels->second, - "'property: implicit-labels' is incompatible " + "'properties: implicit-labels' is incompatible " "with..."); error(explicit_labels->second, - "... 'property: explicit-labels'."); + "... 'properties: explicit-labels'."); } } auto trans_labels = res.props.find("trans-labels"); auto state_labels = res.props.find("state-labels"); + + if (trans_labels != res.props.end() && res.opts.want_kripke) + error(trans_labels->second, + "Kripke structure may not use transition labels"); + if (trans_labels != res.props.end()) { if (state_labels == res.props.end()) @@ -349,9 +363,9 @@ header: format-version header-items else { error(trans_labels->second, - "'property: trans-labels' is incompatible with..."); + "'properties: trans-labels' is incompatible with..."); error(state_labels->second, - "... 'property: state-labels'."); + "... 'properties: state-labels'."); } } else if (state_labels != res.props.end()) @@ -363,12 +377,16 @@ header: format-version header-items else { error(state_labels->second, - "'property: state-labels' is incompatible with..."); + "'properties: state-labels' is incompatible with..."); error(implicit_labels->second, - "... 'property: implicit-labels'."); + "... 'properties: implicit-labels'."); } } + if (res.opts.want_kripke && res.label_style != State_Labels) + error(@$, + "Kripke structure should use 'properties: state-labels'"); + auto state_acc = res.props.find("state-acc"); auto trans_acc = res.props.find("trans-acc"); if (trans_acc != res.props.end()) @@ -380,9 +398,9 @@ header: format-version header-items else { error(trans_acc->second, - "'property: trans-acc' is incompatible with..."); + "'properties: trans-acc' is incompatible with..."); error(state_acc->second, - "... 'property: state-acc'."); + "... 'properties: state-acc'."); } } else if (state_acc != res.props.end()) @@ -392,9 +410,9 @@ header: format-version header-items } { unsigned ss = res.start.size(); + auto det = res.props.find("deterministic"); if (ss > 1) { - auto det = res.props.find("deterministic"); if (det != res.props.end()) { error(det->second, @@ -406,12 +424,12 @@ header: format-version header-items else { // Assume the automaton is deterministic until proven - // wrong. - res.deterministic = true; + // wrong, or unless we are building a Kripke structure. + res.deterministic = !res.opts.want_kripke; } + auto complete = res.props.find("complete"); if (ss < 1) { - auto complete = res.props.find("complete"); if (complete != res.props.end()) { error(complete->second, @@ -424,12 +442,19 @@ header: format-version header-items { // Assume the automaton is complete until proven // wrong. - res.complete = true; + res.complete = !res.opts.want_kripke; } + // if ap_count == 0, then a Kripke structure could be + // declared complete, although that probably doesn't + // matter. + if (res.opts.want_kripke && complete != res.props.end() + && res.ap_count > 0) + error(complete->second, + "Kripke structure may not be complete"); } if (res.opts.trust_hoa) { - auto& a = res.h->aut; + auto& a = res.aut_or_ks; auto& p = res.props; auto e = p.end(); a->prop_stutter_invariant(p.find("stutter-invariant") != e); @@ -450,34 +475,35 @@ version: IDENTIFIER format-version: "HOA:" { res.h->loc = @1; } 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 +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) { - 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; - } + 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 @@ -536,7 +562,7 @@ header-item: "States:" INT } else { - res.h->aut->acc().add_sets($2); + res.aut_or_ks->acc().add_sets($2); res.accset = $2; res.accset_loc = @1 + @2; } @@ -544,7 +570,13 @@ header-item: "States:" INT acceptance-cond { res.ignore_more_acc = true; - res.h->aut->set_acceptance($2, *$4); + // Not setting the acceptance in case of error will + // force it to be true. + if (res.opts.want_kripke && (!$4->is_tt() || $2 > 0)) + error(@2 + @4, + "the acceptance for Kripke structure must be '0 t'"); + else + res.aut_or_ks->set_acceptance($2, *$4); delete $4; } | "acc-name:" IDENTIFIER acc-spec @@ -558,7 +590,7 @@ header-item: "States:" INT } | "name:" STRING { - res.h->aut->set_named_prop("automaton-name", $2); + res.aut_or_ks->set_named_prop("automaton-name", $2); } | "properties:" properties | HEADERNAME header-spec @@ -584,11 +616,11 @@ ap-name: STRING std::ostringstream out; out << "unknown atomic proposition \"" << *$1 << "\""; error(@1, out.str()); - b = res.h->aut->register_ap("$unknown$"); + b = res.aut_or_ks->register_ap("$unknown$"); } else { - b = res.h->aut->register_ap(f); + b = res.aut_or_ks->register_ap(f); if (!res.ap_set.emplace(b).second) { std::ostringstream out; @@ -716,13 +748,13 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' { if ($3 != -1U) { - res.pos_acc_sets |= res.h->aut->acc().mark($3); + res.pos_acc_sets |= res.aut_or_ks->acc().mark($3); if (*$1 == "Inf") $$ = new spot::acc_cond::acc_code - (res.h->aut->acc().inf({$3})); + (res.aut_or_ks->acc().inf({$3})); else $$ = new spot::acc_cond::acc_code - (res.h->aut->acc().fin({$3})); + (res.aut_or_ks->acc().fin({$3})); } else { @@ -734,13 +766,13 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' { if ($4 != -1U) { - res.neg_acc_sets |= res.h->aut->acc().mark($4); + res.neg_acc_sets |= res.aut_or_ks->acc().mark($4); if (*$1 == "Inf") $$ = new spot::acc_cond::acc_code - (res.h->aut->acc().inf_neg({$4})); + (res.aut_or_ks->acc().inf_neg({$4})); else $$ = new spot::acc_cond::acc_code - (res.h->aut->acc().fin_neg({$4})); + (res.aut_or_ks->acc().fin_neg({$4})); } else { @@ -771,7 +803,8 @@ acceptance-cond: IDENTIFIER '(' acc-set ')' | 'f' { { - $$ = new spot::acc_cond::acc_code(res.h->aut->acc().fin({})); + $$ = new spot::acc_cond::acc_code + (res.aut_or_ks->acc().fin({})); } } @@ -824,13 +857,27 @@ checked-state-num: state-num "count..."); error(res.states_loc, "... declared here."); } - int missing = - ((int) $1) - res.h->aut->num_states() + 1; - if (missing >= 0) + if (res.opts.want_kripke) { - res.h->aut->new_states(missing); - res.info_states.resize - (res.info_states.size() + missing); + int missing = + ((int) $1) - res.h->ks->num_states() + 1; + if (missing >= 0) + { + res.h->ks->new_states(missing, bddfalse); + res.info_states.resize + (res.info_states.size() + missing); + } + } + else + { + int missing = + ((int) $1) - res.h->aut->num_states() + 1; + if (missing >= 0) + { + res.h->aut->new_states(missing); + res.info_states.resize + (res.info_states.size() + missing); + } } } // Remember the first place were a state is the @@ -845,7 +892,7 @@ checked-state-num: state-num states: | states state { - if (res.deterministic || res.complete) + if ((res.deterministic || res.complete) && !res.opts.want_kripke) { bdd available = bddtrue; bool det = true; @@ -862,7 +909,8 @@ states: | states state if (p != res.props.end()) { error(@2, "automaton is not deterministic..."); - error(p->second, "... despite 'property: deterministic'"); + error(p->second, + "... despite 'properties: deterministic'"); } } if (res.complete && available != bddfalse) @@ -872,7 +920,7 @@ states: | states state if (p != res.props.end()) { error(@2, "automaton is not complete..."); - error(p->second, "... despite 'property: complete'"); + error(p->second, "... despite 'properties: complete'"); } } } @@ -890,13 +938,17 @@ state: state-name labeled-edges error(@2, "these transitions have implicit labels but the" " automaton is..."); error(res.props["state-labels"], "... declared with " - "'property: state-labels'"); + "'properties: state-labels'"); // Do not repeat this message. res.label_style = Mixed_Labels; } - res.cur_guard = res.guards.begin(); } + else if (res.opts.want_kripke) + { + res.h->ks->state_from_number(res.cur_state)->cond(res.state_label); + } + } | error { @@ -928,6 +980,8 @@ state-name: "State:" state-label_opt checked-state-num string_opt state-acc_opt (*res.state_names)[$3] = std::move(*$4); delete $4; } + if (res.opts.want_kripke && !res.has_state_label) + error(@$, "Kripke structures should have labeled states"); } label: '[' label-expr ']' { @@ -952,11 +1006,12 @@ state-label_opt: { res.has_state_label = false; } "state label used although the automaton was..."); if (res.label_style == Trans_Labels) error(res.props["trans-labels"], - "... declared with 'property: trans-labels' here"); + "... declared with 'properties: trans-labels'" + " here"); else error(res.props["implicit-labels"], - "... declared with 'property: implicit-labels' " - "here"); + "... declared with 'properties: implicit-labels'" + " here"); // Do not show this error anymore. res.label_style = Mixed_Labels; } @@ -977,12 +1032,12 @@ trans-label: label "automaton was..."); if (res.label_style == State_Labels) error(res.props["state-labels"], - "... declared with 'property: state-labels' " + "... declared with 'properties: state-labels' " "here"); else error(res.props["implicit-labels"], - "... declared with 'property: implicit-labels' " - "here"); + "... declared with 'properties: implicit-labels'" + " here"); // Do not show this error anymore. res.label_style = Mixed_Labels; } @@ -1012,7 +1067,7 @@ acc-sets: if (res.ignore_acc || $2 == -1U) $$ = spot::acc_cond::mark_t(0U); else - $$ = $1 | res.h->aut->acc().mark($2); + $$ = $1 | res.aut_or_ks->acc().mark($2); } state-acc_opt: @@ -1060,14 +1115,26 @@ incorrectly-unlabeled-edge: checked-state-num trans-acc_opt "(previous edge is labeled)"); else cond = res.state_label; - res.h->aut->new_edge(res.cur_state, $1, - cond, $2 | res.acc_state); + if (cond != bddfalse) + { + if (res.opts.want_kripke) + res.h->ks->new_edge(res.cur_state, $1); + else + res.h->aut->new_edge(res.cur_state, $1, + cond, + $2 | res.acc_state); + } } labeled-edge: trans-label checked-state-num trans-acc_opt { if (res.cur_label != bddfalse) - res.h->aut->new_edge(res.cur_state, $2, - res.cur_label, $3 | res.acc_state); + { + if (res.opts.want_kripke) + res.h->ks->new_edge(res.cur_state, $2); + else + res.h->aut->new_edge(res.cur_state, $2, + res.cur_label, $3 | res.acc_state); + } } | trans-label state-conj-2 trans-acc_opt { @@ -1104,8 +1171,13 @@ unlabeled-edge: checked-state-num trans-acc_opt } } if (cond != bddfalse) - res.h->aut->new_edge(res.cur_state, $1, - cond, $2 | res.acc_state); + { + if (res.opts.want_kripke) + res.h->ks->new_edge(res.cur_state, $1); + else + res.h->aut->new_edge(res.cur_state, $1, + cond, $2 | res.acc_state); + } } | state-conj-2 trans-acc_opt { @@ -1134,12 +1206,24 @@ dstar_type: "DRA" res.h->type = spot::parsed_aut_type::DRA; res.plus = 1; res.minus = 0; + if (res.opts.want_kripke) + { + error(@$, + "cannot read a Kripke structure out of a DSTAR automaton"); + YYABORT; + } } | "DSA" { res.h->type = spot::parsed_aut_type::DSA; res.plus = 0; res.minus = 1; + if (res.opts.want_kripke) + { + error(@$, + "cannot read a Kripke structure out of a DSTAR automaton"); + YYABORT; + } } dstar_header: dstar_sizes @@ -1301,12 +1385,19 @@ dstar_states: /* Rules for neverclaims */ /**********************************************************************/ -never: "never" { res.namer = res.h->aut->create_namer(); - res.h->aut->set_buchi(); - res.h->aut->prop_state_acc(true); - res.acc_state = State_Acc; - res.pos_acc_sets = res.h->aut->acc().all_sets(); - } +never: "never" + { + if (res.opts.want_kripke) + { + error(@$, "cannot read a Kripke structure out of a never claim."); + YYABORT; + } + res.namer = res.h->aut->create_namer(); + res.h->aut->set_buchi(); + res.h->aut->prop_state_acc(true); + res.acc_state = State_Acc; + res.pos_acc_sets = res.h->aut->acc().all_sets(); + } '{' nc-states '}' { // Add an accept_all state if needed. @@ -1553,6 +1644,13 @@ lbtt: lbtt-header lbtt-body ENDAUT lbtt-header-states: LBTT { + if (res.opts.want_kripke) + { + error(@$, + "cannot read a Kripke structure out of " + "an LBTT automaton"); + YYABORT; + } res.states = $1; res.states_loc = @1; res.h->aut->new_states($1); @@ -1655,7 +1753,7 @@ lbtt-transitions: else { res.states_map.emplace(dst, dst); - } + } res.h->aut->new_edge(res.cur_state, dst, res.cur_label, res.acc_state | $3); @@ -1766,6 +1864,8 @@ fix_acceptance_aux(spot::acc_cond& acc, static void fix_acceptance(result_& r) { + if (r.opts.want_kripke) + return; auto& acc = r.h->aut->acc(); // If a set x appears only as Inf(!x), we can complement it so that @@ -1808,7 +1908,6 @@ static void fix_acceptance(result_& r) static void fix_initial_state(result_& r) { - std::vector start; start.reserve(r.start.size()); for (auto& p : r.start) @@ -1821,7 +1920,10 @@ static void fix_initial_state(result_& r) { // If no initial state has been declared, add one, because // Spot will not work without one. - r.h->aut->set_init_state(r.h->aut->new_state()); + if (r.opts.want_kripke) + r.h->ks->set_init_state(r.h->ks->new_state(bddfalse)); + else + r.h->aut->set_init_state(r.h->aut->new_state()); return; } @@ -1833,10 +1935,20 @@ static void fix_initial_state(result_& r) assert(start.size() >= 1); if (start.size() == 1) { - r.h->aut->set_init_state(start.front()); + if (r.opts.want_kripke) + r.h->ks->set_init_state(start.front()); + else + r.h->aut->set_init_state(start.front()); } else { + if (r.opts.want_kripke) + { + r.h->errors.emplace_front(r.start.front().first, + "Kripke structure only support " + "a single initial state"); + return; + } // Multiple initial states. We might need to add a fake one, // unless one of the actual initial state has no incoming edge. auto& aut = r.h->aut; @@ -1865,11 +1977,11 @@ static void fix_initial_state(result_& r) static void fix_properties(result_& r) { - r.h->aut->prop_deterministic(r.deterministic); - //r.h->aut->prop_complete(r.complete); + r.aut_or_ks->prop_deterministic(r.deterministic); + //r.aut_or_ks->prop_complete(r.complete); if (r.acc_style == State_Acc || (r.acc_style == Mixed_Acc && !r.trans_acc_seen)) - r.h->aut->prop_state_acc(true); + r.aut_or_ks->prop_state_acc(true); } static void check_version(const result_& r) @@ -1935,7 +2047,7 @@ namespace spot hoayyclose(); } - void raise_parse_error(const parsed_aut_ptr& pa) + static void raise_parse_error(const parsed_aut_ptr& pa) { if (pa->aborted) pa->errors.emplace_back(pa->loc, "parsing aborted"); @@ -1957,7 +2069,10 @@ namespace spot result_ r; r.opts = opts_; r.h = std::make_shared(filename_); - r.h->aut = make_twa_graph(dict); + if (opts_.want_kripke) + r.aut_or_ks = r.h->ks = make_kripke_graph(dict); + else + r.aut_or_ks = r.h->aut = make_twa_graph(dict); r.env = &env; hoayy::parser parser(r, last_loc); static bool env_debug = !!getenv("SPOT_DEBUG_PARSER"); @@ -1966,7 +2081,11 @@ namespace spot try { if (parser.parse()) - r.h->aut = nullptr; + { + r.h->aut = nullptr; + r.h->ks = nullptr; + r.aut_or_ks = nullptr; + } } catch (const spot::hoa_abort& e) { @@ -1985,10 +2104,10 @@ namespace spot } if (opts_.raise_errors) raise_parse_error(r.h); - if (!r.h->aut) + if (!r.aut_or_ks) return r.h; if (r.state_names) - r.h->aut->set_named_prop("state-names", r.state_names); + r.aut_or_ks->set_named_prop("state-names", r.state_names); fix_acceptance(r); fix_initial_state(r); fix_properties(r); @@ -2015,7 +2134,7 @@ namespace spot pa->errors.emplace_back(spot::location(), e.what()); return pa; } - if (!pa->aut && pa->errors.empty()) + if (!pa->aut && !pa->ks && pa->errors.empty()) pa->errors.emplace_back(pa->loc, "no automaton read (empty input?)"); if (opts.raise_errors) raise_parse_error(pa); diff --git a/src/parseaut/public.hh b/src/parseaut/public.hh index aedc421cf..db3d0d806 100644 --- a/src/parseaut/public.hh +++ b/src/parseaut/public.hh @@ -20,6 +20,7 @@ #pragma once #include "twa/twagraph.hh" +#include "kripke/kripkegraph.hh" #include "misc/location.hh" #include "tl/defaultenv.hh" #include @@ -52,7 +53,15 @@ namespace spot /// /// May be null if the parser reached the end of the stream or a /// serious error. In the latter case, \c errors is non-empty. + /// May also be null if the parser is used to parse a Kripke + /// structure. twa_graph_ptr aut; + /// \brief The parsed kripke structure. + /// + /// Used instead of \c aut when the parser is called with option + /// want_kripke. + kripke_graph_ptr ks; + /// Whether an HOA file was termined with --ABORT bool aborted = false; /// Location of the automaton in the stream. @@ -86,6 +95,7 @@ namespace spot bool debug = false; ///< Run the parser in debug mode? bool trust_hoa = true; ///< Trust properties in HOA files bool raise_errors = false; ///< Raise errors as exceptions. + bool want_kripke = false; ///< Parse as a Kripke structure. }; /// \brief Parse a stream of automata diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 51b9a0840..75ea2fa42 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -157,8 +157,7 @@ TESTS_graph = \ tgbagraph.test TESTS_kripke = \ - kripke.test \ - bad_parsing.test + kripke.test TESTS_twa = \ acc.test \ diff --git a/src/tests/bad_parsing.test b/src/tests/bad_parsing.test deleted file mode 100755 index 490e75203..000000000 --- a/src/tests/bad_parsing.test +++ /dev/null @@ -1,95 +0,0 @@ -#! /bin/sh -# -*- coding: utf-8 -*- -# Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement -# de l'Epita (LRDE) -# -# This file is part of Spot, a model checking library. -# -# Spot is free software; you can redistribute it and/or modify it -# under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# Spot is distributed in the hope that it will be useful, but WITHOUT -# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -# License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see . - - -. ./defs - -set -e - -cat >input <<\EOF -state; -EOF - -cat >expected <<\EOF -input:1.6: syntax error, unexpected ;, expecting "," -EOF - -run 1 ../parse_print input 2> output -cat output | grep -v + > res -diff expected res - -rm -f output res expected - -cat >input <<\EOF -state1, "a & b, state2; -EOF - -cat >expected <<\EOF -input:1.9-24: unterminated string -input:1.25-24: syntax error, unexpected $end, expecting "," -EOF - -run 1 ../parse_print input 2> output -cat output | grep -v + > res -diff expected res - -rm -f output res expected - - -cat >input <<\EOF -state, "", ; -,,; -EOF - -cat >expected <<\EOF -input:1.9-8: empty input -input:2.1: syntax error, unexpected ",", expecting $end -EOF - -run 1 ../parse_print input 2> output -cat output | grep -v + > res -diff expected res - -# The diagnostic should be the same with DOS return lines -perl -pi -e 's/$/\r/' input -run 1 ../parse_print input 2> output -cat output | grep -v + > res -diff expected res - - -rm -f output res expected - -cat >input <<\EOF -state,, state3 -state2, "a & b", state2; -EOF - - -s="input:2.7: syntax error, unexpected \",\", expecting STRING" -s2=" or UNTERMINATED_STRING or IDENT or ;" -string="$s$s2"; - -echo $string > expected - -run 1 ../parse_print input 2> output -cat output | grep -v + > res -diff expected res - -rm -f output res expected diff --git a/src/tests/ikwiad.cc b/src/tests/ikwiad.cc index 8200665a7..7212619b3 100644 --- a/src/tests/ikwiad.cc +++ b/src/tests/ikwiad.cc @@ -54,7 +54,6 @@ #include "twaalgos/isdet.hh" #include "twaalgos/cycles.hh" #include "twaalgos/isweakscc.hh" -#include "kripkeparse/public.hh" #include "twaalgos/simulation.hh" #include "twaalgos/compsusp.hh" #include "twaalgos/powerset.hh" @@ -523,13 +522,13 @@ checked_main(int argc, char** argv) else if (!strncmp(argv[formula_index], "-KP", 3)) { tm.start("reading -KP's argument"); - - spot::kripke_parse_error_list pel; - system_aut = spot::kripke_parse(argv[formula_index] + 3, - pel, dict, env, debug_opt); - if (spot::format_kripke_parse_errors(std::cerr, - argv[formula_index] + 2, pel)) + spot::automaton_parser_options opts; + opts.debug = debug_opt; + opts.want_kripke = true; + auto paut = spot::parse_aut(argv[formula_index] + 3, dict, env, opts); + if (paut->format_errors(std::cerr)) return 2; + system_aut = paut->ks; tm.stop("reading -KP's argument"); } else if (!strcmp(argv[formula_index], "-KC")) diff --git a/src/tests/kripke.test b/src/tests/kripke.test index 9879afc45..f84d1ec1d 100755 --- a/src/tests/kripke.test +++ b/src/tests/kripke.test @@ -22,51 +22,118 @@ set -e -run2() -{ - run 0 ../parse_print "$1" > "$1.out" - run 0 ../parse_print "$1.out" > "$1.out2" - cmp "$1.out" "$1.out2" -} - cat >input1 < input1.out +run 0 ../parse_print input1.out > input1.out2 + cat >input2 <input3 <output2.err && exit 1 +cat output2.err +cat >expected2<input4 <input5 <input6 <. -#include "kripkeparse/public.hh" -#include "kripke/kripkeprint.hh" +#include "parseaut/public.hh" +#include "twaalgos/hoa.hh" using namespace spot; @@ -28,20 +28,23 @@ int main(int argc, char** argv) (void) argc; assert(argc == 2); int return_value = 0; - kripke_parse_error_list pel; - { - auto k = kripke_parse(argv[1], pel, make_bdd_dict()); - if (!pel.empty()) - { - format_kripke_parse_errors(std::cerr, argv[1], pel); - return_value = 1; - } + spot::automaton_parser_options opts; + opts.want_kripke = true; + spot::automaton_stream_parser parser(argv[1], opts); - if (!return_value) - kripke_save_reachable(std::cout, k); - } - - assert(spot::fnode::instances_check()); + while (auto paut = parser.parse(make_bdd_dict(), + default_environment::instance())) + { + if (paut->format_errors(std::cerr)) + { + return_value = 1; + if (paut->ks) + continue; + } + if (!paut->ks) + break; + print_hoa(std::cout, paut->ks, "k"); + } return return_value; } diff --git a/src/tests/parseaut.test b/src/tests/parseaut.test index 7402bc9a0..22cdef25e 100755 --- a/src/tests/parseaut.test +++ b/src/tests/parseaut.test @@ -360,11 +360,11 @@ EOF expecterr input <input<input<