Commit d072bfba authored by Etienne Renault's avatar Etienne Renault
Browse files

mc: rework product_to_twa

* spot/mc/utils.hh: Here.
parent 43ab5cc2
......@@ -97,241 +97,124 @@ 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;
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);
}
};
intersect(kripkecube<State, SuccIterator>& sys,
twacube_ptr twa, unsigned tid, bool& stop):
sys_(sys), twa_(twa), tid_(tid), stop_(stop)
struct product_state_hash
{
size_t
operator()(const product_state lhs) const noexcept
{
unsigned u = hash(lhs.st_kripke) % (1<<30);
u = wang32_hash(lhs.st_prop) ^ u;
u = u % (1<<30);
return u;
}
};
public:
product_to_twa(kripkecube<State, SuccIterator>& sys,
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");
map.reserve(2000000);
todo.reserve(100000);
}
~intersect()
virtual ~product_to_twa()
{
map.clear();
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, {})))
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, tid_),
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())
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;
forward_iterators(sys_, twa_, todo_.back().it_kripke,
todo_.back().it_prop, true, 0);
map[initial] = ++dfs_number_;
}
while (!todo.empty() && !stop_)
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())
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],
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, tid_);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
sys_.recycle(todo_.back().it_kripke, 0);
todo_.pop_back();
}
}
else
{
++transitions;
++transitions_;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop, tid_).dst
todo_.back().it_kripke->state(),
twa_->trans_storage(todo_.back().it_prop, 0).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 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(self().push_state(dst, dfs_number+1, acc)))
if (SPOT_LIKELY(push_state(dst, dfs_number_+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke, tid_),
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);
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)))
else if (SPOT_UNLIKELY(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;
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 noexcept
{
// 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_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)
{
}
~product_to_twa()
{
}
twa_graph_ptr twa()
{
res_->set_named_prop<std::vector<std::string>>("state-names", names_);
......@@ -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_;
......
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