The following FSM models a basic Vending Machine.
Re-create it in Workcraft:
s0
is the initial state; this can be set by selecting a node and editing its properties using the Property editor panel
s0
to s1
in the picture below) – you can use polylines and/or Bezier curves
Simulate your model (by pressing the button in the Editor tools panel). Try to re-create the following scenarios:
Formally verify (using Verification menu) whether the FSM
Re-create the following FSM in Workcraft (and save it in a different file).
Simulate your model. Try to re-create the following scenarios:
Verify the properties of this FSM as in the previous exercise. Can you explain the verification results?