21 #include <spot/twa/twa.hh>
22 #include <spot/twa/twaproduct.hh>
23 #include <spot/misc/fixpool.hh>
24 #include <spot/kripke/kripke.hh>
25 #include <spot/ta/tgta.hh>
35 const const_tgta_ptr& right);
43 inline twa_ptr product(
const const_kripke_ptr& left,
44 const const_tgta_ptr& right)
46 return std::make_shared<tgta_product>(left, right);
54 const const_kripke_ptr& k,
55 const const_tgta_ptr&
tgta,
64 bool done()
const override;
76 bool find_next_succ_();
86 const_kripke_ptr kripke_;
91 bdd current_condition_;
93 bdd kripke_source_condition;
94 const state* kripke_current_dest_state;
A state for spot::twa_product.
Definition: twaproduct.hh:33
Abstract class for states.
Definition: twa.hh:47
A lazy product. (States are computed on the fly.)
Definition: tgtaproduct.hh:32
virtual twa_succ_iterator * succ_iter(const state *local_state) const override
Get an iterator over the successors of local_state.
virtual const state * get_init_state() const override
Get the initial state of the automaton.
Iterate over the successors of a product computed on the fly.
Definition: tgtaproduct.hh:51
bool done() const override
Check whether the iteration is finished.
bdd cond() const override
Get the condition on the edge leading to this successor.
acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
bool next() override
Jump to the next successor (if any).
state_product * dst() const override
Get the destination state of the current edge.
bool first() override
Position the iterator on the first successor (if any).
A Transition-based Generalized Testing Automaton (TGTA).
Definition: tgta.hh:59
A lazy product. (States are computed on the fly.)
Definition: twaproduct.hh:79
Iterate over the successors of a state.
Definition: twa.hh:394
Definition: automata.hh:26
An acceptance mark.
Definition: acc.hh:84