User Tools

Site Tools


tutorial:modelling:fsm:start

Modelling with Finite State Machines: Vending Machine

Exercise 1: Basic Vending Machine

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 Editor tools panel 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 Editor tools panel). 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):

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

Comments or suggestions for improving this tutorial
234 +8᠎ = ?
  • 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.