specification leader_election [gInfo, gUpDown, gBusReset, gDM, gEvent] : noexit

library BOOLEAN, TYPES endlib

behaviour

LE [ gInfo, gUpDown, gBusReset, gDM, gEvent ]
   ( consnet( consn(false), consn(false)) ) (* all dcms down *)

where

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

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

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

    library BUS, CMM, DCM_SYNC endlib

    process OtherCommunications[ gDM ]
            ( Id: Nat ) 
      : noexit :=

        ( gDM ? j:Nat ? k:Nat ! DMInitRequest ? b:Bool
          [(j<>Id) and (j<>0) and (k<>Id) and (k<>0)] 
          ; OtherCommunications [gDM](Id))
        []
        ( gDM ? j:Nat ? k:Nat ! DMInitReply ? l:Nat
          [(j<>Id) and (j<>0) and (k<>Id) and (k<>0) and (l<>0)]
          ; OtherCommunications [gDM](Id))

    endproc (* OtherCommunications *)

endspec (* leader_election *)