1# -*- coding: utf-8 -*- 2#+TITLE: Implementing an on-the-fly Kripke structure 3#+DESCRIPTION: Implementing an Kripke structure in C++, allowing on-the-fly exploration 4#+INCLUDE: setup.org 5#+HTML_LINK_UP: tut.html 6 7 8Kripke structures, can be defined as ω-automata in which labels are on 9states, and where all runs are accepting (i.e., the acceptance 10condition is =t=). They are typically used by model checkers to 11represent the state space of the model to verify. 12 13* Implementing a toy Kripke structure 14 15In this example, our goal is to implement a Kripke structure that 16constructs its state space on the fly. ([[file:tut52.org][Another page]] shows how to 17implement this Kripke structure using an explicit graph instead.) 18 19The states of our toy model will consist of a pair of modulo-3 20integers $(x,y)$; and at any state the possible actions will be to 21increment any one of the two integer (nondeterministicaly). That 22increment is obviously done modulo 3. For instance state $(1,2)$ has 23two possible successors: 24 - $(2,2)$ if =x= was incremented, or 25 - $(1,0)$ if =y= was incremented. 26Initially both variables will be 0. The complete state space is 27expected to have 9 states. But even if it is small because it is a 28toy example, we do not want to precompute it. It should be computed 29as needed, using [[file:tut50.org::#on-the-fly-interface][the one-the-fly interface]] previously discussed. 30 31In addition, we would like to label each state by atomic propositions 32=odd_x= and =odd_y= that are true only when the corresponding 33variables are odd. Using such variables, we could try to verify 34whether if =odd_x= infinitely often holds, then =odd_y= infinitely 35often holds as well. 36 37** What needs to be done 38 39In Spot, Kripke structures are implemented as subclass of =twa=, but 40some operations have specialized versions that takes advantages of the 41state-labeled nature of Kripke structure. For instance the on-the-fly 42product of a Kripke structure with a =twa= is slightly more efficient 43than the on-the-fly product of two =twa=. 44 45#+NAME: headers 46#+BEGIN_SRC C++ 47#include <spot/kripke/kripke.hh> 48#+END_SRC 49 50The =kripke/kripke.hh= header defines an abstract =kripke= class that 51is a subclass of =twa=, and a =kripke_succ_iterator= that is a subclass 52of =twa_succ_iterator=. Both class defines some of the methods of 53the =twa= interface that are common to all Kripke structure, leaving 54us with a handful of methods to implement. 55 56The following class diagram is a simplified picture of the reality, 57but good enough for show what we have to implement. 58 59#+BEGIN_SRC plantuml :file uml-kripke.svg 60 package spot { 61 together { 62 abstract class twa { 63 #twa_succ_iterator* iter_cache_ 64 #bdd_dict_ptr dict_ 65 __ 66 #twa(const bdd_dict_ptr&) 67 .. exploration .. 68 +{abstract}state* get_init_state() 69 +{abstract}twa_succ_iterator* succ_iter(state*) 70 +internal::succ_iterable succ(const state*) 71 +void release_iter(twa_succ_iterator*) 72 .. state manipulation .. 73 +{abstract} std::string format_state(const state*) 74 +state* project_state(const state*, const const_twa_ptr&) 75 .. other methods not shown.. 76 } 77 abstract class twa_succ_iterator { 78 .. iteration .. 79 {abstract}+bool first() 80 {abstract}+bool next() 81 {abstract}+bool done() 82 .. inspection .. 83 {abstract}+const state* dst() 84 {abstract}+bdd cond() 85 {abstract}+acc_cond::mark_t acc() 86 } 87 88 abstract class state { 89 +{abstract}int compare(const state*) 90 +{abstract}size_t hash() 91 +{abstract}state* clone() 92 +void destroy() 93 #~state() 94 } 95 } 96 together { 97 abstract class kripke { 98 +fair_kripke(const bdd_dict_ptr&) 99 +{abstract}bdd state_condition(const state*) 100 } 101 abstract class kripke_succ_iterator { 102 #bdd cond_ 103 +kripke_succ_iterator(const bdd&) 104 +void recycle(const bdd&) 105 +bdd cond() 106 +acc_cond::mark_t acc() 107 } 108 } 109 twa <|-- kripke 110 twa_succ_iterator <|-- kripke_succ_iterator 111 } 112 113 package "what we have to implement" <<Cloud>> { 114 class demo_kripke { 115 +state* get_init_state() 116 +twa_succ_iterator* succ_iter(state*) 117 +std::string format_state(const state*) 118 +bdd state_condition(const state*) 119 } 120 class demo_succ_iterator { 121 +bool first() 122 +bool next() 123 +bool done() 124 +const state* dst() 125 } 126 class demo_state { 127 +int compare(const state*) 128 +size_t hash() 129 +state* clone() 130 } 131 } 132state <|-- demo_state 133kripke_succ_iterator <|-- demo_succ_iterator 134kripke <|-- demo_kripke 135#+END_SRC 136 137#+RESULTS: 138[[file:uml-kripke.svg]] 139 140 141** Implementing the =state= subclass 142 143Let us start with the =demo_state= class. It should 144- store the values of =x= and =y=, and provide access to them, 145- have a =clone()= function to duplicate the state, 146- have a =hash()= method that returns a =size_t= value usable as hash key, 147- have a =compare()= function that returns an integer less than, equal to, or greater 148 than zero if =this= is found to be less than, equal 149 to, or greater than the other state according to some total order we are free 150 to choose. 151 152Since our state space is so trivial, we could use =(x<<2) + y= as a 153/perfect/ hash function, which implies that in this case we can also 154implement =compare()= using =hash()=. 155 156#+NAME: demo-state 157#+BEGIN_SRC C++ 158 class demo_state: public spot::state 159 { 160 private: 161 unsigned char x_; 162 unsigned char y_; 163 public: 164 demo_state(unsigned char x = 0, unsigned char y = 0) 165 : x_(x % 3), y_(y % 3) 166 { 167 } 168 169 unsigned get_x() const 170 { 171 return x_; 172 } 173 174 unsigned get_y() const 175 { 176 return y_; 177 } 178 179 demo_state* clone() const override 180 { 181 return new demo_state(x_, y_); 182 } 183 184 size_t hash() const override 185 { 186 return (x_ << 2) + y_; 187 } 188 189 int compare(const spot::state* other) const override 190 { 191 auto o = static_cast<const demo_state*>(other); 192 size_t oh = o->hash(); 193 size_t h = hash(); 194 if (h < oh) 195 return -1; 196 else 197 return h > oh; 198 } 199 }; 200#+END_SRC 201 202#+RESULTS: demo-state 203 204Note that a state does not know how to print itself, this 205a job for the automaton. 206 207** Implementing the =kripke_succ_iterator= subclass 208 209 Now let us implement the iterator. It will be constructed from a pair 210 $(x,y)$ and during its iteration it should produce two new states 211 $(x+1,y)$ and $(x,y+1)$. We do not have to deal with the modulo 212 operation, as that is done by the =demo_state= constructor. Since 213 this is an iterator, we also need to remember the position of the 214 iterator: this position can take 3 values: 215 - when =pos=2= then the successor is $(x+1,y)$ 216 - when =pos=1= then the successor is $(x,y+1)$ 217 - when =pos=0= the iteration is over. 218 We decided to use =pos=0= as the last value, as testing for =0= is 219 easier and will occur frequently. 220 221 When need to implement the iteration methods =first()=, =next()=, and 222 =done()=, as well as the =dst()= method. The other =cond()= and 223 =acc()= methods are already implemented in the =kripke_succ_iterator=, 224 but that guy needs to know what condition =cond= labels the state. 225 226 We also add a =recycle()= method that we will discuss later. 227 228 #+NAME: demo-iterator 229 #+BEGIN_SRC C++ 230 class demo_succ_iterator: public spot::kripke_succ_iterator 231 { 232 private: 233 unsigned char x_; 234 unsigned char y_; 235 unsigned char pos_; 236 public: 237 demo_succ_iterator(unsigned char x, unsigned char y, bdd cond) 238 : kripke_succ_iterator(cond), x_(x), y_(y) 239 { 240 } 241 242 bool first() override 243 { 244 pos_ = 2; 245 return true; // There exists a successor. 246 } 247 248 bool next() override 249 { 250 --pos_; 251 return pos_ > 0; // More successors? 252 } 253 254 bool done() const override 255 { 256 return pos_ == 0; 257 } 258 259 demo_state* dst() const override 260 { 261 return new demo_state(x_ + (pos_ == 2), 262 y_ + (pos_ == 1)); 263 } 264 265 void recycle(unsigned char x, unsigned char y, bdd cond) 266 { 267 x_ = x; 268 y_ = y; 269 spot::kripke_succ_iterator::recycle(cond); 270 } 271 }; 272 #+END_SRC 273 274** Implementing the =kripke= subclass itself 275 276 Finally, let us implement the Kripke structure itself. We only have 277 four methods of the interface to implement: 278 - =get_init_state()= should return the initial state, 279 - =succ_iter(s)= should build a =demo_succ_iterator= for edges leaving =s=, 280 - =state_condition(s)= should return the label of =s=, 281 - =format_state(s)= should return a textual representation of the state for display. 282 283 In addition, we need to declare the two atomic propositions =odd_x= 284 and =odd_y= we wanted to use. 285 286 #+NAME: demo-kripke 287 #+BEGIN_SRC C++ 288 class demo_kripke: public spot::kripke 289 { 290 private: 291 bdd odd_x_; 292 bdd odd_y_; 293 public: 294 demo_kripke(const spot::bdd_dict_ptr& d) 295 : spot::kripke(d) 296 { 297 odd_x_ = bdd_ithvar(register_ap("odd_x")); 298 odd_y_ = bdd_ithvar(register_ap("odd_y")); 299 } 300 301 demo_state* get_init_state() const override 302 { 303 return new demo_state(); 304 } 305 306 // To be defined later. 307 demo_succ_iterator* succ_iter(const spot::state* s) const override; 308 309 bdd state_condition(const spot::state* s) const override 310 { 311 auto ss = static_cast<const demo_state*>(s); 312 bool xodd = ss->get_x() & 1; 313 bool yodd = ss->get_y() & 1; 314 return (xodd ? odd_x_ : !odd_x_) & (yodd ? odd_y_ : !odd_y_); 315 } 316 317 std::string format_state(const spot::state* s) const override 318 { 319 auto ss = static_cast<const demo_state*>(s); 320 std::ostringstream out; 321 out << "(x = " << ss->get_x() << ", y = " << ss->get_y() << ')'; 322 return out.str(); 323 } 324 }; 325 #+END_SRC 326 327 We have left the definition of =succ_iter= out, because we will 328 propose two versions. The most straightforward is the following: 329 330 #+NAME: demo-succ-iter-1 331 #+BEGIN_SRC C++ 332 demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const 333 { 334 auto ss = static_cast<const demo_state*>(s); 335 return new demo_succ_iterator(ss->get_x(), ss->get_y(), state_condition(ss)); 336 } 337 #+END_SRC 338 339A better implementation of =demo_kripke::succ_iter= would be to make 340use of recycled iterators. Remember that when an algorithm (such a 341=print_dot=) releases an iterator, it calls =twa::release_iter()=. 342This method stores the last released iterator in =twa::iter_cache_=. 343This cached iterator could be reused by =succ_iter=: this avoids a 344=delete= / =new= pair, and it also avoids the initialization of the 345virtual method table of the iterator. In short: it saves time. Here 346is an implementation that does this. 347 348#+NAME: demo-succ-iter-2 349#+BEGIN_SRC C++ 350 demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const 351 { 352 auto ss = static_cast<const demo_state*>(s); 353 unsigned char x = ss->get_x(); 354 unsigned char y = ss->get_y(); 355 bdd cond = state_condition(ss); 356 if (iter_cache_) 357 { 358 auto it = static_cast<demo_succ_iterator*>(iter_cache_); 359 iter_cache_ = nullptr; // empty the cache 360 it->recycle(x, y, cond); 361 return it; 362 } 363 return new demo_succ_iterator(x, y, cond); 364 } 365#+END_SRC 366 367Note that the =demo_succ_iterator::recycle= method was introduced for 368this reason. 369 370* Displaying the state space 371 372 Here is a short =main= displaying the state space of our toy Kripke structure. 373 374#+NAME: demo-1-aux 375#+BEGIN_SRC C++ :exports none :noweb strip-export 376 <<headers>> 377 <<demo-state>> 378 <<demo-iterator>> 379 <<demo-kripke>> 380 <<demo-succ-iter-2>> 381#+END_SRC 382 383#+NAME: demo-1 384#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim 385#include <spot/twaalgos/dot.hh> 386<<demo-1-aux>> 387int main() 388{ 389 auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict()); 390 spot::print_dot(std::cout, k); 391} 392#+END_SRC 393 394#+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results 395$txt 396#+END_SRC 397 398#+RESULTS: 399[[file:kripke-1.svg]] 400 401* Checking a property on this state space 402 :PROPERTIES: 403 :CUSTOM_ID: prop-check 404 :END: 405 406Let us pretend that we want to verify the following property: if 407=odd_x= infinitely often holds, then =odd_y= infinitely often holds. 408 409In LTL, that would be =GF(odd_x) -> GF(odd_y)=. 410 411To check this formula, we translate its negation into an automaton, 412build the product of this automaton with our Kripke structure, and 413check whether the output is empty. If it is not, that means we have 414found a counterexample. Here is some code that would show this 415counterexample: 416 417#+NAME: demo-2 418#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim 419#include <spot/tl/parse.hh> 420#include <spot/twaalgos/translate.hh> 421#include <spot/twaalgos/emptiness.hh> 422<<demo-1-aux>> 423int main() 424{ 425 auto d = spot::make_bdd_dict(); 426 427 // Parse the input formula. 428 spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); 429 if (pf.format_errors(std::cerr)) 430 return 1; 431 432 // Translate its negation. 433 spot::formula f = spot::formula::Not(pf.f); 434 spot::twa_graph_ptr af = spot::translator(d).run(f); 435 436 // Find a run of or demo_kripke that intersects af. 437 auto k = std::make_shared<demo_kripke>(d); 438 if (auto run = k->intersecting_run(af)) 439 std::cout << "formula is violated by the following run:\n" << *run; 440 else 441 std::cout << "formula is verified\n"; 442} 443#+END_SRC 444 445# temporary fix for an issue in Org 9.2, see 446# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html 447#+BEGIN_SRC text :noweb yes 448<<demo-2()>> 449#+END_SRC 450 451With a small variant of the above code, we could also display the 452counterexample on the state space, but only because our state space is 453so small: displaying large state spaces is not sensible. Besides, 454highlighting a run only works on =twa_graph= automata, so we need to 455convert the Kripke structure to a =twa_graph=: this can be done with 456=make_twa_graph()=. But now =k= is no longer a Kripke structure (also 457not generated on-the-fly anymore), so the =print_dot()= function will 458display it as a classical automaton with conditions on edges rather 459than state: passing the option "~k~" to =print_dot()= will fix that. 460We also pass option "~A~" to hide the acceptance condition (which is 461=t=, i.e., accepting every infinite run). 462 463#+NAME: demo-3-aux 464#+BEGIN_SRC C++ :exports none :noweb strip-export 465 <<headers>> 466 <<demo-state>> 467 <<demo-iterator>> 468 <<demo-kripke>> 469 <<demo-succ-iter-2>> 470#+END_SRC 471 472#+NAME: demo-3 473#+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim 474 #include <spot/twaalgos/dot.hh> 475 #include <spot/tl/parse.hh> 476 #include <spot/twaalgos/translate.hh> 477 #include <spot/twaalgos/emptiness.hh> 478 <<demo-3-aux>> 479 int main() 480 { 481 auto d = spot::make_bdd_dict(); 482 483 // Parse the input formula. 484 spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); 485 if (pf.format_errors(std::cerr)) 486 return 1; 487 488 // Translate its negation. 489 spot::formula f = spot::formula::Not(pf.f); 490 spot::twa_graph_ptr af = spot::translator(d).run(f); 491 492 // Convert demo_kripke into an explicit graph 493 spot::twa_graph_ptr k = 494 spot::make_twa_graph(std::make_shared<demo_kripke>(d), 495 spot::twa::prop_set::all(), true); 496 // Find a run of or demo_kripke that intersects af. 497 if (auto run = k->intersecting_run(af)) 498 { 499 run->highlight(5); // 5 is a color number. 500 spot::print_dot(std::cout, k, ".kA"); 501 } 502 } 503#+END_SRC 504 505#+BEGIN_SRC dot :file kripke-3.svg :cmd circo :var txt=demo-3 :exports results 506$txt 507#+END_SRC 508 509#+RESULTS: 510[[file:kripke-3.svg]] 511 512Note that labeling states with names (the first line) and the 513valuation of all atomic propositions (the second line) will quickly 514produce graphs with large nodes that are problematic to render. A 515trick to reduce the clutter and the size of the graph is to pass 516option "~1~" to =print_dot()=, changing the above call to 517src_cpp[:exports code]{spot::print_dot(std::cout, k, ".kA1");}. This 518will cause all states to be numbered instead, but if the automaton is 519rendered as an SVG figure, the old label will still appear as a 520tooltip when the mouse is over a state. Try that on the following 521figure: 522 523#+NAME: demo-3b 524#+BEGIN_SRC C++ :exports none :noweb strip-export :results verbatim 525 #include <spot/twaalgos/dot.hh> 526 #include <spot/tl/parse.hh> 527 #include <spot/twaalgos/translate.hh> 528 #include <spot/twaalgos/emptiness.hh> 529 <<demo-3-aux>> 530 int main() 531 { 532 auto d = spot::make_bdd_dict(); 533 534 // Parse the input formula. 535 spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); 536 if (pf.format_errors(std::cerr)) 537 return 1; 538 539 // Translate its negation. 540 spot::formula f = spot::formula::Not(pf.f); 541 spot::twa_graph_ptr af = spot::translator(d).run(f); 542 543 // Convert demo_kripke into an explicit graph 544 spot::twa_graph_ptr k = 545 spot::make_twa_graph(std::make_shared<demo_kripke>(d), 546 spot::twa::prop_set::all(), true); 547 // Find a run of or demo_kripke that intersects af. 548 if (auto run = k->intersecting_run(af)) 549 { 550 run->highlight(5); // 5 is a color number. 551 spot::print_dot(std::cout, k, ".kA1"); 552 } 553 } 554#+END_SRC 555 556#+BEGIN_SRC dot :file kripke-3b.svg :cmd circo :var txt=demo-3b :exports results 557$txt 558#+END_SRC 559 560#+RESULTS: 561[[file:kripke-3b.svg]] 562 563* Possible improvements 564 565The on-the-fly interface, especially as implemented here, involves a 566lot of memory allocation. In particular, each state is allocated via 567=new demo_state=. Algorithms that receive such a state =s= will later 568call =s->destroy()= to release them, and the default implementation of 569=state::destroy()= is to call =delete=. 570 571But this is only one possible implementation. (It is probably the 572worst.) 573 574It is perfectly possible to write a =kripke= (or even =twa=) subclass 575that returns pointers to preallocated states. In that case 576=state::destroy()= would have to be overridden with an empty body so 577that no deallocation occurs, and the automaton would have to get rid 578of the allocated states in its destructor. Also the =state::clone()= 579methods is overridden by a function that returns the identity. An 580example of class following this convention is =twa_graph=, were states 581returned by the on-the-fly interface are just pointers into the actual 582state vector (which is already known). 583 584Even if the state space is not already known, it is possible to 585implement the on-the-fly interface in such a way that all =state*= 586pointers returned for a state are unique. This requires a state 587unicity table into the automaton, and then =state::clone()= and 588=state::destroy()= could be used to do just reference counting. An 589example of class implementing this scheme is the =spot::twa_product= 590class, used to build on-the-fly product. 591 592# LocalWords: utf Kripke SETUPFILE html automata precompute twa SRC 593# LocalWords: nondeterministicaly kripke succ plantuml uml png iter 594# LocalWords: bdd ptr const init bool dst cond acc pos ithvar ap ss 595# LocalWords: xodd yodd str nullptr noweb cmdline Tpng cmd circo GF 596# LocalWords: txt LTL af preallocated deallocation destructor svg 597# LocalWords: unicity kA src cpp tooltip 598