From c4f6722b5390bbdbec749b142d45dd282974a066 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Feb 2019 15:35:42 +0100 Subject: [PATCH] org: add explicit Kripke structure example Fixes #376. * doc/org/tut52.org: New file. * doc/org/tut.org, doc/org/tut51.org: Link to it. * doc/Makefile.am: Add it. --- doc/Makefile.am | 3 +- doc/org/tut.org | 1 + doc/org/tut51.org | 19 +-- doc/org/tut52.org | 305 ++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 319 insertions(+), 9 deletions(-) create mode 100644 doc/org/tut52.org diff --git a/doc/Makefile.am b/doc/Makefile.am index c6fbe19bf..de8eac0ab 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2010-2011, 2013-2018 Laboratoire de Recherche et +## Copyright (C) 2010-2011, 2013-2019 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -113,6 +113,7 @@ ORG_FILES = \ org/tut31.org \ org/tut50.org \ org/tut51.org \ + org/tut52.org \ org/upgrade2.org \ org/satmin.org \ org/satmin.tex \ diff --git a/doc/org/tut.org b/doc/org/tut.org index a68751a92..7e812b2f3 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++. - [[file:tut22.org][Creating an automaton by adding states and transitions]] - [[file:tut23.org][Creating an alternating automaton by adding states and transitions]] - [[file:tut24.org][Iterating over alternating automata]] +- [[file:tut52.org][Creating an explicit Kripke structure]] * Examples in C++ only diff --git a/doc/org/tut51.org b/doc/org/tut51.org index 884cd3272..3ad26467c 100644 --- a/doc/org/tut51.org +++ b/doc/org/tut51.org @@ -13,11 +13,14 @@ 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: +constructs its state space on the fly. ([[file:tut52.org][Another page]] shows how to +implement this Kripke structure using an explicit graph instead.) + +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 @@ -396,6 +399,9 @@ $txt [[file:kripke-1.svg]] * Checking a property on this state space + :PROPERTIES: + :CUSTOM_ID: prop-check + :END: Let us pretend that we want to verify the following property: if =odd_x= infinitely often holds, then =odd_y= infinitely often holds. @@ -412,7 +418,6 @@ counterexample: #+BEGIN_SRC C++ :exports code :noweb strip-export :results verbatim #include #include -#include #include <> int main() @@ -469,7 +474,6 @@ We also pass option "~A~" to hide the acceptance condition (which is #include #include #include - #include #include <> int main() @@ -521,7 +525,6 @@ figure: #include #include #include - #include #include <> int main() diff --git a/doc/org/tut52.org b/doc/org/tut52.org new file mode 100644 index 000000000..f75865f3f --- /dev/null +++ b/doc/org/tut52.org @@ -0,0 +1,305 @@ +# -*- coding: utf-8 -*- +#+TITLE: Playing with explicit Kripke structures +#+DESCRIPTION: Kripke structures that are fully stored in memory, as explicit graphs. +#+INCLUDE: 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. + +On [[file:tut51.org][another page]] we have described how to implement a Kripke structure +that can be explored on the fly, by implementing a function that take +the current state, and produce its successor states. While +implementing an on-the-fly Kripke structure is good for large example, +it requires some implementation effort we are not always willing to +put for a toy example. + +This document shows how to create a Kripke structure that is stored as +an explicit graph. The class for those is =spot::kripke_graph= and +works in a similar way as the class =spot::twa_graph= used for +automata. The main difference between those two classes is that +Kripke structures labels the states instead of the transitions. Using +=spot::kripke_graph= instead of =spot::twa_graph= saves a bit of +memory. + +Our Kripke structure represent a model whose states consist of pairs +of modulo-3 integers $(x,y)$. 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 has +9 states, that we will store explicitly as a graph. + +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. + + +* C++ implementation +** Building the state space + +Here is how we could create the Kripke structure: + +#+NAME: create-kripke +#+BEGIN_SRC C++ + #include + + spot::kripke_graph_ptr create_kripke(spot::bdd_dict_ptr dict, + bool named_states = false) + { + spot::kripke_graph_ptr k = spot::make_kripke_graph(dict); + + bdd odd_x = bdd_ithvar(k->register_ap("odd_x")); + bdd odd_y = bdd_ithvar(k->register_ap("odd_y")); + + unsigned x0y0 = k->new_state((!odd_x) & !odd_y); + unsigned x0y1 = k->new_state((!odd_x) & odd_y); + unsigned x0y2 = k->new_state((!odd_x) & !odd_y); + unsigned x1y0 = k->new_state(odd_x & !odd_y); + unsigned x1y1 = k->new_state(odd_x & odd_y); + unsigned x1y2 = k->new_state(odd_x & !odd_y); + unsigned x2y0 = k->new_state((!odd_x) & !odd_y); + unsigned x2y1 = k->new_state((!odd_x) & odd_y); + unsigned x2y2 = k->new_state((!odd_x) & !odd_y); + + k->set_init_state(x0y0); + + k->new_edge(x0y0, x0y1); k->new_edge(x0y0, x1y0); + k->new_edge(x0y1, x0y2); k->new_edge(x0y1, x1y1); + k->new_edge(x0y2, x0y0); k->new_edge(x0y2, x1y2); + k->new_edge(x1y0, x1y1); k->new_edge(x1y0, x2y0); + k->new_edge(x1y1, x1y2); k->new_edge(x1y1, x2y1); + k->new_edge(x1y2, x1y0); k->new_edge(x1y2, x2y2); + k->new_edge(x2y0, x2y1); k->new_edge(x2y0, x0y0); + k->new_edge(x2y1, x2y2); k->new_edge(x2y1, x0y1); + k->new_edge(x2y2, x2y0); k->new_edge(x2y2, x0y2); + + if (named_states) + { + auto names = new std::vector + { "x0y0", "x0y1", "x0y2", + "x1y0", "x1y1", "x1y2", + "x2y0", "x2y1", "x2y2" }; + k->set_named_prop("state-names", names); + } + return k; + } +#+END_SRC + +To display this Kripke structure, we can call the =print_dot()= +function: + +#+NAME: print-dot +#+BEGIN_SRC C++ :noweb strip-export :results verbatim :export code + #include + <> + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::print_dot(std::cout, create_kripke(dict)); + } +#+END_SRC + +=print_dot()= will output the graph in [[https://graphviz.gitlab.io/][GraphViz's syntax]], and you just +have to pass it to GraphViz's =dot= command to render it: + +#+BEGIN_SRC dot :file kripke-52.svg :cmd circo :var txt=print-dot :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52.svg]] + +By default, states are just numbered. If you want to name them, for +instance for debugging, you should define the ="state-names"= +properties to a vector of names. Our =create_kripke()= function does +that when passed a true argument. + +#+NAME: print-dot-2 +#+BEGIN_SRC C++ :noweb strip-export :results verbatim :export code + #include + <> + int main() + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::print_dot(std::cout, create_kripke(dict, true)); + } +#+END_SRC + +#+BEGIN_SRC dot :file kripke-52b.svg :cmd circo :var txt=print-dot-2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52b.svg]] + +** 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 +#+BEGIN_SRC C++ -r :exports code :noweb strip-export :results verbatim +#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); + + // Find a run of our Kripke structure that intersects af. + auto k = create_kripke(d, true); (ref:ck) + if (auto run = k->intersecting_run(af)) + std::cout << "formula is violated by the following run:\n" << *run; + else + std::cout << "formula is verified\n"; +} +#+END_SRC + +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC + +Note that this main function is similar to the main function we used +for [[file:tut51.org::#check-prop][the on-the-fly version]] except for [[(ck)][the line that creates the Kripke +structure]]. You can modify it to display the counterexample in a +similar way. + +* Python implementation +** Building the state space + +#+NAME: create-kripke-py +#+BEGIN_SRC python -r + import spot + from buddy import bdd_ithvar + + def create_kripke(bdddict, name_states=False): + k = spot.make_kripke_graph(bdddict) + odd_x = bdd_ithvar(k.register_ap("odd_x")) + odd_y = bdd_ithvar(k.register_ap("odd_y")) + + x0y0 = k.new_state(-odd_x & -odd_y); + x0y1 = k.new_state(-odd_x & odd_y); + x0y2 = k.new_state(-odd_x & -odd_y); + x1y0 = k.new_state(odd_x & -odd_y); + x1y1 = k.new_state(odd_x & odd_y); + x1y2 = k.new_state(odd_x & -odd_y); + x2y0 = k.new_state(-odd_x & -odd_y); + x2y1 = k.new_state(-odd_x & odd_y); + x2y2 = k.new_state(-odd_x & -odd_y); + + k.set_init_state(x0y0); + + k.new_edge(x0y0, x0y1); k.new_edge(x0y0, x1y0); + k.new_edge(x0y1, x0y2); k.new_edge(x0y1, x1y1); + k.new_edge(x0y2, x0y0); k.new_edge(x0y2, x1y2); + k.new_edge(x1y0, x1y1); k.new_edge(x1y0, x2y0); + k.new_edge(x1y1, x1y2); k.new_edge(x1y1, x2y1); + k.new_edge(x1y2, x1y0); k.new_edge(x1y2, x2y2); + k.new_edge(x2y0, x2y1); k.new_edge(x2y0, x0y0); + k.new_edge(x2y1, x2y2); k.new_edge(x2y1, x0y1); + k.new_edge(x2y2, x2y0); k.new_edge(x2y2, x0y2); + + if name_states: + k.set_state_names(["x0y0", "x0y1", "x0y2", (ref:ns) + "x1y0", "x1y1", "x1y2", + "x2y0", "x2y1", "x2y2"]) + return k; +#+END_SRC + +To display this structure, we would just call =to_str('dot')= (and +convert the resulting textual output into graphical form using the +=dot= command). + +#+NAME: print-dot-py +#+BEGIN_SRC python :noweb strip-export :results output :export code +<> +k = create_kripke(spot.make_bdd_dict()) +print(k.to_str('dot')) +#+END_SRC + +=print_dot()= will output the graph in [[https://graphviz.gitlab.io/][GraphViz's syntax]], and you just +have to pass it to GraphViz's =dot= command to render it: + +#+BEGIN_SRC dot :file kripke-52c.svg :cmd circo :var txt=print-dot-py :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52c.svg]] + +Again, states may be named if that can help. This is done by passing +a vector of names (indexed by state numbers) to the =set_name_states()= method, +[[(ns)][as done conditionally in our =create_kripke()= function]]. + + +#+NAME: print-dot-py-2 +#+BEGIN_SRC python :noweb strip-export :results output :export code +<> +k = create_kripke(spot.make_bdd_dict(), True) +print(k.to_str('dot')) +#+END_SRC + +#+BEGIN_SRC dot :file kripke-52d.svg :cmd circo :var txt=print-dot-py-2 :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:kripke-52d.svg]] + + +** Checking a property on this state space + +Here is the Python code equivalent to our C++ check. Please +read the C++ description for details. + +#+NAME: demo-2py +#+BEGIN_SRC python -r :exports code :noweb strip-export :results output + <> + + d = spot.make_bdd_dict() + + # Translate the negation of the formula + f = spot.formula.Not("GF(odd_x) -> GF(odd_y)") + af = spot.translate(f, dict=d) + + # Find a run of our Kripke structure that intersects af. + k = create_kripke(d, True) + run = k.intersecting_run(af) + if run: + print("formula is violated by the following run:\n", run) + else: + print("formula is verified") +#+END_SRC + +# temporary fix for an issue in Org 9.2, see +# http://lists.gnu.org/archive/html/emacs-orgmode/2019-01/msg00226.html +#+BEGIN_SRC text :noweb yes +<> +#+END_SRC