% Data Transfer Protocol design in 1980's
% translated from the Promela version in the
% SPIN book (Holzmann, G., The SPIN Model Checker,
% Addison-Wesley, 2004), p.27.

{
 ch_m(empty), ch_w(empty), m, w.
 
 m :- m(s1).
 m(s1), ch_w(empty)  :- m(s2), ch_w(ini).
 m(s2), ch_m(ack)    :- m(s3), ch_m(empty).
 m(s3), timeout      :- m(s4).
 m(s4), ch_w(empty)  :- m(se), ch_w(shutup).
 m(s4), ch_w(empty)  :- m(s7), ch_w(dreq).
 m(s7), ch_m(data)   :- m(s8), ch_m(empty).
 m(s8), ch_w(empty)  :- m(s8), ch_w(data).
 m(s8), ch_w(empty)  :- m(se), ch_w(shutup).
 m(se), ch_m(shutup) :- m(sf), ch_m(empty).
 m(sf), ch_w(empty)  :- m(sg), ch_w(quiet).
 m(sg), ch_m(dead)   :- mEnd.
 
 w :- w(s1).
 w(s1), ch_w(ini)    :- w(s2), ch_w(empty).
 w(s2), ch_m(empty)  :- w(s3), ch_m(ack).
 w(s3), ch_w(dreq)   :- w(s5), ch_w(empty).
 w(s5), ch_m(empty)  :- w(s3), ch_m(data).
 w(s3), ch_w(data)   :- w(s3), ch_w(empty).
 w(s3), ch_w(shutup) :- w(s9), ch_w(empty).
 w(s9), ch_m(empty)  :- w(sc), ch_m(shutup).
 w(sc), ch_w(quiet)  :- w(sd), ch_w(empty).
 w(sd), ch_m(empty)  :- wEnd,  ch_m(dead).
}.
{$p,@p}/ :- \+($p=(mEnd,wEnd,$q)) | {timeout,$p,@p}.

% The original SPIN version
%   mtype = {ini,ack,dreq,data,shutup,quiet,dead};
%   chan M = [1] of { mtype };
%   chan W = [1] of { mtype };
%   active proctype Mproc () {
% /*s1*/     W!ini;
% /*s2*/     M?ack;
% /*s3*/     timeout ->
% /*s4*/     if
% /*s5*/     :: W!shutup
% /*s6*/     :: W!dreq;
% /*s7*/         M?data ->
% /*s8*/         do
% /*s9*/         :: W!data
% /*sa*/         :: W!shutup;
% /*sb*/              break
% /*sc*/         od
% /*sd*/     fi;
% /*se*/     M?shutup;
% /*sf*/     W!quiet;
% /*sg*/     M?dead;
%   }
%   active proctype Wproc () {
% /*s1*/     W?ini;
% /*s2*/     M!ack;
% /*s3*/     do
% /*s4*/     :: W?dreq ->
% /*s5*/         M!data
% /*s6*/     :: W?data ->
% /*s7*/         skip
% /*s8*/     :: W?shutup ->
% /*s9*/         M!shutup;
% /*sa*/         break
% /*sb*/     od;
% /*sc*/     W?quiet;
% /*sd*/     M!dead
%   }