agent AppSender(link,datum) = 'datum.'link<datum>.link(x).[x=datum]datum.AppSender(link,datum)

agent AppReceiver(link) = link(x).'link<x>.AppReceiver(link)

agent Spec(datum) = (^link) (AppSender(link,datum) | AppReceiver(link))

agent Phy(llink,rlink) = llink(x).'rlink<x>.Phy(llink,rlink) + rlink(x).'llink<x>.Phy(llink,rlink)

agent ProtNodeActive(ucontrol,dcontrol,ulink,dlink) = ulink(x).'dlink<x>.ProtNodeActive(ucontrol,dcontrol,ulink,dlink) + dlink(x).'ulink<x>.ProtNodeActive(ucontrol,dcontrol,ulink,dlink) + 'ucontrol<ulink>.ProtNodeOnlyDown(ucontrol,dcontrol,dlink) + 'dcontrol<dlink>.ProtNodeOnlyUp(ucontrol,dcontrol,ulink)

agent ProtNodeOnlyDown(ucontrol,dcontrol,dlink) = ucontrol(ulink).ProtNodeActive(ucontrol,dcontrol,ulink,dlink) + 'dcontrol<dlink>.ProtNodeInactive(ucontrol,dcontrol)

agent ProtNodeOnlyUp(ucontrol,dcontrol,ulink) = dcontrol(dlink).ProtNodeActive(ucontrol,dcontrol,ulink,dlink) + 'ucontrol<ulink>.ProtNodeInactive(ucontrol,dcontrol)

agent ProtNodeInactive(ucontrol,dcontrol) = dcontrol(dlink).ProtNodeOnlyDown(ucontrol,dcontrol,dlink) + ucontrol(ulink).ProtNodeOnlyUp(ucontrol,dcontrol,ulink)

agent Control(control1, control2) = control1(ln).'control2<ln>.control2(ln).'control1<ln>.Control(control1,control2)

agent System(datum) = (^ucontrol11,ucontrol12,ucontrol21,ucontrol22,dcontrol11,dcontrol12,dcontrol21,dcontrol22,link1,link2,link3,link4) (AppSender(link1,datum) | Control(ucontrol11,ucontrol12) | Control(dcontrol11,dcontrol12) | Control(ucontrol21,ucontrol22) | Control(dcontrol21,dcontrol22) | ProtNodeActive(ucontrol11,dcontrol11,link1,link2) | ProtNodeInactive(ucontrol12,dcontrol12) | Phy(link2,link3) | ProtNodeActive(ucontrol21,dcontrol21,link4,link3) | ProtNodeInactive(ucontrol22,dcontrol22) | AppReceiver(link4))

agent System'(datum) = (^ucontrol11,ucontrol12,dcontrol11,dcontrol12,link1,link2,link3) (AppSender(link1,datum) | Control(ucontrol11,ucontrol12) | Control(dcontrol11,dcontrol12) | ProtNodeActive(ucontrol11,dcontrol11,link1,link2) | ProtNodeInactive(ucontrol12,dcontrol12) | Phy(link2,link3) | AppReceiver(link3))