A Simple State Machine (Dezyne Reference Manual)

4.2 A Simple State Machine

The ihello_bool interface introduces stateful behavior that is somewhat more interesting

interface ihello_bool
{
  in void hello ();
  in bool cruel ();
  out void world ();

  behavior
  {
    bool idle = true;
    [idle] on hello: idle = false;
    [!idle]
      {
        on cruel: {idle = true; reply (idle);}
        on cruel: reply (idle);
        on inevitable: {world; idle = true;}
      }
  }
}

This example introduces some new language aspects

bool idle = true;: A boolean state variable, defining idle=true as the initial state,
[idle]: A guard. Only when the expression between the brackets evaluates to true the on is eligible to execute. In the initial state, the hello trigger is the only thing that can occur. The guard and the on are declarative statements. After the declarative statements follows a,
idle = false;: An imperative statement. When hello trigger occurs, the interface transitions to state !idle,
on cruel: … on cruel: …: A non-deterministic choice³. In the !idle state, cruel is accepted; it can either...
reply (true): reply false and remain not idle, or
{idle = true; reply (idle);}: execute a compound of two imperative statements: Set the reply value to true and transition to the idle state,
inevitable: If no cruel trigger occurs, inevitably the world action will occur. inevitable is a modeling event and is not visible on the trail. The effect is that world action now has become decoupled from the caller.

The state diagram (See Invoking dzn graph) depicts this protocol graphically:

This model is already interesting enough to have the mCRL2 model-checker verify if all is well (See Invoking dzn verify and See Verification Checks and Errors)

$ dzn -v verify doc/examples/ihello-bool.dzn
verify: ihello_bool: check: deadlock: ok
verify: ihello_bool: check: unreachable: ok
verify: ihello_bool: check: livelock: ok
verify: ihello_bool: check: deterministic: ok

which is luckily the case. The model-checker can also be used to generate all possible⁴ traces (See Invoking dzn traces) for ihello_bool:

$ dzn -v traces doc/examples/ihello-bool.dzn

produces three trace files (ihello_bool.trace.0,ihello_bool.trace.1, and ihello_bool.trace.2) with these traces (the order may differ):

hello,return,world
hello,return,cruel,true
hello,return,cruel,false

The sequence for the first trace with the asynchronous world looks like this

client          ihello_bool
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .            return:
  .<-----------------:
  .                  :
  .                  :
  .             world:
  .<-----------------:

and for the second trace where cruel happens looks like this

client          ihello_bool
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .            return:
  .<-----------------:
  .                  :
  .                  :
  .cruel             :
  .----------------->:
  .                  :
  .              true:
  .<-----------------:

the third trace is looks like this

client          ihello_bool
  .                  :
  .                  :
  .hello             :
  .----------------->:
  .                  :
  .            return:
  .<-----------------:
  .                  :
  .                  :
  .cruel             :
  .----------------->:
  .                  :
  .             false:
  .<-----------------:

You may have noticed that the first two traces start and end in the initial state, while the third trace starts in the initial state and ends in the !idle state (also see the corresponding state diagram).

Now have a look at the component simple_state_machine

import ihello-bool.dzn;

interface iworld
{
  in void hello ();
  out void world ();
  behavior
  {
    on hello: {}
    on hello: world;
  }
}

component simple_state_machine
{
  provides ihello_bool p;
  requires ihello_bool r1;
  requires iworld r2;
  behavior
  {
    enum status {A, B, C};
    status s = status.A;
    [s.A]
    {
      on p.hello (): {s=status.B; r2.hello (); r1.hello ();}
    }
    [s.B]
    {
      on p.cruel (): {if (r1.cruel ()) s=status.A; reply (s.A);}
      on r2.world (): s=status.C;
    }
    [s.B || s.C] on r1.world (): {s=status.A; p.world ();}
    [s.C] on p.cruel (): reply (s.A);
  }
}

It introduces the following concepts:

enum status {A, B, C}: User defined enum type named status,
[s.A]: Field test of enum variable s: evaluates to true if s has field value A, it is equivalent to s == status.A,
[s.B || s.C]: Logical or || in guard expression (see See Expressions),
on r2.world (): {}: A skip statement: upon receiving the r2.world trigger, the component does “nothing” and is ready for the next event. Omitting this line would make the occurrence of r2.world illegal.

Verification suceeds

$ dzn -v verify doc/examples/simple-state-machine.dzn
verify: ihello_bool: check: deadlock: ok
verify: ihello_bool: check: unreachable: ok
verify: ihello_bool: check: livelock: ok
verify: ihello_bool: check: deterministic: ok
verify: iworld: check: deadlock: ok
verify: iworld: check: unreachable: ok
verify: iworld: check: livelock: ok
verify: iworld: check: deterministic: ok
verify: simple_state_machine: check: deterministic: ok
verify: simple_state_machine: check: illegal: ok
verify: simple_state_machine: check: deadlock: ok
verify: simple_state_machine: check: unreachable: ok
verify: simple_state_machine: check: livelock: ok
verify: simple_state_machine: check: compliance: ok

you may want to see what happens to verification or the state diagram when you comment-out a statement of your choosing in the component’s behavior.

4.2 A Simple State Machine

Footnotes

(3)

(4)