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

* doc/org/tut03.org: Fix typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-09-30 18:50:57 +02:00
parent d183bf2b5c
commit 7c5f345d68
1 changed files with 19 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

37
doc/org/tut03.org
View file

@ -3,14 +3,14 @@
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
This page explains how to build formula and iterate over their tree. This page explains how to build formulas and how to iterate over their
syntax trees.
On this page, we'll first describe how to build a formula from We'll first describe how to build a formula from scratch, by using the
scratch, by using the constructor functions associated to each constructor functions associated to each operators, and show that
operators, and explain how to inspect a formula using some basic basic accessor methods for formulas. We will do that for C++ first,
methods. We will do that for C++ first, and then Python. Once these and then Python. Once these basics are covered, we will show examples
basics are covered, we will show examples for traversing and for traversing and transforming formulas (again in C++ then Python).
transforming formulas (again in C++ then Python).
* Constructing formulas * Constructing formulas
@ -74,7 +74,7 @@ true and false constants, impotence (=F(F(e))=F(e)=), involutions
(=And({And({e1,e2},e3})=And({e1,e2,e3})=). See [[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]] for a list of (=And({And({e1,e2},e3})=And({e1,e2,e3})=). See [[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]] for a list of
these /trivial identities/. these /trivial identities/.
In addition the arguments of commutative operators In addition, the arguments of commutative operators
(e.g. =Xor(e1,e2)=Xor(e2,e1)=) are always reordered. The order used (e.g. =Xor(e1,e2)=Xor(e2,e1)=) are always reordered. The order used
always put the Boolean subformulas before the temporal subformulas, always put the Boolean subformulas before the temporal subformulas,
sorts the atomic propositions in alphabetic order, and otherwise order sorts the atomic propositions in alphabetic order, and otherwise order
@ -192,9 +192,10 @@ children of a formula are explored only if =fun= returns =false=. If
In the following we use a lambda function to count the number of =G= In the following we use a lambda function to count the number of =G=
in the formula. We also print each subformula to show the recursion, in the formula. We also print each subformula to show the recursion,
and stop the recursion as soon as we encounter a Boolean formula (the and stop the recursion as soon as we encounter a subformula without
=is_boolean()= method is a constant-time operation, so we actually sugar (the =is_sugar_free_ltl()= method is a constant-time operation,
save time by not exploring further). that tells whether a formulas contains a =F= or =G= operator) to save
time time by not exploring further.
#+BEGIN_SRC C++ :results verbatim :exports both #+BEGIN_SRC C++ :results verbatim :exports both
@ -213,7 +214,7 @@ save time by not exploring further).
std::cout << f << '\n'; std::cout << f << '\n';
if (f.is(spot::op::G)) if (f.is(spot::op::G))
++gcount; ++gcount;
return f.is_boolean(); return f.is_sugar_free_ltl();
}); });
std::cout << "=== " << gcount << " G seen ===\n"; std::cout << "=== " << gcount << " G seen ===\n";
return 0; return 0;
@ -258,7 +259,7 @@ in a formula:
if (in.is(spot::op::G)) if (in.is(spot::op::G))
return spot::formula::F(xchg_fg(in[0])); return spot::formula::F(xchg_fg(in[0]));
// No need to transform Boolean subformulas // No need to transform Boolean subformulas
if (in.is_boolean()) if (in.is_sugar_free_ltl())
return in; return in;
// Apply xchg_fg recursively on any other operator's children // Apply xchg_fg recursively on any other operator's children
return in.map(xchg_fg); return in.map(xchg_fg);
@ -280,9 +281,9 @@ in a formula:
** Python ** Python
The Python version of the above to example use a very similar syntax. The Python version of the above two examples uses a very similar
Python only supports a very limited form of lambda expressions, so we syntax. Python only supports a very limited form of lambda
declare a complete function instead: expressions, so we have to write a standard function instead:
#+BEGIN_SRC python :results output :exports both #+BEGIN_SRC python :results output :exports both
import spot import spot
@ -293,7 +294,7 @@ declare a complete function instead:
print(f) print(f)
if f._is(spot.op_G): if f._is(spot.op_G):
gcount += 1 gcount += 1
return f.is_boolean() return f.is_sugar_free_ltl()
f = spot.formula("FGa -> (GFb & GF(c & b & d))") f = spot.formula("FGa -> (GFb & GF(c & b & d))")
f.traverse(countg) f.traverse(countg)
@ -327,7 +328,7 @@ Here is the =F= and =G= exchange:
if i._is(spot.op_G): if i._is(spot.op_G):
return spot.formula.F(xchg_fg(i[0])); return spot.formula.F(xchg_fg(i[0]));
# No need to transform Boolean subformulas # No need to transform Boolean subformulas
if i.is_boolean(): if i.is_sugar_free_ltl():
return i; return i;
# Apply xchg_fg recursively on any other operator's children # Apply xchg_fg recursively on any other operator's children
return i.map(xchg_fg); return i.map(xchg_fg);