alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/org/tut51.org: Typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2016-10-12 10:53:03 +02:00
parent 8a8fcf2ac1
commit 062643cc88
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
doc/org/tut51.org
View file

@ -8,20 +8,20 @@
Kripke structures, can be defined as ω-automata in which labels are on Kripke structures, can be defined as ω-automata in which labels are on
states, and where all runs are accepting (i.e., the acceptance states, and where all runs are accepting (i.e., the acceptance
condition is =t=). They are typically used by model checkers to condition is =t=). They are typically used by model checkers to
represent the state-space of the model to verify. represent the state space of the model to verify.
* Implementing a toy Kripke structure * Implementing a toy Kripke structure
In this example, our goal is to implement a Kripke structure that 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 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 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 the possible actions will be to increment any one of the two integer
(nondeterministicaly). That increment is obviously done modulo 3. (nondeterministicaly). That increment is obviously done modulo 3.
For instance state $(1,2)$ has two possible successors: For instance state $(1,2)$ has two possible successors:
- $(2,2)$ if =x= was incremented, or - $(2,2)$ if =x= was incremented, or
- $(1,0)$ if =y= was incremented. - $(1,0)$ if =y= was incremented.
Initially both variables will be 0. The complete state-space is 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 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 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. as needed, using [[file:tut50.org::#on-the-fly-interface][the one-the-fly interface]] previously discussed.
@ -365,9 +365,9 @@ is an implementation that does this.
Note that the =demo_succ_iterator::recycle= method was introduced for Note that the =demo_succ_iterator::recycle= method was introduced for
this reason. this reason.
* Displaying the state-space * Displaying the state space
Here is a short =main= displaying the state-space of our toy Kripke structure. Here is a short =main= displaying the state space of our toy Kripke structure.
#+NAME: demo-1-aux #+NAME: demo-1-aux
#+BEGIN_SRC C++ :exports none :noweb strip-export #+BEGIN_SRC C++ :exports none :noweb strip-export
@ -559,7 +559,7 @@ example of class following this convention is =twa_graph=, were states
returned by the on-the-fly interface are just pointers into the actual returned by the on-the-fly interface are just pointers into the actual
state vector (which is already known). state vector (which is already known).
Even if the state-space is not already known, it is possible to 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*= implement the on-the-fly interface in such a way that all =state*=
pointers returned for a state are unique. This requires a state pointers returned for a state are unique. This requires a state
unicity table into the automaton, and then =state::clone()= and unicity table into the automaton, and then =state::clone()= and