Commit 975a9aca authored by Etienne Renault's avatar Etienne Renault

ltsmin: prodcuce kripkecube

Warning! this patch introduces redundancy (or difference)
between wether you ask for a kripkecube or a kripke.

* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: here.
parent cc0ef16c
This diff is collapsed.
......@@ -25,6 +25,8 @@
namespace spot
{
struct spins_interface;
class cspins_iterator;
using cspins_state = int*;
class SPOT_API ltsmin_model final
{
......@@ -71,6 +73,14 @@ namespace spot
formula dead = formula::tt(),
int compress = 0) const;
// \brief The same as above but returns a kripkecube, i.e. a kripke
// that can be use in parallel. Moreover, it support more ellaborated
// atomic propositions such as "P.a == P.c"
spot::kripkecube<spot::cspins_state, spot::cspins_iterator>*
kripkecube(const atomic_prop_set* to_observe,
formula dead = formula::tt(),
int compress = 0) const;
/// Number of variables in a state
int state_size() const;
/// Name of each variable
......
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