agent App(send,recv,datum) = 'datum.'send.recv(x).[x=datum]datum.App(send,recv,datum) agent Phy(send,recv) = recv(x).'send.Phy(send,recv) agent Spec(datum) = (^ln1,ln2) (App(ln1,ln2,datum) | Phy(ln2,ln1)) agent ProtNodeActive(rcontrol,scontrol,recv,send) = recv(x).'send.ProtNodeActive(rcontrol,scontrol,recv,send) + 'rcontrol.ProtNodeSend(rcontrol,scontrol,send) + 'scontrol.ProtNodeRecv(rcontrol,scontrol,recv) agent ProtNodeSend(rcontrol,scontrol,send) = rcontrol(recv).ProtNodeActive(rcontrol,scontrol,recv,send) + 'scontrol.ProtNodeInactive(rcontrol,scontrol) agent ProtNodeRecv(rcontrol,scontrol,recv) = scontrol(send).ProtNodeActive(rcontrol,scontrol,recv,send) + 'rcontrol.ProtNodeInactive(rcontrol,scontrol) agent ProtNodeInactive(rcontrol,scontrol) = rcontrol(recv).ProtNodeRecv(rcontrol,scontrol,recv) + scontrol(send).ProtNodeSend(rcontrol,scontrol,send) agent Control(control1, control2, control3) = control1(ln).('control2.Control(control2,control1,control3) + 'control3.Control(control3,control2,control1)) agent System(datum) = (^ucontrol1,ucontrol2,ucontrol3,dcontrol1,dcontrol2,dcontrol3,ln1,ln2,ln3) (App(ln1,ln3, datum) | Phy(ln3,ln2) | Control(ucontrol1,ucontrol2,ucontrol3) | Control(dcontrol1,dcontrol2,dcontrol3) | ProtNodeActive(ucontrol1, dcontrol1, ln1, ln2) | ProtNodeInactive(ucontrol2, dcontrol2) | ProtNodeInactive(ucontrol3, dcontrol3))