22 #include <spot/ltsmin/spins_interface.hh>
23 #include <spot/ltsmin/spins_kripke.hh>
24 #include <spot/kripke/kripke.hh>
25 #include <spot/twacube/twacube.hh>
26 #include <spot/tl/apcollect.hh>
74 int compress = 0)
const;
82 unsigned int nb_threads = 1)
const;
100 ltsmin_model(std::shared_ptr<const spins_interface> iface) : iface(iface)
103 std::shared_ptr<const spins_interface> iface;
Interface for a Kripke structure.
Definition: kripke.hh:178
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
const char * type_name(int type) const
Name of each type.
int type_value_count(int type)
Count of enumerated values for a type.
int type_count() const
Number of different types.
const char * type_value_name(int type, int val)
Name of each enumerated value for a type.
int state_variable_type(int var) const
Type of each variable.
const char * state_variable_name(int var) const
Name of each variable.
int state_size() const
Number of variables in a state.
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:36
Definition: automata.hh:27
std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > ltsmin_kripkecube_ptr
shortcut to manipulate the kripke below
Definition: spins_kripke.hh:257