1 // -*- coding: utf-8 -*- 2 // Copyright (C) 2011-2019 Laboratoire de Recherche et Développement de 3 // l'Epita (LRDE) 4 // 5 // This file is part of Spot, a model checking library. 6 // 7 // Spot is free software; you can redistribute it and/or modify it 8 // under the terms of the GNU General Public License as published by 9 // the Free Software Foundation; either version 3 of the License, or 10 // (at your option) any later version. 11 // 12 // Spot is distributed in the hope that it will be useful, but WITHOUT 13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public 15 // License for more details. 16 // 17 // You should have received a copy of the GNU General Public License 18 // along with this program. If not, see <http://www.gnu.org/licenses/>. 19 20 #pragma once 21 22 #include <iosfwd> 23 #include <spot/kripke/kripke.hh> 24 #include <spot/graph/graph.hh> 25 #include <spot/tl/formula.hh> 26 27 namespace spot 28 { 29 /// \brief Concrete class for kripke_graph states. 30 struct SPOT_API kripke_graph_state: public spot::state 31 { 32 public: kripke_graph_statespot::kripke_graph_state33 kripke_graph_state(bdd cond = bddfalse) noexcept 34 : cond_(cond) 35 { 36 } 37 kripke_graph_statespot::kripke_graph_state38 kripke_graph_state(const kripke_graph_state& other) noexcept 39 : cond_(other.cond_) 40 { 41 } 42 operator =spot::kripke_graph_state43 kripke_graph_state& operator=(const kripke_graph_state& other) noexcept 44 { 45 cond_ = other.cond_; 46 return *this; 47 } 48 ~kripke_graph_statespot::kripke_graph_state49 virtual ~kripke_graph_state() noexcept 50 { 51 } 52 comparespot::kripke_graph_state53 virtual int compare(const spot::state* other) const override 54 { 55 auto o = down_cast<const kripke_graph_state*>(other); 56 57 // Do not simply return "other - this", it might not fit in an int. 58 if (o < this) 59 return -1; 60 if (o > this) 61 return 1; 62 return 0; 63 } 64 hashspot::kripke_graph_state65 virtual size_t hash() const override 66 { 67 return reinterpret_cast<size_t>(this); 68 } 69 70 virtual kripke_graph_state* clonespot::kripke_graph_state71 clone() const override 72 { 73 return const_cast<kripke_graph_state*>(this); 74 } 75 destroyspot::kripke_graph_state76 virtual void destroy() const override 77 { 78 } 79 condspot::kripke_graph_state80 bdd cond() const 81 { 82 return cond_; 83 } 84 condspot::kripke_graph_state85 void cond(bdd c) 86 { 87 cond_ = c; 88 } 89 90 private: 91 bdd cond_; 92 }; 93 94 template<class Graph> 95 class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator 96 { 97 private: 98 typedef typename Graph::edge edge; 99 typedef typename Graph::state_data_t state; 100 const Graph* g_; 101 edge t_; 102 edge p_; 103 public: kripke_graph_succ_iterator(const Graph * g,const typename Graph::state_storage_t * s)104 kripke_graph_succ_iterator(const Graph* g, 105 const typename Graph::state_storage_t* s): 106 kripke_succ_iterator(s->cond()), 107 g_(g), 108 t_(s->succ) 109 { 110 } 111 ~kripke_graph_succ_iterator()112 ~kripke_graph_succ_iterator() 113 { 114 } 115 recycle(const typename Graph::state_storage_t * s)116 void recycle(const typename Graph::state_storage_t* s) 117 { 118 cond_ = s->cond(); 119 t_ = s->succ; 120 } 121 first()122 virtual bool first() override 123 { 124 p_ = t_; 125 return p_; 126 } 127 next()128 virtual bool next() override 129 { 130 p_ = g_->edge_storage(p_).next_succ; 131 return p_; 132 } 133 done() const134 virtual bool done() const override 135 { 136 return !p_; 137 } 138 dst() const139 virtual kripke_graph_state* dst() const override 140 { 141 SPOT_ASSERT(!done()); 142 return const_cast<kripke_graph_state*> 143 (&g_->state_data(g_->edge_storage(p_).dst)); 144 } 145 }; 146 147 148 /// \class kripke_graph 149 /// \brief Kripke Structure. 150 class SPOT_API kripke_graph final : public kripke 151 { 152 public: 153 typedef digraph<kripke_graph_state, void> graph_t; 154 // We avoid using graph_t::edge_storage_t because graph_t is not 155 // instantiated in the SWIG bindings, and SWIG would therefore 156 // handle graph_t::edge_storage_t as an abstract type. 157 typedef internal::edge_storage<unsigned, unsigned, unsigned, 158 internal::boxed_label 159 <void, true>> 160 edge_storage_t; 161 static_assert(std::is_same<typename graph_t::edge_storage_t, 162 edge_storage_t>::value, "type mismatch"); 163 164 typedef internal::distate_storage<unsigned, 165 internal::boxed_label<kripke_graph_state, false>> 166 state_storage_t; 167 static_assert(std::is_same<typename graph_t::state_storage_t, 168 state_storage_t>::value, "type mismatch"); 169 typedef std::vector<state_storage_t> state_vector; 170 171 // We avoid using graph_t::state for the very same reason. 172 typedef unsigned state_num; 173 static_assert(std::is_same<typename graph_t::state, state_num>::value, 174 "type mismatch"); 175 176 protected: 177 graph_t g_; 178 mutable unsigned init_number_; 179 public: kripke_graph(const bdd_dict_ptr & d)180 kripke_graph(const bdd_dict_ptr& d) 181 : kripke(d), init_number_(0) 182 { 183 } 184 ~kripke_graph()185 virtual ~kripke_graph() 186 { 187 get_dict()->unregister_all_my_variables(this); 188 } 189 num_states() const190 unsigned num_states() const 191 { 192 return g_.num_states(); 193 } 194 num_edges() const195 unsigned num_edges() const 196 { 197 return g_.num_edges(); 198 } 199 set_init_state(state_num s)200 void set_init_state(state_num s) 201 { 202 if (SPOT_UNLIKELY(s >= num_states())) 203 throw std::invalid_argument 204 ("set_init_state() called with nonexisiting state"); 205 init_number_ = s; 206 } 207 get_init_state_number() const208 state_num get_init_state_number() const 209 { 210 // If the kripke has no state, it has no initial state. 211 if (num_states() == 0) 212 throw std::runtime_error("kripke has no state at all"); 213 return init_number_; 214 } 215 get_init_state() const216 virtual const kripke_graph_state* get_init_state() const override 217 { 218 return state_from_number(get_init_state_number()); 219 } 220 221 /// \brief Allow to get an iterator on the state we passed in 222 /// parameter. 223 virtual kripke_graph_succ_iterator<graph_t>* succ_iter(const spot::state * st) const224 succ_iter(const spot::state* st) const override 225 { 226 auto s = down_cast<const typename graph_t::state_storage_t*>(st); 227 SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ)); 228 229 if (this->iter_cache_) 230 { 231 auto it = 232 down_cast<kripke_graph_succ_iterator<graph_t>*>(this->iter_cache_); 233 it->recycle(s); 234 this->iter_cache_ = nullptr; 235 return it; 236 } 237 return new kripke_graph_succ_iterator<graph_t>(&g_, s); 238 239 } 240 241 state_num state_number(const state * st) const242 state_number(const state* st) const 243 { 244 auto s = down_cast<const typename graph_t::state_storage_t*>(st); 245 return s - &g_.state_storage(0); 246 } 247 248 const kripke_graph_state* state_from_number(state_num n) const249 state_from_number(state_num n) const 250 { 251 return &g_.state_data(n); 252 } 253 254 kripke_graph_state* state_from_number(state_num n)255 state_from_number(state_num n) 256 { 257 return &g_.state_data(n); 258 } 259 format_state(unsigned n) const260 std::string format_state(unsigned n) const 261 { 262 auto named = get_named_prop<std::vector<std::string>>("state-names"); 263 if (named && n < named->size()) 264 return (*named)[n]; 265 266 return std::to_string(n); 267 } 268 format_state(const state * st) const269 virtual std::string format_state(const state* st) const override 270 { 271 return format_state(state_number(st)); 272 } 273 274 /// \brief Get the condition on the state state_condition(const state * s) const275 virtual bdd state_condition(const state* s) const override 276 { 277 auto gs = down_cast<const kripke_graph_state*>(s); 278 return gs->cond(); 279 } 280 edge_storage(unsigned t)281 edge_storage_t& edge_storage(unsigned t) 282 { 283 return g_.edge_storage(t); 284 } 285 edge_storage(unsigned t) const286 const edge_storage_t edge_storage(unsigned t) const 287 { 288 return g_.edge_storage(t); 289 } 290 new_state(bdd cond)291 unsigned new_state(bdd cond) 292 { 293 return g_.new_state(cond); 294 } 295 new_states(unsigned n,bdd cond)296 unsigned new_states(unsigned n, bdd cond) 297 { 298 return g_.new_states(n, cond); 299 } 300 new_edge(unsigned src,unsigned dst)301 unsigned new_edge(unsigned src, unsigned dst) 302 { 303 return g_.new_edge(src, dst); 304 } 305 306 307 #ifndef SWIG states() const308 const state_vector& states() const 309 { 310 return g_.states(); 311 } 312 #endif 313 states()314 state_vector& states() 315 { 316 return g_.states(); 317 } 318 319 #ifndef SWIG 320 internal::all_trans<const graph_t> edges() const321 edges() const noexcept 322 { 323 return g_.edges(); 324 } 325 #endif 326 327 internal::all_trans<graph_t> edges()328 edges() noexcept 329 { 330 return g_.edges(); 331 } 332 333 #ifndef SWIG 334 internal::state_out<const graph_t> out(unsigned src) const335 out(unsigned src) const 336 { 337 return g_.out(src); 338 } 339 #endif 340 341 internal::state_out<graph_t> out(unsigned src)342 out(unsigned src) 343 { 344 return g_.out(src); 345 } 346 347 }; 348 349 typedef std::shared_ptr<kripke_graph> kripke_graph_ptr; 350 351 inline kripke_graph_ptr make_kripke_graph(const bdd_dict_ptr & d)352 make_kripke_graph(const bdd_dict_ptr& d) 353 { 354 return std::make_shared<kripke_graph>(d); 355 } 356 } 357