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 const state * get_init_state() const override
Get the initial state of the automaton.
virtual twa_succ_iterator * succ_iter(const state *local_state) const override
Get an iterator over the successors of local_state.
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).
bool first() override
Position the iterator on the first successor (if any).
state_product * dst() const override
Get the destination state of the current edge.
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