22 #include <spot/ta/ta.hh>
23 #include <spot/kripke/kripke.hh>
40 ta_state_(ta_state), kripke_state_(kripke_state)
57 get_kripke_state()
const
63 compare(
const state* other)
const override;
65 hash()
const override;
66 virtual state_ta_product*
67 clone()
const override;
70 const state* ta_state_;
71 const state* kripke_state_;
85 virtual bool first()
override;
86 virtual bool next()
override;
87 virtual bool done()
const override;
91 virtual bdd cond()
const override;
95 bool is_stuttering_transition()
const;
101 bool next_non_stuttering_();
116 bdd current_condition_;
118 bool is_stuttering_transition_;
119 bdd kripke_source_condition;
120 const state* kripke_current_dest_state;
133 ta_product(
const const_ta_ptr& testing_automaton,
134 const const_kripke_ptr& kripke_structure);
139 virtual ta::const_states_set_t
140 get_initial_states_set()
const override;
146 succ_iter(
const spot::state* s, bdd changeset)
const override;
155 is_accepting_state(
const spot::state* s)
const override;
158 is_livelock_accepting_state(
const spot::state* s)
const override;
161 is_initial_state(
const spot::state* s)
const override;
166 is_hole_state_in_ta_component(
const spot::state* s)
const;
169 get_state_condition(
const spot::state* s)
const override;
180 const const_kripke_ptr&
189 const_kripke_ptr kripke_;
197 typedef std::shared_ptr<ta_product> ta_product_ptr;
198 typedef std::shared_ptr<const ta_product> const_ta_product_ptr;
199 inline ta_product_ptr product(
const const_ta_ptr& testing_automaton,
200 const const_kripke_ptr& kripke_structure)
202 return std::make_shared<ta_product>(testing_automaton, kripke_structure);
214 void next_kripke_dest();
A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly...
Definition: taproduct.hh:127
Interface for a Kripke structure.
Definition: kripke.hh:90
Abstract class for states.
Definition: twa.hh:43
Iterate over the successors of a state.
Definition: twa.hh:390
Iterate over the successors of a product computed on the fly.
Definition: taproduct.hh:75
Definition: taproduct.hh:205
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