Modelling with Finite State Machines: Vending machine

Exercise 1: Basic Vending Machine

The following FSM models a basic Vending Machine:

tutorial:model:vending_machine:vm-basic.svg

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 [M] Simulate 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

Exercise 2: Dodgy Vending Machine

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):

tutorial:model:vending_machine:vm-nondet-unreach.svg

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?

===== Feedback =====

As discussed in https://www.dokuwiki.org/plugin:include#controlling_header_size_in_included_pages, by default, the headers in included pages start one level lower than the last header in the current page. This can be tweaked by adding an empty header above the include:\\
```
====== ======
{{page>:tutorial:feedback&inline}}
```
For offline help generation the content of feedback page should be temporary wrapped in <WRAP hide>. Note that the headers still propagate to the table of contents even if inside the hidden wrap. Therefore the Feedback title needs to be converted to something else, e.g. to code by adding two spaces in front.