remainder_m3_c1.pp 1.18 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
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 }
    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 }
    }
    initial {_mod0 _mod1 _mod2}
    true {_mod1 _modpassivetrue}
    false {_mod0 _mod2 _modpassivefalse}
    predicate {
        EXISTS k : (_mod1 + 2 * _mod2 = 1 + 3*k)
    }
}