Skip to content

GitLab

Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

Commit 9642fa72 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Made examples more readable

parent c6f93bf3
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 288 additions and 423 deletions
examples/broadcast.pp
View file @ 9642fa72
population protocol "Broadcast Protocol" {
states { _true _false }
states { _true _false }
transitions { x_false_true }
arcs {
{ _false, _true } -> x_false_true -> { _true, _true }
}
initial { _true _false }
true { _true }
false { _false }
initial { _true _false }
true { _true }
false { _false }
predicate { _true >= 1 }
}
examples/flockofbirds_c10.pp deleted 100644 → 0
View file @ c6f93bf3
population protocol "Flock of birds protocol with c = 10" {
states { _0 _1 _2 _3 _4 _5 _6 _7 _8 _9 _10}
transitions { x__0__10 x__1__1 x__1__2 x__1__3 x__1__4 x__1__5 x__1__6 x__1__7 x__1__8 x__1__9 x__1__10 x__2__2 x__2__3 x__2__4 x__2__5 x__2__6 x__2__7 x__2__8 x__2__9 x__2__10 x__3__3 x__3__4 x__3__5 x__3__6 x__3__7 x__3__8 x__3__9 x__3__10 x__4__4 x__4__5 x__4__6 x__4__7 x__4__8 x__4__9 x__4__10 x__5__5 x__5__6 x__5__7 x__5__8 x__5__9 x__5__10 x__6__6 x__6__7 x__6__8 x__6__9 x__6__10 x__7__7 x__7__8 x__7__9 x__7__10 x__8__8 x__8__9 x__8__10 x__9__9 x__9__10 }
arcs {
{ _0, _10 } -> x__0__10 -> { _10, _10 }
{ _1, _1 } -> x__1__1 -> { _2, _0 }
{ _1, _2 } -> x__1__2 -> { _3, _0 }
{ _1, _3 } -> x__1__3 -> { _4, _0 }
{ _1, _4 } -> x__1__4 -> { _5, _0 }
{ _1, _5 } -> x__1__5 -> { _6, _0 }
{ _1, _6 } -> x__1__6 -> { _7, _0 }
{ _1, _7 } -> x__1__7 -> { _8, _0 }
{ _1, _8 } -> x__1__8 -> { _9, _0 }
{ _1, _9 } -> x__1__9 -> { _10, _10 }
{ _1, _10 } -> x__1__10 -> { _10, _10 }
{ _2, _2 } -> x__2__2 -> { _4, _0 }
{ _2, _3 } -> x__2__3 -> { _5, _0 }
{ _2, _4 } -> x__2__4 -> { _6, _0 }
{ _2, _5 } -> x__2__5 -> { _7, _0 }
{ _2, _6 } -> x__2__6 -> { _8, _0 }
{ _2, _7 } -> x__2__7 -> { _9, _0 }
{ _2, _8 } -> x__2__8 -> { _10, _10 }
{ _2, _9 } -> x__2__9 -> { _10, _10 }
{ _2, _10 } -> x__2__10 -> { _10, _10 }
{ _3, _3 } -> x__3__3 -> { _6, _0 }
{ _3, _4 } -> x__3__4 -> { _7, _0 }
{ _3, _5 } -> x__3__5 -> { _8, _0 }
{ _3, _6 } -> x__3__6 -> { _9, _0 }
{ _3, _7 } -> x__3__7 -> { _10, _10 }
{ _3, _8 } -> x__3__8 -> { _10, _10 }
{ _3, _9 } -> x__3__9 -> { _10, _10 }
{ _3, _10 } -> x__3__10 -> { _10, _10 }
{ _4, _4 } -> x__4__4 -> { _8, _0 }
{ _4, _5 } -> x__4__5 -> { _9, _0 }
{ _4, _6 } -> x__4__6 -> { _10, _10 }
{ _4, _7 } -> x__4__7 -> { _10, _10 }
{ _4, _8 } -> x__4__8 -> { _10, _10 }
{ _4, _9 } -> x__4__9 -> { _10, _10 }
{ _4, _10 } -> x__4__10 -> { _10, _10 }
{ _5, _5 } -> x__5__5 -> { _10, _10 }
{ _5, _6 } -> x__5__6 -> { _10, _10 }
{ _5, _7 } -> x__5__7 -> { _10, _10 }
{ _5, _8 } -> x__5__8 -> { _10, _10 }
{ _5, _9 } -> x__5__9 -> { _10, _10 }
{ _5, _10 } -> x__5__10 -> { _10, _10 }
{ _6, _6 } -> x__6__6 -> { _10, _10 }
{ _6, _7 } -> x__6__7 -> { _10, _10 }
{ _6, _8 } -> x__6__8 -> { _10, _10 }
{ _6, _9 } -> x__6__9 -> { _10, _10 }
{ _6, _10 } -> x__6__10 -> { _10, _10 }
{ _7, _7 } -> x__7__7 -> { _10, _10 }
{ _7, _8 } -> x__7__8 -> { _10, _10 }
{ _7, _9 } -> x__7__9 -> { _10, _10 }
{ _7, _10 } -> x__7__10 -> { _10, _10 }
{ _8, _8 } -> x__8__8 -> { _10, _10 }
{ _8, _9 } -> x__8__9 -> { _10, _10 }
{ _8, _10 } -> x__8__10 -> { _10, _10 }
{ _9, _9 } -> x__9__9 -> { _10, _10 }
{ _9, _10 } -> x__9__10 -> { _10, _10 }
}
initial {_0 _1}
true {_10}
false {_0 _1 _2 _3 _4 _5 _6 _7 _8 _9}
predicate { _1 >= 10 }
}
examples/flockofbirds_v1_c4.pp 0 → 100644
View file @ 9642fa72
population protocol "Flock of Birds Protocol (variant 1) with c = 4" {
states { _0 _1 _2 _3 _4 }
transitions { x_0_4 x_1_1 x_1_2 x_1_3 x_1_4 x_2_2 x_2_3 x_2_4 x_3_3 x_3_4 }
arcs {
{ _0, _4 } -> x_0_4 -> { _4, _4 }
{ _1, _1 } -> x_1_1 -> { _2, _0 }
{ _1, _2 } -> x_1_2 -> { _3, _0 }
{ _1, _3 } -> x_1_3 -> { _4, _4 }
{ _1, _4 } -> x_1_4 -> { _4, _4 }
{ _2, _2 } -> x_2_2 -> { _4, _4 }
{ _2, _3 } -> x_2_3 -> { _4, _4 }
{ _2, _4 } -> x_2_4 -> { _4, _4 }
{ _3, _3 } -> x_3_3 -> { _4, _4 }
{ _3, _4 } -> x_3_4 -> { _4, _4 }
}
initial { _0 _1 }
true { _4 }
false { _0 _1 _2 _3 }
predicate { _1 >= 4 }
}
examples/flockofbirds_v2_c4.pp 0 → 100644
View file @ 9642fa72
population protocol "Flock of Birds Protocol (variant 2) with c = 4" {
states { _0 _1 _2 _3 _4 }
transitions { x_0_4 x_1_1 x_1_4 x_2_2 x_2_4 x_3_3 x_3_4 }
arcs {
{ _0, _4 } -> x_0_4 -> { _4, _4 }
{ _1, _1 } -> x_1_1 -> { _1, _2 }
{ _1, _4 } -> x_1_4 -> { _4, _4 }
{ _2, _2 } -> x_2_2 -> { _2, _3 }
{ _2, _4 } -> x_2_4 -> { _4, _4 }
{ _3, _3 } -> x_3_3 -> { _3, _4 }
{ _3, _4 } -> x_3_4 -> { _4, _4 }
}
initial { _0 _1 }
true { _4 }
false { _0 _1 _2 _3 }
predicate { _1 >= 4 }
}
examples/majority.pp
View file @ 9642fa72
population protocol "Majority Protocol" {
states { good bad neutral mildlybad}
states { good bad neutral mildlybad }
transitions { x_good_bad x_good_mildlybad x_bad_neutral x_neutral_mildlybad }
arcs {
{ good, bad } -> x_good_bad -> { neutral, mildlybad }
{ good, mildlybad } -> x_good_mildlybad -> { good, neutral }
{ bad, neutral } -> x_bad_neutral -> { bad, mildlybad }
{ good, bad } -> x_good_bad -> { neutral, mildlybad }
{ good, mildlybad } -> x_good_mildlybad -> { good, neutral }
{ bad, neutral } -> x_bad_neutral -> { bad, mildlybad }
{ neutral, mildlybad } -> x_neutral_mildlybad -> { mildlybad, mildlybad }
}
initial { good bad }
true { good neutral }
false { bad mildlybad }
initial { good bad }
true { good neutral }
false { bad mildlybad }
predicate { good > bad }
}
examples/newbirds_c10.pp deleted 100644 → 0
View file @ c6f93bf3
population protocol "New birds protocol with c = 10" {
states { _0 _1 _2 _3 _4 _5 _6 _7 _8 _9 _10}
transitions { x__0__10 x__1__1 x__1__10 x__2__2 x__2__10 x__3__3 x__3__10 x__4__4 x__4__10 x__5__5 x__5__10 x__6__6 x__6__10 x__7__7 x__7__10 x__8__8 x__8__10 x__9__9 x__9__10 }
arcs {
{ _0, _10 } -> x__0__10 -> { _10, _10 }
{ _1, _1 } -> x__1__1 -> { _1, _2 }
{ _1, _10 } -> x__1__10 -> { _10, _10 }
{ _2, _2 } -> x__2__2 -> { _2, _3 }
{ _2, _10 } -> x__2__10 -> { _10, _10 }
{ _3, _3 } -> x__3__3 -> { _3, _4 }
{ _3, _10 } -> x__3__10 -> { _10, _10 }
{ _4, _4 } -> x__4__4 -> { _4, _5 }
{ _4, _10 } -> x__4__10 -> { _10, _10 }
{ _5, _5 } -> x__5__5 -> { _5, _6 }
{ _5, _10 } -> x__5__10 -> { _10, _10 }
{ _6, _6 } -> x__6__6 -> { _6, _7 }
{ _6, _10 } -> x__6__10 -> { _10, _10 }
{ _7, _7 } -> x__7__7 -> { _7, _8 }
{ _7, _10 } -> x__7__10 -> { _10, _10 }
{ _8, _8 } -> x__8__8 -> { _8, _9 }
{ _8, _10 } -> x__8__10 -> { _10, _10 }
{ _9, _9 } -> x__9__9 -> { _9, _10 }
{ _9, _10 } -> x__9__10 -> { _10, _10 }
}
initial {_0 _1}
true {_10}
false {_0 _1 _2 _3 _4 _5 _6 _7 _8 _9}
predicate { _1 >= 10 }
}
examples/remainder_m3_c1.pp
View file @ 9642fa72
population protocol "Modulo Protocol with m = 3 and c = 1" {
states { _mod0 _mod1 _mod2 _modpassivetrue _modpassivefalse}
transitions { x__mod0__mod0 x__mod0__mod1 x__mod0__mod2 x__mod0__modpassivetrue x__mod1__mod1 x__mod1__mod2 x__mod1__modpassivefalse x__mod2__mod2 x__mod2__modpassivetrue }
population protocol "Remainder Protocol with m = 3 and c = 1" {
states { _0 _1 _2 _true _false }
transitions { x_0_0 x_0_1 x_0_2 x_0_true x_1_1 x_1_2 x_1_false x_2_2 x_2_true }
arcs {
{ _mod0, _mod0 } -> x__mod0__mod0 -> { _mod0, _modpassivefalse }
{ _mod0, _mod1 } -> x__mod0__mod1 -> { _mod1, _modpassivetrue }
{ _mod0, _mod2 } -> x__mod0__mod2 -> { _mod2, _modpassivefalse }
{ _mod0, _modpassivetrue } -> x__mod0__modpassivetrue -> { _mod0, _modpassivefalse }
{ _mod1, _mod1 } -> x__mod1__mod1 -> { _mod2, _modpassivefalse }
{ _mod1, _mod2 } -> x__mod1__mod2 -> { _mod0, _modpassivefalse }
{ _mod1, _modpassivefalse } -> x__mod1__modpassivefalse -> { _mod1, _modpassivetrue }
{ _mod2, _mod2 } -> x__mod2__mod2 -> { _mod1, _modpassivetrue }
{ _mod2, _modpassivetrue } -> x__mod2__modpassivetrue -> { _mod2, _modpassivefalse }
{ _0, _0 } -> x_0_0 -> { _0, _false }
{ _0, _1 } -> x_0_1 -> { _1, _true }
{ _0, _2 } -> x_0_2 -> { _2, _false }
{ _0, _true } -> x_0_true -> { _0, _false }
{ _1, _1 } -> x_1_1 -> { _2, _false }
{ _1, _2 } -> x_1_2 -> { _0, _false }
{ _1, _false } -> x_1_false -> { _1, _true }
{ _2, _2 } -> x_2_2 -> { _1, _true }
{ _2, _true } -> x_2_true -> { _2, _false }
}
initial {_mod0 _mod1 _mod2}
true {_mod1 _modpassivetrue}
false {_mod0 _mod2 _modpassivefalse}
initial { _0 _1 _2 }
true { _1 _true }
false { _0 _2 _false }
predicate {
EXISTS k : (_mod1 + 2 * _mod2 = 1 + 3*k)
EXISTS k : _1 + 2 * _2 = 1 + 3*k
}
}
examples/threshold_l2_c1.pp 0 → 100644
View file @ 9642fa72
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
}
}
examples/threshold_l3_c1.pp deleted 100644 → 0
View file @ c6f93bf3
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment