terminating-v2.pnet 611 Bytes
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
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
petri net "terminating" {
    places { q1 s2 s3 s4 s5 p2 p3 p4 p5 q2 }
    transitions { t1 t2 t3 t4 u1 u2 u3 u4 v1 v2 }
    arcs {
        q1 -> t1 -> s2
        s2 -> t2 -> q1
        s3 -> t3 -> s4
        s3 -> t1 -> s3
        s4 -> t4 -> s3
        s4 -> t2 -> s4
        s5 -> t4

        q1 -> u1 -> p2
        p2 -> u2 -> q1
        p3 -> u3 -> p4
        p3 -> u1 -> p3
        p4 -> u4 -> p3
        p4 -> u2 -> p4
        p5 -> u4

        s2 -> v1 -> p2
        q2 -> v1
        p2 -> v2 -> s2
        q2 -> v2
    }
    initial { q1 s3 s5 p3 p5 q2 }
}
liveness property "terminating" {
    true
}