22 #include <spot/kripke/fairkripke.hh>
23 #include <spot/twacube/cube.hh>
25 #include <type_traits>
38 template<
typename State,
typename SuccIterator>
40 public std::enable_shared_from_this<kripkecube<State, SuccIterator>>
51 std::string
to_string(
const State,
unsigned tid)
const;
54 SuccIterator*
succ(
const State,
unsigned tid);
58 void recycle(SuccIterator*,
unsigned tid);
61 const std::vector<std::string>
ap();
70 template <
typename T,
typename State,
typename SuccIter>
74 using yes = std::true_type;
75 using no = std::false_type;
78 template<
typename U,
typename V>
static auto test_kripke(
U u, V v)
81 std::is_same<State, decltype(u->initial(0))>::value &&
82 std::is_same<
unsigned, decltype(u->get_threads())>::value &&
83 std::is_same<std::string, decltype(u->to_string(State(), 0))>::value &&
84 std::is_same<SuccIter*, decltype(u->succ(State(), 0))>::value &&
85 std::is_same<
void, decltype(u->recycle(
nullptr, 0))>::value &&
86 std::is_same<
const std::vector<std::string>,
87 decltype(u->ap())>::value &&
88 std::is_same<
void, decltype(u->recycle(
nullptr, 0))>::value &&
91 std::is_same<
void, decltype(v->next())>::value &&
92 std::is_same<
bool, decltype(v->done())>::value &&
93 std::is_same<State, decltype(v->state())>::value &&
94 std::is_same<
spot::cube, decltype(v->condition())>::value
100 template<
typename,
typename>
static no test_kripke(...);
106 static constexpr
bool value =
107 std::is_same< decltype(test_kripke<T, SuccIter*>(
nullptr,
nullptr)), yes
142 void recycle(
const bdd& cond)
147 virtual ~kripke_succ_iterator();
149 virtual bdd
cond()
const override;
180 kripke(
const bdd_dict_ptr& d)
191 typedef std::shared_ptr<kripke> kripke_ptr;
192 typedef std::shared_ptr<const kripke> const_kripke_ptr;
Interface for a Fair Kripke structure.
Definition: fairkripke.hh:88
This class allows to ensure (at compile time) if a given parameter is of type kripkecube....
Definition: kripke.hh:72
Iterator code for Kripke structure.
Definition: kripke.hh:131
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
kripke_succ_iterator(const bdd &cond)
Constructor.
Definition: kripke.hh:137
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:178
virtual acc_cond::mark_t state_acceptance_mark(const state *) const override
The acceptance mark that labels state s.
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
std::string to_string(const State, unsigned tid) const
Provides a string representation of the parameter state.
const std::vector< std::string > ap()
This method allow to deallocate a given state.
unsigned get_threads()
Returns the number of threads that are handled by the kripkecube.
SuccIterator * succ(const State, unsigned tid)
Returns an iterator over the successors of the parameter state.
State initial(unsigned tid)
Returns the initial State of the System. The tid parameter is used internally for sharing this struct...
void recycle(SuccIterator *, unsigned tid)
Allocation and deallocation of iterator is costly. This method allows to reuse old iterators.
Abstract class for states.
Definition: twa.hh:51
Iterate over the successors of a state.
Definition: twa.hh:398
Definition: automata.hh:27
unsigned * cube
A cube is only a set of bits in memory.
Definition: cube.hh:66
An acceptance mark.
Definition: acc.hh:85