tut03.org 10.8 KB
 Alexandre Duret-Lutz committed Sep 28, 2015 1 2 ``````# -*- coding: utf-8 -*- #+TITLE: Constructing and transforming formulas `````` Alexandre Duret-Lutz committed May 10, 2016 3 ``````#+DESCRIPTION: Code example for constructing and transforming formulas in Spot `````` Alexandre Duret-Lutz committed Sep 28, 2015 4 5 6 ``````#+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html `````` Alexandre Duret-Lutz committed Sep 30, 2015 7 8 ``````This page explains how to build formulas and how to iterate over their syntax trees. `````` Alexandre Duret-Lutz committed Sep 28, 2015 9 `````` `````` Alexandre Duret-Lutz committed Sep 30, 2015 10 11 12 13 14 ``````We'll first describe how to build a formula from scratch, by using the constructor functions associated to each operators, and show that basic accessor methods for formulas. 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). `````` Alexandre Duret-Lutz committed Sep 28, 2015 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 `````` * 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/. `````` Alexandre Duret-Lutz committed Sep 30, 2015 78 ``````In addition, the arguments of commutative operators `````` Alexandre Duret-Lutz committed Sep 28, 2015 79 80 81 82 83 84 85 86 87 88 89 90 91 92 ``````(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 `````` Alexandre Duret-Lutz committed Dec 04, 2015 93 94 `````` #include #include `````` Alexandre Duret-Lutz committed Sep 28, 2015 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 `````` 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, `````` Alexandre Duret-Lutz committed Sep 30, 2015 195 196 197 198 ``````and stop the recursion as soon as we encounter a subformula without sugar (the =is_sugar_free_ltl()= method is a constant-time operation, that tells whether a formulas contains a =F= or =G= operator) to save time time by not exploring further. `````` Alexandre Duret-Lutz committed Sep 28, 2015 199 200 201 202 `````` #+BEGIN_SRC C++ :results verbatim :exports both #include `````` Alexandre Duret-Lutz committed Dec 04, 2015 203 204 205 `````` #include #include #include `````` Alexandre Duret-Lutz committed Sep 28, 2015 206 207 208 209 210 211 212 213 214 215 216 `````` 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; `````` Alexandre Duret-Lutz committed Sep 30, 2015 217 `````` return f.is_sugar_free_ltl(); `````` Alexandre Duret-Lutz committed Sep 28, 2015 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 `````` }); 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 `````` Alexandre Duret-Lutz committed Dec 04, 2015 251 252 253 `````` #include #include #include `````` Alexandre Duret-Lutz committed Sep 28, 2015 254 255 256 257 258 259 260 261 `````` 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 `````` Alexandre Duret-Lutz committed Sep 30, 2015 262 `````` if (in.is_sugar_free_ltl()) `````` Alexandre Duret-Lutz committed Sep 28, 2015 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 `````` 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 `````` Alexandre Duret-Lutz committed Sep 30, 2015 284 285 286 ``````The Python version of the above two examples uses a very similar syntax. Python only supports a very limited form of lambda expressions, so we have to write a standard function instead: `````` Alexandre Duret-Lutz committed Sep 28, 2015 287 288 289 290 291 292 293 294 295 296 `````` #+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 `````` Alexandre Duret-Lutz committed Sep 30, 2015 297 `````` return f.is_sugar_free_ltl() `````` Alexandre Duret-Lutz committed Sep 28, 2015 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 `````` 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 `````` Alexandre Duret-Lutz committed Sep 30, 2015 331 `````` if i.is_sugar_free_ltl(): `````` Alexandre Duret-Lutz committed Sep 28, 2015 332 333 334 335 336 337 338 339 340 341 342 343 `````` 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))``````