HOLD_PREVIOUS

TYPE
   T#SYSTEM#state: ENUM {ready,busy};

MODULE SYSTEM()
{
VAR
   request: BOOLEAN;
   state: T#SYSTEM#state;

       v#SYSTEM#state(state, request)

}

MODULE v#SYSTEM#state(state: T#SYSTEM#state, request: BOOLEAN)
{
VAR
   __init: BOOLEAN INITVAL TRUE;

TRANS T_state_0:
    enable:   __init;
    relation: (state'=ready) /\ !__init';

TRANS T_state_1:
    enable:   !__init /\ (state=ready /\ request);
    relation: state'=busy;

TRANS T_state_2:
    enable:   !__init /\ !(state=ready /\ request);
    relation: state'=ready \/ state'=busy;

}