22 #include <spot/twa/twa.hh>
23 #include <spot/kripke/fwd.hh>
57 virtual bdd
cond()
const override;
An acceptance condition.
Definition: acc.hh:62
Iterator code for a Fair Kripke structure.
Definition: fairkripke.hh:47
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
fair_kripke_succ_iterator(const bdd &cond, acc_cond::mark_t acc_cond)
Constructor.
virtual acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
Interface for a Fair Kripke structure.
Definition: fairkripke.hh:88
virtual acc_cond::mark_t state_acceptance_mark(const state *s) const =0
The acceptance mark that labels state s.
virtual bdd state_condition(const state *s) const =0
The condition that label the state s.
Abstract class for states.
Definition: twa.hh:51
Iterate over the successors of a state.
Definition: twa.hh:398
A Transition-based ω-Automaton.
Definition: twa.hh:623
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85