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 fixed-size memory pool implementation.
Definition fixpool.hh:46
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