22 #include <spot/twa/twa.hh>
23 #include <spot/twa/twaproduct.hh>
24 #include <spot/misc/fixpool.hh>
25 #include <spot/kripke/kripke.hh>
26 #include <spot/ta/tgta.hh>
36 const const_tgta_ptr& right);
44 inline twa_ptr product(
const const_kripke_ptr& left,
45 const const_tgta_ptr& right)
47 return std::make_shared<tgta_product>(left, right);
55 const const_kripke_ptr& k,
56 const const_tgta_ptr&
tgta,
65 bool done()
const override;
77 bool find_next_succ_();
87 const_kripke_ptr kripke_;
92 bdd current_condition_;
94 bdd kripke_source_condition;
95 const state* kripke_current_dest_state;
A state for spot::twa_product.
Definition: twaproduct.hh:37
Abstract class for states.
Definition: twa.hh:51
A lazy product. (States are computed on the fly.)
Definition: tgtaproduct.hh:33
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:52
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:60
A lazy product. (States are computed on the fly.)
Definition: twaproduct.hh:83
Iterate over the successors of a state.
Definition: twa.hh:398
Definition: automata.hh:27
An acceptance mark.
Definition: acc.hh:85