MONTEREY PHOENIX model checker

In this blog post I discuss a model involving two actors: a car and a driver. Each actor has an associated set of actions they can take.

For a video walkthrough of this code, see https://youtu.be/r6aPKem6WLs

Using the web interface https://firebird.nps.edu/, run this model

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue */

/* with space as the separator, 
   the events (blue) are an ordered sequence */

ROOT Driver: enters_car 
             starts_car
             move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

Introduce branching logic

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

/* 
      ( A | B ) are alternative events 
*/

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

Events among actors are coordinated

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  move_forward turn_left turn_right 
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          move_forward
          turn_left
          turn_right
          shutting_down;

/* the two processes are related by specific events */

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;

Actors may take zero or more actions

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

/* 
    {* *} is an unordered set of zero or more events 
*/

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  {* ( move_forward | 
                  turn_left | 
                  turn_right ) *}
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          {* ( move_forward | 
               turn_left | 
               turn_right ) *}
          shutting_down;

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;

Events are shared among actors

SCHEMA using_a_car /* model title */

/* Actor Behaviors */

/* purple text is an MP keyword,
   actors are green text,
   atomic events are blue,
   composit events are orange */

ROOT Driver: enters_car (starts_car | exits_car);
starts_car:  {* ( move_forward | 
                  turn_left | 
                  turn_right ) *}
             stops_car
             exits_car;

ROOT Car: off
          starting 
          running_idle
          {* ( move_forward | 
               turn_left | 
               turn_right ) *}
          shutting_down;

Driver, Car SHARE ALL move_forward, 
                      turn_left, 
                      turn_right;

COORDINATE
$a: starts_car FROM Driver,
$b: starting FROM Car
DO
ADD $a PROCEEDS $b;
OD;

COORDINATE
$a: stops_car FROM Driver,
$b: shutting_down FROM Car
DO
ADD $a PROCEEDS $b;
OD;