From 3bafe693efb805573f26f2126d7d14ad94fcf774 Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Thu, 17 Mar 2016 16:23:28 +0100 Subject: [PATCH] ec: Renault et al LPAR'13 emptiness check In order to reuse the computation of the intersection between kripke and twa efficiently, we use template inheritance through the "mixin templates" technique. * spot/Makefile.am, spot/mc/Makefile.am, spot/mc/ec.hh, spot/mc/unionfind.cc, spot/mc/unionfind.hh: here. --- spot/Makefile.am | 3 +- spot/mc/Makefile.am | 13 +-- spot/mc/ec.hh | 266 +++++++++++++++++++++++++++++++++++++++++++ spot/mc/unionfind.cc | 93 +++++++++++++++ spot/mc/unionfind.hh | 52 +++++++++ 5 files changed, 419 insertions(+), 8 deletions(-) create mode 100644 spot/mc/ec.hh create mode 100644 spot/mc/unionfind.cc create mode 100644 spot/mc/unionfind.hh diff --git a/spot/Makefile.am b/spot/Makefile.am index b61a180ea..f30a501ef 100644 --- a/spot/Makefile.am +++ b/spot/Makefile.am @@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects # end, after building '.' (since the current directory contains # libspot.la needed by the tests) SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \ - twacube_algos parseaut parsetl . ltsmin gen + twacube_algos mc parseaut parsetl . ltsmin gen lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -44,6 +44,7 @@ libspot_la_LIBADD = \ twa/libtwa.la \ twacube_algos/libtwacube_algos.la \ twacube/libtwacube.la \ + mc/libmc.la \ ../lib/libgnu.la \ ../picosat/libpico.la diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index a98d105f2..2bc3291b2 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -1,9 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire -## de Recherche et Développement de l'Epita (LRDE). -## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -## département Systèmes Répartis Coopératifs (SRC), Université Pierre -## et Marie Curie. +## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de +## l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -24,7 +21,9 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc - -mc_HEADERS = reachability.hh intersect.hh +mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh noinst_LTLIBRARIES = libmc.la + +libmc_la_SOURCES = \ + unionfind.cc diff --git a/spot/mc/ec.hh b/spot/mc/ec.hh new file mode 100644 index 000000000..f2ffee636 --- /dev/null +++ b/spot/mc/ec.hh @@ -0,0 +1,266 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016 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 +#include +#include + +namespace spot +{ + /// \brief This class implements the sequential emptiness check as + /// presented in "Three SCC-based Emptiness Checks for Generalized + /// B\¨uchi Automata" (Renault et al, LPAR 2013). Among the three + /// emptiness check that has been proposed we opted to implement + /// the Gabow's one. + template + class ec_renault13lpar : public intersect> + { + // Ease the manipulation + using typename intersect>::product_state; + + public: + ec_renault13lpar(kripkecube& sys, + twacube* twa) + : intersect>(sys, twa), + acc_(twa->acc()) + { + } + + virtual ~ec_renault13lpar() + { + + } + + /// \brief This method is called at the begining of the exploration. + /// here we do not need to setup any information. + void setup() + { + } + + /// \brief This method is called to notify the emptiness checks + /// that a new state has been discovered. If this method return + /// false, the state will not be explored. The parameter \a dfsnum + /// specify an unique id for the state \a s. Parameter \a cond represents + /// The value on the ingoing edge to \a s. + bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond) + { + uf_.makeset(dfsnum); + roots_.push_back({dfsnum, cond, 0U}); + return true; + } + + /// \brief This method is called to notify the emptiness checks + /// that a state will be popped. If the method return false, then + /// the state will be popped. Otherwise the state \a newtop will + /// become the new top of the DFS stack. If the state \a top is + /// the only one in the DFS stak, the parameter \a is_initial is set + /// to true and both \a newtop and \a newtop_dfsnum have inconsistency + /// values. + bool pop_state(product_state, unsigned top_dfsnum, bool, + product_state, unsigned) + { + if (top_dfsnum == roots_.back().dfsnum) + { + roots_.pop_back(); + uf_.markdead(top_dfsnum); + } + return true; + } + + /// \brief This method is called for every closing, back, or forward edge. + /// Return true if a counterexample has been found. + bool update(product_state, unsigned, + product_state, unsigned dst_dfsnum, + acc_cond::mark_t cond) + { + if (uf_.isdead(dst_dfsnum)) + return false; + + while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum)) + { + auto& el = roots_.back(); + roots_.pop_back(); + uf_.unite(dst_dfsnum, el.dfsnum); + cond |= el.acc | el.ingoing; + } + roots_.back().acc |= cond; + found_ = acc_.accepting(roots_.back().acc); + return found_; + } + + bool counterexample_found() + { + return found_; + } + + std::string trace() + { + assert(counterexample_found()); + std::string res = "Prefix:\n"; + + // Compute the prefix of the accepting run + for (auto& s : this->todo) + res += " " + std::to_string(s.st.st_prop) + + + "*" + this->sys_.to_string(s.st.st_kripke) + "\n"; + + // Compute the accepting cycle + res += "Cycle:\n"; + + struct ctrx_element + { + const product_state* prod_st; + ctrx_element* parent_st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; + }; + std::queue bfs; + + acc_cond::mark_t acc = 0U; + + bfs.push(new ctrx_element({&this->todo.back().st, nullptr, + this->sys_.succ(this->todo.back().st.st_kripke), + this->twa_->succ(this->todo.back().st.st_prop)})); + while (true) + { + here: + auto* front = bfs.front(); + bfs.pop(); + // PUSH all successors of the state. + while (!front->it_kripke->done()) + { + while (!front->it_prop->done()) + { + if (this->twa_->get_cubeset().intersect + (this->twa_->trans_data(front->it_prop).cube_, + front->it_kripke->condition())) + { + const product_state dst = { + front->it_kripke->state(), + this->twa_->trans_storage(front->it_prop).dst + }; + + // Skip Unknown states or not same SCC + auto it = this->map.find(dst); + if (it == this->map.end() || + !uf_.sameset(it->second, + this->map[this->todo.back().st])) + { + front->it_prop->next(); + continue; + } + + // This is a valid transition. If this transition + // is the one we are looking for, update the counter- + // -example and flush the bfs queue. + auto mark = this->twa_->trans_data(front->it_prop).acc_; + if (!acc.has(mark)) + { + ctrx_element* current = front; + while (current != nullptr) + { + // FIXME also display acc? + res = res + " " + + std::to_string(current->prod_st->st_prop) + + + "*" + + this->sys_. to_string(current->prod_st + ->st_kripke) + + "\n"; + current = current->parent_st; + } + + // empty the queue + while (!bfs.empty()) + { + auto* e = bfs.front(); + bfs.pop(); + delete e; + } + + // update acceptance + acc |= mark; + if (this->twa_->acc().accepting(acc)) + return res; + + const product_state* q = &(it->first); + ctrx_element* root = new ctrx_element({ + q , nullptr, + this->sys_.succ(q->st_kripke), + this->twa_->succ(q->st_prop) + }); + bfs.push(root); + goto here; + } + + // Otherwise increment iterator and push successor. + const product_state* q = &(it->first); + ctrx_element* root = new ctrx_element({ + q , nullptr, + this->sys_.succ(q->st_kripke), + this->twa_->succ(q->st_prop) + }); + bfs.push(root); + } + front->it_prop->next(); + } + front->it_prop->reset(); + front->it_kripke->next(); + } + } + + // never reach here; + return res; + } + + // Refine stats to display + virtual std::string stats() override + { + return + std::to_string(this->dfs_number) + " unique states visited\n" + + std::to_string(roots_.size()) + + " strongly connected components in search stack\n" + + std::to_string(this->transitions) + " transitions explored\n"; + } + + private: + + bool found_ = false; ///< \brief A counterexample is detected? + + struct root_element { + unsigned dfsnum; + acc_cond::mark_t ingoing; + acc_cond::mark_t acc; + }; + + /// \brief the root stack. + std::vector roots_; + int_unionfind uf_; + acc_cond acc_; + }; +} diff --git a/spot/mc/unionfind.cc b/spot/mc/unionfind.cc new file mode 100644 index 000000000..e0ce9f089 --- /dev/null +++ b/spot/mc/unionfind.cc @@ -0,0 +1,93 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016 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 . + +#include +#include + +namespace spot +{ + int int_unionfind::root(int i) + { + assert(i > 0); + int p = id[i]; + if (p == DEAD) + return DEAD; + if (p < 0) + return i; + int gp = id[p]; + if (gp == DEAD) + return DEAD; + if (gp < 0) + return p; + p = root(p); + id[i] = p; + return p; + } + + int_unionfind::int_unionfind() : id() + { + id.push_back(DEAD); + } + + void int_unionfind::makeset(int e) + { + assert(e == (int) id.size()); + id.push_back(-1); + } + + bool int_unionfind::unite(int e1, int e2) + { + // IPC - Immediate Parent Check + int p1 = id[e1]; + int p2 = id[e2]; + if ((p1 < 0 ? e1 : p1) == (p2 < 0 ? e2 : p2)) + return false; + int root1 = root(e1); + int root2 = root(e2); + if (root1 == root2) + return false; + int rk1 = -id[root1]; + int rk2 = -id[root2]; + if (rk1 < rk2) + id[root1] = root2; + else { + id[root2] = root1; + if (rk1 == rk2) + id[root1] = -(rk1 + 1); + } + return true; + } + + void int_unionfind::markdead(int e) + { + id[root(e)] = DEAD; + } + + bool int_unionfind::sameset(int e1, int e2) + { + assert(e1 < (int)id.size() && e2 < (int)id.size()); + return root(e1) == root(e2); + } + + bool int_unionfind::isdead(int e) + { + assert(e < (int)id.size()); + return root(e) == DEAD; + } +} diff --git a/spot/mc/unionfind.hh b/spot/mc/unionfind.hh new file mode 100644 index 000000000..39f2d5e24 --- /dev/null +++ b/spot/mc/unionfind.hh @@ -0,0 +1,52 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015, 2016 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 +#include + +namespace spot +{ + + /// \brief This Union-Find data structure is a particular + /// union-find, dedicated for emptiness checks below, see ec.hh. The + /// key of this union-find is int. Moreover, we suppose that only + /// consecutive int are inserted. This union-find includes most of + /// the classical optimisations (IPC, LR, PC, MS). + class SPOT_API int_unionfind final + { + private: + // Store the parent relation, i.e. -1 or x < id.size() + std::vector id; + + // id of a specially managed partition of "dead" elements + const int DEAD = 0; + + int root(int i); + + public: + int_unionfind(); + void makeset(int e); + bool unite(int e1, int e2); + void markdead(int e); + bool sameset(int e1, int e2); + bool isdead(int e); + }; +}