From c67540db1487a0dfefd20adb4b6c97da99ca4f49 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Sep 2015 23:17:04 +0200 Subject: [PATCH] doc: more examples of the formula interface * src/tl/formula.hh, src/tl/formula.cc: Add an operator<< to print formulas. * doc/org/tut01.org, doc/org/tut02.org: Adjust. * doc/org/tut03.org: New file. * doc/org/tut.org, doc/Makefile.am: Add it. --- doc/Makefile.am | 1 + doc/org/tut.org | 4 + doc/org/tut01.org | 41 +++--- doc/org/tut02.org | 3 +- doc/org/tut03.org | 342 ++++++++++++++++++++++++++++++++++++++++++++++ src/tl/formula.cc | 6 + src/tl/formula.hh | 15 +- 7 files changed, 387 insertions(+), 25 deletions(-) create mode 100644 doc/org/tut03.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 01152e924..992870a9f 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -86,6 +86,7 @@ ORG_FILES = \ org/tut.org \ org/tut01.org \ org/tut02.org \ + org/tut03.org \ org/tut10.org \ org/tut20.org \ org/tut21.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index 7251fb43a..7fb7f123d 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -18,6 +18,10 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut20.org][Converting a never claim into HOA]] +* Examples in Python and C++ + +- [[file:tut03.org][Constructing and transforming formulas]] + * Examples in C++ only The following examples are too low-level to be implemented in shell or diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 6fb23f2c9..91c3f849f 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -15,14 +15,16 @@ using different options such as (=--spin=, =--lbt=, =--latex=, etc.). Full parentheses can also be requested using =-p=. #+BEGIN_SRC sh :results verbatim :exports both -ltlfilt -f '[]<>p0 || <>[]p1' --latex +ltlfilt -f '[]<>p0 || <>[]p1' formula='& & G p0 p1 p2' +ltlfilt --lbt-input -f "$formula" --latex ltlfilt --lbt-input -f "$formula" --lbt ltlfilt --lbt-input -f "$formula" --spin -p #+END_SRC #+RESULTS: -: \G \F p_{0} \lor \F \G p_{1} +: GFp0 | FGp1 +: p_{1} \land p_{2} \land \G p_{0} : & & p1 p2 G p0 : (p1) && (p2) && ([](p0)) @@ -37,15 +39,16 @@ Here are the same operation in Python #+BEGIN_SRC python :results output :exports both import spot -f = spot.formula('[]<>p0 || <>[]p1') -print(f.to_str('latex')) +print(spot.formula('[]<>p0 || <>[]p1')) f = spot.formula('& & G p0 p1 p2') +print(f.to_str('latex')) print(f.to_str('lbt')) print(f.to_str('spin', parenth=True)) #+END_SRC #+RESULTS: -: \G \F p_{0} \lor \F \G p_{1} +: GFp0 | FGp1 +: p_{1} \land p_{2} \land \G p_{0} : & & p1 p2 G p0 : (p1) && (p2) && ([](p0)) @@ -71,8 +74,9 @@ exceptions. int main() { - print_latex_psl(std::cout, spot::parse_formula("[]<>p0 || <>[]p1")) << '\n'; + std::cout << spot::parse_formula("[]<>p0 || <>[]p1") << '\n'; spot::formula f = spot::parse_formula("& & G p0 p1 p2"); + print_latex_psl(std::cout, f) << '\n'; print_lbt_ltl(std::cout, f) << '\n'; print_spin_ltl(std::cout, f, true) << '\n'; return 0; @@ -80,16 +84,18 @@ exceptions. #+END_SRC #+RESULTS: -: \G \F p_{0} \lor \F \G p_{1} +: GFp0 | FGp1 +: p_{1} \land p_{2} \land \G p_{0} : & & p1 p2 G p0 : (p1) && (p2) && ([](p0)) -Notice that the different output routines specify in their name the -syntax the output, and the type of formula they can output. Here we -are only using LTL formulas for demonstration, so those three -functions are OK with that. +Notice that, except for the =<<= operator, the different output +routines specify in their name the syntax the output, and the type of +formula they can output. Here we are only using LTL formulas for +demonstration, so those three functions are OK with that. The +routine used by =<<= is =print_psl()=. -We do not recommend using this =parse_formula()= interface because of +We do not recommend using the =parse_formula()= interface because of the potential formulas (like =f= or =t=) that have different meanings in the two parsers that are tried. @@ -99,7 +105,7 @@ parser. Additionally, this give you control over how to print errors. ** Calling the infix parser explicitly -Here is how to call the infix parser explicitly,: +Here is how to call the infix parser explicitly: #+BEGIN_SRC C++ :results verbatim :exports both #include @@ -114,13 +120,13 @@ Here is how to call the infix parser explicitly,: spot::formula f = spot::parse_infix_psl(input, pel); if (spot::format_parse_errors(std::cerr, input, pel)) return 1; - print_latex_psl(std::cout, f) << '\n'; + std::cout << f << '\n'; return 0; } #+END_SRC #+RESULTS: -: \G \F p_{0} \lor \F \G p_{1} +: GFp0 | FGp1 So =parse_infix_psl()= processes =input=, and stores any diagnostic in =pel=, which is a list of pairs associating each error to a location. @@ -159,8 +165,7 @@ with the "fixed" formula if you wish. Here is an example: (void) spot::format_parse_errors(std::cout, input, pel); if (f == nullptr) return 1; - std::cout << "Parsed formula: "; - print_psl(std::cout, f) << '\n'; + std::cout << "Parsed formula: " << f << '\n'; return 0; } #+END_SRC @@ -198,6 +203,7 @@ of =parse_infix_psl()=. spot::formula f = spot::parse_prefix_ltl(input, pel); if (spot::format_parse_errors(std::cerr, input, pel)) return 1; + print_latex_psl(std::cout, f) << '\n'; print_lbt_ltl(std::cout, f) << '\n'; print_spin_ltl(std::cout, f, true) << '\n'; return 0; @@ -205,6 +211,7 @@ of =parse_infix_psl()=. #+END_SRC #+RESULTS: +: p_{1} \land p_{2} \land \G p_{0} : & & p1 p2 G p0 : (p1) && (p2) && ([](p0)) diff --git a/doc/org/tut02.org b/doc/org/tut02.org index 79b894bf3..e87e72c4f 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -95,8 +95,7 @@ destructor. f = spot::relabel(f, spot::Pnn, &m); for (auto& i: m) { - std::cout << "#define "; - print_psl(std::cout, i.first) << " ("; + std::cout << "#define " << i.first << " ("; print_spin_ltl(std::cout, i.second, true) << ")\n"; } print_spin_ltl(std::cout, f, true) << '\n'; diff --git a/doc/org/tut03.org b/doc/org/tut03.org new file mode 100644 index 000000000..f5a385be9 --- /dev/null +++ b/doc/org/tut03.org @@ -0,0 +1,342 @@ +# -*- coding: utf-8 -*- +#+TITLE: Constructing and transforming formulas +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +This page explains how to build formula and iterate over their tree. + +On this page, we'll first describe how to build a formula from +scratch, by using the constructor functions associated to each +operators, and explain how to inspect a formula using some basic +methods. We will do that for C++ first, and then Python. Once these +basics are covered, we will show examples for traversing and +transforming formulas (again in C++ then Python). + +* Constructing formulas + +** C++ + +The =spot::formula= class contains static methods that act as +constructors for each supported operator. + +The Boolean constants true and false are returned by =formula::tt()= +and =formula:ff()=. Atomic propositions can be built with +=formula::ap("name")=. Unary and binary operators use a +straighforward syntax like =formula::F(arg)= or =formula::U(first, +second)=, while n-ary operators take an initializer list as argument +as in =formula::And({arg1, arg2, arg3})=. + +Here is the list of supported operators: + +#+BEGIN_SRC C++ + // atomic proposition + formula::ap(string) + // constants + formula::ff(); + formula::tt(); + formula::eword(); // empty word (for regular expressions) + // unary operators + formula::Not(arg); + formula::X(arg); + formula::F(arg); + formula::G(arg); + formula::Closure(arg); + formula::NegClosure(arg); + // binary operators + formula::Xor(left, right); + formula::Implies(left, right); + formula::Equiv(left, right); + formula::U(left, right); // (strong) until + formula::R(left, right); // (weak) release + formula::W(left, right); // weak until + formula::M(left, right); // strong release + formula::EConcat(left, right); // Seq + formula::UConcat(left, right); // Triggers + // n-ary operators + formula::Or({args,...}); // omega-rational Or + formula::OrRat({args,...}); // rational Or (for regular expressions) + formula::And({args,...}); // omega-rational And + formula::AndRat({args,...}); // rational And (for regular expressions) + formula::AndNLM({args,...}); // non-length-matching rational And (for r.e.) + formula::Concat({args,...}); // concatenation (for regular expressions) + formula::Fusion({args,...}); // concatenation (for regular expressions) + // star-like operators + formula::Star(arg, min, max); // Star (for a Kleene star, set min=0 and omit max) + formula::FStar(arg, min, max); // Fusion Star +#+END_SRC + +These functions implement some very limited type of automatic +simplifications called /trivial identities/. For instance +=formula::F(formula::X(formula::tt()))= will return the same formula +as =formula::tt()=. These simplifications are those that involve the +true and false constants, impotence (=F(F(e))=F(e)=), involutions +(=Not(Not(e)=e=), associativity +(=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/. + +In addition the arguments of commutative operators +(e.g. =Xor(e1,e2)=Xor(e2,e1)=) are always reordered. The order used +always put the Boolean subformulas before the temporal subformulas, +sorts the atomic propositions in alphabetic order, and otherwise order +subformulas by their unique identifier (a constant incremented each +time a new subformula is created). This reordering is useful to favor +sharing of subformulas, but also helps algorithms that perform +memoization. + +Building a formula using these operators is quite straightforward. +The second part of the following example shows how to print some +detail of the top-level oeprator in the formula. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include "tl/formula.hh" + #include "tl/print.hh" + + int main() + { + // Build FGa -> (GFb & GFc) + spot::formula fga = spot::formula::F(spot::formula::G(spot::formula::ap("a"))); + spot::formula gfb = spot::formula::G(spot::formula::F(spot::formula::ap("b"))); + spot::formula gfc = spot::formula::G(spot::formula::F(spot::formula::ap("c"))); + spot::formula f = spot::formula::Implies(fga, spot::formula::And({gfb, gfc})); + + std::cout << f << '\n'; + + // kindstar() prints the name of the operator + // size() return the number of operands of the operators + std::cout << f.kindstr() << ", " << f.size() << " children\n"; + // operator[] accesses each operand + std::cout << "left: " << f[0] << ", right: " << f[1] << '\n'; + // you can also iterate over all operands using a for loop + for (auto child: f) + std::cout << " * " << child << '\n'; + // the type of the operator can be accessed with kind(), which + // return an element of the spot::op enum. + std::cout << f[1][0] + << (f[1][0].kind() == spot::op::F ? " is F\n" : " is not F\n"); + // however because writing f.kind() == spot::op::XXX is quite common, there + // is also a is() shortcut: + std::cout << f[1][1] + << (f[1][1].is(spot::op::G) ? " is G\n" : " is not G\n"); + return 0; + } +#+END_SRC + +#+RESULTS: +: FGa -> (GFb & GFc) +: Implies, 2 children +: left: FGa, right: GFb & GFc +: * FGa +: * GFb & GFc +: GFb is not F +: GFc is G + +** Python + +The Python equivalent is similar: + +#+BEGIN_SRC python :results output :exports both + import spot + + # Build FGa -> (GFb & GFc) + fga = spot.formula.F(spot.formula.G(spot.formula.ap("a"))) + gfb = spot.formula.G(spot.formula.F(spot.formula.ap("b"))); + gfc = spot.formula.G(spot.formula.F(spot.formula.ap("c"))); + f = spot.formula.Implies(fga, spot.formula.And([gfb, gfc])); + + print(f) + + # kindstar() prints the name of the operator + # size() return the number of operands of the operators + print("{}, {} children".format(f.kindstr(), f.size())) + # [] accesses each operand + print("left: {f[0]}, right: {f[1]}".format(f=f)) + # you can also iterate over all operands using a for loop + for child in f: + print(" *", child) + # the type of the operator can be accessed with kind(), which returns + # an op_XXX constant (corresponding the the spot::op enum of C++) + print(f[1][0], "is F" if f[1][0].kind() == spot.op_F else "is not F") + # "is" is keyword in Python, the so shortcut is called _is: + print(f[1][1], "is G" if f[1][1]._is(spot.op_G) else "is not G") +#+END_SRC + +#+RESULTS: +: FGa -> (GFb & GFc) +: Implies, 2 children +: left: FGa, right: GFb & GFc +: * FGa +: * GFb & GFc +: GFb is not F +: GFc is G + + +* Transforming formulas + +** C++ + +In Spot, Formula objects are immutable: this allows identical subtrees +to be shared among multiple formulas. Algorithm that "transform" +formulas (for instance the [[file:tut02.org][relabeling function]]) actually recursively +traverses the input formula to construct the output formula. + +Using the operators described in the previous section is enough to +write algorithms on formulas. However there are two special methods +that makes it a lot easier: =traverse= and =map=. + +=traverse= takes a function =fun=, and applies it to a subformulas of +a formula, including the formula itself. The formula is explored in a +DFS fashion (without skipping subformula that appear twice). The +children of a formula are explored only if =fun= returns =false=. If +=fun= returns =true=, that indicates to stop the recursion. + +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, +and stop the recursion as soon as we encounter a Boolean formula (the +=is_boolean()= method is a constant-time operation, so we actually +save time by not exploring further). + + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include "tl/formula.hh" + #include "tl/print.hh" + #include "ltlparse/public.hh" + + int main() + { + spot::formula f = spot::parse_formula("FGa -> (GFb & GF(c & b & d))"); + + int gcount = 0; + f.traverse([&gcount](spot::formula f) + { + std::cout << f << '\n'; + if (f.is(spot::op::G)) + ++gcount; + return f.is_boolean(); + }); + std::cout << "=== " << gcount << " G seen ===\n"; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +FGa -> (GFb & GF(b & c & d)) +FGa +Ga +a +GFb & GF(b & c & d) +GFb +Fb +b +GF(b & c & d) +F(b & c & d) +b & c & d +=== 3 G seen === +#+end_example + + +The other useful operation is =map=. This also takes a functional +argument, but that function should input a formula and output a +replacement formula. =f.map(fun)= applies =fun= to all children of +=f=, and rebuild a same formula as =f=. + +Here is a demonstration of how to exchange all =F= and =G= operators +in a formula: + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include "tl/formula.hh" + #include "tl/print.hh" + #include "ltlparse/public.hh" + + spot::formula xchg_fg(spot::formula in) + { + if (in.is(spot::op::F)) + return spot::formula::G(xchg_fg(in[0])); + if (in.is(spot::op::G)) + return spot::formula::F(xchg_fg(in[0])); + // No need to transform Boolean subformulas + if (in.is_boolean()) + return in; + // Apply xchg_fg recursively on any other operator's children + return in.map(xchg_fg); + } + + int main() + { + spot::formula f = spot::parse_formula("FGa -> (GFb & GF(c & b & d))"); + std::cout << "before: " << f << '\n'; + std::cout << "after: " << xchg_fg(f) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +: before: FGa -> (GFb & GF(b & c & d)) +: after: GFa -> (FGb & FG(b & c & d)) + + +** Python + +The Python version of the above to example use a very similar syntax. +Python only supports a very limited form of lambda expressions, so we +declare a complete function instead: + +#+BEGIN_SRC python :results output :exports both + import spot + + gcount = 0 + def countg(f): + global gcount + print(f) + if f._is(spot.op_G): + gcount += 1 + return f.is_boolean() + + f = spot.formula("FGa -> (GFb & GF(c & b & d))") + f.traverse(countg) + print("===", gcount, "G seen ===") +#+END_SRC + +#+RESULTS: +#+begin_example +FGa -> (GFb & GF(b & c & d)) +FGa +Ga +a +GFb & GF(b & c & d) +GFb +Fb +b +GF(b & c & d) +F(b & c & d) +b & c & d +=== 3 G seen === +#+end_example + +Here is the =F= and =G= exchange: + +#+BEGIN_SRC python :results output :exports both + import spot + + def xchg_fg(i): + if i._is(spot.op_F): + return spot.formula.G(xchg_fg(i[0])); + if i._is(spot.op_G): + return spot.formula.F(xchg_fg(i[0])); + # No need to transform Boolean subformulas + if i.is_boolean(): + return i; + # Apply xchg_fg recursively on any other operator's children + return i.map(xchg_fg); + + f = spot.formula("FGa -> (GFb & GF(c & b & d))") + print("before:", f) + print("after: ", xchg_fg(f)) +#+END_SRC + +#+RESULTS: +: before: FGa -> (GFb & GF(b & c & d)) +: after: GFa -> (FGb & FG(b & c & d)) diff --git a/src/tl/formula.cc b/src/tl/formula.cc index 4a5145134..c7b10a218 100644 --- a/src/tl/formula.cc +++ b/src/tl/formula.cc @@ -27,6 +27,7 @@ #include #include #include "misc/bareword.hh" +#include "print.hh" #ifndef HAVE_STRVERSCMP // If the libc does not have this, a version is compiled in lib/. @@ -1743,4 +1744,9 @@ namespace spot return out; } + + std::ostream& operator<<(std::ostream& os, const formula& f) + { + return print_psl(os, f); + } } diff --git a/src/tl/formula.hh b/src/tl/formula.hh index f50b8c019..6e85a54cf 100644 --- a/src/tl/formula.hh +++ b/src/tl/formula.hh @@ -164,19 +164,19 @@ namespace spot return c; } - uint8_t min() const + unsigned min() const { assert(op_ == op::FStar || op_ == op::Star); return min_; } - uint8_t max() const + unsigned max() const { assert(op_ == op::FStar || op_ == op::Star); return max_; } - uint8_t size() const + unsigned size() const { return size_; } @@ -1001,17 +1001,17 @@ namespace spot } #endif - uint8_t min() const + unsigned min() const { return ptr_->min(); } - uint8_t max() const + unsigned max() const { return ptr_->max(); } - uint8_t size() const + unsigned size() const { return ptr_->size(); } @@ -1258,6 +1258,9 @@ namespace spot /// List the properties of formula \a f. SPOT_API std::list list_formula_props(const formula& f); + + SPOT_API + std::ostream& operator<<(std::ostream& os, const formula& f); } #ifndef SWIG