newbirds_c10.pp 1.24 KB
Newer Older
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
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 }
}