tut02.org 4.18 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#+TITLE: Relabeling Formulas
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html

The task is to read an LTL formula, relabel all (possibly complex)
atomic propositions, and provide =#define= statements for each of
these renamings, writing everything in Spin's syntax.


* Shell

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -ps --relabel=pnn --define -f '"Proc@Here" U ("var > 10" | "var < 4")'
#+END_SRC

#+RESULTS:
18
19
20
: #define p0 (Proc@Here)
: #define p1 (var < 4)
: #define p2 (var > 10)
21
22
23
: (p0) U ((p1) || (p2))

When is this output interesting, you may ask?  It is useful for
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
24
instance if you want to call =ltl2ba= (or any other LTL-to-Büchi
25
26
27
28
29
30
31
32
33
34
35
36
translator) using a formula with complex atomic propositions it cannot
parse.  Then you can pass the rewritten formula to =ltl2ba=, and
prepend all those =#define= to its output.  For instance:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -ps --relabel=pnn --define=tmp.defs -f '"Proc@Here" U ("var > 10" | "var < 4")' >tmp.ltl
cat tmp.defs; ltl2ba -F tmp.ltl
rm tmp.defs tmp.ltl
#+END_SRC

#+RESULTS:
#+begin_example
37
38
39
#define p0 (Proc@Here)
#define p1 (var < 4)
#define p2 (var > 10)
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
never { /* (p0) U ((p1) || (p2))
 */
T0_init:
	if
	:: (p0) -> goto T0_init
	:: (p1) || (p2) -> goto accept_all
	fi;
accept_all:
	skip
}
#+end_example


* Python

The =spot.relabel= function takes an optional third parameter that
should be a =relabeling_map=.  If supplied, this map is filled with
pairs of atomic propositions of the form (new-name, old-name).

#+BEGIN_SRC python :results output :exports both
import spot
f = spot.formula('"Proc@Here" U ("var > 10" | "var < 4")')
m = spot.relabeling_map()
g = spot.relabel(f, spot.Pnn, m)
for newname, oldname in m.items():
  print("#define {} ({})".format(newname.to_str(), oldname.to_str('spin', True)))
print(g.to_str('spin', True))
#+END_SRC

#+RESULTS:
: #define p0 ((Proc@Here))
: #define p1 ((var < 4))
: #define p2 ((var > 10))
: (p0) U ((p1) || (p2))

* C++

The =spot::ltl::relabeling_map= is just a =std::map= with a custom
destructor.

#+BEGIN_SRC C++ :results verbatim :exports both
  #include <string>
  #include <iostream>
  #include "ltlparse/public.hh"
  #include "ltlvisit/print.hh"
  #include "ltlvisit/relabel.hh"

  int main()
  {
    std::string input = "\"Proc@Here\" U (\"var > 10\" | \"var < 4\")";
    spot::ltl::parse_error_list pel;
91
    spot::ltl::formula f = spot::ltl::parse_infix_psl(input, pel);
92
    if (spot::ltl::format_parse_errors(std::cerr, input, pel))
93
      return 1;
94
    spot::ltl::relabeling_map m;
95
    f = spot::ltl::relabel(f, spot::ltl::Pnn, &m);
96
97
98
99
100
101
    for (auto& i: m)
      {
        std::cout << "#define ";
        print_psl(std::cout, i.first) << " (";
        print_spin_ltl(std::cout, i.second, true) << ")\n";
      }
102
    print_spin_ltl(std::cout, f, true) << '\n';
103
104
105
106
107
    return 0;
  }
#+END_SRC

#+RESULTS:
108
109
110
: #define p0 (Proc@Here)
: #define p1 (var < 4)
: #define p2 (var > 10)
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
: (p0) U ((p1) || (p2))


* Additional comments

** Two ways to name atomic propositions

   Instead of =--relabel=pnn= (or =spot.Pnn=, or =spot::ltl::Pnn=), you can
   actually use =--relabel=abc= (or =spot.Abc=, or =spot::ltl::Abc=) to have
   the atomic propositions named =a=, =b=, =c=, etc.

** Relabeling Boolean sub-expressions

   Instead of relabeling each atomic proposition, you could decide to
   relabel each Boolean sub-expression:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -ps --relabel-bool=pnn --define -f '"Proc@Here" U ("var > 10" | "var < 4")'
#+END_SRC

#+RESULTS:
132
: #define p0 (Proc@Here)
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
: #define p1 ((var < 4) || (var > 10))
: (p0) U (p1)

   The relabeling routine is smart enough to not give different names
   to Boolean expressions that have some sub-expression in common.

   For instance =a U (a & b)= will not be relabeled into =(p0) U (p1)=
   because that would hide the fact that both =p0= and =p1= check for
   =a=.  Instead we get this:

#+BEGIN_SRC sh :results verbatim :exports both
ltlfilt -ps --relabel-bool=pnn --define -f 'a U (a & b)'
#+END_SRC

#+RESULTS:
148
149
: #define p0 (a)
: #define p1 (b)
150
151
152
153
154
: (p0) U ((p0) && (p1))

   This "Boolean sub-expression" relabeling is available in Python and
   C++ via the =relabel_bse= function.  The interface is identical to
   =relabel=.