
omod ELECTION is 
  including LF-REPR .
  protecting LF-VALUE-TIME .
  protecting RUNTIME-APG .

  ops id elected : -> RVarId [ctor] .
  ops node0 node1 node2 : -> ReactorId [ctor] .
  ops in out : -> RPortId [ctor] .
  ops startup a : -> RActionId [ctor] .
  op init : -> Configuration .

  eq init
   = < node0 : Reactor |
          inports : < in : Port | value : [0] >,
	      outports : < out : Port | value : [0] >,
	      state : (id |-> [0]) ; (elected |-> [0]),
	      timers : none,
	      actions : < a : LogicalAction | minDelay : 10, 
                                                    minSpacing : 0, 
                                                    policy : defer, 
                                                    payload : [0] >
                                                    
                    < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	      reactions :
	        (reaction when startup --> out do { (id := [0]); (out <- id)})
	        (reaction when a --> out do { out <- a })
             reaction when in --> a do {if (in > id) then schedule(a, [0], in) 
                else if (in === id) then elected := [1] fi fi} 
      >
            
      < node1 : Reactor |
          inports : < in : Port | value : [0] >,
	      outports : < out : Port | value : [0] >,
	      state : (id |-> [0]) ; (elected |-> [0]),
	      timers : none,
	      actions : < a : LogicalAction | minDelay : 10, 
                                                    minSpacing : 0, 
                                                    policy : defer, 
                                                    payload : [0] >
                                                    
                    < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	      reactions :
	        (reaction when startup --> out do { (id := [1]); (out <- id)})
	        (reaction when a --> out do { out <- a })
             reaction when in --> a do {if (in > id) then schedule(a, [0], in) 
                else if (in === id) then elected := [1] fi fi} 
      > 
            
      < node2 : Reactor |
          inports : < in : Port | value : [0] >,
	      outports : < out : Port | value : [0] >,
	      state : (id |-> [0]) ; (elected |-> [0]),
	      timers : none,
	      actions : < a : LogicalAction | minDelay : 10, 
                                                    minSpacing : 0, 
                                                    policy : defer, 
                                                    payload : [0] >
                                                    
                    < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	      reactions :
	        (reaction when startup --> out do { (id := [2]); (out <- id)})
	        (reaction when a --> out do { out <- a })
             reaction when in --> a do {if (in > id) then schedule(a, [0], in) 
                else if (in === id) then elected := [1] fi fi} 
      > 
      
      (node0 : out --> node1 : in)
      (node1 : out --> node2 : in)
       node2 : out --> node0 : in .
endom

omod TEST-ELECTION is
  including ELECTION .
  including DYNAMICS-WITHOUT-TICK .

  ops env queue rxns : -> Oid [ctor] .

  op initSystem : -> GlobalSystem .
  eq initSystem =
      {< env : Environment | physicalActions : none >
       addReactionIndices(init)
       < queue : EventQueue | queue : addStartup(startup, init, empty) >
       < rxns : Invoked | reactions : none >} .
endom


***( the main property in the LF repository is

spec="F[0, 20 msec]((Election_i0_elected + Election_i1_elected + Election_i2_elected) == 1)", expect=true

)***

---(
omod TIME-BOUNDED-ELECTION is
  including TEST-ELECTION .
  including TIME-BOUNDED-DYNAMICS .
  eq timeBound = 20 .
endom  

in model-checker.maude

omod MODEL-CHECK-ELECTION is
  including MODEL-CHECKER .
  including TIME-BOUNDED-ELECTION .
  subsort ClockedSystem < State .

  var REST : Configuration .
  vars N0 N1 N2 SUM : Nat .
  vars RS0 RS1 RS2 : ReactorState .
  var T : Time .

  op sumIs_ : Nat -> Prop [ctor] .
  eq {REST  < node0 : Reactor | state : (elected |-> [ N0 ]) ; RS0 >
            < node1 : Reactor | state : (elected |-> [ N1 ]) ; RS1 >
            < node2 : Reactor | state : (elected |-> [ N2 ]) ; RS2 >
      } in time T
      |= sumIs SUM = N0 + N1 + N2 == SUM .
endom

red modelCheck(initSystem in time 0, <> (sumIs 1)) .

***(    Result:
reduce in MODEL-CHECK-ELECTION : modelCheck(initSystem in time 0, <> sumIs 1) .
rewrites: 679 in 1ms cpu (0ms real) (679000 rewrites/second)
result Bool: true
)***
)---

omod MODEL-CHECK-ELECTION is
  including TEST-ELECTION .
  including LF-OUTPUT-COUNTEREXAMPLE .
  including LF-PROP-EXT .
  including MODEL-CHECKER .
endom

red modelCheck(initSystem timeBound 20, 
               <> ((((@ elected in node0) + (@ elected in node1)) + (@ elected in node2)) === @ [1])) .

red modelCheck(initSystem timeBound 20, 
               <> ((((@ elected in node0) + (@ elected in node1)) + (@ elected in node2)) === @ [10])) .
