The following FSM models a basic Vending Machine:

Re-create it in Workcraft:

• Select File→Create work…
• Select Finite State Machine from the list of model types
• Use Model tools toolbar to draw the FSM. Note that:
  • s0 is the initial state; this can be set by selecting a node and editing its properties using the Property editor panel
  • action names are given on arcs – they can be set by selecting an arc and editing its properties using the Property editor panel
  • the arcs don’t have to be straight (see e.g. the arc from s0 to s1 in the picture below) – you can use polylines and/or Bezier curves
• Make sure to save your work!

Simulate your model (by pressing the button in the Model tools toolbar). Try to re-create the following scenarios:

• buying a coke and then a chocolate
• inserting a coin and then cancelling
• inserting a coin, ordering coke and then cancelling (this scenario should be impossible)

Formally verify (using Verification menu) whether the FSM

• has deadlocks
• has unreachable states
• is reversible
• is deterministic

Re-create the following FSM in Workcraft and save it in a different file (to draw curved arcs you need to change the connection type from Polyline to Bezier as explained here):

Simulate your model. Try to re-create the following scenarios:

• buying a coke and then a chocolate
• inserting a coin and then cancelling
• ordering a chocolate but getting a coke instead
• try to drive the FSM to state s6 that enables a windfall of coins (this scenario should be impossible)

Verify the properties of this FSM as in the previous exercise. Can you explain the verification results?