
omod PIPE is 
  including LF-REPR .
  protecting LF-VALUE-TIME .

  ops value received count payload : -> RVarId [ctor] .
  ops source node1 node2 node3 node4 node5 sink : -> ReactorId [ctor] .
  ops in out : -> RPortId [ctor] .
  ops a sendOutput : -> RActionId [ctor] .
  op t : -> TimerId [ctor] .

  op init : -> Configuration .

  eq init
   = < source : Reactor | inports : none,
	  outports : < out : Port | value : [0] >,
	  state : value |-> [0],
	  timers : < t : Timer | offset : 0, period : 2 >,
	  actions : < a : LogicalAction | minDelay : 1, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when t --> a ; out do { (value := value + [1]) ; (out <- value) ; schedule(a,[0],[0])})
	     reaction when a --> out do { out <- value }
	>

    < node1 : Reactor | inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : (count |-> [0]) ; (payload |-> [0]),
	  timers : none,
	  actions : < sendOutput : LogicalAction | minDelay : 0, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when in --> sendOutput do { (payload := in) ; (count := count + [1]) ; schedule(sendOutput,[0],[0])})
	     reaction when sendOutput --> out do { (out <- payload) ; (count := count - [1]) }> 

    < node2 : Reactor | inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : (count |-> [0]) ; (payload |-> [0]),
	  timers : none,
	  actions : < sendOutput : LogicalAction | minDelay : 0, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when in --> sendOutput do { (payload := in) ; (count := count + [1]) ; schedule(sendOutput,[0],[0])})
	     reaction when sendOutput --> out do { (out <- payload) ; (count := count - [1]) }> 	 
	
    < node3 : Reactor | inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : (count |-> [0]) ; (payload |-> [0]),
	  timers : none,
	  actions : < sendOutput : LogicalAction | minDelay : 0, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when in --> sendOutput do { (payload := in) ; (count := count + [1]) ; schedule(sendOutput,[0],[0])})
	     reaction when sendOutput --> out do { (out <- payload) ; (count := count - [1]) }>      
	
    < node4 : Reactor | inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : (count |-> [0]) ; (payload |-> [0]),
	  timers : none,
	  actions : < sendOutput : LogicalAction | minDelay : 0, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when in --> sendOutput do { (payload := in) ; (count := count + [1]) ; schedule(sendOutput,[0],[0])})
	     reaction when sendOutput --> out do { (out <- payload) ; (count := count - [1]) }>      
	
    < node5 : Reactor | inports : < in : Port | value : [0] >,
	  outports : < out : Port | value : [0] >,
	  state : (count |-> [0]) ; (payload |-> [0]),
	  timers : none,
	  actions : < sendOutput : LogicalAction | minDelay : 0, 
                                      minSpacing : 0, 
                                      policy : defer, 
                                      payload : [0] >,
	  reactions : 
	    (reaction when in --> sendOutput do { (payload := in) ; (count := count + [1]) ; schedule(sendOutput,[0],[0])})
	     reaction when sendOutput --> out do { (out <- payload) ; (count := count - [1]) }> 
	     
	< sink : Reactor | inports : < in : Port | value : [0] >,
	  outports : none,
	  state : received |-> [0],
	  timers : none,
	  actions : none,
	  reactions : reaction when in do {received := in} > 
 
    (source : out --> node1 : in)
    (node1 : out --> node2 : in)
	(node2 : out --> node3 : in)
	(node3 : out --> node4 : in)
	(node4 : out --> node5 : in)
	 node5 : out --> sink : in .

endom

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

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

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

red initSystem .

omod TIME-BOUNDED-PIPE is
  including TEST-PIPE .
  including TIME-BOUNDED-DYNAMICS .
  eq timeBound = 1 .
endom  

rew initSystem in time 0 .


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

spec="G[0, 1 sec](!(Pipe_node1_count <= 1 && Pipe_node2_count <= 1 && Pipe_node3_count <= 1 && Pipe_node4_count <= 1 && Pipe_node5_count <= 1))", expect=false

)***



omod MODEL-CHECK-PIPE is
  including MODEL-CHECKER .
  including TIME-BOUNDED-PIPE .
  including LF-PROP .
endom


red modelCheck(initSystem in time 0, 
    [] (count in node1 <= [1] /\ count in node2 <= [1] /\ count in node3 <= [1] /\ count in node4 <= [1] /\ count in node5 <= [1])) .

***(  Result:
reduce in MODEL-CHECK-PIPE : modelCheck(initSystem in time 0, []countersLessThan 1) .
rewrites: 1466 in 1ms cpu (1ms real) (1466000 rewrites/second)
result Bool: true
)***

