ProtocolAnalysisExp1&2&3

exp1_stop_wait.pml

#define MAXSEQ 5  
mtype={Msg,Ack,Nak,Err,Mis};  
chan SenderToReceiver=[1] of {mtype,byte,byte};  
chan ReceiverToSender=[1] of {mtype,byte,byte};  
  
proctype SENDER(chan InCh,OutCh)  
{  
    byte SendData;  
    byte SendSeq;  
    byte ReceivedSeq;  
    SendData=MAXSEQ-1;  
    do  
        ::SendData=(SendData+1)%MAXSEQ;  
    again:  if //由于是随机选择执行, 所以多放置一些Msg提高命中概率  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Msg(SendData,SendSeq)  
            ::OutCh!Err(0,0)  
            ::OutCh!Mis(0,0)  
        fi;  
  
        if  
            ::timeout->  
                goto again  
            ::InCh?Mis(0,0)->  
                goto again  
            ::InCh?Err(0,0)->  
                goto again  
            ::InCh?Nak(ReceivedSeq,0)->  
                end1: goto again  
            ::InCh?Ack(ReceivedSeq,0)->  
                if  
                    ::(ReceivedSeq==SendSeq)->  
                        goto progress  
                    ::(ReceivedSeq!=SendSeq)->  
                        end2: goto again  
                fi  
        fi;  
    progress: SendSeq=1-SendSeq;  
    od;  
}  
  
proctype RECEIVER(chan InCh,OutCh)  
{  
    byte ReceivedData;  
    byte ReceivedSeq;  
    byte ExpectedData;  
    byte ExpectedSeq;  
  
    do  
        ::InCh?Msg(ReceivedData,ReceivedSeq)->  
            if  
                ::(ReceivedSeq==ExpectedSeq)->  
                    assert(ReceivedData==ExpectedData);  
                progress: ExpectedSeq=1-ExpectedSeq;  
                ExpectedData=(ExpectedData+1)%MAXSEQ;  
                if //由于是随机选择执行, 所以多放置一些Ack提高命中概率  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Ack(ReceivedSeq,0);  
                    ::OutCh!Err(0,0);  
                    ExpectedSeq=1-ExpectedSeq;  
                    ExpectedData=(ExpectedData+4)%MAXSEQ;  
                    ::OutCh!Mis(0,0);  
                    ExpectedSeq=1-ExpectedSeq;  
                    ExpectedData=(ExpectedData+4)%MAXSEQ;  
                fi  
  
                ::(ReceivedSeq!=ExpectedSeq)->  
                    if  
                        ::OutCh!Nak(ReceivedSeq,0);  
                        ::OutCh!Err(0,0);  
                    fi  
            fi  
        ::InCh?Err(0,0)->OutCh!Nak(ReceivedSeq,0);  
        ::InCh?Mis(0,0)->skip;  
    od;  
}  
  
init  
{  
    atomic //不可分割性  
    {  
        run SENDER(ReceiverToSender,SenderToReceiver);  
        run RECEIVER(SenderToReceiver,ReceiverToSender);  
    }  
}  

exp2_ab.pml

#define MAX 4                /* file ex.2 */  
proctype A(chan in, out)  
{   byte mt; /* message data */  
    bit  vr;  
S1: mt = (mt+1)%MAX;  
    out!mt,1;  
    goto S2;  
S2: in?vr;  
    if  
    :: (vr == 1) -> goto S1  
    :: (vr == 0) -> goto S3  
    :: printf("MSC: AERROR1\n") -> goto S5  
    fi;  
S3: out!mt,1;  
    goto S2;  
S4: in?vr;  
    if  
    :: goto S1  
    :: printf("MSC: AERROR2\n"); goto S5  
    fi;  
S5: out!mt,0;  
    goto S4  
}  
proctype B(chan in, out)  
{   byte mr, lmr;  
    bit ar;  
    goto S2; /* initial state */  
S1: assert(mr == (lmr+1)%MAX);  
    lmr = mr;  
    out!1;  
    goto S2;  
S2: in?mr,ar;  
    if  
    :: (ar == 1) -> goto S1  
    :: (ar == 0) -> goto S3  
    :: printf("MSC: ERROR1\n"); goto S5  
    fi;  
S3: out!1;  
    goto S2;  
S4: in?mr,ar;  
    if  
    :: goto S1  
    :: printf("MSC: ERROR2\n"); goto S5  
    fi;  
S5: out!0;  
    goto S4  
}  
init {  
    chan a2b = [2] of { bit };  
    chan b2a = [2] of { byte, bit };  
    atomic {  
        run A(a2b, b2a);  
        run B(b2a, a2b)  
    }  
}  

exp3_goback.pml

#define MaxSeq  3   /* window size */  
#define Wrong(x)    x = (x+1) % (MaxSeq)  
#define Right(x)    x = (x+1) % (MaxSeq + 1)  
#define inc(x)      Right(x)  
                                            /* file ex.9 */  
chan q[2] = [MaxSeq] of { byte, byte }; /* message passing channel */  
  
active [2] proctype p5()    /* starts two copies of proctype p5 */  
{   byte    NextFrame, AckExp, FrameExp, r, s, nbuf, i;  
    chan    in, out;  
    in  = q[_pid];  
    out = q[1-_pid];  
    xr in; xs out;      /* partial order reduction claims */  
  
    do  
    :: nbuf < MaxSeq ->   /* outgoing messages */  
        nbuf++;  
        out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);  
        inc(NextFrame)  
  
    :: q[_pid]?r,s ->    /* incoming messages */  
        if  
        :: r == FrameExp ->  
            printf("MSC: accept %d\n", r);  
            inc(FrameExp)  
        :: else /* ignore message */  
        fi;  
        do  
        :: ((AckExp <= s) && (s <  NextFrame))  
        :: ((AckExp <= s) && (NextFrame <  AckExp))  
        :: ((s <  NextFrame) && (NextFrame <  AckExp)) ->  
            nbuf--;  
            inc(AckExp)  
        :: else -> break  
        od  
  
    :: timeout ->        /* retransmission timeout */  
        NextFrame = AckExp;  
        printf("MSC: timeout\n");  
        i = 1;  
        do  
        :: i <= nbuf ->  
            out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);  
            inc(NextFrame);  
            i++  
        :: else -> break  
        od  
    od  
}