Commit 7d0c7860 authored by Etienne Renault's avatar Etienne Renault

intersection: for kripke and twacube

* spot/mc/Makefile.am, spot/mc/intersect.hh: here.
parent 22c4c4a1
......@@ -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
// -*- 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 <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/kripke/kripke.hh>
#include <spot/twacube/twacube.hh>
#include <queue>
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<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename EmptinessCheck>
class SPOT_API intersect
{
public:
intersect(kripkecube<State, SuccIterator>& 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<EmptinessCheck&>(*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<trans_index> it_prop;
};
kripkecube<State, SuccIterator>& sys_;
twacube* twa_;
std::vector<todo_element> todo;
typedef std::unordered_map<const product_state, int,
product_state_hash,
product_state_equal> visited_map;
visited_map map;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
};
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment