in dynamics

(tomod PINGPONG is 
  including RUNTIME-APG .

  ops pingsLeft count expected : -> IVarId [ctor] .
  ops ping pong : -> ReactorId [ctor] .
  ops receive send : -> IPortId [ctor] .
  ops startup serve : -> IActionId [ctor] .
  op init : -> Configuration .

  eq init
   = < ping : Reactor |
          inports : < receive : Port | value : [0] >,
	      outports : < send : Port | value : [0] >,
	      state : (pingsLeft |-> [10]),
	      timers : none,
	      actions : < serve : LogicalAction | minDelay : 1, 
                                                   minSpacing : 0, 
                                                   policy : defer, 
                                                   payload : [0] >
	                < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	      reactions :
	        (reaction when startup --> serve do { schedule(serve,[0],[0]) })
	        (reaction when serve --> send do { (send <- pingsLeft) ; (pingsLeft := pingsLeft - [1]) })
             reaction when receive --> serve do {if (pingsLeft > [0]) then schedule(serve,[0],[0]) fi} 
      >
            
      < pong : Reactor |
          inports : < receive : Port | value : [0] >,
	      outports : < send : Port | value : [0] >,
	      state : (count |-> [0]) ; (expected |-> [10]),
	      timers : none,
	      actions : < startup : LogicalAction | minDelay : 0, 
                                                minSpacing : 0, 
                                                policy : defer, 
                                                payload : [0] >,
	      reactions :
	        reaction when receive --> send do { (count := count + [1]); (send <- receive) } 
      > 
      
      (ping : send --> pong : receive)
       pong : send --> ping : receive .
endtom)

(tomod TEST-PINGPONG is
  including PINGPONG .
  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 >} .
endtom)

(tomod SIMULATE-PINGPONG is
  including TEST-PINGPONG .
  including SIMULATION-DYNAMICS .
endtom)

(rew initSystem .)

(search initSystem =>! GS:GlobalSystem .)    --- obvious trivial result

(tomod CHECK-PINGPONG is
  including TEST-PINGPONG .
  including TCTL-MODEL-CHECKER  .
  including UNBOUNDED-ANALYSIS-DYNAMICS .

  op reaction_invoked : ReactionId -> Prop [ctor] .

  var REST : Configuration .
  var RID : ReactionId .
  var RIDS : ReactionIdSet .
  var T : Time .
  var O : Oid .

  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}
     |=  reaction RID invoked = true .

  eq {REST}
     |=  reaction RID invoked = false [owise] .

  eq {REST
      < O : Invoked | reactions : (RID ; RIDS) >}  in time T
     |=  reaction RID invoked = true .

  eq {REST}  in time T
     |=  reaction RID invoked = false [owise] .

endtom)

(search initSystem =>* {none} .)

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

spec="G[0, 4 nsec](PingPong_ping_reaction_1 ==> X(!PingPong_ping_reaction_1))", expect=false

How do we express X?
should be done in rtm???


)***

