23 #include <spot/kripke/kripke.hh>
24 #include <spot/graph/graph.hh>
55 auto o = down_cast<const kripke_graph_state*>(other);
65 virtual size_t hash()
const override
68 reinterpret_cast<const char*
>(
this) -
static_cast<const char*
>(
nullptr);
99 typedef typename Graph::edge edge;
100 typedef typename Graph::state_data_t state;
106 const typename Graph::state_storage_t* s):
117 void recycle(
const typename Graph::state_storage_t* s)
131 p_ = g_->edge_storage(p_).next_succ;
135 virtual bool done()
const override
142 SPOT_ASSERT(!done());
144 (&g_->state_data(g_->edge_storage(p_).dst));
170 typedef std::vector<state_storage_t> state_vector;
173 typedef unsigned state_num;
174 static_assert(std::is_same<typename graph_t::state, state_num>::value,
179 mutable unsigned init_number_;
182 :
kripke(d), init_number_(0)
188 get_dict()->unregister_all_my_variables(
this);
191 unsigned num_states()
const
196 unsigned num_edges()
const
201 void set_init_state(state_num s)
203 if (SPOT_UNLIKELY(s >= num_states()))
204 throw std::invalid_argument
205 (
"set_init_state() called with nonexisiting state");
209 state_num get_init_state_number()
const
212 if (num_states() == 0)
213 throw std::runtime_error(
"kripke has no state at all");
219 return state_from_number(get_init_state_number());
227 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
230 if (this->iter_cache_)
233 down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_);
235 this->iter_cache_ =
nullptr;
243 state_number(
const state* st)
const
245 auto s = down_cast<const typename graph_t::state_storage_t*>(st);
249 const kripke_graph_state*
250 state_from_number(state_num n)
const
256 state_from_number(state_num n)
261 std::string format_state(
unsigned n)
const
263 auto named = get_named_prop<std::vector<std::string>>(
"state-names");
264 if (named && n < named->size())
267 return std::to_string(n);
272 return format_state(state_number(st));
278 auto gs = down_cast<const kripke_graph_state*>(s);
282 edge_storage_t& edge_storage(
unsigned t)
287 const edge_storage_t edge_storage(
unsigned t)
const
292 unsigned new_state(bdd cond)
297 unsigned new_states(
unsigned n, bdd cond)
302 unsigned new_edge(
unsigned src,
unsigned dst)
309 const state_vector& states()
const
315 state_vector& states()
321 internal::all_trans<const graph_t>
322 edges() const noexcept
328 internal::all_trans<graph_t>
335 internal::state_out<const graph_t>
336 out(
unsigned src)
const
342 internal::state_out<graph_t>
350 typedef std::shared_ptr<kripke_graph> kripke_graph_ptr;
352 inline kripke_graph_ptr
353 make_kripke_graph(
const bdd_dict_ptr& d)
355 return std::make_shared<kripke_graph>(d);
unsigned num_states() const
The number of states in the automaton.
Definition: graph.hh:645
const state_vector & states() const
Return the vector of states.
Definition: graph.hh:918
state new_states(unsigned n, Args &&... args)
Create n new states.
Definition: graph.hh:684
state new_state(Args &&... args)
Create a new states.
Definition: graph.hh:670
bool is_valid_edge(edge t) const
Test whether the given edge is valid.
Definition: graph.hh:969
edge_storage_t & edge_storage(edge s)
return a reference to the storage of an edge
Definition: graph.hh:735
internal::state_out< digraph > out(state src)
Return a fake container with all edges leaving src.
Definition: graph.hh:874
state_storage_t & state_storage(state s)
return a reference to the storage of a state
Definition: graph.hh:699
unsigned num_edges() const
The number of edges in the automaton.
Definition: graph.hh:653
state_storage_t::data_t & state_data(state s)
return the State_Data associated to a state
Definition: graph.hh:717
edge new_edge(state src, state dst, Args &&... args)
Create a new edge.
Definition: graph.hh:772
internal::all_trans< const digraph > edges() const
Return a fake container with all edges (exluding erased edges)
Definition: graph.hh:933
Definition: kripkegraph.hh:97
virtual bool first() override
Position the iterator on the first successor (if any).
Definition: kripkegraph.hh:123
virtual bool done() const override
Check whether the iteration is finished.
Definition: kripkegraph.hh:135
virtual bool next() override
Jump to the next successor (if any).
Definition: kripkegraph.hh:129
virtual kripke_graph_state * dst() const override
Get the destination state of the current edge.
Definition: kripkegraph.hh:140
Kripke Structure.
Definition: kripkegraph.hh:152
virtual kripke_graph_succ_iterator< graph_t > * succ_iter(const spot::state *st) const override
Allow to get an iterator on the state we passed in parameter.
Definition: kripkegraph.hh:225
virtual std::string format_state(const state *st) const override
Format the state as a string for printing.
Definition: kripkegraph.hh:270
virtual const kripke_graph_state * get_init_state() const override
Get the initial state of the automaton.
Definition: kripkegraph.hh:217
virtual bdd state_condition(const state *s) const override
Get the condition on the state.
Definition: kripkegraph.hh:276
Iterator code for Kripke structure.
Definition: kripke.hh:131
virtual bdd cond() const override
Get the condition on the edge leading to this successor.
Interface for a Kripke structure.
Definition: kripke.hh:178
Abstract class for states.
Definition: twa.hh:51
Definition: automata.hh:27
Concrete class for kripke_graph states.
Definition: kripkegraph.hh:31
virtual size_t hash() const override
Hash a state.
Definition: kripkegraph.hh:65
virtual kripke_graph_state * clone() const override
Duplicate a state.
Definition: kripkegraph.hh:72
virtual void destroy() const override
Release a state.
Definition: kripkegraph.hh:77
virtual int compare(const spot::state *other) const override
Compares two states (that come from the same automaton).
Definition: kripkegraph.hh:53