remainder_m3_c1.pp 828 Bytes
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
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 }
4
    arcs {
Philipp Meyer's avatar
Philipp Meyer committed
5
6
7
8
9
10
11
12
13
       { _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 }
14
    }
Philipp Meyer's avatar
Philipp Meyer committed
15
16
17
    initial { _0 _1 _2 }
    true    { _1 _true }
    false   { _0 _2 _false }
18
    predicate {
Philipp Meyer's avatar
Philipp Meyer committed
19
        EXISTS k : _1 + 2 * _2 = 1 + 3*k
20
21
    }
}