====== Modelling with Finite State Machines: Vending machine ======

===== Exercise 1: Basic Vending Machine =====

The following FSM models a basic Vending Machine:

{{ vm-basic.svg?50%,nolink |}}

Re-create it in Workcraft:
  * Select //File->Create work…//
  * Select //Finite State Machine// from the list of model types
  * Use //[[:help:core:model_tools|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 //[[:help:core:property_editor|Property editor]]// panel
    * action names are given on arcs – they can be set by selecting an arc and editing its properties using the //[[:help:core:property_editor|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 {{help:core:editor_tools-simulate.png?nolink|[M] Simulate}} button in the //[[:help:core:model_tools|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 [[help:core:property_editor#connection_properties|here]]):

{{ vm-nondet-unreach.svg?50%,nolink |}}

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?

{{page>:tutorial:feedback&inline}}