mc: rework product_to_twa
* spot/mc/utils.hh: Here.
This commit is contained in:
Etienne Renault
parent
369a8b8b14
commit
568fcdfc9a
1 changed files with 111 additions and 223 deletions
334
spot/mc/utils.hh
334
spot/mc/utils.hh
|
|
@ -97,145 +97,14 @@ namespace spot
|
|||
std::unordered_map<int, int> reverse_binder_;
|
||||
};
|
||||
|
||||
// FIXME: should be merge into the next algorithm.
|
||||
/// \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).
|
||||
|
||||
|
||||
/// \brief convert a (cube) product automaton into a twa
|
||||
/// Note that this algorithm cannot be run in parallel.
|
||||
template<typename State, typename SuccIterator,
|
||||
typename StateHash, typename StateEqual,
|
||||
typename EmptinessCheck>
|
||||
class SPOT_API intersect
|
||||
typename StateHash, typename StateEqual>
|
||||
class SPOT_API product_to_twa
|
||||
{
|
||||
public:
|
||||
intersect(const intersect<State, SuccIterator, StateHash,
|
||||
StateEqual, EmptinessCheck>& i) = default;
|
||||
|
||||
intersect(kripkecube<State, SuccIterator>& sys,
|
||||
twacube_ptr twa, unsigned tid, bool& stop):
|
||||
sys_(sys), twa_(twa), tid_(tid), stop_(stop)
|
||||
{
|
||||
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
|
||||
State, SuccIterator>::value,
|
||||
"error: does not match the kripkecube requirements");
|
||||
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(tid_), twa_->get_initial()};
|
||||
if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, {})))
|
||||
{
|
||||
todo.push_back({initial, sys_.succ(initial.st_kripke, tid_),
|
||||
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(sys_, twa_, todo.back().it_kripke,
|
||||
todo.back().it_prop, true, 0);
|
||||
map[initial] = ++dfs_number;
|
||||
}
|
||||
while (!todo.empty() && !stop_)
|
||||
{
|
||||
// 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, tid_);
|
||||
// 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, tid_).dst
|
||||
};
|
||||
auto acc = twa_->trans_data(todo.back().it_prop, tid_).acc_;
|
||||
forward_iterators(sys_, twa_, todo.back().it_kripke,
|
||||
todo.back().it_prop, false, 0);
|
||||
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, tid_),
|
||||
twa_->succ(dst.st_prop)});
|
||||
forward_iterators(sys_, twa_, todo.back().it_kripke,
|
||||
todo.back().it_prop, true, 0);
|
||||
}
|
||||
}
|
||||
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();
|
||||
}
|
||||
|
||||
public:
|
||||
struct product_state
|
||||
{
|
||||
State st_kripke;
|
||||
|
|
@ -257,80 +126,94 @@ namespace spot
|
|||
struct product_state_hash
|
||||
{
|
||||
size_t
|
||||
operator()(const product_state that) const noexcept
|
||||
operator()(const product_state lhs) const noexcept
|
||||
{
|
||||
// FIXME! wang32_hash(that.st_prop) could have
|
||||
// been pre-calculated!
|
||||
StateHash hasher;
|
||||
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
|
||||
unsigned u = hash(lhs.st_kripke) % (1<<30);
|
||||
u = wang32_hash(lhs.st_prop) ^ u;
|
||||
u = u % (1<<30);
|
||||
return u;
|
||||
}
|
||||
};
|
||||
|
||||
struct todo_element
|
||||
{
|
||||
product_state st;
|
||||
SuccIterator* it_kripke;
|
||||
std::shared_ptr<trans_index> it_prop;
|
||||
};
|
||||
kripkecube<State, SuccIterator>& sys_;
|
||||
twacube_ptr 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;
|
||||
unsigned tid_;
|
||||
bool& stop_; // Do not need to be atomic.
|
||||
};
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
template<typename State, typename SuccIterator,
|
||||
typename StateHash, typename StateEqual>
|
||||
class SPOT_API product_to_twa :
|
||||
public intersect<State, SuccIterator,
|
||||
StateHash, StateEqual,
|
||||
product_to_twa<State, SuccIterator,
|
||||
StateHash, StateEqual>>
|
||||
{
|
||||
// Ease the manipulation
|
||||
using typename intersect<State, SuccIterator, StateHash, StateEqual,
|
||||
product_to_twa<State, SuccIterator,
|
||||
StateHash,
|
||||
StateEqual>>::product_state;
|
||||
|
||||
public:
|
||||
product_to_twa(kripkecube<State, SuccIterator>& sys,
|
||||
twacube_ptr twa)
|
||||
: intersect<State, SuccIterator, StateHash, StateEqual,
|
||||
product_to_twa<State, SuccIterator,
|
||||
StateHash, StateEqual>>(sys, twa)
|
||||
{
|
||||
}
|
||||
twacube_ptr twa):
|
||||
sys_(sys), twa_(twa)
|
||||
{
|
||||
static_assert(spot::is_a_kripkecube_ptr<decltype(&sys),
|
||||
State, SuccIterator>::value,
|
||||
"error: does not match the kripkecube requirements");
|
||||
}
|
||||
|
||||
~product_to_twa()
|
||||
{
|
||||
}
|
||||
virtual ~product_to_twa()
|
||||
{
|
||||
map.clear();
|
||||
}
|
||||
|
||||
bool run()
|
||||
{
|
||||
setup();
|
||||
product_state initial = {sys_.initial(0), twa_->get_initial()};
|
||||
if (SPOT_LIKELY(push_state(initial, dfs_number_+1, {})))
|
||||
{
|
||||
todo_.push_back({initial, sys_.succ(initial.st_kripke, 0),
|
||||
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(sys_, twa_, todo_.back().it_kripke,
|
||||
todo_.back().it_prop, true, 0);
|
||||
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(pop_state(todo_.back().st,
|
||||
map[todo_.back().st],
|
||||
is_init,
|
||||
newtop,
|
||||
map[newtop])))
|
||||
{
|
||||
sys_.recycle(todo_.back().it_kripke, 0);
|
||||
todo_.pop_back();
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
++transitions_;
|
||||
product_state dst = {
|
||||
todo_.back().it_kripke->state(),
|
||||
twa_->trans_storage(todo_.back().it_prop, 0).dst
|
||||
};
|
||||
auto acc = twa_->trans_data(todo_.back().it_prop, 0).acc_;
|
||||
forward_iterators(sys_, twa_, todo_.back().it_kripke,
|
||||
todo_.back().it_prop, false, 0);
|
||||
auto it = map.find(dst);
|
||||
if (it == map.end())
|
||||
{
|
||||
if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
|
||||
{
|
||||
map[dst] = ++dfs_number_;
|
||||
todo_.push_back({dst, sys_.succ(dst.st_kripke, 0),
|
||||
twa_->succ(dst.st_prop)});
|
||||
forward_iterators(sys_, twa_, todo_.back().it_kripke,
|
||||
todo_.back().it_prop, true, 0);
|
||||
}
|
||||
}
|
||||
else if (SPOT_UNLIKELY(update(todo_.back().st, dfs_number_,
|
||||
dst, map[dst], acc)))
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
twa_graph_ptr twa()
|
||||
{
|
||||
|
|
@ -355,19 +238,19 @@ 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())
|
||||
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());
|
||||
(this->todo_.back().it_prop).cube_,
|
||||
this->todo_.back().it_kripke->condition());
|
||||
|
||||
bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
|
||||
reverse_binder_);
|
||||
this->twa_->get_cubeset().release(c);
|
||||
res_->new_edge(this->map[this->todo.back().st]-1, i-1, x,
|
||||
res_->new_edge(this->map[this->todo_.back().st]-1, i-1, x,
|
||||
this->twa_->trans_data
|
||||
(this->todo.back().it_prop).acc_);
|
||||
(this->todo_.back().it_prop).acc_);
|
||||
}
|
||||
|
||||
unsigned st = res_->new_state();
|
||||
|
|
@ -377,15 +260,14 @@ namespace spot
|
|||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool update(product_state, unsigned src,
|
||||
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());
|
||||
(this->todo_.back().it_prop).cube_,
|
||||
this->todo_.back().it_kripke->condition());
|
||||
|
||||
bdd x = spot::cube_to_bdd(c, this->twa_->get_cubeset(),
|
||||
reverse_binder_);
|
||||
|
|
@ -394,23 +276,29 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
|
||||
// These callbacks are useless here
|
||||
bool counterexample_found()
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
std::string trace()
|
||||
{
|
||||
return "";
|
||||
}
|
||||
|
||||
bool pop_state(product_state, unsigned, bool, product_state, unsigned)
|
||||
{
|
||||
return true;
|
||||
}
|
||||
|
||||
private:
|
||||
struct todo__element
|
||||
{
|
||||
product_state st;
|
||||
SuccIterator* it_kripke;
|
||||
std::shared_ptr<trans_index> it_prop;
|
||||
};
|
||||
|
||||
typedef std::unordered_map<const product_state, int,
|
||||
product_state_hash,
|
||||
product_state_equal> visited_map;
|
||||
|
||||
kripkecube<State, SuccIterator>& sys_;
|
||||
twacube_ptr twa_;
|
||||
std::vector<todo__element> todo_;
|
||||
visited_map map;
|
||||
unsigned int dfs_number_ = 0;
|
||||
unsigned int transitions_ = 0;
|
||||
spot::twa_graph_ptr res_;
|
||||
std::vector<std::string>* names_;
|
||||
std::unordered_map<int, int> reverse_binder_;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue