terminating-complex.pnet 587 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
petri net "terminating" {
    places { p1 p2 p3 p4 q1 q2 q3 q4 }
    transitions { t1 t2 t3 t4 u1 u2 u3 }
    arcs {
        p1 -> t1 -> p2
        p3 -> t1 -> p3
        q1 -> t1 -> q1
        p2 -> t2 -> p1
        p4 -> t2 -> p4
        q2 -> t2 -> q2
        p3 -> t3 -> p4
        p2 -> t3 -> p2
        q3 -> t3 -> q3
        p4 -> t4 -> p3
        p1 -> t4 -> p1
        q4 -> t4 -> q4

        q1 -> u1 -> q2
        q2 -> u2 -> q3
        q3 -> u3 -> q4
    }
    initial { p1 p3 q1 q2 q3 }
}
liveness property "terminating" {
    true // t1 + t2 + t3 + t4 + u1 + u2 + u3 > 0
}