(* ------------------------------------------------------------------------- *)
(* Asynchronous version of the HAVi protocol                                 *)
(* ------------------------------------------------------------------------- *)

% DEFAULT_PROCESS_FILE="HAVi_asyn.lotos"

"HAVi_asyn.bcg" = root leaf strong reduction of
    (
        BusReset [gUpDown, gBusReset, gEvent]
                 (consnet (consn (false), consn (false))) (* all dcms down *)
        |[gUpDown, gBusReset]|
        (
            (
                DCM [gInfo, gUpDown, gDMin, gDMout, gEvent] (1)
                |||
                DCM [gInfo, gUpDown, gDMin, gDMout, gEvent] (2)
            )
            |[gInfo, gUpDown, gDMin, gDMout]|
            (
                (
                    CMM [gInfo, gUpDown, gBusReset] (1)
                    |[gBusReset]|
                    CMM [gInfo, gUpDown, gBusReset] (2)
                )
                |[gUpDown, gBusReset]|
                (
                    MS [gUpDown, gBusReset, gDMout, gDMin] (1)
                    (* DM's out is MS's in and vv *)
                    |[gBusReset]|
                    MS [gUpDown, gBusReset, gDMout, gDMin] (2)
                    (* DM's out is MS's in and vv *)
                )
            )
        )
    );

(* ------------------------------------------------------------------------- *)
(* Synchronous version of the HAVi protocol                                  *)
(* ------------------------------------------------------------------------- *)

% DEFAULT_PROCESS_FILE="HAVi_sync.lotos"

"HAVi_sync.bcg" = root leaf strong reduction of
    (
        BusReset [gUpDown, gBusReset, gEvent]
                 (consnet (consn (false), consn (false))) (* all dcms down *)
        |[gUpDown, gBusReset]|
        (
            (
                (
                    DCM [gInfo, gUpDown, gDM, gEvent] (1)
                    |||
                    OtherCommunications [gDM] (1)
                )
                |[gDM]|
                (
                    DCM [gInfo, gUpDown, gDM, gEvent] (2)
                    |||
                    OtherCommunications [gDM] (2)
                )
            )
            |[gInfo, gUpDown]|
            (
                CMM [gInfo, gUpDown, gBusReset] (1)
                |[gBusReset]|
                CMM [gInfo, gUpDown, gBusReset] (2)
            )
        )
    );

(* ------------------------------------------------------------------------- *)