diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index d0eb7fe68..e84815433 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -21,8 +21,8 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc -mc_HEADERS = reachability.hh intersect.hh lpar13.hh unionfind.hh utils.hh\ - mc.hh mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh +mc_HEADERS = intersect.hh lpar13.hh unionfind.hh utils.hh mc.hh\ + mc_instanciator.hh deadlock.hh bloemen.hh bloemen_ec.hh cndfs.hh noinst_LTLIBRARIES = libmc.la diff --git a/spot/mc/reachability.hh b/spot/mc/reachability.hh deleted file mode 100644 index 53d82e728..000000000 --- a/spot/mc/reachability.hh +++ /dev/null @@ -1,126 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2019 Laboratoire de Recherche et -// Developpement de l'Epita -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#pragma once - -#include - -namespace spot -{ - /// \brief This template class provide a sequential reachability - /// of a kripkecube. The algorithm uses a single DFS since it - /// is the most efficient in a sequential setting - template - class SPOT_API seq_reach_kripke - { - public: - seq_reach_kripke(kripkecube& sys, unsigned tid): - sys_(sys), tid_(tid) - { - static_assert(spot::is_a_kripkecube_ptr::value, - "error: does not match the kripkecube requirements"); - visited.reserve(2000000); - todo.reserve(100000); - } - - ~seq_reach_kripke() - { - // States will be destroyed by the system, so just clear map - visited.clear(); - } - - Visitor& self() - { - return static_cast(*this); - } - - void run() - { - self().setup(); - State initial = sys_.initial(tid_); - if (SPOT_LIKELY(self().push(initial, dfs_number))) - { - todo.push_back({initial, sys_.succ(initial, tid_)}); - visited[initial] = ++dfs_number; - } - while (!todo.empty()) - { - if (todo.back().it->done()) - { - if (SPOT_LIKELY(self().pop(todo.back().s))) - { - sys_.recycle(todo.back().it, tid_); - todo.pop_back(); - } - } - else - { - ++transitions; - State dst = todo.back().it->state(); - auto it = visited.insert({dst, dfs_number+1}); - if (it.second) - { - ++dfs_number; - if (SPOT_LIKELY(self().push(dst, dfs_number))) - { - todo.back().it->next(); - todo.push_back({dst, sys_.succ(dst, tid_)}); - } - } - else - { - self().edge(visited[todo.back().s], visited[dst]); - todo.back().it->next(); - } - } - } - self().finalize(); - } - - unsigned int states() - { - return dfs_number; - } - - unsigned int trans() - { - return transitions; - } - - protected: - struct todo_element - { - State s; - SuccIterator* it; - }; - kripkecube& sys_; - std::vector todo; - // FIXME: The system already handle a set of visited states so - // this map is redundant: an we avoid this new map? - typedef std::unordered_map visited_map; - visited_map visited; - unsigned int dfs_number = 0; - unsigned int transitions = 0; - unsigned int tid_; - }; -} diff --git a/spot/mc/utils.hh b/spot/mc/utils.hh index 8ffdc6831..9f80c8764 100644 --- a/spot/mc/utils.hh +++ b/spot/mc/utils.hh @@ -19,86 +19,149 @@ #pragma once -#include #include #include #include namespace spot { + /// \brief convert a (cube) model into a twa. + /// Note that this algorithm cannot be run in parallel but could. template - class SPOT_API kripke_to_twa : - public seq_reach_kripke> + class SPOT_API kripkecube_to_twa { public: - kripke_to_twa(kripkecube& sys, bdd_dict_ptr dict) - : seq_reach_kripke>(sys), - dict_(dict) - {} - ~kripke_to_twa() - { - } + kripkecube_to_twa(kripkecube& sys, bdd_dict_ptr dict): + sys_(sys), dict_(dict) + { + static_assert(spot::is_a_kripkecube_ptr::value, + "error: does not match the kripkecube requirements"); + } + + ~kripkecube_to_twa() + { + visited_.clear(); + } + + void run() + { + setup(); + State initial = sys_.initial(0); + if (SPOT_LIKELY(push(initial, dfs_number_+1))) + { + visited_[initial] = dfs_number_++; + todo_.push_back({initial, sys_.succ(initial, 0)}); + } + while (!todo_.empty()) + { + if (todo_.back().it->done()) + { + if (SPOT_LIKELY(pop(todo_.back().s))) + { + sys_.recycle(todo_.back().it, 0); + todo_.pop_back(); + } + } + else + { + ++transitions_; + State dst = todo_.back().it->state(); + auto it = visited_.find(dst); + if (it == visited_.end()) + { + if (SPOT_LIKELY(push(dst, dfs_number_+1))) + { + visited_[dst] = dfs_number_++; + todo_.back().it->next(); + todo_.push_back({dst, sys_.succ(dst, 0)}); + } + } + else + { + edge(visited_[todo_.back().s], visited_[dst]); + todo_.back().it->next(); + } + } + } + finalize(); + } void setup() { - res_ = make_twa_graph(dict_); - names_ = new std::vector(); + auto d = spot::make_bdd_dict(); + res_ = make_twa_graph(d); + names_ = new std::vector(); - // padding to simplify computation. - res_->new_state(); - - // Compute the reverse binder. - auto aps = this->sys_.ap(); - for (unsigned i = 0; i < aps.size(); ++i) - { - auto k = res_->register_ap(aps[i]); - reverse_binder_.insert({i, k}); - } + int i = 0; + for (auto ap : sys_.ap()) + { + auto idx = res_->register_ap(ap); + reverse_binder_[i++] = idx; + } } - void push(State s, unsigned i) + bool push(State s, unsigned i) { + unsigned st = res_->new_state(); - names_->push_back(this->sys_.to_string(s)); - SPOT_ASSERT(st == i); + names_->push_back(sys_.to_string(s)); + if (!todo_.empty()) + { + edge(visited_[todo_.back().s], st); + } + + SPOT_ASSERT(st+1 == i); + return true; + } + + bool pop(State) + { + return true; } void edge(unsigned src, unsigned dst) { - cubeset cs(this->sys_.ap().size()); - bdd cond = cube_to_bdd(this->todo.back().it->condition(), - cs, reverse_binder_); - res_->new_edge(src, dst, cond); + cubeset cs(sys_.ap().size()); + bdd cond = cube_to_bdd(todo_.back().it->condition(), + cs, reverse_binder_); + res_->new_edge(src, dst, cond); } void finalize() { - res_->set_init_state(1); - res_->purge_unreachable_states(); - res_->set_named_prop>("state-names", names_); + res_->purge_unreachable_states(); + res_->set_named_prop>("state-names", names_); } twa_graph_ptr twa() { - return res_; + return res_; } - private: + protected: + struct todo__element + { + State s; + SuccIterator* it; + }; + + typedef std::unordered_map visited__map; + + kripkecube& sys_; + std::vector todo_; + visited__map visited_; + unsigned int dfs_number_ = 0; + unsigned int transitions_ = 0; spot::twa_graph_ptr res_; std::vector* names_; bdd_dict_ptr dict_; std::unordered_map reverse_binder_; }; - - /// \brief convert a (cube) product automaton into a twa /// Note that this algorithm cannot be run in parallel. templatepurge_unreachable_states(); res_->set_named_prop>("state-names", names_); return res_; } @@ -228,7 +293,7 @@ namespace spot names_ = new std::vector(); int i = 0; - for (auto ap : this->twa_->ap()) + for (auto ap : sys_.ap()) { auto idx = res_->register_ap(ap); reverse_binder_[i++] = idx; @@ -237,24 +302,25 @@ namespace spot bool push_state(product_state s, unsigned i, acc_cond::mark_t) { - // push also implies edge (when it's not the initial state) - if (this->todo_.size()) - { - auto c = this->twa_->get_cubeset() - .intersection(this->twa_->trans_data - (this->todo_.back().it_prop).cube_, - this->todo_.back().it_kripke->condition()); + unsigned st = res_->new_state(); - bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(), + if (!todo_.empty()) + { + auto c = twa_->get_cubeset() + .intersection(twa_->trans_data + (todo_.back().it_prop).cube_, + todo_.back().it_kripke->condition()); + + bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(), reverse_binder_); - this->twa_->get_cubeset().release(c); - res_->new_edge(this->map[this->todo_.back().st]-1, i-1, x, - this->twa_->trans_data - (this->todo_.back().it_prop).acc_); + twa_->get_cubeset().release(c); + res_->new_edge(map[todo_.back().st]-1, st, x, + twa_->trans_data + (todo_.back().it_prop).acc_); } - unsigned st = res_->new_state(); - names_->push_back(this->sys_.to_string(s.st_kripke) + + + names_->push_back(sys_.to_string(s.st_kripke) + ('*' + std::to_string(s.st_prop))); SPOT_ASSERT(st+1 == i); return true; @@ -264,14 +330,14 @@ namespace spot product_state, unsigned dst, acc_cond::mark_t cond) { - auto c = this->twa_->get_cubeset() - .intersection(this->twa_->trans_data - (this->todo_.back().it_prop).cube_, - this->todo_.back().it_kripke->condition()); + auto c = twa_->get_cubeset() + .intersection(twa_->trans_data + (todo_.back().it_prop).cube_, + todo_.back().it_kripke->condition()); - bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(), + bdd x = spot::cube_to_bdd(c, twa_->get_cubeset(), reverse_binder_); - this->twa_->get_cubeset().release(c); + twa_->get_cubeset().release(c); res_->new_edge(src-1, dst-1, x, cond); return false; } diff --git a/tests/Makefile.am b/tests/Makefile.am index 0d7c65816..00f8d42cd 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -458,6 +458,7 @@ EXTRA_DIST = \ if USE_LTSMIN check_PROGRAMS += ltsmin/modelcheck +check_PROGRAMS += ltsmin/testconvert ltsmin_modelcheck_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib ltsmin_modelcheck_CXXFLAGS = $(CXXFLAGS) -pthread @@ -468,19 +469,31 @@ ltsmin_modelcheck_LDADD = \ $(top_builddir)/spot/libspot.la \ $(top_builddir)/spot/ltsmin/libspotltsmin.la +ltsmin_testconvert_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) \ + $(BUDDY_CPPFLAGS) \-I$(top_builddir)/lib -I$(top_srcdir)/lib +ltsmin_testconvert_CXXFLAGS = $(CXXFLAGS) -pthread +ltsmin_testconvert_SOURCES = ltsmin/testconvert.cc +ltsmin_testconvert_LDADD = \ + $(top_builddir)/bin/libcommon.a \ + $(top_builddir)/lib/libgnu.la \ + $(top_builddir)/spot/libspot.la \ + $(top_builddir)/spot/ltsmin/libspotltsmin.la + + check_SCRIPTS += ltsmin/defs ltsmin/defs: $(top_builddir)/config.status $(srcdir)/core/defs.in $(top_builddir)/config.status --file ltsmin/defs:core/defs.in -TESTS_ltsmin = \ - ltsmin/check.test \ - ltsmin/check2.test \ - ltsmin/check3.test \ - ltsmin/finite.test \ +TESTS_ltsmin = \ + ltsmin/check.test \ + ltsmin/check2.test \ + ltsmin/check3.test \ + ltsmin/finite.test \ ltsmin/finite2.test \ ltsmin/finite3.test \ - ltsmin/kripke.test + ltsmin/kripke.test \ + ltsmin/testconvert.test EXTRA_DIST += ltsmin/beem-peterson.4.dve ltsmin/beem-peterson.4.gal \ ltsmin/elevator2.1.pm ltsmin/finite.dve ltsmin/finite.pm ltsmin/finite.gal diff --git a/tests/ltsmin/.gitignore b/tests/ltsmin/.gitignore index b3518bd8b..7659746cc 100644 --- a/tests/ltsmin/.gitignore +++ b/tests/ltsmin/.gitignore @@ -1,2 +1,3 @@ defs modelcheck +testconvert diff --git a/tests/ltsmin/testconvert.cc b/tests/ltsmin/testconvert.cc new file mode 100644 index 000000000..cfd84333c --- /dev/null +++ b/tests/ltsmin/testconvert.cc @@ -0,0 +1,133 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2020 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 "config.h" +#include +#include "bin/common_conv.hh" +#include "bin/common_setup.hh" +#include "bin/common_output.hh" + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include +#include + +// FIXME (1) model (2)formula +int main(int argc, char** argv) +{ + // Build the formula + char* formula = argv[2]; + spot::formula f = nullptr; + spot::default_environment& env = spot::default_environment::instance(); + spot::atomic_prop_set ap; + spot::const_twa_graph_ptr prop = nullptr; + auto dict = spot::make_bdd_dict(); + { + auto pf = spot::parse_infix_psl(formula, env, false); + f = pf.f; + spot::translator trans(dict); + prop = trans.run(&f); + } + + atomic_prop_collect(f, &ap); + + auto propcube = spot::twa_to_twacube(prop); + + // Load model + spot::ltsmin_kripkecube_ptr modelcube = nullptr; + try + { + modelcube = spot::ltsmin_model::load(argv[1]) + .kripkecube(propcube->ap(), spot::formula::tt(), 0, 1); + } + catch (const std::runtime_error& e) + { + std::cerr << e.what() << '\n'; + } + + // ------------------------------------------------------------------ + // check that cube and bdd approaches agree for the size of the model + // ------------------------------------------------------------------ + auto result0 = + spot::ec_instanciator + (spot::mc_algorithm::REACHABILITY, modelcube, propcube, false); + std::cout << "[CUBE] Model: " + << result0.states[0] << ',' + << result0.transitions[0] + << '\n'; + + + spot::kripkecube_to_twa ktt(*modelcube, dict); + ktt.run(); + auto twa_from_model = ktt.twa(); + std::cout << "[BDD] Model: " + << twa_from_model->num_states() << ',' + << twa_from_model->num_edges() << '\n'; + + + + // ------------------------------------------------------------------ + // check that cube and bdd approaches agree for the emptiness and the + // size of the synchronous product + // ------------------------------------------------------------------ + auto result1 = + spot::ec_instanciator + (spot::mc_algorithm::BLOEMEN_EC, modelcube, propcube, false); + auto result2 = + spot::ec_instanciator + (spot::mc_algorithm::REACHABILITY, modelcube, propcube, false); + + std::cout << "[CUBE] Product: " + << result1.value[0] << ',' + << result1.states[0] << ',' + << result1.transitions[0] + << '\n'; + + spot::product_to_twa ptt(*modelcube, propcube); + ptt.run(); + auto twa_from_product = ptt.twa(); + std::cout << "[BDD] Product: " + << (twa_from_product->is_empty() ? "empty" : "not_empty") + << ',' + << twa_from_product->num_states() << ',' + << twa_from_product->num_edges() + << '\n'; +} diff --git a/tests/ltsmin/testconvert.test b/tests/ltsmin/testconvert.test new file mode 100644 index 000000000..7e925782c --- /dev/null +++ b/tests/ltsmin/testconvert.test @@ -0,0 +1,54 @@ + #! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2020 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 . + + + +. ./defs + +divine compile > output 2>&1 + +if grep -i 'ltsmin ' output; then + : +else + echo "divine not installed, or no ltsmin interface" + exit 77 +fi + +set -e + +run 0 ../testconvert $srcdir/finite.dve 'true' > output +cat << EOF > expected +[CUBE] Model: 15,24 +[BDD] Model: 15,24 +[CUBE] Product: not_empty,4,4 +[BDD] Product: not_empty,15,24 +EOF + +cmp output expected + +run 0 ../testconvert $srcdir/finite.dve 'G "P.a==5"' > output +cat << EOF > expected +[CUBE] Model: 15,24 +[BDD] Model: 15,24 +[CUBE] Product: empty,1,0 +[BDD] Product: empty,1,0 +EOF + +cmp output expected