specification leader_election [ginfo, gUpDown, gBusReset, gDMin, gDMout, gEvent] : noexit

library BOOLEAN, TYPES endlib

behaviour

LE [ ginfo, gUpDown, gBusReset, gDMin, gDMout, gEvent ]
   ( consnet(consn(false), consn(false)) ) (* all dcms down *)

where

    process LE [ gInfo, gUpDown, gBusReset, gDMin, gDMout, gEvent ]
               ( net:Network )
      : noexit :=

      ( BusReset[gUpDown,gBusReset,gEvent] (net)
      )

      |[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 *)
          )
        )
      )
    endproc (* LE *)

    library BUS, CMM, MS, DCM_ASYN endlib

endspec (* leader_election *)