From 87de88c80c8e5af854012273b318fd8b06c7b9cb Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Mon, 30 Nov 2015 15:26:42 +0100 Subject: [PATCH] intersection: for kripke and twacube * spot/mc/Makefile.am, spot/mc/intersect.hh: here. --- spot/mc/Makefile.am | 2 +- spot/mc/intersect.hh | 258 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 259 insertions(+), 1 deletion(-) create mode 100644 spot/mc/intersect.hh diff --git a/spot/mc/Makefile.am b/spot/mc/Makefile.am index f463a9e6a..a98d105f2 100644 --- a/spot/mc/Makefile.am +++ b/spot/mc/Makefile.am @@ -25,6 +25,6 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS) mcdir = $(pkgincludedir)/mc -mc_HEADERS = reachability.hh +mc_HEADERS = reachability.hh intersect.hh noinst_LTLIBRARIES = libmc.la diff --git a/spot/mc/intersect.hh b/spot/mc/intersect.hh new file mode 100644 index 000000000..8605ba073 --- /dev/null +++ b/spot/mc/intersect.hh @@ -0,0 +1,258 @@ +// -*- 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 explores (with a DFS) a product between a + /// system and a twa. This exploration is performed on-the-fly. + /// Since this exploration aims to be a generic we need to define + /// hooks to the various emptiness checks. + /// Actually, we use "mixins templates" in order to efficiently + /// call emptiness check procedure. This means that we add + /// a template \a EmptinessCheck that will be called though + /// four functions: + /// - setup: called before any operation + /// - push: called for every new state + /// - pop: called every time a state leave the DFS stack + /// - update: called for every closing edge + /// - trace: must return a counterexample (if exists) + /// + /// The other template parameters allows to consider any kind + /// of state (and so any kind of kripke structures). + template + class SPOT_API intersect + { + public: + intersect(kripkecube& sys, + twacube* twa): + sys_(sys), twa_(twa) + { + assert(is_a_kripkecube(sys)); + map.reserve(2000000); + todo.reserve(100000); + } + + ~intersect() + { + map.clear(); + } + + /// \brief In order to implement "mixin paradigm", we + /// must be abble to access the acual definition of + /// the emptiness check that, in turn, has to access + /// local variables. + EmptinessCheck& self() + { + return static_cast(*this); + } + + /// \brief The main function that will perform the + /// product on-the-fly and call the emptiness check + /// when necessary. + bool run() + { + self().setup(); + product_state initial = {sys_.initial(), twa_->get_initial()}; + if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U))) + { + todo.push_back({initial, sys_.succ(initial.st_kripke), + twa_->succ(initial.st_prop)}); + + // Not going further! It's a product with a single state. + if (todo.back().it_prop->done()) + return false; + + forward_iterators(true); + map[initial] = ++dfs_number; + } + while (!todo.empty()) + { + // Check the kripke is enough since it's the outer loop. More + // details in forward_iterators. + if (todo.back().it_kripke->done()) + { + bool is_init = todo.size() == 1; + auto newtop = is_init? todo.back().st: todo[todo.size() -2].st; + if (SPOT_LIKELY(self().pop_state(todo.back().st, + map[todo.back().st], + is_init, + newtop, + map[newtop]))) + { + sys_.recycle(todo.back().it_kripke); + // FIXME a local storage for twacube iterator? + todo.pop_back(); + if (SPOT_UNLIKELY(self().counterexample_found())) + return true; + } + } + else + { + ++transitions; + product_state dst = { + todo.back().it_kripke->state(), + twa_->trans_storage(todo.back().it_prop).dst + }; + auto acc = twa_->trans_data(todo.back().it_prop).acc_; + forward_iterators(false); + auto it = map.find(dst); + if (it == map.end()) + { + if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc))) + { + map[dst] = ++dfs_number; + todo.push_back({dst, sys_.succ(dst.st_kripke), + twa_->succ(dst.st_prop)}); + forward_iterators(true); + } + } + else if (SPOT_UNLIKELY(self().update(todo.back().st, + dfs_number, + dst, map[dst], acc))) + return true; + } + } + return false; + } + + unsigned int states() + { + return dfs_number; + } + + unsigned int trans() + { + return transitions; + } + + std::string counterexample() + { + return self().trace(); + } + + + virtual std::string stats() + { + return + std::to_string(dfs_number) + " unique states visited\n" + + std::to_string(transitions) + " transitions explored\n"; + } + + protected: + + /// \brief Find the first couple of iterator (from the top of the + /// todo stack) that intersect. The \a parameter indicates wheter + /// the state has just been pushed since the underlying job + /// is slightly different. + void forward_iterators(bool just_pushed) + { + assert(!todo.empty()); + assert(!(todo.back().it_prop->done() && todo.back().it_kripke->done())); + + // Sometimes kripke state may have no successors. + if (todo.back().it_kripke->done()) + return; + + // The state has just been push and the 2 iterators intersect. + // There is no need to move iterators forward. + assert(!(todo.back().it_prop->done())); + if (just_pushed && twa_->get_cubeset() + .intersect(twa_->trans_data(todo.back().it_prop).cube_, + todo.back().it_kripke->condition())) + return; + + // Otherwise we have to compute the next valid successor (if it exits). + // This requires two loops. The most inner one is for the twacube since + // its costless + if (todo.back().it_prop->done()) + todo.back().it_prop->reset(); + else + todo.back().it_prop->next(); + + while (!todo.back().it_kripke->done()) + { + while (!todo.back().it_prop->done()) + { + if (SPOT_UNLIKELY(twa_->get_cubeset() + .intersect(twa_->trans_data(todo.back().it_prop).cube_, + todo.back().it_kripke->condition()))) + return; + todo.back().it_prop->next(); + } + todo.back().it_prop->reset(); + todo.back().it_kripke->next(); + } + } + + public: + struct product_state + { + State st_kripke; + unsigned st_prop; + }; + + struct product_state_equal + { + bool + operator()(const product_state lhs, + const product_state rhs) const + { + StateEqual equal; + return (lhs.st_prop == rhs.st_prop) && + equal(lhs.st_kripke, rhs.st_kripke); + } + }; + + struct product_state_hash + { + size_t + operator()(const product_state that) const + { + // FIXME! wang32_hash(that.st_prop) could have + // been pre-calculated! + StateHash hasher; + return wang32_hash(that.st_prop) ^ hasher(that.st_kripke); + } + }; + + struct todo_element + { + product_state st; + SuccIterator* it_kripke; + std::shared_ptr it_prop; + }; + kripkecube& sys_; + twacube* twa_; + std::vector todo; + typedef std::unordered_map visited_map; + visited_map map; + unsigned int dfs_number = 0; + unsigned int transitions = 0; + }; +}