We have now proposed a model, which obviously is in accordance with the specification. However, we may ask if there is some way to formally analyse the model and check that the properties are in accordance with our expectations, i.e., check that the specification is sound.In order to find out how the control works, we record the states of the model. The state of the model is the number of tokens in the places. We represent the state as a vector, with the places ordered as (R CR GS GF).
( R CR GS GF) ( 1 0 5 0) 0. Initial | | READ V ( 0 1 5 0) 1. | | DISP V ( 1 0 4 1) 2.One cycle of the machine's working is completed and the READ transition is again enabled. The working is obviously in accordance with our expectations. Successive transitions READ, DISP eventually leads to a state in which both READ and REF are enabled giving the possibilities:( R CR GS GF) ( 1 0 0 5) 10. / \ READ / \ REF v v ( 0 1 0 5) 11.1 (1 0 5 0) 11.2 = 0. | | REF V ( 0 1 5 0) 12. = 1.We have found all possible states and can conclude that the machine will never reach a state from which it cannot continue properly. It will loop forever by dispensating until the goods storage is empty, and retain this dispensating after the goods storage is replenished.The state tree derived above is called the reachability tree. Much of the analysis of Petri Nets is based on the reachability tree.