22 #include <spot/ta/ta.hh> 23 #include <spot/kripke/kripke.hh> 40 ta_state_(ta_state), kripke_state_(kripke_state)
56 get_kripke_state()
const 62 compare(
const state* other)
const override;
64 hash()
const override;
66 clone()
const override;
69 const state* ta_state_;
70 const state* kripke_state_;
84 virtual bool first()
override;
85 virtual bool next()
override;
86 virtual bool done()
const override;
90 virtual bdd cond()
const override;
94 bool is_stuttering_transition()
const;
100 bool next_non_stuttering_();
115 bdd current_condition_;
117 bool is_stuttering_transition_;
118 bdd kripke_source_condition;
119 const state* kripke_current_dest_state;
132 ta_product(
const const_ta_ptr& testing_automaton,
133 const const_kripke_ptr& kripke_structure);
138 virtual ta::const_states_set_t
139 get_initial_states_set()
const override;
145 succ_iter(
const spot::state* s, bdd changeset)
const override;
154 is_accepting_state(
const spot::state* s)
const override;
157 is_livelock_accepting_state(
const spot::state* s)
const override;
160 is_initial_state(
const spot::state* s)
const override;
165 is_hole_state_in_ta_component(
const spot::state* s)
const;
168 get_state_condition(
const spot::state* s)
const override;
179 const const_kripke_ptr&
188 const_kripke_ptr kripke_;
196 typedef std::shared_ptr<ta_product> ta_product_ptr;
197 typedef std::shared_ptr<const ta_product> const_ta_product_ptr;
198 inline ta_product_ptr
product(
const const_ta_ptr& testing_automaton,
199 const const_kripke_ptr& kripke_structure)
201 return std::make_shared<ta_product>(testing_automaton, kripke_structure);
213 void next_kripke_dest();
Definition: automata.hh:26
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly...
Definition: taproduct.hh:126
Interface for a Kripke structure.
Definition: kripke.hh:90
Abstract class for states.
Definition: twa.hh:50
Iterate over the successors of a state.
Definition: twa.hh:397
Iterate over the successors of a product computed on the fly.
Definition: taproduct.hh:74
Definition: taproduct.hh:204
A Testing Automaton.
Definition: ta.hh:75
state_ta_product(const state *ta_state, const state *kripke_state)
Constructor.
Definition: taproduct.hh:39
A state for spot::ta_product.
Definition: taproduct.hh:33
Iterate over the successors of a state.
Definition: ta.hh:197
An acceptance mark.
Definition: acc.hh:87
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.