diff --git a/NEWS b/NEWS index c19813150..871c158d5 100644 --- a/NEWS +++ b/NEWS @@ -179,6 +179,10 @@ New in spot 2.0.3a (not yet released) * A new page discusses explicit vs. on-the-fly interfaces for exploring automata in C++. https://spot.lrde.epita.fr/tut50.html + * Another new page shows how to implement an on-the-fly Kripke + structure to implement a custom state space. + https://spot.lrde.epita.fr/tut51.html + * The concepts.html page now lists all named properties used by automata. diff --git a/doc/Makefile.am b/doc/Makefile.am index 342ab6629..5334e6ce2 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -107,6 +107,7 @@ ORG_FILES = \ org/tut22.org \ org/tut30.org \ org/tut50.org \ + org/tut51.org \ org/upgrade2.org \ org/satmin.org \ org/satmin.tex \ diff --git a/doc/org/tut.org b/doc/org/tut.org index d847dc52a..b0904ff9c 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -36,6 +36,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. * Examples in C++ only - [[file:tut50.org][Explicit vs. on-the-fly: two interfaces for exploring automata]] +- [[file:tut51.org][Implementing an on-the-fly Kripke structure]] * Examples in Python only diff --git a/doc/org/tut51.org b/doc/org/tut51.org new file mode 100644 index 000000000..5b3d404e6 --- /dev/null +++ b/doc/org/tut51.org @@ -0,0 +1,575 @@ +# -*- coding: utf-8 -*- +#+TITLE: Implementing an on-the-fly Kripke structure +#+DESCRIPTION: Implementing an Kripke structure in C++, allowing on-the-fly exploration +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + + +Kripke structures, can be defined as ω-automata in which labels are on +states, and where all runs are accepting (i.e., the acceptance +condition is =t=). They are typically used by model checkers to +represent the state-space of the model to verify. + + +* Implementing a toy Kripke structure + +In this example, our goal is to implement a Kripke structure that +constructs its state-space on the fly. The states of our toy model +will consist of a pair of modulo-3 integers $(x,y)$; and at any state +the possible actions will be to increment any one of the two integer +(nondeterministicaly). That increment is obviously done modulo 3. +For instance state $(1,2)$ has two possible successors: + - $(2,2)$ if =x= was incremented, or + - $(1,0)$ if =y= was incremented. +Initially both variables will be 0. The complete state-space is +expected to have 9 states. But even if it is small because it is a +toy example, we do not want to precompute it. It should be computed +as needed, using [[file:tut50.org::#on-the-fly-interface][the one-the-fly interface]] previously discussed. + +In addition, we would like to label each state by atomic propositions +=odd_x= and =odd_y= that are true only when the corresponding +variables are odd. Using such variables, we could try to verify +whether if =odd_x= infinitely often holds, then =odd_y= infinitely +often holds as well. + +** What needs to be done + +In Spot, Kripke structures are implemented as subclass of =twa=, but +some operations have specialized versions that takes advantages of the +state-labeled nature of Kripke structure. For instance the on-the-fly +product of a Kripke structure with a =twa= is slightly more efficient +than the on-the-fly product of two =twa=. + +#+NAME: headers +#+BEGIN_SRC C++ +#include +#+END_SRC + +The =kripke/kripke.hh= header defines an abstract =kripke= class that +is a subclass of =twa=, and a =kripke_succ_iterator= that is a subclass +of =twa_succ_iterator=. Both class defines some of the methods of +the =twa= interface that are common to all Kripke structure, leaving +us with a handful of methods to implement. + +The following class diagram is a simplified picture of the reality, +but good enough for show what we have to implement. + +#+BEGIN_SRC plantuml :file uml-kripke.png + package spot { + together { + abstract class twa { + #twa_succ_iterator* iter_cache_ + #bdd_dict_ptr dict_ + __ + #twa(const bdd_dict_ptr&) + .. exploration .. + +{abstract}state* get_init_state() + +{abstract}twa_succ_iterator* succ_iter(state*) + +internal::succ_iterable succ(const state*) + +void release_iter(twa_succ_iterator*) + .. state manipulation .. + +{abstract} std::string format_state(const state*) + +state* project_state(const state*, const const_twa_ptr&) + .. other methods not shown.. + } + abstract class twa_succ_iterator { + .. iteration .. + {abstract}+bool first() + {abstract}+bool next() + {abstract}+bool done() + .. inspection .. + {abstract}+const state* dst() + {abstract}+bdd cond() + {abstract}+acc_cond::mark_t acc() + } + + abstract class state { + +{abstract}int compare(const state*) + +{abstract}size_t hash() + +{abstract}state* clone() + +void destroy() + #~state() + } + } + together { + abstract class kripke { + +fair_kripke(const bdd_dict_ptr&) + +{abstract}bdd state_condition(const state*) + } + abstract class kripke_succ_iterator { + #bdd cond_ + +kripke_succ_iterator(const bdd&) + +void recycle(const bdd&) + +bdd cond() + +acc_cond::mark_t acc() + } + } + twa <|-- kripke + twa_succ_iterator <|-- kripke_succ_iterator + } + + package "what we have to implement" <> { + class demo_kripke { + +state* get_init_state() + +twa_succ_iterator* succ_iter(state*) + +std::string format_state(const state*) + +bdd state_condition(const state*) + } + class demo_succ_iterator { + +bool first() + +bool next() + +bool done() + +const state* dst() + } + class demo_state { + +int compare(const state*) + +size_t hash() + +state* clone() + } + } +state <|-- demo_state +kripke_succ_iterator <|-- demo_succ_iterator +kripke <|-- demo_kripke +#+END_SRC + +#+RESULTS: +[[file:uml-kripke.png]] + + +** Implementing the =state= subclass + +Let us start with the =demo_state= class. It should +- store the values of =x= and =y=, and provide access to them, +- have a =clone()= function to duplicate the state, +- have a =hash()= method that returns a =size_t= value usable as hash key, +- have a =compare()= function that returns an integer less than, equal to, or greater + than zero if =this= is found to be less than, equal + to, or greater than the other state according to some total order we are free + to choose. + +Since our state space is so trivial, we could use =(x<<2) + y= as a +/perfect/ hash function, which implies that in this case we can also +implement =compare()= using =hash()=. + +#+NAME: demo-state +#+BEGIN_SRC C++ + class demo_state: public spot::state + { + private: + unsigned char x_; + unsigned char y_; + public: + demo_state(unsigned char x = 0, unsigned char y = 0) + : x_(x % 3), y_(y % 3) + { + } + + unsigned get_x() const + { + return x_; + } + + unsigned get_y() const + { + return y_; + } + + demo_state* clone() const override + { + return new demo_state(x_, y_); + } + + size_t hash() const override + { + return (x_ << 2) + y_; + } + + int compare(const spot::state* other) const override + { + auto o = static_cast(other); + size_t oh = o->hash(); + size_t h = hash(); + if (h < oh) + return -1; + else + return h > oh; + } + }; +#+END_SRC + +#+RESULTS: demo-state + +Note that a state does not know how to print itself, this +a job for the automaton. + +** Implementing the =kripke_succ_iterator= subclass + + Now let us implement the iterator. It will be constructed from a pair + $(x,y)$ and during its iteration it should produce two new states + $(x+1,y)$ and $(x,y+1)$. We do not have to deal with the modulo + operation, as that is done by the =demo_state= constructor. Since + this is an iterator, we also need to remember the position of the + iterator: this position can take 3 values: + - when =pos=2= then the successor is $(x+1,y)$ + - when =pos=1= then the successor is $(x,y+1)$ + - when =pos=0= the iteration is over. + We decided to use =pos=0= as the last value, as testing for =0= is + easier and will occur frequently. + + When need to implement the iteration methods =first()=, =next()=, and + =done()=, as well as the =dst()= method. The other =cond()= and + =acc()= methods are already implemented in the =kripke_succ_iterator=, + but that guy needs to know what condition =cond= labels the state. + + We also add a =recycle()= method that we will discuss later. + + #+NAME: demo-iterator + #+BEGIN_SRC C++ + class demo_succ_iterator: public spot::kripke_succ_iterator + { + private: + unsigned char x_; + unsigned char y_; + unsigned char pos_; + public: + demo_succ_iterator(unsigned char x, unsigned char y, bdd cond) + : kripke_succ_iterator(cond), x_(x), y_(y) + { + } + + bool first() override + { + pos_ = 2; + return true; // There exists a successor. + } + + bool next() override + { + --pos_; + return pos_ > 0; // More successors? + } + + bool done() const override + { + return pos_ == 0; + } + + demo_state* dst() const override + { + return new demo_state(x_ + (pos_ == 2), + y_ + (pos_ == 1)); + } + + void recycle(unsigned char x, unsigned char y, bdd cond) + { + x_ = x; + y_ = y; + spot::kripke_succ_iterator::recycle(cond); + } + }; + #+END_SRC + +** Implementing the =kripke= subclass itself + + Finally, let us implement the Kripke structure itself. We only have + four methods of the interface to implement: + - =get_init_state()= should return the initial state, + - =succ_iter(s)= should build a =demo_succ_iterator= for edges leaving =s=, + - =state_condition(s)= should return the label of =s=, + - =format_state(s)= should return a textual representation of the state for display. + + In addition, we need to declare the two atomic propositions =odd_x= + and =odd_y= we wanted to use. + + #+NAME: demo-kripke + #+BEGIN_SRC C++ + class demo_kripke: public spot::kripke + { + private: + bdd odd_x_; + bdd odd_y_; + public: + demo_kripke(const spot::bdd_dict_ptr& d) + : spot::kripke(d) + { + odd_x_ = bdd_ithvar(register_ap("odd_x")); + odd_y_ = bdd_ithvar(register_ap("odd_y")); + } + + demo_state* get_init_state() const override + { + return new demo_state(); + } + + // To be defined later. + demo_succ_iterator* succ_iter(const spot::state* s) const override; + + bdd state_condition(const spot::state* s) const override + { + auto ss = static_cast(s); + bool xodd = ss->get_x() & 1; + bool yodd = ss->get_y() & 1; + return (xodd ? odd_x_ : !odd_x_) & (yodd ? odd_y_ : !odd_y_); + } + + std::string format_state(const spot::state* s) const override + { + auto ss = static_cast(s); + std::ostringstream out; + out << "(x = " << ss->get_x() << ", y = " << ss->get_y() << ')'; + return out.str(); + } + }; + #+END_SRC + + We have left the definition of =succ_iter= out, because we will + propose two versions. The most straightforward is the following: + + #+NAME: demo-succ-iter-1 + #+BEGIN_SRC C++ + demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const + { + auto ss = static_cast(s); + return new demo_succ_iterator(ss->get_x(), ss->get_y(), state_condition(ss)); + } + #+END_SRC + +A better implementation of =demo_kripke::succ_iter= would be to make +use of recycled iterators. Remember that when an algorithm (such a +=print_dot=) releases an iterator, it calls =twa::release_iter()=. +This method stores the last released iterator in =twa::iter_cache_=. +This cached iterator could be reused by =succ_iter=: this avoids a +=delete= / =new= pair, and it also avoids the initialization of the +virtual method table of the iterator. In short: it saves time. Here +is an implementation that does this. + +#+NAME: demo-succ-iter-2 +#+BEGIN_SRC C++ + demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const + { + auto ss = static_cast(s); + unsigned char x = ss->get_x(); + unsigned char y = ss->get_y(); + bdd cond = state_condition(ss); + if (iter_cache_) + { + auto it = static_cast(iter_cache_); + iter_cache_ = nullptr; // empty the cache + it->recycle(x, y, cond); + return it; + } + return new demo_succ_iterator(x, y, cond); + } +#+END_SRC + +Note that the =demo_succ_iterator::recycle= method was introduced for +this reason. + +* Displaying the state-space + + Here is a short =main= displaying the state-space of our toy Kripke structure. + +#+NAME: demo-1-aux +#+BEGIN_SRC C++ :exports none :noweb strip-export + <> + <> + <> + <> + <> +#+END_SRC + + #+NAME: demo-1 + #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim + #include + <> + int main() + { + auto k = std::make_shared(spot::make_bdd_dict()); + spot::print_dot(std::cout, k); + } + #+END_SRC + + #+BEGIN_SRC dot :file kripke-1.png :cmdline -Tpng :cmd circo :var txt=demo-1 :exportss results + $txt + #+END_SRC + + #+RESULTS: + [[file:kripke-1.png]] + +* Checking a property on this state space + +Let us pretend that we want to verify the following property: if +=odd_x= infinitely often holds, then =odd_y= infinitely often holds. + +In LTL, that would be =GF(odd_x) -> GF(odd_y)=. + +To check this formula, we translate its negation into an automaton, +build the product of this automaton with our Kripke structure, and +check whether the output is empty. If it is not, that means we have +found a counterexample. Here is some code that would show this +counterexample: + +#+NAME: demo-2-aux +#+BEGIN_SRC C++ :exports none :noweb strip-export + <> + <> + <> + <> + <> +#+END_SRC + + #+NAME: demo-2 + #+BEGIN_SRC C++ :exports both :noweb strip-export :results verbatim + #include + #include + #include + #include + <> + int main() + { + auto d = spot::make_bdd_dict(); + + // Parse the input formula. + spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); + if (pf.format_errors(std::cerr)) + return 1; + + // Translate its negation. + spot::formula f = spot::formula::Not(pf.f); + spot::twa_graph_ptr af = spot::translator(d).run(f); + + // Construct an "on-the-fly product" + auto k = std::make_shared(d); + auto p = spot::otf_product(k, af); + + if (auto run = p->accepting_run()) + { + std::cout << "formula is violated by the following run:\n"; + // "run" is an accepting run over the product. Project it on + // the Kripke structure before displaying it. + std::cout << *run->project(k); + } + else + { + std::cout << "formula is verified\n"; + } + } + #+END_SRC + + #+RESULTS: demo-2 + #+begin_example + formula is violated by the following run: + Prefix: + (x = 0, y = 0) + | !odd_x & !odd_y + (x = 1, y = 0) + | odd_x & !odd_y + (x = 1, y = 1) + | odd_x & odd_y + (x = 1, y = 2) + | odd_x & !odd_y + Cycle: + (x = 2, y = 2) + | !odd_x & !odd_y + (x = 0, y = 2) + | !odd_x & !odd_y + (x = 1, y = 2) + | odd_x & !odd_y +#+end_example + +With a small variant of the above code, we could also display the +counterexample on the state space, but only because our state space is +so small: displaying large state spaces is not sensible. Besides, highlighting +a run only works on =twa_graph= automata, so we need to convert the +Kripke structure to a =twa_graph=: this can be done with =copy()=. But +now =k= is no longer a Kripke structure (also not generated +on-the-fly anymore), so the =print_dot()= function will display it as +a classical automaton with conditions on edges rather than state: +passing the option "~k~" to =print_dot()= will fix that. + +#+NAME: demo-3-aux +#+BEGIN_SRC C++ :exports none :noweb strip-export + <> + <> + <> + <> + <> +#+END_SRC + + #+NAME: demo-3 + #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim + #include + #include + #include + #include + #include + #include + <> + int main() + { + auto d = spot::make_bdd_dict(); + + // Parse the input formula. + spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)"); + if (pf.format_errors(std::cerr)) + return 1; + + // Translate its negation. + spot::formula f = spot::formula::Not(pf.f); + spot::twa_graph_ptr af = spot::translator(d).run(f); + + // Construct an "on-the-fly product" + auto k = spot::copy(std::make_shared(d), spot::twa::prop_set::all(), true); + auto p = spot::otf_product(k, af); + + if (auto run = p->accepting_run()) + { + run->project(k)->highlight(5); // 5 is a color number. + spot::print_dot(std::cout, k, ".k"); + } + } + #+END_SRC + + #+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results + $txt + #+END_SRC + + #+RESULTS: + [[file:kripke-3.png]] + + +* Possible improvements + +The on-the-fly interface, especially as implemented here, involves a +lot of memory allocation. In particular, each state is allocated via +=new demo_state=. Algorithms that receive such a state =s= will later +call =s->destroy()= to release them, and the default implementation of +=state::destroy()= is to call =delete=. + +But this is only one possible implementation. (It is probably the +worst.) + +It is perfectly possible to write a =kripke= (or even =twa=) subclass +that returns pointers to preallocated states. In that case +=state::destroy()= would have to be overridden with an empty body so +that no deallocation occurs, and the automaton would have to get rid +of the allocated states in its destructor. Also the =state::clone()= +methods is overridden by a function that returns the identity. An +example of class following this convention is =twa_graph=, were states +returned by the on-the-fly interface are just pointers into the actual +state vector (which is already known). + +Even if the state-space is not already known, it is possible to +implement the on-the-fly interface in such a way that all =state*= +pointers returned for a state are unique. This requires a state +unicity table into the automaton, and then =state::clone()= and +=state::destroy()= could be used to do just reference counting. An +example of class implementing this scheme is the =spot::twa_product= +class, used to build on-the-fly product. + +# LocalWords: utf Kripke SETUPFILE html automata precompute twa SRC +# LocalWords: nondeterministicaly kripke succ plantuml uml png iter +# LocalWords: bdd ptr const init bool dst cond acc pos ithvar ap ss +# LocalWords: xodd yodd str nullptr noweb cmdline Tpng cmd circo GF +# LocalWords: txt LTL af preallocated deallocation destructor +# LocalWords: unicity diff --git a/elisp/Makefile.am b/elisp/Makefile.am index 0b1213234..b3c105ca1 100644 --- a/elisp/Makefile.am +++ b/elisp/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2015 Laboratoire de Recherche et Développement de -## l'Epita (LRDE). +## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -17,7 +17,7 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -EXTRA_DIST = hoa-mode.el +EXTRA_DIST = hoa-mode.el ob-dot.el GIT = https://gitlab.lrde.epita.fr/spot/emacs-modes/raw/master/ diff --git a/elisp/README b/elisp/README index 97e556ec8..fb779a1ae 100644 --- a/elisp/README +++ b/elisp/README @@ -1,3 +1,7 @@ hoa-mode.el is used when building the documentation for syntax highlighting the HOA files displayed in the examples. But you may also want to use it for editing and displaying HOA files. + +Old versions of org-mode have a version of ob-dot.el that do not +correctly deal with backslashs in dot output. This version fixes +that. diff --git a/elisp/ob-dot.el b/elisp/ob-dot.el new file mode 100644 index 000000000..e2e885788 --- /dev/null +++ b/elisp/ob-dot.el @@ -0,0 +1,91 @@ +;;; ob-dot.el --- org-babel functions for dot evaluation + +;; Copyright (C) 2009-2016 Free Software Foundation, Inc. + +;; Author: Eric Schulte +;; Keywords: literate programming, reproducible research +;; Homepage: http://orgmode.org + +;; This file is part of GNU Emacs. + +;; GNU Emacs is free software: you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation, either version 3 of the License, or +;; (at your option) any later version. + +;; GNU Emacs is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs. If not, see . + +;;; Commentary: + +;; Org-Babel support for evaluating dot source code. +;; +;; For information on dot see http://www.graphviz.org/ +;; +;; This differs from most standard languages in that +;; +;; 1) there is no such thing as a "session" in dot +;; +;; 2) we are generally only going to return results of type "file" +;; +;; 3) we are adding the "file" and "cmdline" header arguments +;; +;; 4) there are no variables (at least for now) + +;;; Code: +(require 'ob) + +(defvar org-babel-default-header-args:dot + '((:results . "file") (:exports . "results")) + "Default arguments to use when evaluating a dot source block.") + +(defun org-babel-expand-body:dot (body params) + "Expand BODY according to PARAMS, return the expanded body." + (let ((vars (mapcar #'cdr (org-babel-get-header params :var)))) + (mapc + (lambda (pair) + (let ((name (symbol-name (car pair))) + (value (cdr pair))) + (setq body + (replace-regexp-in-string + (concat "$" (regexp-quote name)) + (if (stringp value) value (format "%S" value)) + body + t + t)))) + vars) + body)) + +(defun org-babel-execute:dot (body params) + "Execute a block of Dot code with org-babel. +This function is called by `org-babel-execute-src-block'." + (let* ((result-params (cdr (assoc :result-params params))) + (out-file (cdr (or (assoc :file params) + (error "You need to specify a :file parameter")))) + (cmdline (or (cdr (assoc :cmdline params)) + (format "-T%s" (file-name-extension out-file)))) + (cmd (or (cdr (assoc :cmd params)) "dot")) + (in-file (org-babel-temp-file "dot-"))) + (with-temp-file in-file + (insert (org-babel-expand-body:dot body params))) + (org-babel-eval + (concat cmd + " " (org-babel-process-file-name in-file) + " " cmdline + " -o " (org-babel-process-file-name out-file)) "") + nil)) ;; signal that output has already been written to file + +(defun org-babel-prep-session:dot (session params) + "Return an error because Dot does not support sessions." + (error "Dot does not support sessions")) + +(provide 'ob-dot) + + + +;;; ob-dot.el ends here