* Use abp to test logic bits & pieces
**********************************************************************
*  abp   (written by Rance Cleaveland)
*
*  This file contains a version of the Alternating Bit Protocol.
*
*  The specification of the protocol is represented by the agent
*  "Spec", and there are two implementations, "ABP-lossy", which
*  uses a lossy medium "Mlossy", and "ABP-safe, which uses a
*  reliable medum "Msafe".
*
*  "ABP-lossy" is correct in the sense that it is observationally
*  equivalent to "Spec", whereas "ABP-safe" is not. This can be
*  confirmed by analysing the deadlockability of "ABP-safe" in any
*  of the following ways:
*      - using the "find deadlocks" command to note that "ABP-safe"
*        may deadlock, whereas "ABP-lossy" cannot.
*      - using the "check proposition" command to note that
*        "ABP-lossy" can always either send or receive, whereas this
*        is not so for "ABP-safe". This is possible with either of
*        the following two propositions:
*                   #  Bx ((Can send) | (Can receive))
*                   #  Bx (<<send>>T | <<receive>>T)
*        The operators "Bx" and "Can" are defined below.
**********************************************************************
**********************************************************************
*  The definition of the specification "Spec"
**********************************************************************
agent Spec = send.receive.Spec;
**********************************************************************
*  The definition of the sender
**********************************************************************
agent S0 = send.S0';
agent S0' = 's0.(rack0.S1 + rack1.S0' + tau.S0');
agent S1 = send.S1';
agent S1' = 's1.(rack1.S0 + rack0.S1' + tau.S1');
**********************************************************************
*  The definition of the receiver
**********************************************************************
agent R0 = r0.receive.'sack0.R1 + r1.'sack1.R0 + tau.'sack1.R0;
agent R1 = r1.receive.'sack1.R0 + r0.'sack0.R1 + tau.'sack0.R1;
**********************************************************************
*  The definition of the reliable medium "Msafe"
**********************************************************************
agent Msafe = s0.'r0.Msafe + s1.'r1.Msafe + sack0.'rack0.Msafe + sack1.'rack1.Msafe;
**********************************************************************
*  The definition of the lossy medium "Mlossy"
**********************************************************************
agent Mlossy = s0.('r0.Mlossy + Mlossy) + s1.('r1.Mlossy + Mlossy) + sack0.('rack0.Mlossy + Mlossy) + sack1.('rack1.Mlossy + Mlossy);
**********************************************************************
*  The Internal actions to be hidden
**********************************************************************
set Internals = {r0,r1,s0,s1,rack0,rack1,sack0,sack1};
**********************************************************************
*  The definition of the safe implementation "ABP-safe"
**********************************************************************
agent Abp-safe = (R0 | Msafe | S0)\Internals;
**********************************************************************
*  The definition of the lossy implementation "ABP-lossy"
**********************************************************************
agent Abp-lossy = (R0 | Mlossy | S0)\Internals;
**********************************************************************
*  The definition of the "Can" temporal operator
**********************************************************************
prop Can(a) =      <<a>>T;
**********************************************************************
*  The definition of the "Bx" temporal operator
**********************************************************************
prop Bx(P) =      max(Z.P & [-]Z);
* May as well test pmi etc while we're here:
* prop Can;
* print ;
* * Now let's actually check some propositions:
* cp (Spec,Bx ((Can (send)) | (Can (receive))));
* cp (Abp-lossy,Bx ((Can (send)) | (Can (receive))));
* cp (Abp-safe,Bx ((Can (send)) | (Can (receive))));
* cp (Spec,Bx (<<send>>T | <<receive>>T));
* cp (Abp-lossy,Bx (<<send>>T | <<receive>>T));
* cp (Abp-safe,Bx (<<send>>T | <<receive>>T));
* fd Spec;
* fd Abp-safe;
* fd Abp-lossy;
* strongeq (Spec,Abp-lossy);
* strongeq (Spec,Abp-safe);
* strongeq (Abp-safe,Abp-lossy);
* eq (Spec,Abp-lossy);
* eq (Spec,Abp-safe);
* eq (Abp-safe,Abp-lossy);
* cong (Spec,Abp-lossy);
* cong (Spec,Abp-safe);
* cong (Abp-safe,Abp-lossy);
* mayeq (Spec,Abp-lossy);
* mayeq (Spec,Abp-safe);
* mayeq (Abp-safe,Abp-lossy);
* musteq (Spec,Abp-lossy);
* musteq (Spec,Abp-safe);
* musteq (Abp-safe,Abp-lossy);
* testeq (Spec,Abp-lossy);
* testeq (Spec,Abp-safe);
* testeq (Abp-safe,Abp-lossy);
* twothirdseq (Spec,Abp-lossy);
* twothirdseq (Spec,Abp-safe);
* twothirdseq (Abp-safe,Abp-lossy);
* dfstrong (Spec,Abp-lossy);
* dfstrong (Spec,Abp-safe);
* dfstrong (Abp-safe,Abp-lossy);
* dfweak (Spec,Abp-lossy);
* dfweak (Spec,Abp-safe);
* dfweak (Abp-safe,Abp-lossy);
* dftrace (Spec,Abp-lossy);
* dftrace (Spec,Abp-safe);
* dftrace (Abp-safe,Abp-lossy);