diff --git a/README b/README index 53a53e167..fcd48be58 100644 --- a/README +++ b/README @@ -174,6 +174,7 @@ bench/ Benchmarks for ... ltlclasses/ ... translation of more classes of LTL formulae, spin13/ ... compositional suspension and other improvements, wdba/ ... WDBA minimization (for obligation properties). + stutter/ ... stutter-invariance checking algorithms wrap/ Wrappers for other languages. python/ Python bindings for Spot and BuDDy tests/ Tests for these bindings diff --git a/bench/Makefile.am b/bench/Makefile.am index 073f5f73e..406c4511a 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -19,4 +19,4 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat +SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat stutter diff --git a/bench/stutter/Makefile.am b/bench/stutter/Makefile.am new file mode 100644 index 000000000..79db00164 --- /dev/null +++ b/bench/stutter/Makefile.am @@ -0,0 +1,31 @@ +## -*- coding: utf-8 -*- +## Copyright (C) 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 . + +SUBDIRS = . + +AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \ + -I$(top_builddir)/lib -I$(top_srcdir)/lib +AM_CXXFLAGS = $(WARNING_CXXFLAGS) +LDADD = $(top_builddir)/src/bin/libcommon.a ../../lib/libgnu.la ../../src/libspot.la + +bin_PROGRAMS = stutter_invariance_randomgraph \ + stutter_invariance_formulas + +stutter_invariance_randomgraph_SOURCES = stutter_invariance_randomgraph.cc +stutter_invariance_formulas_SOURCES = stutter_invariance_formulas.cc diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc new file mode 100644 index 000000000..b90d49ff2 --- /dev/null +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -0,0 +1,128 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 "bin/common_sys.hh" +#include "bin/common_setup.hh" +#include "bin/common_finput.hh" +#include "bin/common_output.hh" +#include "tgbaalgos/translate.hh" +#include "tgbaalgos/stutter_invariance.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/apcollect.hh" +#include "ltlvisit/length.hh" +#include "misc/timer.hh" +#include +#include "error.h" + +#include "tgbaalgos/closure.hh" +#include "tgbaalgos/stutterize.hh" +#include "tgbaalgos/dotty.hh" +#include "tgba/tgbaproduct.hh" + +static unsigned n = 10; + +const char argp_program_doc[] =""; + +const struct argp_child children[] = + { + { &finput_argp, 0, 0, 1 }, + { &output_argp, 0, 0, -20 }, + { &misc_argp, 0, 0, -1 }, + { 0, 0, 0, 0 } + }; + +namespace +{ + class stut_processor: public job_processor + { + public: + spot::translator& trans; + std::string formula; + + stut_processor(spot::translator& trans) : trans(trans) + { + } + + int + process_string(const std::string& input, + const char* filename, int linenum) + { + formula = input; + return job_processor::process_string(input, filename, linenum); + } + + int + process_formula(const spot::ltl::formula* f, + const char*, int) + { + const spot::ltl::formula* nf = + spot::ltl::unop::instance(spot::ltl::unop::Not, + f->clone()); + spot::const_tgba_digraph_ptr a = trans.run(f); + spot::const_tgba_digraph_ptr na = trans.run(nf); + spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f); + bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a); + bool res; + bool prev = true; + for (char algo = '1'; algo <= '8'; ++algo) + { + // set SPOT_STUTTER_CHECK environment variable + char algostr[2] = { 0 }; + algostr[0] = algo; + setenv("SPOT_STUTTER_CHECK", algostr, true); + + spot::stopwatch sw; + sw.start(); + for (unsigned i = 0; i < n; ++i) + res = spot::is_stutter_invariant(a, na, apdict); + const double time = sw.stop(); + + std::cout << formula << ", " << algo << ", " << ap->size() << ", " + << a->num_states() << ", " << res << ", " << time << std::endl; + + if (algo > '1') + assert(res == prev); + prev = res; + } + f->destroy(); + nf->destroy(); + delete(ap); + return 0; + } + }; +} + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { 0, 0, "[FILENAME[/COL]...]", + argp_program_doc, children, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) + exit(err); + + spot::translator trans; + stut_processor processor(trans); + if (processor.run()) + return 2; + + return 0; +} diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc new file mode 100644 index 000000000..c479db5b2 --- /dev/null +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -0,0 +1,100 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 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 "misc/timer.hh" +#include "ltlast/atomic_prop.hh" +#include "tgbaalgos/dtgbacomp.hh" +#include "tgbaalgos/stutter_invariance.hh" +#include "tgbaalgos/randomgraph.hh" +#include "tgbaalgos/dotty.hh" +#include "tgbaalgos/product.hh" +#include "tgbaalgos/stutterize.hh" +#include "tgbaalgos/closure.hh" +#include "tgba/tgbagraph.hh" +#include "tgba/bdddict.hh" +#include +#include +#include + +int +main() +{ + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::tgba_digraph_ptr a; + spot::tgba_digraph_ptr na; + unsigned n = 10; + for (unsigned states_n = 1; states_n <= 50; ++states_n) + for (float d = 0; d <= 1; d += 0.1) + { + for (unsigned props_n = 1; props_n <= 4; ++props_n) + { + // random ap set + auto ap = new spot::ltl::atomic_prop_set(); + spot::ltl::default_environment& e = + spot::ltl::default_environment::instance(); + for (unsigned i = 1; i < props_n; ++i) + { + std::ostringstream p; + p << 'p' << i; + ap->insert(static_cast + (e.require(p.str()))); + } + + // ap set as bdd + bdd apdict = bddtrue; + for (auto& i: *ap) + apdict &= bdd_ithvar(dict->register_proposition(i, a)); + + // generate n random automata + typedef std::pair + aut_pair_t; + std::vector vec; + for (unsigned i = 0; i < n; ++i) + { + a = spot::random_graph(states_n, d, ap, dict, 2, 0.1, 0.5, + true); + na = spot::dtgba_complement(a); + vec.push_back(aut_pair_t(a, na)); + } + + for (char algo = '1'; algo <= '8'; ++algo) + { + // set SPOT_STUTTER_CHECK environment variable + char algostr[2] = { 0 }; + algostr[0] = algo; + setenv("SPOT_STUTTER_CHECK", algostr, true); + + spot::stopwatch sw; + sw.start(); + bool res; + for (auto& a: vec) + res = spot::is_stutter_invariant(a.first, a.second, apdict); + const double time = sw.stop(); + + std::cout << algo << ", " << props_n << ", " << states_n + << ", " << res << ", " << time << std::endl; + } + spot::ltl::destroy_atomic_prop_set(*ap); + delete(ap); + } + } + + + return 0; +} diff --git a/configure.ac b/configure.ac index 9436f3275..582f06632 100644 --- a/configure.ac +++ b/configure.ac @@ -164,6 +164,7 @@ AC_CONFIG_FILES([ bench/ltl2tgba/defs bench/spin13/Makefile bench/wdba/Makefile + bench/stutter/Makefile doc/Doxyfile doc/Makefile doc/tl/Makefile diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 71e302ad6..954872306 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -45,6 +45,7 @@ #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/safety.hh" +#include "tgbaalgos/stutter_invariance.hh" const char argp_program_doc[] ="\ Read a list of formulas and output them back after some optional processing.\v\ @@ -550,8 +551,7 @@ namespace matched &= !implied_by || simpl.implication(implied_by, f); matched &= !imply || simpl.implication(f, imply); matched &= !equivalent_to || simpl.are_equivalent(f, equivalent_to); - matched &= !stutter_insensitive || (f->is_ltl_formula() - && is_stutter_insensitive(f)); + matched &= !stutter_insensitive || spot::is_stutter_invariant(f); // Match obligations and subclasses using WDBA minimization. // Because this is costly, we compute it later, so that we don't @@ -609,8 +609,6 @@ main(int argc, char** argv) if (jobs.empty()) jobs.emplace_back("-", 1); - // --stutter-insensitive implies --ltl - ltl |= stutter_insensitive; if (boolean_to_isop && simplification_level == 0) simplification_level = 1; spot::ltl::ltl_simplifier_options opt = simplifier_options(); diff --git a/src/ltlvisit/remove_x.cc b/src/ltlvisit/remove_x.cc index 4b44aa2d0..f186e3c0c 100644 --- a/src/ltlvisit/remove_x.cc +++ b/src/ltlvisit/remove_x.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -117,18 +117,5 @@ namespace spot remove_x_visitor v(f); return v.recurse(f); } - - bool is_stutter_insensitive(const formula* f) - { - assert(f->is_ltl_formula()); - if (f->is_X_free()) - return true; - const formula* g = remove_x(f); - ltl_simplifier ls; - bool res = ls.are_equivalent(f, g); - g->destroy(); - return res; - } - } } diff --git a/src/ltlvisit/remove_x.hh b/src/ltlvisit/remove_x.hh index a7d1039af..87a0b243b 100644 --- a/src/ltlvisit/remove_x.hh +++ b/src/ltlvisit/remove_x.hh @@ -48,27 +48,6 @@ namespace spot \endverbatim */ SPOT_API const formula* remove_x(const formula* f); - - /// \brief Whether an LTL formula \a f is stutter-insensitive. - /// - /// This is simply achieved by checking whether the output of - /// remove_x(f) is equivalent to \a f. This only - /// works for LTL formulas, not PSL formulas. - /// - /** \verbatim - @Article{ etessami.00.ipl, - author = {Kousha Etessami}, - title = {A note on a question of {P}eled and {W}ilke regarding - stutter-invariant {LTL}}, - journal = {Information Processing Letters}, - volume = {75}, - number = {6}, - year = {2000}, - pages = {261--263} - } - \endverbatim */ - SPOT_API - bool is_stutter_insensitive(const formula* f); } } diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index a71091724..678b5b202 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -37,7 +37,8 @@ tgba_HEADERS = \ tgbamask.hh \ tgbaproxy.hh \ tgbaproduct.hh \ - tgbasafracomplement.hh + tgbasafracomplement.hh \ + tgbasl.hh noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ @@ -50,4 +51,5 @@ libtgba_la_SOURCES = \ tgbaproduct.cc \ tgbamask.cc \ tgbaproxy.cc \ - tgbasafracomplement.cc + tgbasafracomplement.cc \ + tgbasl.cc diff --git a/src/tgba/tgbasl.cc b/src/tgba/tgbasl.cc new file mode 100644 index 000000000..12a8141b1 --- /dev/null +++ b/src/tgba/tgbasl.cc @@ -0,0 +1,234 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012, 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 "tgbasl.hh" +#include "bddprint.hh" + +namespace spot +{ + namespace + { + class state_tgbasl: public state + { + public: + state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond) + { + } + + virtual + ~state_tgbasl() + { + s_->destroy(); + } + + virtual int + compare(const state* other) const + { + const state_tgbasl* o = + down_cast(other); + assert(o); + int res = s_->compare(o->real_state()); + if (res != 0) + return res; + return cond_.id() - o->cond_.id(); + } + + virtual size_t + hash() const + { + return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id()); + } + + virtual + state_tgbasl* clone() const + { + return new state_tgbasl(*this); + } + + state* + real_state() const + { + return s_; + } + + bdd + cond() const + { + return cond_; + } + + private: + state* s_; + bdd cond_; + }; + + class tgbasl_succ_iterator : public tgba_succ_iterator + { + public: + tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state, + bdd_dict_ptr d, bdd atomic_propositions) + : it_(it), state_(state), aps_(atomic_propositions), d_(d) + { + } + + virtual + ~tgbasl_succ_iterator() + { + delete it_; + } + + // iteration + + bool + first() + { + loop_ = false; + done_ = false; + need_loop_ = true; + if (it_->first()) + { + cond_ = it_->current_condition(); + next_edge(); + } + return true; + } + + bool + next() + { + if (cond_ != bddfalse) + { + next_edge(); + return true; + } + if (!it_->next()) + { + if (loop_ || !need_loop_) + done_ = true; + loop_ = true; + return !done_; + } + else + { + cond_ = it_->current_condition(); + next_edge(); + return true; + } + } + + bool + done() const + { + return it_->done() && done_; + } + + // inspection + + state_tgbasl* + current_state() const + { + if (loop_) + return new state_tgbasl(state_->real_state(), state_->cond()); + return new state_tgbasl(it_->current_state(), one_); + } + + bdd + current_condition() const + { + if (loop_) + return state_->cond(); + return one_; + } + + acc_cond::mark_t + current_acceptance_conditions() const + { + if (loop_) + return 0U; + return it_->current_acceptance_conditions(); + } + + private: + void + next_edge() + { + one_ = bdd_satoneset(cond_, aps_, bddtrue); + cond_ -= one_; + if (need_loop_ && (state_->cond() == one_) + && (state_ == it_->current_state())) + need_loop_ = false; + } + + tgba_succ_iterator* it_; + const state_tgbasl* state_; + bdd cond_; + bdd one_; + bdd aps_; + bdd_dict_ptr d_; + bool loop_; + bool need_loop_; + bool done_; + }; + } + + tgbasl::tgbasl(const const_tgba_ptr& a, bdd atomic_propositions) + : tgba(a->get_dict()), a_(a), aps_(atomic_propositions) + { + auto d = get_dict(); + d->register_all_propositions_of(&a_, this); + assert(acc_.num_sets() == 0); + acc_.add_sets(a_->acc().num_sets()); + } + + tgbasl::~tgbasl() + { + get_dict()->unregister_all_my_variables(this); + } + + state* + tgbasl::get_init_state() const + { + return new state_tgbasl(a_->get_init_state(), bddfalse); + } + + tgba_succ_iterator* + tgbasl::succ_iter(const state* state) const + { + const state_tgbasl* s = down_cast(state); + assert(s); + return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s, + a_->get_dict(), aps_); + } + + bdd + tgbasl::compute_support_conditions(const state*) const + { + return bddtrue; + } + + std::string + tgbasl::format_state(const state* state) const + { + const state_tgbasl* s = down_cast(state); + assert(s); + return (a_->format_state(s->real_state()) + + ", " + + bdd_format_formula(a_->get_dict(), s->cond())); + } +} diff --git a/src/tgba/tgbasl.hh b/src/tgba/tgbasl.hh new file mode 100644 index 000000000..dc5040917 --- /dev/null +++ b/src/tgba/tgbasl.hh @@ -0,0 +1,49 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2013, 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 . + +#ifndef SPOT_TGBA_TGBASL_HH +# define SPOT_TGBA_TGBASL_HH + +#include "tgba.hh" + +namespace spot +{ + class SPOT_API tgbasl : public tgba + { + public: + tgbasl(const const_tgba_ptr& a, bdd ap); + + virtual ~tgbasl(); + + virtual state* get_init_state() const; + + virtual tgba_succ_iterator* succ_iter(const state* state) const; + + virtual std::string format_state(const state* state) const; + + protected: + virtual bdd compute_support_conditions(const state* state) const; + + private: + const_tgba_ptr a_; + bdd aps_; + }; +} + +#endif diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 095334fb4..314f193eb 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos tgbaalgos_HEADERS = \ bfssteps.hh \ + closure.hh \ complete.hh \ compsusp.hh \ cycles.hh \ @@ -69,6 +70,8 @@ tgbaalgos_HEADERS = \ simulation.hh \ stats.hh \ stripacc.hh \ + stutter_invariance.hh \ + stutterize.hh \ tau03.hh \ tau03opt.hh \ translate.hh \ @@ -77,6 +80,7 @@ tgbaalgos_HEADERS = \ noinst_LTLIBRARIES = libtgbaalgos.la libtgbaalgos_la_SOURCES = \ bfssteps.cc \ + closure.cc \ complete.cc \ compsusp.cc \ cycles.cc \ @@ -117,6 +121,8 @@ libtgbaalgos_la_SOURCES = \ simulation.cc \ stats.cc \ stripacc.cc \ + stutter_invariance.cc \ + stutterize.cc \ tau03.cc \ tau03opt.cc \ translate.cc \ diff --git a/src/tgbaalgos/closure.cc b/src/tgbaalgos/closure.cc new file mode 100644 index 000000000..83ed4fffe --- /dev/null +++ b/src/tgbaalgos/closure.cc @@ -0,0 +1,121 @@ +// Copyright (C) 2014 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 . + + +#include +#include +#include "closure.hh" +#include "dupexp.hh" + +namespace spot +{ + namespace + { + struct transition + { + unsigned dst; + acc_cond::mark_t acc; + transition(unsigned dst, acc_cond::mark_t acc) : + dst(dst), acc(acc) + { + } + }; + + struct transition_hash + { + size_t + operator()(const transition& t) const + { + return wang32_hash(t.dst) ^ wang32_hash(t.acc); + } + }; + + struct transition_equal + { + bool + operator()(const transition& left, const transition& right) const + { + return left.dst == right.dst + && left.acc == right.acc; + } + }; + + typedef std::unordered_map tmap_t; + typedef std::set tset_t; + } + + tgba_digraph_ptr + closure(const const_tgba_digraph_ptr& a) + { + tgba_digraph_ptr res = tgba_dupexp_dfs(a); + unsigned n = res->num_states(); + tset_t todo; + + for (unsigned state = 0; state < n; ++state) + { + tmap_t uniq; + auto trans = res->out(state); + + for (auto it = trans.begin(); it != trans.end(); ++it) + { + todo.insert(it.trans()); + uniq.emplace(transition(it->dst, it->acc), it.trans()); + } + + while (!todo.empty()) + { + unsigned t1 = *todo.begin(); + todo.erase(t1); + tgba_graph_trans_data td = res->trans_data(t1); + unsigned dst = res->trans_storage(t1).dst; + + for (auto& t2 : res->out(dst)) + { + bdd cond = td.cond & t2.cond; + if (cond != bddfalse) + { + acc_cond::mark_t acc = td.acc | t2.acc; + transition jump(t2.dst, acc); + unsigned i; + auto u = uniq.find(jump); + + if (u == uniq.end()) + { + i = res->new_transition(state, t2.dst, cond, acc); + uniq.emplace(jump, i); + todo.insert(i); + } + + else + { + bdd old_cond = res->trans_data(u->second).cond; + if (!bdd_implies(cond, old_cond)) + { + res->trans_data(u->second).cond = cond | old_cond; + todo.insert(u->second); + } + } + } + } + } + uniq.clear(); + } + return res; + } +} diff --git a/src/tgbaalgos/closure.hh b/src/tgbaalgos/closure.hh new file mode 100644 index 000000000..c51fbfb3d --- /dev/null +++ b/src/tgbaalgos/closure.hh @@ -0,0 +1,31 @@ +// Copyright (C) 2014 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_TGBAALGOS_CLOSURE_HH +# define SPOT_TGBAALGOS_CLOSURE_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + SPOT_API tgba_digraph_ptr + closure(const const_tgba_digraph_ptr&); +} + +#endif diff --git a/src/tgbaalgos/stutter_invariance.cc b/src/tgbaalgos/stutter_invariance.cc new file mode 100644 index 000000000..d19aa8b1a --- /dev/null +++ b/src/tgbaalgos/stutter_invariance.cc @@ -0,0 +1,126 @@ +// Copyright (C) 2014 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 . + + +#include +#include "tgba/tgbagraph.hh" +#include "closure.hh" +#include "stutterize.hh" +#include "ltlvisit/remove_x.hh" +#include "tgbaalgos/translate.hh" +#include "ltlast/allnodes.hh" +#include "ltlvisit/apcollect.hh" +#include "stutter_invariance.hh" +#include "tgba/tgbasl.hh" +#include "tgba/tgbaproduct.hh" +#include "tgbaalgos/dupexp.hh" + +namespace spot +{ + bool + is_stutter_invariant(const ltl::formula* f) + { + const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); + char algo = stutter_check ? stutter_check[0] : '1'; + if (f->is_ltl_formula() && f->is_X_free()) + return true; + + if (algo == '0') + { + // Syntactic checking. + if (f->is_ltl_formula()) + { + const ltl::formula* g = remove_x(f); + ltl::ltl_simplifier ls; + bool res = ls.are_equivalent(f, g); + g->destroy(); + return res; + } + else + { + throw std::runtime_error("Cannot use the syntactic-based " \ + "approach to stutter-invariance " \ + "checking on non-ltl formula"); + } + } + const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone()); + translator trans; + auto aut_f = trans.run(f); + auto aut_nf = trans.run(nf); + bdd aps = atomic_prop_collect_as_bdd(f, aut_f); + nf->destroy(); + return is_stutter_invariant(aut_f, aut_nf, aps); + } + + bool + is_stutter_invariant(const const_tgba_digraph_ptr& aut_f, + const const_tgba_digraph_ptr& aut_nf, bdd aps) + { + const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); + char algo = stutter_check ? stutter_check[0] : '8'; + + switch (algo) + { + // sl(aut_f) x sl(aut_nf) + case '1': + { + return product(sl(aut_f, aps), sl(aut_nf, aps))->is_empty(); + } + // sl(cl(aut_f)) x aut_nf + case '2': + { + return product(sl(closure(aut_f), aps), aut_nf)->is_empty(); + } + // (cl(sl(aut_f)) x aut_nf + case '3': + { + return product(closure(sl(aut_f, aps)), aut_nf)->is_empty(); + } + // sl2(aut_f) x sl2(aut_nf) + case '4': + { + return product(sl2(aut_f, aps), sl2(aut_nf, aps))->is_empty(); + } + // sl2(cl(aut_f)) x aut_nf + case '5': + { + return product(sl2(closure(aut_f), aps), aut_nf)->is_empty(); + } + // (cl(sl2(aut_f)) x aut_nf + case '6': + { + return product(closure(sl2(aut_f, aps)), aut_nf)->is_empty(); + } + // on-the-fly sl(aut_f) x sl(aut_nf) + case '7': + { + auto slf = std::make_shared(aut_f, aps); + auto slnf = std::make_shared(aut_nf, aps); + return product(slf, slnf)->is_empty(); + } + // cl(aut_f) x cl(aut_nf) + case '8': + { + return product(closure(aut_f), closure(aut_nf))->is_empty(); + } + default: + throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); + break; + } + } +} diff --git a/src/tgbaalgos/stutter_invariance.hh b/src/tgbaalgos/stutter_invariance.hh new file mode 100644 index 000000000..a5efee93b --- /dev/null +++ b/src/tgbaalgos/stutter_invariance.hh @@ -0,0 +1,36 @@ +// Copyright (C) 2014 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_TGBAALGOS_STUTTER_INVARIANCE_HH +# define SPOT_TGBAALGOS_STUTTER_INVARIANCE_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + // TODO doc + SPOT_API bool + is_stutter_invariant(const ltl::formula* f); + + SPOT_API bool + is_stutter_invariant(const const_tgba_digraph_ptr& aut_f, + const const_tgba_digraph_ptr& aut_nf, bdd aps); +} + +#endif diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc new file mode 100644 index 000000000..24ae54211 --- /dev/null +++ b/src/tgbaalgos/stutterize.cc @@ -0,0 +1,170 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 "stutterize.hh" +#include "tgba/tgba.hh" +#include "dupexp.hh" +#include "misc/hash.hh" +#include "misc/hashfunc.hh" +#include "ltlvisit/apcollect.hh" +#include +#include +#include +#include + +namespace spot +{ + namespace + { + typedef std::pair stutter_state; + + struct stutter_state_hash + { + size_t + operator()(const stutter_state& s) const + { + return wang32_hash(s.first) ^ wang32_hash(s.second.id()); + } + }; + + // Associate the stutter state to its number. + typedef std::unordered_map ss2num_map; + + // Queue of state to be processed. + typedef std::deque queue_t; + } + + tgba_digraph_ptr + sl(const const_tgba_digraph_ptr& a, const ltl::formula* f) + { + bdd aps = atomic_prop_collect_as_bdd(f, a); + return sl(a, aps); + } + + tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f) + { + bdd aps = atomic_prop_collect_as_bdd(f, a); + return sl2(a, aps); + } + + tgba_digraph_ptr + sl(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + { + // The result automaton uses numbered states. + tgba_digraph_ptr res = make_tgba_digraph(a->get_dict()); + // We use the same BDD variables as the input. + res->copy_ap_of(a); + res->copy_acceptance_conditions_of(a); + // These maps make it possible to convert stutter_state to number + // and vice-versa. + ss2num_map ss2num; + + queue_t todo; + + unsigned s0 = a->get_init_state_number(); + stutter_state s(s0, bddfalse); + ss2num[s] = 0; + res->new_state(); + todo.push_back(s); + + while (!todo.empty()) + { + s = todo.front(); + todo.pop_front(); + unsigned src = ss2num[s]; + + bool self_loop_needed = true; + + for (auto& t : a->out(s.first)) + { + bdd all = t.cond; + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); + all -= one; + + stutter_state d(t.dst, one); + + auto r = ss2num.emplace(d, ss2num.size()); + unsigned dest = r.first->second; + + if (r.second) + { + todo.push_back(d); + unsigned u = res->new_state(); + assert(u == dest); + (void)u; + } + + // Create the transition. + res->new_transition(src, dest, one, t.acc); + + if (src == dest) + self_loop_needed = false; + } + } + + if (self_loop_needed && s.second != bddfalse) + res->new_transition(src, src, s.second, 0U); + } + res->merge_transitions(); + return res; + } + + tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + { + tgba_digraph_ptr res = tgba_dupexp_dfs(a); + unsigned num_states = res->num_states(); + for (unsigned state = 0; state < num_states; ++state) + { + std::vector out; + auto trans = res->out(state); + + for (auto it = trans.begin(); it != trans.end(); ++it) + out.push_back(it.trans()); + for (auto it: out) + { + if (res->trans_storage(it).dst != state) + { + bdd all = res->trans_storage(it).cond; + while (all != bddfalse) + { + unsigned dst = res->trans_storage(it).dst; + bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); + unsigned tmp = res->new_state(); + res->new_transition(state, tmp, one, + res->trans_storage(it).acc); + res->new_transition(tmp, tmp, one, 0U); + res->new_transition(tmp, dst, one, + res->trans_storage(it).acc); + all -= one; + } + } + } + } + res->merge_transitions(); + return res; + } +} diff --git a/src/tgbaalgos/stutterize.hh b/src/tgbaalgos/stutterize.hh new file mode 100644 index 000000000..93de1aa70 --- /dev/null +++ b/src/tgbaalgos/stutterize.hh @@ -0,0 +1,43 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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_TGBAALGOS_STUTTERIZE_HH +# define SPOT_TGBAALGOS_STUTTERIZE_HH + +#include "tgba/tgbagraph.hh" + +namespace spot +{ + SPOT_API tgba_digraph_ptr + sl(const const_tgba_digraph_ptr&, const ltl::formula*); + + SPOT_API tgba_digraph_ptr + sl(const const_tgba_digraph_ptr&, bdd); + + SPOT_API tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr&, const ltl::formula*); + + SPOT_API tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr&, bdd); +} + +#endif diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 13cf35a0a..e2cefcdb4 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -121,6 +121,7 @@ TESTS = \ emptchk.test \ emptchke.test \ dfs.test \ + stutter_invariant.test \ ltlcrossce.test \ emptchkr.test \ ltlcounter.test \ diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index de4ee4e48..9329fc946 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -69,6 +69,8 @@ #include "tgbaalgos/complete.hh" #include "tgbaalgos/dtbasat.hh" #include "tgbaalgos/dtgbasat.hh" +#include "tgbaalgos/closure.hh" +#include "tgbaalgos/stutterize.hh" #include "taalgos/tgba2ta.hh" #include "taalgos/dotty.hh" @@ -376,6 +378,8 @@ checked_main(int argc, char** argv) bool reject_bigger = false; bool opt_monitor = false; bool containment = false; + bool opt_closure = false; + bool opt_stutterize = false; bool spin_comments = false; const char* hoaf_opt = 0; spot::ltl::environment& env(spot::ltl::default_environment::instance()); @@ -790,6 +794,14 @@ checked_main(int argc, char** argv) { dupexp = BFS; } + else if (!strcmp(argv[formula_index], "-CL")) + { + opt_closure = true; + } + else if (!strcmp(argv[formula_index], "-ST")) + { + opt_stutterize = true; + } else if (!strcmp(argv[formula_index], "-t")) { output = 6; @@ -1395,6 +1407,16 @@ checked_main(int argc, char** argv) } } + if (opt_closure) + { + a = closure(ensure_digraph(a)); + } + + if (opt_stutterize) + { + a = sl(ensure_digraph(a), f); + } + if (opt_monitor) { tm.start("Monitor minimization"); diff --git a/src/tgbatest/stutter_invariant.test b/src/tgbatest/stutter_invariant.test new file mode 100755 index 000000000..4c0a8d348 --- /dev/null +++ b/src/tgbatest/stutter_invariant.test @@ -0,0 +1,47 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2008, 2009, 2010, 2014 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de +# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +# Université Pierre et Marie Curie. +# +# 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 + +check_stutter() +{ + FORMULAS=$1 + SPOT_STUTTER_CHECK=$2 + run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >exp + for i in `seq $3 $4` + do + SPOT_STUTTER_CHECK=$i + run 0 ../../bin/ltlfilt --stutter-invariant -F $FORMULAS >out + diff out exp + done +} + +cat >ltl <