Coverability Graph
Analysing the coverability graph we have:
- Reachability: all marking are reachable through some firing sequence starting from M0
- Boundness: all places are bounded. In no moment there is a place with more than 3 tokens
- Liveness: there is no deadlock state