ltlfilt.org 7.99 KB
Newer Older
 Alexandre Duret-Lutz committed Apr 09, 2013 1 2 3 4 5 6 7 8 9 10 11 12 13 14 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 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 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 ``````#+TITLE: =ltlfilt= #+EMAIL spot@lrde.epita.fr #+OPTIONS: H:2 num:nil toc:t #+LINK_UP: file:tools.html This tool is a filter for LTL formulas. (It will also work with PSL formulas.) It can be used to perform a number of tasks. Essentially: - converting formulas from one syntax to another, - transforming formulas, - selecting formulas matching some criterion. * Changing syntaxes Because it read and write formulas, =ltlfilt= accepts all the [[file:ioltl.org][common input and output options]]. Additionally, if no =-f= or =-F= option is specified, =ltlfilt= will read formulas from the standard input. For instance the following will convert two LTL formulas expressed using infix notation (with different names supported for the same operators) and convert it into LBT's syntax. #+BEGIN_SRC sh :results verbatim :exports results ltlfilt -l -f 'p1 U (p2 & GFp3)' -f 'X<>[]p4' #+END_SRC #+RESULTS: : U p1 & p2 G F p3 : X F G p4 Conversely, here is how to rewrite formulas expressed using the LBT's Polish notation. Let's take the following four formulas taken from examples distributed with =scheck=: #+BEGIN_SRC sh :results verbatim :exports both cat >scheck.ltl<= INT --equivalent-to=FORMULA match formulas equivalent to FORMULA --eventual match pure eventualities --guarantee match guarantee formulas (even pathological) --implied-by=FORMULA match formulas implied by FORMULA --imply=FORMULA match formulas implying FORMULA --ltl match only LTL formulas (no PSL operator) --nox match X-free formulas --obligation match obligation formulas (even pathological) --safety match safety formulas (even pathological) --size-max=INT match formulas with size <= INT --size-min=INT match formulas with size >= INT `````` Alexandre Duret-Lutz committed Apr 11, 2013 130 131 `````` --stutter-insensitive, --stutter-invariant match stutter-insensitive LTL formulas `````` Alexandre Duret-Lutz committed Apr 09, 2013 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 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 `````` --syntactic-guarantee match syntactic-guarantee formulas --syntactic-obligation match syntactic-obligation formulas --syntactic-persistence match syntactic-persistence formulas --syntactic-recurrence match syntactic-recurrence formulas --syntactic-safety match syntactic-safety formulas --universal match purely universal formulas -u, --unique drop formulas that have already been output (not affected by -v) -v, --invert-match select non-matching formulas #+end_example Most of the above options should be self-explanatory. For instance the following command will extract all formulas from =scheck.ltl= which do not represent guarantee properties. #+BEGIN_SRC sh :results verbatim :exports both ltlfilt --lbt-input -F scheck.ltl -v --guarantee #+END_SRC #+RESULTS: : !(Gp0 | (Gp1 & Fp3)) Combining =ltlfilt= with [[file:randltl.org][=randltl=]] makes it easier to generate random formulas that respect certain constraints. For instance let us generate 10 formulas that are equivalent to =a U b=: #+BEGIN_SRC sh :results verbatim :exports both randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' | head -n 10 #+END_SRC #+RESULTS: #+begin_example !(!a R !b) (!Gb -> a) U b a U b Fb & (a W b) ((a <-> !(a | b)) W a) U ((!b M b) U b) (b <-> (Xb M a)) -> b (a | b) U b ((!b U b) -> (a W b)) U b (a xor b) U b b R (Fb & (a U (a W b))) #+end_example The =-n -1= option to =randltl= will cause it to output an infinite stream of random formulas. =ltlfilt=, which reads its standard input by default, will select only those equivalent to =a U b=. The output of =ltlfilt= would still be an infinite stream of random formulas, so we display only the first 10 using the standard =head= utility. Less trivial formulas could be obtained by adding the =-r= option to =randltl= (or equivalently adding the =-r= and =-u= option to =ltlfilt=). Another similar example, that requires two calls to =ltlfilt=, is the generation of random pathological safety formulas. Pathological safety formulas are safety formulas that do not /look/ so syntactically. We can generate some starting again with =randltl=, then ignoring all syntactic safety formulas, and keeping only the safety formulas in the remaining list. #+BEGIN_SRC sh :results verbatim :exports both randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety | head -n 10 #+END_SRC #+RESULTS: #+begin_example (!a & Fa) R Xa !a | (a & b) | (((!a & b) | (a & !b)) M (!a M X!a)) G(!a M Xa) G((G!b & !a) | (a & Fb)) R a G!a M !a G(!a M ((!b & XGb) | (b & XF!b))) F(b | G!b) F(Xa | G!a) G(XXa | (b & F!a)) G((!a & (!a M !b)) | (a & (a W b))) #+end_example =ltlfilt='s filtering ability can also be used to answer questions about a single formula. For instance is =a U (b U a)= equivalent to =b U a=? #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a' #+END_SRC #+RESULTS: : a U (b U a) The commands prints the formula and returns an exit status of 0 if the two formulas are equivalent. It would print nothing and set the exit status to 1, were the two formulas not equivalent. # LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck # LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc # LocalWords: pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb # LocalWords: XF XXa``````