process BusReset [ gUpDown, gBusReset , gEvent ]
        ( net: Network )

  : noexit :=
  
  gBusReset ! bus_reset_start 
  ; BusReset2[gUpDown,gBusReset,gEvent]
    (net,1)

  where

    process BusReset2 [ gUpDown, gBusReset, gEvent ]
            (net: Network, j:Nat)

      : noexit :=

    ( [j==0]
        -> ( gBusReset !  bus_reset_end ! net
             ; BusReset[gUpDown,gBusReset,gEvent](net)
           )
    )
    []
    ( [j<>0]
        -> ( ( gUpDown ! j ! power_change
               ; BusReset2[gUpDown,gBusReset,gEvent]
                 (flip(j,net),j+1)
             )
             []
             ( i
               ; BusReset2[gUpDown,gBusReset,gEvent]
                 (net,j+1)
             )
           )
    )
    endproc (* BusReset2 *)

endproc (* BusReset *)

process FlushBusReset[gBusReset]
  : noexit :=

  ( gBusReset ! bus_reset_start
    ; FlushBusReset[gBusReset] )
  []
  ( choice b1,b2:Bool
    [] ( gBusReset ! bus_reset_end ! consnet(consn(b1),consn(b2))
         ; FlushBusReset[gBusReset] ) )

endproc (* FlushBusReset *)