tut10.org 4.72 KB
 Alexandre Duret-Lutz committed Jun 07, 2015 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 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 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 ``````#+TITLE: Translating an LTL formula into a never claim #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html Here is how to translate an LTL (or PSL) formula into a never claim. * Shell #+BEGIN_SRC sh :results verbatim :exports both ltl2tgba --spin 'GFa -> GFb' #+END_SRC #+RESULTS: #+begin_example never { /* F(GFb | G!a) */ T0_init: if :: ((!(a))) -> goto accept_S0 :: ((true)) -> goto T0_init :: ((b)) -> goto accept_S2 fi; accept_S0: if :: ((!(a))) -> goto accept_S0 fi; accept_S2: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; T0_S3: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; } #+end_example * Python The =formula= function returns a formula object (or raises a parse-error exception). Formula objects have a =translate()= method that returns an automaton, and the automata objects have a =to_str= method that can output in one of the supported syntaxes. So the translation is actually a one-liner in Python: #+BEGIN_SRC python :results output :exports both import spot print(spot.formula('GFa -> GFb').translate('BA').to_str('spin')) #+END_SRC #+RESULTS: #+begin_example never { T0_init: if :: ((!(a))) -> goto accept_S0 :: ((true)) -> goto T0_init :: ((b)) -> goto accept_S2 fi; accept_S0: if :: ((!(a))) -> goto accept_S0 fi; accept_S2: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; T0_S3: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; } #+end_example The above line can actually be made a bit shorter, because =translate()= can also be used as a function (as opposed to a method) that take a formula (possibly as a string) as first argument: #+BEGIN_SRC python :results output :exports both import spot print(spot.translate('GFa -> GFb', 'BA').to_str('spin')) #+END_SRC #+RESULTS: #+begin_example never { T0_init: if :: ((!(a))) -> goto accept_S0 :: ((true)) -> goto T0_init :: ((b)) -> goto accept_S2 fi; accept_S0: if :: ((!(a))) -> goto accept_S0 fi; accept_S2: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; T0_S3: if :: ((b)) -> goto accept_S2 :: ((!(b))) -> goto T0_S3 fi; } #+end_example * C++ All the translation pipeline (this include simplifying the formula, translating the simplified formula into an automaton, and simplifying the resulting automaton) is handled by the =spot::translator= object. This object can configured by calling =set_type()= to chose the type of automaton to output, =set_level()= to set the level of optimization (it's high by default), and =set_pref()= to set various preferences (like small or deterministic) or characteristic (complete, unambiguous) for the resulting automaton. Finally, the output as a never claim is done via the =print_never_claim= function. #+BEGIN_SRC C++ :results verbatim :exports both #include #include #include "ltlparse/public.hh" #include "ltlvisit/print.hh" #include "twaalgos/translate.hh" #include "twaalgos/neverclaim.hh" int main() { std::string input = "[]<>p0 || <>[]p1"; spot::ltl::parse_error_list pel; const spot::ltl::formula* f = spot::ltl::parse_infix_psl(input, pel); if (spot::ltl::format_parse_errors(std::cerr, input, pel)) { if (f) f->destroy(); return 1; } spot::translator trans; trans.set_type(spot::postprocessor::BA); spot::twa_graph_ptr aut = trans.run(f); print_never_claim(std::cout, aut) << '\n'; f->destroy(); return 0; } #+END_SRC #+RESULTS: #+begin_example never { T0_init: if :: ((p1)) -> goto accept_S0 :: ((true)) -> goto T0_init :: ((p0)) -> goto accept_S2 fi; accept_S0: if :: ((p1)) -> goto accept_S0 fi; accept_S2: if :: ((p0)) -> goto accept_S2 :: ((!(p0))) -> goto T0_S3 fi; T0_S3: if :: ((p0)) -> goto accept_S2 :: ((!(p0))) -> goto T0_S3 fi; } #+end_example * Additional comments The Python version of =translate()= is documented as follows: #+BEGIN_SRC python :results output :exports both import spot help(spot.translate) #+END_SRC #+RESULTS: #+begin_example Help on function translate in module spot: translate(formula, *args) Translate a formula into an automaton. Keep in mind that pref expresses just a preference that may not be satisfied. The optional arguments should be strings among the following: - at most one in 'TGBA', 'BA', or 'Monitor' (type of automaton to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' (optimization level) - any combination of 'Complete', 'Unambiguous', and 'StateBasedAcceptance' (or 'SBAcc' for short) The default correspond to 'tgba', 'small' and 'high'. #+end_example``````