flockofbirds_c10.pp 3.08 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
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
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 }
}