threshold_l2_c1.pp 18.9 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
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
214
215
216
217
218
219
220
221
222
223
224
population protocol "Threshold Protocol with l = 2 and c = 1" {
    states {
        _l_true__m2 _l_true__m1 _l_true___0 _l_true__p1 _l_true__p2
        _l_false_m2 _l_false_m1 _l_false__0 _l_false_p1 _l_false_p2
        _n_true__m2 _n_true__m1 _n_true___0 _n_true__p1 _n_true__p2
        _n_false_m2 _n_false_m1 _n_false__0 _n_false_p1 _n_false_p2
    }
    transitions {
        x_l_true__m2_l_true__m2 x_l_true__m2_l_true__m1 x_l_true__m2_l_true___0 x_l_true__m2_l_true__p1 x_l_true__m2_l_true__p2
                                x_l_true__m1_l_true__m1 x_l_true__m1_l_true___0 x_l_true__m1_l_true__p1 x_l_true__m1_l_true__p2
                                                        x_l_true___0_l_true___0 x_l_true___0_l_true__p1 x_l_true___0_l_true__p2
                                                                                x_l_true__p1_l_true__p1 x_l_true__p1_l_true__p2
                                                                                                        x_l_true__p2_l_true__p2

        x_l_false_m2_l_true__m2 x_l_false_m2_l_true__m1 x_l_false_m2_l_true___0 x_l_false_m2_l_true__p1 x_l_false_m2_l_true__p2
        x_l_false_m2_l_false_m2 x_l_false_m2_l_false_m1 x_l_false_m2_l_false__0 x_l_false_m2_l_false_p1 x_l_false_m2_l_false_p2

        x_l_false_m1_l_true__m2 x_l_false_m1_l_true__m1 x_l_false_m1_l_true___0 x_l_false_m1_l_true__p1 x_l_false_m1_l_true__p2
                                x_l_false_m1_l_false_m1 x_l_false_m1_l_false__0 x_l_false_m1_l_false_p1 x_l_false_m1_l_false_p2

        x_l_false__0_l_true__m2 x_l_false__0_l_true__m1 x_l_false__0_l_true___0 x_l_false__0_l_true__p1 x_l_false__0_l_true__p2
                                                        x_l_false__0_l_false__0 x_l_false__0_l_false_p1 x_l_false__0_l_false_p2

        x_l_false_p1_l_true__m2 x_l_false_p1_l_true__m1 x_l_false_p1_l_true___0 x_l_false_p1_l_true__p1 x_l_false_p1_l_true__p2
                                                                                x_l_false_p1_l_false_p1 x_l_false_p1_l_false_p2

        x_l_false_p2_l_true__m2 x_l_false_p2_l_true__m1 x_l_false_p2_l_true___0 x_l_false_p2_l_true__p1 x_l_false_p2_l_true__p2
                                                                                                        x_l_false_p2_l_false_p2

                                x_n_true__m2_l_true__m1 x_n_true__m2_l_true___0 x_n_true__m2_l_true__p1 x_n_true__m2_l_true__p2
        x_n_true__m2_l_false_m2 x_n_true__m2_l_false_m1 x_n_true__m2_l_false__0 x_n_true__m2_l_false_p1 x_n_true__m2_l_false_p2

                                x_n_true__m1_l_true__m1 x_n_true__m1_l_true___0 x_n_true__m1_l_true__p1 x_n_true__m1_l_true__p2
        x_n_true__m1_l_false_m2 x_n_true__m1_l_false_m1 x_n_true__m1_l_false__0 x_n_true__m1_l_false_p1 x_n_true__m1_l_false_p2

                                                                                x_n_true___0_l_true__p1 x_n_true___0_l_true__p2
        x_n_true___0_l_false_m2 x_n_true___0_l_false_m1 x_n_true___0_l_false__0 x_n_true___0_l_false_p1 x_n_true___0_l_false_p2

        x_n_true__p1_l_true__m2 x_n_true__p1_l_true__m1 x_n_true__p1_l_true___0 x_n_true__p1_l_true__p1 x_n_true__p1_l_true__p2
        x_n_true__p1_l_false_m2 x_n_true__p1_l_false_m1 x_n_true__p1_l_false__0 x_n_true__p1_l_false_p1 x_n_true__p1_l_false_p2

        x_n_true__p2_l_true__m2 x_n_true__p2_l_true__m1 x_n_true__p2_l_true___0 x_n_true__p2_l_true__p1 x_n_true__p2_l_true__p2
        x_n_true__p2_l_false_m2 x_n_true__p2_l_false_m1 x_n_true__p2_l_false__0 x_n_true__p2_l_false_p1 x_n_true__p2_l_false_p2

        x_n_false_m2_l_true__m2 x_n_false_m2_l_true__m1 x_n_false_m2_l_true___0 x_n_false_m2_l_true__p1 x_n_false_m2_l_true__p2
        x_n_false_m2_l_false_m2 x_n_false_m2_l_false_m1 x_n_false_m2_l_false__0 x_n_false_m2_l_false_p1 x_n_false_m2_l_false_p2

        x_n_false_m1_l_true__m2 x_n_false_m1_l_true__m1 x_n_false_m1_l_true___0 x_n_false_m1_l_true__p1 x_n_false_m1_l_true__p2
        x_n_false_m1_l_false_m2 x_n_false_m1_l_false_m1 x_n_false_m1_l_false__0 x_n_false_m1_l_false_p1 x_n_false_m1_l_false_p2

        x_n_false__0_l_true__m2 x_n_false__0_l_true__m1 x_n_false__0_l_true___0 x_n_false__0_l_true__p1 x_n_false__0_l_true__p2
        x_n_false__0_l_false_m2 x_n_false__0_l_false_m1 x_n_false__0_l_false__0

        x_n_false_p1_l_true__m2 x_n_false_p1_l_true__m1 x_n_false_p1_l_true___0 x_n_false_p1_l_true__p1 x_n_false_p1_l_true__p2
        x_n_false_p1_l_false_m2 x_n_false_p1_l_false_m1 x_n_false_p1_l_false__0 x_n_false_p1_l_false_p1

        x_n_false_p2_l_true__m2 x_n_false_p2_l_true__m1 x_n_false_p2_l_true___0 x_n_false_p2_l_true__p1 x_n_false_p2_l_true__p2
        x_n_false_p2_l_false_m2 x_n_false_p2_l_false_m1 x_n_false_p2_l_false__0 x_n_false_p2_l_false_p1
    }
    arcs {
       { _l_true__m2, _l_true__m2 } -> x_l_true__m2_l_true__m2 -> { _l_true__m2, _n_true__m2 }
       { _l_true__m2, _l_true__m1 } -> x_l_true__m2_l_true__m1 -> { _l_true__m2, _n_true__m1 }
       { _l_true__m2, _l_true___0 } -> x_l_true__m2_l_true___0 -> { _l_true__m2, _n_true___0 }
       { _l_true__m2, _l_true__p1 } -> x_l_true__m2_l_true__p1 -> { _l_true__m1, _n_true___0 }
       { _l_true__m2, _l_true__p2 } -> x_l_true__m2_l_true__p2 -> { _l_true___0, _n_true___0 }
       { _l_true__m1, _l_true__m1 } -> x_l_true__m1_l_true__m1 -> { _l_true__m2, _n_true___0 }
       { _l_true__m1, _l_true___0 } -> x_l_true__m1_l_true___0 -> { _l_true__m1, _n_true___0 }
       { _l_true__m1, _l_true__p1 } -> x_l_true__m1_l_true__p1 -> { _l_true___0, _n_true___0 }
       { _l_true__m1, _l_true__p2 } -> x_l_true__m1_l_true__p2 -> { _l_false_p1, _n_false__0 }
       { _l_true___0, _l_true___0 } -> x_l_true___0_l_true___0 -> { _l_true___0, _n_true___0 }
       { _l_true___0, _l_true__p1 } -> x_l_true___0_l_true__p1 -> { _l_false_p1, _n_false__0 }
       { _l_true___0, _l_true__p2 } -> x_l_true___0_l_true__p2 -> { _l_false_p2, _n_false__0 }
       { _l_true__p1, _l_true__p1 } -> x_l_true__p1_l_true__p1 -> { _l_false_p2, _n_false__0 }
       { _l_true__p1, _l_true__p2 } -> x_l_true__p1_l_true__p2 -> { _l_false_p2, _n_false_p1 }
       { _l_true__p2, _l_true__p2 } -> x_l_true__p2_l_true__p2 -> { _l_false_p2, _n_false_p2 }
       { _l_false_m2, _l_true__m2 } -> x_l_false_m2_l_true__m2 -> { _l_true__m2, _n_true__m2 }
       { _l_false_m2, _l_true__m1 } -> x_l_false_m2_l_true__m1 -> { _l_true__m2, _n_true__m1 }
       { _l_false_m2, _l_true___0 } -> x_l_false_m2_l_true___0 -> { _l_true__m2, _n_true___0 }
       { _l_false_m2, _l_true__p1 } -> x_l_false_m2_l_true__p1 -> { _l_true__m1, _n_true___0 }
       { _l_false_m2, _l_true__p2 } -> x_l_false_m2_l_true__p2 -> { _l_true___0, _n_true___0 }
       { _l_false_m2, _l_false_m2 } -> x_l_false_m2_l_false_m2 -> { _l_true__m2, _n_true__m2 }
       { _l_false_m2, _l_false_m1 } -> x_l_false_m2_l_false_m1 -> { _l_true__m2, _n_true__m1 }
       { _l_false_m2, _l_false__0 } -> x_l_false_m2_l_false__0 -> { _l_true__m2, _n_true___0 }
       { _l_false_m2, _l_false_p1 } -> x_l_false_m2_l_false_p1 -> { _l_true__m1, _n_true___0 }
       { _l_false_m2, _l_false_p2 } -> x_l_false_m2_l_false_p2 -> { _l_true___0, _n_true___0 }
       { _l_false_m1, _l_true__m2 } -> x_l_false_m1_l_true__m2 -> { _l_true__m2, _n_true__m1 }
       { _l_false_m1, _l_true__m1 } -> x_l_false_m1_l_true__m1 -> { _l_true__m2, _n_true___0 }
       { _l_false_m1, _l_true___0 } -> x_l_false_m1_l_true___0 -> { _l_true__m1, _n_true___0 }
       { _l_false_m1, _l_true__p1 } -> x_l_false_m1_l_true__p1 -> { _l_true___0, _n_true___0 }
       { _l_false_m1, _l_true__p2 } -> x_l_false_m1_l_true__p2 -> { _l_false_p1, _n_false__0 }
       { _l_false_m1, _l_false_m1 } -> x_l_false_m1_l_false_m1 -> { _l_true__m2, _n_true___0 }
       { _l_false_m1, _l_false__0 } -> x_l_false_m1_l_false__0 -> { _l_true__m1, _n_true___0 }
       { _l_false_m1, _l_false_p1 } -> x_l_false_m1_l_false_p1 -> { _l_true___0, _n_true___0 }
       { _l_false_m1, _l_false_p2 } -> x_l_false_m1_l_false_p2 -> { _l_false_p1, _n_false__0 }
       { _l_false__0, _l_true__m2 } -> x_l_false__0_l_true__m2 -> { _l_true__m2, _n_true___0 }
       { _l_false__0, _l_true__m1 } -> x_l_false__0_l_true__m1 -> { _l_true__m1, _n_true___0 }
       { _l_false__0, _l_true___0 } -> x_l_false__0_l_true___0 -> { _l_true___0, _n_true___0 }
       { _l_false__0, _l_true__p1 } -> x_l_false__0_l_true__p1 -> { _l_false_p1, _n_false__0 }
       { _l_false__0, _l_true__p2 } -> x_l_false__0_l_true__p2 -> { _l_false_p2, _n_false__0 }
       { _l_false__0, _l_false__0 } -> x_l_false__0_l_false__0 -> { _l_true___0, _n_true___0 }
       { _l_false__0, _l_false_p1 } -> x_l_false__0_l_false_p1 -> { _l_false_p1, _n_false__0 }
       { _l_false__0, _l_false_p2 } -> x_l_false__0_l_false_p2 -> { _l_false_p2, _n_false__0 }
       { _l_false_p1, _l_true__m2 } -> x_l_false_p1_l_true__m2 -> { _l_true__m1, _n_true___0 }
       { _l_false_p1, _l_true__m1 } -> x_l_false_p1_l_true__m1 -> { _l_true___0, _n_true___0 }
       { _l_false_p1, _l_true___0 } -> x_l_false_p1_l_true___0 -> { _l_false_p1, _n_false__0 }
       { _l_false_p1, _l_true__p1 } -> x_l_false_p1_l_true__p1 -> { _l_false_p2, _n_false__0 }
       { _l_false_p1, _l_true__p2 } -> x_l_false_p1_l_true__p2 -> { _l_false_p2, _n_false_p1 }
       { _l_false_p1, _l_false_p1 } -> x_l_false_p1_l_false_p1 -> { _l_false_p2, _n_false__0 }
       { _l_false_p1, _l_false_p2 } -> x_l_false_p1_l_false_p2 -> { _l_false_p2, _n_false_p1 }
       { _l_false_p2, _l_true__m2 } -> x_l_false_p2_l_true__m2 -> { _l_true___0, _n_true___0 }
       { _l_false_p2, _l_true__m1 } -> x_l_false_p2_l_true__m1 -> { _l_false_p1, _n_false__0 }
       { _l_false_p2, _l_true___0 } -> x_l_false_p2_l_true___0 -> { _l_false_p2, _n_false__0 }
       { _l_false_p2, _l_true__p1 } -> x_l_false_p2_l_true__p1 -> { _l_false_p2, _n_false_p1 }
       { _l_false_p2, _l_true__p2 } -> x_l_false_p2_l_true__p2 -> { _l_false_p2, _n_false_p2 }
       { _l_false_p2, _l_false_p2 } -> x_l_false_p2_l_false_p2 -> { _l_false_p2, _n_false_p2 }
       { _n_true__m2, _l_true__m1 } -> x_n_true__m2_l_true__m1 -> { _l_true__m2, _n_true__m1 }
       { _n_true__m2, _l_true___0 } -> x_n_true__m2_l_true___0 -> { _l_true__m2, _n_true___0 }
       { _n_true__m2, _l_true__p1 } -> x_n_true__m2_l_true__p1 -> { _l_true__m1, _n_true___0 }
       { _n_true__m2, _l_true__p2 } -> x_n_true__m2_l_true__p2 -> { _l_true___0, _n_true___0 }
       { _n_true__m2, _l_false_m2 } -> x_n_true__m2_l_false_m2 -> { _l_true__m2, _n_true__m2 }
       { _n_true__m2, _l_false_m1 } -> x_n_true__m2_l_false_m1 -> { _l_true__m2, _n_true__m1 }
       { _n_true__m2, _l_false__0 } -> x_n_true__m2_l_false__0 -> { _l_true__m2, _n_true___0 }
       { _n_true__m2, _l_false_p1 } -> x_n_true__m2_l_false_p1 -> { _l_true__m1, _n_true___0 }
       { _n_true__m2, _l_false_p2 } -> x_n_true__m2_l_false_p2 -> { _l_true___0, _n_true___0 }
       { _n_true__m1, _l_true__m1 } -> x_n_true__m1_l_true__m1 -> { _l_true__m2, _n_true___0 }
       { _n_true__m1, _l_true___0 } -> x_n_true__m1_l_true___0 -> { _l_true__m1, _n_true___0 }
       { _n_true__m1, _l_true__p1 } -> x_n_true__m1_l_true__p1 -> { _l_true___0, _n_true___0 }
       { _n_true__m1, _l_true__p2 } -> x_n_true__m1_l_true__p2 -> { _l_false_p1, _n_false__0 }
       { _n_true__m1, _l_false_m2 } -> x_n_true__m1_l_false_m2 -> { _l_true__m2, _n_true__m1 }
       { _n_true__m1, _l_false_m1 } -> x_n_true__m1_l_false_m1 -> { _l_true__m2, _n_true___0 }
       { _n_true__m1, _l_false__0 } -> x_n_true__m1_l_false__0 -> { _l_true__m1, _n_true___0 }
       { _n_true__m1, _l_false_p1 } -> x_n_true__m1_l_false_p1 -> { _l_true___0, _n_true___0 }
       { _n_true__m1, _l_false_p2 } -> x_n_true__m1_l_false_p2 -> { _l_false_p1, _n_false__0 }
       { _n_true___0, _l_true__p1 } -> x_n_true___0_l_true__p1 -> { _l_false_p1, _n_false__0 }
       { _n_true___0, _l_true__p2 } -> x_n_true___0_l_true__p2 -> { _l_false_p2, _n_false__0 }
       { _n_true___0, _l_false_m2 } -> x_n_true___0_l_false_m2 -> { _l_true__m2, _n_true___0 }
       { _n_true___0, _l_false_m1 } -> x_n_true___0_l_false_m1 -> { _l_true__m1, _n_true___0 }
       { _n_true___0, _l_false__0 } -> x_n_true___0_l_false__0 -> { _l_true___0, _n_true___0 }
       { _n_true___0, _l_false_p1 } -> x_n_true___0_l_false_p1 -> { _l_false_p1, _n_false__0 }
       { _n_true___0, _l_false_p2 } -> x_n_true___0_l_false_p2 -> { _l_false_p2, _n_false__0 }
       { _n_true__p1, _l_true__m2 } -> x_n_true__p1_l_true__m2 -> { _l_true__m1, _n_true___0 }
       { _n_true__p1, _l_true__m1 } -> x_n_true__p1_l_true__m1 -> { _l_true___0, _n_true___0 }
       { _n_true__p1, _l_true___0 } -> x_n_true__p1_l_true___0 -> { _l_false_p1, _n_false__0 }
       { _n_true__p1, _l_true__p1 } -> x_n_true__p1_l_true__p1 -> { _l_false_p2, _n_false__0 }
       { _n_true__p1, _l_true__p2 } -> x_n_true__p1_l_true__p2 -> { _l_false_p2, _n_false_p1 }
       { _n_true__p1, _l_false_m2 } -> x_n_true__p1_l_false_m2 -> { _l_true__m1, _n_true___0 }
       { _n_true__p1, _l_false_m1 } -> x_n_true__p1_l_false_m1 -> { _l_true___0, _n_true___0 }
       { _n_true__p1, _l_false__0 } -> x_n_true__p1_l_false__0 -> { _l_false_p1, _n_false__0 }
       { _n_true__p1, _l_false_p1 } -> x_n_true__p1_l_false_p1 -> { _l_false_p2, _n_false__0 }
       { _n_true__p1, _l_false_p2 } -> x_n_true__p1_l_false_p2 -> { _l_false_p2, _n_false_p1 }
       { _n_true__p2, _l_true__m2 } -> x_n_true__p2_l_true__m2 -> { _l_true___0, _n_true___0 }
       { _n_true__p2, _l_true__m1 } -> x_n_true__p2_l_true__m1 -> { _l_false_p1, _n_false__0 }
       { _n_true__p2, _l_true___0 } -> x_n_true__p2_l_true___0 -> { _l_false_p2, _n_false__0 }
       { _n_true__p2, _l_true__p1 } -> x_n_true__p2_l_true__p1 -> { _l_false_p2, _n_false_p1 }
       { _n_true__p2, _l_true__p2 } -> x_n_true__p2_l_true__p2 -> { _l_false_p2, _n_false_p2 }
       { _n_true__p2, _l_false_m2 } -> x_n_true__p2_l_false_m2 -> { _l_true___0, _n_true___0 }
       { _n_true__p2, _l_false_m1 } -> x_n_true__p2_l_false_m1 -> { _l_false_p1, _n_false__0 }
       { _n_true__p2, _l_false__0 } -> x_n_true__p2_l_false__0 -> { _l_false_p2, _n_false__0 }
       { _n_true__p2, _l_false_p1 } -> x_n_true__p2_l_false_p1 -> { _l_false_p2, _n_false_p1 }
       { _n_true__p2, _l_false_p2 } -> x_n_true__p2_l_false_p2 -> { _l_false_p2, _n_false_p2 }
       { _n_false_m2, _l_true__m2 } -> x_n_false_m2_l_true__m2 -> { _l_true__m2, _n_true__m2 }
       { _n_false_m2, _l_true__m1 } -> x_n_false_m2_l_true__m1 -> { _l_true__m2, _n_true__m1 }
       { _n_false_m2, _l_true___0 } -> x_n_false_m2_l_true___0 -> { _l_true__m2, _n_true___0 }
       { _n_false_m2, _l_true__p1 } -> x_n_false_m2_l_true__p1 -> { _l_true__m1, _n_true___0 }
       { _n_false_m2, _l_true__p2 } -> x_n_false_m2_l_true__p2 -> { _l_true___0, _n_true___0 }
       { _n_false_m2, _l_false_m2 } -> x_n_false_m2_l_false_m2 -> { _l_true__m2, _n_true__m2 }
       { _n_false_m2, _l_false_m1 } -> x_n_false_m2_l_false_m1 -> { _l_true__m2, _n_true__m1 }
       { _n_false_m2, _l_false__0 } -> x_n_false_m2_l_false__0 -> { _l_true__m2, _n_true___0 }
       { _n_false_m2, _l_false_p1 } -> x_n_false_m2_l_false_p1 -> { _l_true__m1, _n_true___0 }
       { _n_false_m2, _l_false_p2 } -> x_n_false_m2_l_false_p2 -> { _l_true___0, _n_true___0 }
       { _n_false_m1, _l_true__m2 } -> x_n_false_m1_l_true__m2 -> { _l_true__m2, _n_true__m1 }
       { _n_false_m1, _l_true__m1 } -> x_n_false_m1_l_true__m1 -> { _l_true__m2, _n_true___0 }
       { _n_false_m1, _l_true___0 } -> x_n_false_m1_l_true___0 -> { _l_true__m1, _n_true___0 }
       { _n_false_m1, _l_true__p1 } -> x_n_false_m1_l_true__p1 -> { _l_true___0, _n_true___0 }
       { _n_false_m1, _l_true__p2 } -> x_n_false_m1_l_true__p2 -> { _l_false_p1, _n_false__0 }
       { _n_false_m1, _l_false_m2 } -> x_n_false_m1_l_false_m2 -> { _l_true__m2, _n_true__m1 }
       { _n_false_m1, _l_false_m1 } -> x_n_false_m1_l_false_m1 -> { _l_true__m2, _n_true___0 }
       { _n_false_m1, _l_false__0 } -> x_n_false_m1_l_false__0 -> { _l_true__m1, _n_true___0 }
       { _n_false_m1, _l_false_p1 } -> x_n_false_m1_l_false_p1 -> { _l_true___0, _n_true___0 }
       { _n_false_m1, _l_false_p2 } -> x_n_false_m1_l_false_p2 -> { _l_false_p1, _n_false__0 }
       { _n_false__0, _l_true__m2 } -> x_n_false__0_l_true__m2 -> { _l_true__m2, _n_true___0 }
       { _n_false__0, _l_true__m1 } -> x_n_false__0_l_true__m1 -> { _l_true__m1, _n_true___0 }
       { _n_false__0, _l_true___0 } -> x_n_false__0_l_true___0 -> { _l_true___0, _n_true___0 }
       { _n_false__0, _l_true__p1 } -> x_n_false__0_l_true__p1 -> { _l_false_p1, _n_false__0 }
       { _n_false__0, _l_true__p2 } -> x_n_false__0_l_true__p2 -> { _l_false_p2, _n_false__0 }
       { _n_false__0, _l_false_m2 } -> x_n_false__0_l_false_m2 -> { _l_true__m2, _n_true___0 }
       { _n_false__0, _l_false_m1 } -> x_n_false__0_l_false_m1 -> { _l_true__m1, _n_true___0 }
       { _n_false__0, _l_false__0 } -> x_n_false__0_l_false__0 -> { _l_true___0, _n_true___0 }
       { _n_false_p1, _l_true__m2 } -> x_n_false_p1_l_true__m2 -> { _l_true__m1, _n_true___0 }
       { _n_false_p1, _l_true__m1 } -> x_n_false_p1_l_true__m1 -> { _l_true___0, _n_true___0 }
       { _n_false_p1, _l_true___0 } -> x_n_false_p1_l_true___0 -> { _l_false_p1, _n_false__0 }
       { _n_false_p1, _l_true__p1 } -> x_n_false_p1_l_true__p1 -> { _l_false_p2, _n_false__0 }
       { _n_false_p1, _l_true__p2 } -> x_n_false_p1_l_true__p2 -> { _l_false_p2, _n_false_p1 }
       { _n_false_p1, _l_false_m2 } -> x_n_false_p1_l_false_m2 -> { _l_true__m1, _n_true___0 }
       { _n_false_p1, _l_false_m1 } -> x_n_false_p1_l_false_m1 -> { _l_true___0, _n_true___0 }
       { _n_false_p1, _l_false__0 } -> x_n_false_p1_l_false__0 -> { _l_false_p1, _n_false__0 }
       { _n_false_p1, _l_false_p1 } -> x_n_false_p1_l_false_p1 -> { _l_false_p2, _n_false__0 }
       { _n_false_p2, _l_true__m2 } -> x_n_false_p2_l_true__m2 -> { _l_true___0, _n_true___0 }
       { _n_false_p2, _l_true__m1 } -> x_n_false_p2_l_true__m1 -> { _l_false_p1, _n_false__0 }
       { _n_false_p2, _l_true___0 } -> x_n_false_p2_l_true___0 -> { _l_false_p2, _n_false__0 }
       { _n_false_p2, _l_true__p1 } -> x_n_false_p2_l_true__p1 -> { _l_false_p2, _n_false_p1 }
       { _n_false_p2, _l_true__p2 } -> x_n_false_p2_l_true__p2 -> { _l_false_p2, _n_false_p2 }
       { _n_false_p2, _l_false_m2 } -> x_n_false_p2_l_false_m2 -> { _l_true___0, _n_true___0 }
       { _n_false_p2, _l_false_m1 } -> x_n_false_p2_l_false_m1 -> { _l_false_p1, _n_false__0 }
       { _n_false_p2, _l_false__0 } -> x_n_false_p2_l_false__0 -> { _l_false_p2, _n_false__0 }
       { _n_false_p2, _l_false_p1 } -> x_n_false_p2_l_false_p1 -> { _l_false_p2, _n_false_p1 }
    }
    initial   {
        _l_true__m2 _l_true__m1 _l_true___0 _l_true__p1 _l_true__p2
        _l_false_m2 _l_false_m1 _l_false__0 _l_false_p1 _l_false_p2
    }
    true      {
        _l_true__m2 _l_true__m1 _l_true___0 _l_true__p1 _l_true__p2
        _n_true__m2 _n_true__m1 _n_true___0 _n_true__p1 _n_true__p2
    }
    false     {
        _l_false_m2 _l_false_m1 _l_false__0 _l_false_p1 _l_false_p2
        _n_false_m2 _n_false_m1 _n_false__0 _n_false_p1 _n_false_p2
    }
    predicate {
        -2 * _l_true__m2 + -1 * _l_true__m1 + 0 * _l_true___0 + 1 * _l_true__p1 + 2 * _l_true__p2 +
        -2 * _l_false_m2 + -1 * _l_false_m1 + 0 * _l_false__0 + 1 * _l_false_p1 + 2 * _l_false_p2 < 1
    }
}