The following FSM models a Concurrent Vending Machine that allows the user to insert a £1 coin (action pound
) concurrently with making an order (actions coke
and choc
). Note that the concurrency between actions pound
and coke
as well as pound
and choc
is represented by interleaving – there are two corresponding diamonds in this FSM, and the layout is chosen so as to highlight them. Re-create it in Workcraft.
Simulate your model to make sure that the concurrent actions can happen in any order, and that the Vending Machine processes the orders correctly.
Formally verify whether the FSM
FSMs can be considered as a special case of Petri nets where each transition has exactly one incoming and one outgoing arcs and the initial marking consists of one token. In particular, any FSM can be automatically converted to a Petri net by replacing its states with places, arcs with transitions, and putting a single token on a place corresponding to the initial state. Perform this conversion in Workcraft using the Tools→Conversion→Petri Net menu item:
Simulate your model and make sure that it is equivalent to the above FSM model, in particular the executions are the same. Also, formally verify its correctness properties as above. Pragmatically speaking, this Petri net model does not offer any advantage over the original FSM model:
A better Petri net can often be obtained from the initial FSM model by the process called synthesis. It is a much more complicated procedure than the one outlined above, but it can be automated. Starting from the original FSM, synthesise a Petri net with the same reachability graph as this FSM using the Tools→Conversion→Net synthesis [Petrify] menu item. You can improve the layout manually. Note that transitions pound
and coke
as well as pound
and choc
are concurrent in this Petri net.
Simulate this Petri net, to make sure that it is equivalent to the original FSM model, and formally verify its correctness properties.
Construct the reachability graph of this Petri net (Tools→Conversion→Finite State Transducer [Petrify] menu item). Make sure that this reachability graph is the same as the original FSM (you will need to do manual layout to make it look like the original FSM).