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);
38 virtual const state* get_init_state()
const override;
41 succ_iter(
const state* local_state)
const override;
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,
63 bool first()
override;
65 bool done()
const override;
69 bdd cond()
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;
Definition: automata.hh:26
A lazy product. (States are computed on the fly.)
Definition: twaproduct.hh:82
Abstract class for states.
Definition: twa.hh:50
Iterate over the successors of a product computed on the fly.
Definition: tgtaproduct.hh:51
A lazy product. (States are computed on the fly.)
Definition: tgtaproduct.hh:32
Iterate over the successors of a state.
Definition: twa.hh:397
A state for spot::twa_product.
Definition: twaproduct.hh:36
A Transition-based Generalized Testing Automaton (TGTA).
Definition: tgta.hh:59
An acceptance mark.
Definition: acc.hh:81
twa_graph_ptr product(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, const output_aborter *aborter=nullptr)
Intersect two automata using a synchronous product.
A fixed-size memory pool implementation.
Definition: fixpool.hh:31