specification CO4System [user,up1,down1,up2,down2,up3,down3,signal,OK] : noexit

  library CO4_DATATYPES endlib
  library Boolean, NaturalNumber endlib

behaviour

(
  ( UserInput [user] [> exit )
  |[user]|
  KBHierarchy [user,up1,down1,up2,down2,up3,down3,signal]
)
>> Ring [OK]

where


  process KBHierarchy [user,up1,down1,up2,down2,up3,down3,signal] : exit :=
    (
      (
        (
  	(
  	  IdleIndividualKB [user,down1,up1,signal] (base1, some(base3))
  	  |||
  	  IdleIndividualKB [user,down1,up1,signal] (base2, some(base3))
  	)
  	|[user,down1,up1]|
  	SerializeIndividualKB [user,down1,up1]
        )
        |[up1,down1]|
        ( hide up in InitQueue [up1,up] |[up]|
          IdleGroupKB [up,down1,down2,up2,signal] (base3, some(base5),
            insert(base1, insert(base2, {}))) )
      )
      |||
      IdleIndividualKB [user,down2,up2,signal] (base4, some(base5))
    )
    |[up2,down2]|
    ( hide up in InitQueue [up2,up] |[up]|
      IdleGroupKB [up,down2,down3,up3,signal] (base5, none,
        insert(base3, insert(base4, {}))) )
    |[down3,up3]|
    exit (* base5 has no parent *)
  endproc


  process UserInput [user] : noexit :=
      user !base1 !doforward !reqachieve(assert(white) + <>);
      stop
      |||
      AllUserReply [user]
  endproc


  library CO4_PROCESSES endlib

endspec