terminating.pnet 349 Bytes
Newer Older
1
petri net "terminating" {
Philipp Meyer's avatar
Philipp Meyer committed
2
3
    places { p1 p2 p3 p4 p5 }
    transitions { t1 t2 t3 t4 }
4
5
    arcs {
        p1 -> t1 -> p2
Philipp Meyer's avatar
Philipp Meyer committed
6
        p3 -> t1 -> p3
7
        p2 -> t2 -> p1
Philipp Meyer's avatar
Philipp Meyer committed
8
9
10
11
        p4 -> t2 -> p4
        p3 -> t3 -> p4
        p4 -> t4 -> p3
        p5 -> t4
12
    }
Philipp Meyer's avatar
Philipp Meyer committed
13
14
15
16
    initial { p1 p3 p5 }
}
liveness property "terminating" {
    t1 + t2 + t3 + t4 > 0
17
}