MONTEREY PHOENIX grammar, keywords, and common patterns

MONTEREY PHOENIX grammar

In this table A is an event and B and C are events in A

description of pattern	grammar rule
Ordered sequence of events (B followed by C)	A: B C;
Alternative events (B or C)	A: ( B | C );
Optional event (B or no event at all)	A: [ B ];
Ordered sequence of zero or more events B	A: (* B *);
Ordered sequence of one or more events B	A: (+ B +);
Unordered set of events B and C (B and C may happen concurrently)	A: { B, C };
Unordered set of zero or more events B	A: {* B *};
Unordered set of one or more events B	A: {+ B +};

 

description of pattern	grammar rule
name of model	SCHEMA
Identifies an actor	ROOT
event precedence across swimlanes	COORDINATE
if and only if	<->
	<!>
a condition that each valid trace should satisfy	ENSURE
	FOREACH
	BUILD
	DISJ
	MARK
	ONFAIL
	CHECK
	AFTER
	EXISTS
	MAP
	CLEAR
	SHOW
message box that prints text	SAY("hello world")

Common pattern: branching logic in swimlane

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

Common pattern: dependency across swimlanes

COORDINATE
$a: turn_steering_wheel_right FROM driver,
$b: right FROM front_tires
DO 
ADD $a PRECEDES $b; 
OD;

Common pattern: shared events

Driver, Car SHARE ALL move_forward, 
                      turn_left, 
                      turn_right;

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;