+++ /dev/null
-# To unbundle, sh this file
-echo README 1>&2
-sed 's/.//' >README <<'//GO.SYSIN DD README'
--Readme
--------
--The files in this set contain the text of examples
--used in the Design and Validation of Computer
--Protocols book. The name of each file corresponds to the
--page number in the book where the example appears in its
--most useful version. The overview below gives a short
--descriptive phrase for each file.
--
--Description Page Nr = Filename
------------- ------------------
--hello world = p95.1
--tiny examples = p94 p95.2 p96.1 p97.1 p97.2 p101 p102 p104.1
--useful demos = p99 p104.2 p105.2 p116 p248
--mutual excl. = p96.2 p105.1 p117 p320
--Lynch's prot. = p107 p312
--alternatin bit = p123
--chappe's prot. = p319
--
--Large runs
------------
--ackerman's fct = p108 # read info at start of the file
--
--Pftp Protocol
---------------
--upper tester = p325.test # not runnable
--flow control l. = p329 p330
--session layer = p337.pftp.ses p342.pftp.ses1 p347.pftp.ses5
--all pftp = App.F.pftp - plus 8 include files
--
--See also the single file version of pftp in: Test/pftp
--
--General
---------
--Use these examples for inspiration, and to get quickly
--acquainted with the language and the Spin software.
--All examples - except p123 - can be used with both version
--1 and version 2 of SPIN. (p123 was modifed for versoin 2.0
--to use the new syntax for remote referencing).
--If you repeat the runs that are listed in the book for
--these examples, you should expect to get roughly the same
--numbers in the result - although in some cases there may
--be small differences that are due to changes in bookkeeping.
--
--For instance, for p329, the book (Spin V1.0) says
--on pg. 332, using a BITSTATE run, that there are:
-- 90845 + 317134 + 182425 states (stored + linked + matched)
--Spin V2.0 reports the numbers:
-- 90837 + 317122 + 182421 states (stored + atomic + matched)
--and when compiled for partial order reduction (-DREDUCE):
-- 74016 + 203616 + 104008 states (stored + atomic + matched)
--
--If you repeat a BITSTATE run, of course, by the nature of the
--machine dependent effect of hashing, you may get different
--coverage and hash-factors for larger runs. The implementation
--of the hash functions has also been improved in version 2.0,
--so the numbers you see will likely differ. The numbers, though,
--should still be in the same range as those reported in the book.
--
--The last set of file (prefixed App.F) is included for completeness.
--As explained in the book: don't expect to be able to do an
--exhaustive verification for this specification as listed.
--In chapter 14 it is illustrated how the spec can be broken up
--into smaller portions that are more easily verified.
--
--Some Small Experiments
-------------------------
--Try:
-- spin p95.1 # small simulation run
--
-- spin -s p108 # bigger simulation run, track send stmnts
--
-- spin -a p312 # lynch's protocol - generate verifier
-- cc -o pan pan.c # compile it for exhaustive verification
-- pan # prove correctness of assertions etc.
-- spin -t -r -s p312 # display the error trace
--
--now edit p312 to change all three channel declarations in init
--to look like: ``chan AtoB = [1] of { mtype byte }''
--and repeat the above four steps.
--note the improvement in the trace.
--
-- spin -a p123 # alternating bit protocol - generate verifier
-- cc -o pan pan.c # compile it for exhaustive verification
-- pan -a # check violations of the never claim
-- spin -t -r -s p123 # display the error trace
--
--for more intuitive use of all the above options: try using the
--graphical interface xspin, and repeat the experiments.
-//GO.SYSIN DD README
-echo App.F.datalink 1>&2
-sed 's/.//' >App.F.datalink <<'//GO.SYSIN DD App.F.datalink'
--/*
-- * Datalink Layer Validation Model
-- */
--
--proctype data_link()
--{ byte type, seq;
--
--end: do
-- :: flow_to_dll[0]?type,seq ->
-- if
-- :: dll_to_flow[1]!type,seq
-- :: skip /* lose message */
-- fi
-- :: flow_to_dll[1]?type,seq ->
-- if
-- :: dll_to_flow[0]!type,seq
-- :: skip /* lose message */
-- fi
-- od
--}
-//GO.SYSIN DD App.F.datalink
-echo App.F.defines 1>&2
-sed 's/.//' >App.F.defines <<'//GO.SYSIN DD App.F.defines'
--/*
-- * Global Definitions
-- */
--
--#define LOSS 0 /* message loss */
--#define DUPS 0 /* duplicate msgs */
--#define QSZ 2 /* queue size */
--
--mtype = {
-- red, white, blue,
-- abort, accept, ack, sync_ack, close, connect,
-- create, data, eof, open, reject, sync, transfer,
-- FATAL, NON_FATAL, COMPLETE
-- }
--
--chan use_to_pres[2] = [QSZ] of { byte };
--chan pres_to_use[2] = [QSZ] of { byte };
--chan pres_to_ses[2] = [QSZ] of { byte };
--chan ses_to_pres[2] = [QSZ] of { byte, byte };
--chan ses_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_ses[2] = [QSZ] of { byte, byte };
--chan dll_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_dll[2] = [QSZ] of { byte, byte };
--chan ses_to_fsrv[2] = [0] of { byte };
--chan fsrv_to_ses[2] = [0] of { byte };
-//GO.SYSIN DD App.F.defines
-echo App.F.flow_cl 1>&2
-sed 's/.//' >App.F.flow_cl <<'//GO.SYSIN DD App.F.flow_cl'
--/*
-- * Flow Control Layer Validation Model
-- */
--
--#define true 1
--#define false 0
--
--#define M 4 /* range sequence numbers */
--#define W 2 /* window size: M/2 */
--
--proctype fc(bit n)
--{ bool busy[M]; /* outstanding messages */
-- byte q; /* seq# oldest unacked msg */
-- byte m; /* seq# last msg received */
-- byte s; /* seq# next msg to send */
-- byte window; /* nr of outstanding msgs */
-- byte type; /* msg type */
-- bit received[M]; /* receiver housekeeping */
-- bit x; /* scratch variable */
-- byte p; /* seq# of last msg acked */
-- byte I_buf[M], O_buf[M]; /* message buffers */
--
-- /* sender part */
--end: do
-- :: atomic {
-- (window < W && len(ses_to_flow[n]) > 0
-- && len(flow_to_dll[n]) < QSZ) ->
-- ses_to_flow[n]?type,x;
-- window = window + 1;
-- busy[s] = true;
-- O_buf[s] = type;
-- flow_to_dll[n]!type,s;
-- if
-- :: (type != sync) ->
-- s = (s+1)%M
-- :: (type == sync) ->
-- window = 0;
-- s = M;
-- do
-- :: (s > 0) ->
-- s = s-1;
-- busy[s] = false
-- :: (s == 0) ->
-- break
-- od
-- fi
-- }
-- :: atomic {
-- (window > 0 && busy[q] == false) ->
-- window = window - 1;
-- q = (q+1)%M
-- }
--#if DUPS
-- :: atomic {
-- (len(flow_to_dll[n]) < QSZ
-- && window > 0 && busy[q] == true) ->
-- flow_to_dll[n]! O_buf[q],q
-- }
--#endif
-- :: atomic {
-- (timeout && len(flow_to_dll[n]) < QSZ
-- && window > 0 && busy[q] == true) ->
-- flow_to_dll[n]! O_buf[q],q
-- }
--
-- /* receiver part */
--#if LOSS
-- :: dll_to_flow[n]?type,m /* lose any message */
--#endif
-- :: dll_to_flow[n]?type,m ->
-- if
-- :: atomic {
-- (type == ack) ->
-- busy[m] = false
-- }
-- :: atomic {
-- (type == sync) ->
-- flow_to_dll[n]!sync_ack,m;
-- m = 0;
-- do
-- :: (m < M) ->
-- received[m] = 0;
-- m = m+1
-- :: (m == M) ->
-- break
-- od
-- }
-- :: (type == sync_ack) ->
-- flow_to_ses[n]!sync_ack,m
-- :: (type != ack && type != sync && type != sync_ack)->
-- if
-- :: atomic {
-- (received[m] == true) ->
-- x = ((0<p-m && p-m<=W)
-- || (0<p-m+M && p-m+M<=W)) };
-- if
-- :: (x) -> flow_to_dll[n]!ack,m
-- :: (!x) /* else skip */
-- fi
-- :: atomic {
-- (received[m] == false) ->
-- I_buf[m] = type;
-- received[m] = true;
-- received[(m-W+M)%M] = false
-- }
-- fi
-- fi
-- :: (received[p] == true && len(flow_to_ses[n])<QSZ
-- && len(flow_to_dll[n])<QSZ) ->
-- flow_to_ses[n]!I_buf[p],0;
-- flow_to_dll[n]!ack,p;
-- p = (p+1)%M
-- od
--}
-//GO.SYSIN DD App.F.flow_cl
-echo App.F.fserver 1>&2
-sed 's/.//' >App.F.fserver <<'//GO.SYSIN DD App.F.fserver'
--/*
-- * File Server Validation Model
-- */
--
--proctype fserver(bit n)
--{
--end: do
-- :: ses_to_fsrv[n]?create -> /* incoming */
-- if
-- :: fsrv_to_ses[n]!reject
-- :: fsrv_to_ses[n]!accept ->
-- do
-- :: ses_to_fsrv[n]?data
-- :: ses_to_fsrv[n]?eof -> break
-- :: ses_to_fsrv[n]?close -> break
-- od
-- fi
-- :: ses_to_fsrv[n]?open -> /* outgoing */
-- if
-- :: fsrv_to_ses[n]!reject
-- :: fsrv_to_ses[n]!accept ->
-- do
-- :: fsrv_to_ses[n]!data -> progress: skip
-- :: ses_to_fsrv[n]?close -> break
-- :: fsrv_to_ses[n]!eof -> break
-- od
-- fi
-- od
--}
-//GO.SYSIN DD App.F.fserver
-echo App.F.pftp 1>&2
-sed 's/.//' >App.F.pftp <<'//GO.SYSIN DD App.F.pftp'
--/*
-- * PROMELA Validation Model - startup script
-- */
--
--#include "App.F.defines"
--#include "App.F.user"
--#include "App.F.present"
--#include "App.F.session"
--#include "App.F.fserver"
--#include "App.F.flow_cl"
--#include "App.F.datalink"
--
--init
--{ atomic {
-- run userprc(0); run userprc(1);
-- run present(0); run present(1);
-- run session(0); run session(1);
-- run fserver(0); run fserver(1);
-- run fc(0); run fc(1);
-- run data_link()
-- }
--}
-//GO.SYSIN DD App.F.pftp
-echo App.F.present 1>&2
-sed 's/.//' >App.F.present <<'//GO.SYSIN DD App.F.present'
--/*
-- * Presentation Layer Validation Model
-- */
--
--proctype present(bit n)
--{ byte status, uabort;
--
--endIDLE:
-- do
-- :: use_to_pres[n]?transfer ->
-- uabort = 0;
-- break
-- :: use_to_pres[n]?abort ->
-- skip
-- od;
--
--TRANSFER:
-- pres_to_ses[n]!transfer;
-- do
-- :: use_to_pres[n]?abort ->
-- if
-- :: (!uabort) ->
-- uabort = 1;
-- pres_to_ses[n]!abort
-- :: (uabort) ->
-- assert(1+1!=2)
-- fi
-- :: ses_to_pres[n]?accept,0 ->
-- goto DONE
-- :: ses_to_pres[n]?reject(status) ->
-- if
-- :: (status == FATAL || uabort) ->
-- goto FAIL
-- :: (status == NON_FATAL && !uabort) ->
--progress: goto TRANSFER
-- fi
-- od;
--DONE:
-- pres_to_use[n]!accept;
-- goto endIDLE;
--FAIL:
-- pres_to_use[n]!reject;
-- goto endIDLE
--}
-//GO.SYSIN DD App.F.present
-echo App.F.session 1>&2
-sed 's/.//' >App.F.session <<'//GO.SYSIN DD App.F.session'
--/*
-- * Session Layer Validation Model
-- */
--
--proctype session(bit n)
--{ bit toggle;
-- byte type, status;
--
--endIDLE:
-- do
-- :: pres_to_ses[n]?type ->
-- if
-- :: (type == transfer) ->
-- goto DATA_OUT
-- :: (type != transfer) /* ignore */
-- fi
-- :: flow_to_ses[n]?type,0 ->
-- if
-- :: (type == connect) ->
-- goto DATA_IN
-- :: (type != connect) /* ignore */
-- fi
-- od;
--
--DATA_IN: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!create;
-- do
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_flow[n]!reject,0;
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- ses_to_flow[n]!accept,0;
-- break
-- od;
-- /* 2. Receive the data, upto eof */
-- do
-- :: flow_to_ses[n]?data,0 ->
-- ses_to_fsrv[n]!data
-- :: flow_to_ses[n]?eof,0 ->
-- ses_to_fsrv[n]!eof;
-- break
-- :: pres_to_ses[n]?transfer ->
-- ses_to_pres[n]!reject(NON_FATAL)
-- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
-- ses_to_fsrv[n]!close;
-- break
-- :: timeout -> /* got disconnected */
-- ses_to_fsrv[n]!close;
-- goto endIDLE
-- od;
-- /* 3. Close the connection */
-- ses_to_flow[n]!close,0;
-- goto endIDLE;
--
--DATA_OUT: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!open;
-- if
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- skip
-- fi;
-- /* 2. initialize flow control */
-- ses_to_flow[n]!sync,toggle;
-- do
-- :: atomic {
-- flow_to_ses[n]?sync_ack,type ->
-- if
-- :: (type != toggle)
-- :: (type == toggle) -> break
-- fi
-- }
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- od;
-- toggle = 1 - toggle;
-- /* 3. prepare remote file fsrver */
-- ses_to_flow[n]!connect,0;
-- if
-- :: flow_to_ses[n]?reject,0 ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?connect,0 ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(NON_FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?accept,0 ->
-- skip
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- fi;
-- /* 4. Transmit the data, upto eof */
-- do
-- :: fsrv_to_ses[n]?data ->
-- ses_to_flow[n]!data,0
-- :: fsrv_to_ses[n]?eof ->
-- ses_to_flow[n]!eof,0;
-- status = COMPLETE;
-- break
-- :: pres_to_ses[n]?abort -> /* local user aborted */
-- ses_to_fsrv[n]!close;
-- ses_to_flow[n]!close,0;
-- status = FATAL;
-- break
-- od;
-- /* 5. Close the connection */
-- do
-- :: pres_to_ses[n]?abort /* ignore */
-- :: flow_to_ses[n]?close,0 ->
-- if
-- :: (status == COMPLETE) ->
-- ses_to_pres[n]!accept,0
-- :: (status != COMPLETE) ->
-- ses_to_pres[n]!reject(status)
-- fi;
-- break
-- :: timeout ->
-- ses_to_pres[n]!reject(FATAL);
-- break
-- od;
-- goto endIDLE
--}
-//GO.SYSIN DD App.F.session
-echo App.F.user 1>&2
-sed 's/.//' >App.F.user <<'//GO.SYSIN DD App.F.user'
--/*
-- * User Layer Validation Model
-- */
--
--proctype userprc(bit n)
--{
-- use_to_pres[n]!transfer;
-- if
-- :: pres_to_use[n]?accept -> goto Done
-- :: pres_to_use[n]?reject -> goto Done
-- :: use_to_pres[n]!abort -> goto Aborted
-- fi;
--Aborted:
-- if
-- :: pres_to_use[n]?accept -> goto Done
-- :: pres_to_use[n]?reject -> goto Done
-- fi;
--Done:
-- skip
--}
-//GO.SYSIN DD App.F.user
-echo p101 1>&2
-sed 's/.//' >p101 <<'//GO.SYSIN DD p101'
--#define msgtype 33
--
--chan name = [0] of { byte, byte };
--
--/* byte name; typo - this line shouldn't have been here */
--
--proctype A()
--{ name!msgtype(124);
-- name!msgtype(121)
--}
--proctype B()
--{ byte state;
-- name?msgtype(state)
--}
--init
--{ atomic { run A(); run B() }
--}
-//GO.SYSIN DD p101
-echo p102 1>&2
-sed 's/.//' >p102 <<'//GO.SYSIN DD p102'
--#define a 1
--#define b 2
--
--chan ch = [1] of { byte };
--
--proctype A() { ch!a }
--proctype B() { ch!b }
--proctype C()
--{ if
-- :: ch?a
-- :: ch?b
-- fi
--}
--init { atomic { run A(); run B(); run C() } }
-//GO.SYSIN DD p102
-echo p104.1 1>&2
-sed 's/.//' >p104.1 <<'//GO.SYSIN DD p104.1'
--#define N 128
--#define size 16
--
--chan in = [size] of { short };
--chan large = [size] of { short };
--chan small = [size] of { short };
--
--proctype split()
--{ short cargo;
--
-- do
-- :: in?cargo ->
-- if
-- :: (cargo >= N) -> large!cargo
-- :: (cargo < N) -> small!cargo
-- fi
-- od
--}
--init { run split() }
-//GO.SYSIN DD p104.1
-echo p104.2 1>&2
-sed 's/.//' >p104.2 <<'//GO.SYSIN DD p104.2'
--#define N 128
--#define size 16
--
--chan in = [size] of { short };
--chan large = [size] of { short };
--chan small = [size] of { short };
--
--proctype split()
--{ short cargo;
--
-- do
-- :: in?cargo ->
-- if
-- :: (cargo >= N) -> large!cargo
-- :: (cargo < N) -> small!cargo
-- fi
-- od
--}
--proctype merge()
--{ short cargo;
--
-- do
-- :: if
-- :: large?cargo
-- :: small?cargo
-- fi;
-- in!cargo
-- od
--}
--init
--{ in!345; in!12; in!6777; in!32; in!0;
-- run split(); run merge()
--}
-//GO.SYSIN DD p104.2
-echo p105.1 1>&2
-sed 's/.//' >p105.1 <<'//GO.SYSIN DD p105.1'
--#define p 0
--#define v 1
--
--chan sema = [0] of { bit };
--
--proctype dijkstra()
--{ do
-- :: sema!p -> sema?v
-- od
--}
--proctype user()
--{ sema?p;
-- /* critical section */
-- sema!v
-- /* non-critical section */
--}
--init
--{ atomic {
-- run dijkstra();
-- run user(); run user(); run user()
-- }
--}
-//GO.SYSIN DD p105.1
-echo p105.2 1>&2
-sed 's/.//' >p105.2 <<'//GO.SYSIN DD p105.2'
--proctype fact(int n; chan p)
--{ int result;
--
-- if
-- :: (n <= 1) -> p!1
-- :: (n >= 2) ->
-- chan child = [1] of { int };
-- run fact(n-1, child);
-- child?result;
-- p!n*result
-- fi
--}
--init
--{ int result;
-- chan child = [1] of { int };
--
-- run fact(7, child);
-- child?result;
-- printf("result: %d\n", result)
--}
-//GO.SYSIN DD p105.2
-echo p107 1>&2
-sed 's/.//' >p107 <<'//GO.SYSIN DD p107'
--mtype = { ack, nak, err, next, accept }
--
--proctype transfer(chan in, out, chin, chout)
--{ byte o, i;
--
-- in?next(o);
-- do
-- :: chin?nak(i) -> out!accept(i); chout!ack(o)
-- :: chin?ack(i) -> out!accept(i); in?next(o); chout!ack(o)
-- :: chin?err(i) -> chout!nak(o)
-- od
--}
--init
--{ chan AtoB = [1] of { byte, byte };
-- chan BtoA = [1] of { byte, byte };
-- chan Ain = [2] of { byte, byte };
-- chan Bin = [2] of { byte, byte };
-- chan Aout = [2] of { byte, byte };
-- chan Bout = [2] of { byte, byte };
--
-- atomic {
-- run transfer(Ain, Aout, AtoB, BtoA);
-- run transfer(Bin, Bout, BtoA, AtoB)
-- };
-- AtoB!err(0)
--}
-//GO.SYSIN DD p107
-echo p108 1>&2
-sed 's/.//' >p108 <<'//GO.SYSIN DD p108'
--/***** Ackermann's function *****/
--
--/* a good example where a simulation run is the
-- better choice - and verification is overkill.
--
-- 1. simulation
-- -> straight simulation (spin p108) takes
-- -> approx. 6.4 sec on an SGI R3000
-- -> prints the answer: ack(3,3) = 61
-- -> after creating 2433 processes
--
-- note: all process invocations can, at least in one
-- feasible execution scenario, overlap - if each
-- process chooses to hang around indefinitely in
-- its dying state, at the closing curly brace.
-- this means that the maximum state vector `could' grow
-- to hold all 2433 processes or about 2433*12 bytes of data.
-- the assert(0) at the end makes sure though that the run
-- stops the first time we complete an execution sequence
-- that computes the answer, so the following suffices:
--
-- 2. verification
-- -> spin -a p108
-- -> cc -DVECTORSZ=2048 -o pan pan.c
-- -> pan -m15000
-- -> which completes in about 5 sec
-- */
--
--proctype ack(short a, b; chan ch1)
--{ chan ch2 = [1] of { short };
-- short ans;
--
-- if
-- :: (a == 0) ->
-- ans = b+1
-- :: (a != 0) ->
-- if
-- :: (b == 0) ->
-- run ack(a-1, 1, ch2)
-- :: (b != 0) ->
-- run ack(a, b-1, ch2);
-- ch2?ans;
-- run ack(a-1, ans, ch2)
-- fi;
-- ch2?ans
-- fi;
-- ch1!ans
--}
--init
--{ chan ch = [1] of { short };
-- short ans;
--
-- run ack(3, 3, ch);
-- ch?ans;
-- printf("ack(3,3) = %d\n", ans);
-- assert(0) /* a forced stop, (Chapter 6) */
--}
-//GO.SYSIN DD p108
-echo p116 1>&2
-sed 's/.//' >p116 <<'//GO.SYSIN DD p116'
--byte state = 1;
--
--proctype A()
--{ (state == 1) -> state = state + 1;
-- assert(state == 2)
--}
--proctype B()
--{ (state == 1) -> state = state - 1;
-- assert(state == 0)
--}
--init { run A(); run B() }
-//GO.SYSIN DD p116
-echo p117 1>&2
-sed 's/.//' >p117 <<'//GO.SYSIN DD p117'
--#define p 0
--#define v 1
--
--chan sema = [0] of { bit }; /* typo in original `=' was missing */
--
--proctype dijkstra()
--{ do
-- :: sema!p -> sema?v
-- od
--}
--byte count;
--
--proctype user()
--{ sema?p;
-- count = count+1;
-- skip; /* critical section */
-- count = count-1;
-- sema!v;
-- skip /* non-critical section */
--}
--proctype monitor() { assert(count == 0 || count == 1) }
--init
--{ atomic {
-- run dijkstra(); run monitor();
-- run user(); run user(); run user()
-- }
--}
-//GO.SYSIN DD p117
-echo p123 1>&2
-sed 's/.//' >p123 <<'//GO.SYSIN DD p123'
--/* alternating bit - version with message loss */
--
--#define MAX 3
--
--mtype = { msg0, msg1, ack0, ack1 };
--
--chan sender =[1] of { byte };
--chan receiver=[1] of { byte };
--
--proctype Sender()
--{ byte any;
--again:
-- do
-- :: receiver!msg1;
-- if
-- :: sender?ack1 -> break
-- :: sender?any /* lost */
-- :: timeout /* retransmit */
-- fi
-- od;
-- do
-- :: receiver!msg0;
-- if
-- :: sender?ack0 -> break
-- :: sender?any /* lost */
-- :: timeout /* retransmit */
-- fi
-- od;
-- goto again
--}
--
--proctype Receiver()
--{ byte any;
--again:
-- do
-- :: receiver?msg1 -> sender!ack1; break
-- :: receiver?msg0 -> sender!ack0
-- :: receiver?any /* lost */
-- od;
--P0:
-- do
-- :: receiver?msg0 -> sender!ack0; break
-- :: receiver?msg1 -> sender!ack1
-- :: receiver?any /* lost */
-- od;
--P1:
-- goto again
--}
--
--init { atomic { run Sender(); run Receiver() } }
--
--never {
-- do
-- :: skip /* allow any time delay */
-- :: receiver?[msg0] -> goto accept0
-- :: receiver?[msg1] -> goto accept1
-- od;
--accept0:
-- do
-- :: !Receiver[2]@P0 /* n.b. new syntax of remote reference */
-- od;
--accept1:
-- do
-- :: !Receiver[2]@P1
-- od
--}
-//GO.SYSIN DD p123
-echo p248 1>&2
-sed 's/.//' >p248 <<'//GO.SYSIN DD p248'
--proctype fact(int n; chan p)
--{ int result;
--
-- if
-- :: (n <= 1) -> p!1
-- :: (n >= 2) ->
-- chan child = [1] of { int };
-- run fact(n-1, child);
-- child?result;
-- p!n*result
-- fi
--}
--init
--{ int result;
-- chan child = [1] of { int };
--
-- run fact(12, child);
-- child?result;
-- printf("result: %d\n", result)
--}
-//GO.SYSIN DD p248
-echo p312 1>&2
-sed 's/.//' >p312 <<'//GO.SYSIN DD p312'
--#define MIN 9 /* first data message to send */
--#define MAX 12 /* last data message to send */
--#define FILL 99 /* filler message */
--
--mtype = { ack, nak, err }
--
--proctype transfer(chan chin, chout)
--{ byte o, i, last_i=MIN;
--
-- o = MIN+1;
-- do
-- :: chin?nak(i) ->
-- assert(i == last_i+1);
-- chout!ack(o)
-- :: chin?ack(i) ->
-- if
-- :: (o < MAX) -> o = o+1 /* next */
-- :: (o >= MAX) -> o = FILL /* done */
-- fi;
-- chout!ack(o)
-- :: chin?err(i) ->
-- chout!nak(o)
-- od
--}
--
--proctype channel(chan in, out)
--{ byte md, mt;
-- do
-- :: in?mt,md ->
-- if
-- :: out!mt,md
-- :: out!err,0
-- fi
-- od
--}
--
--init
--{ chan AtoB = [1] of { byte, byte };
-- chan BtoC = [1] of { byte, byte };
-- chan CtoA = [1] of { byte, byte };
-- atomic {
-- run transfer(AtoB, BtoC);
-- run channel(BtoC, CtoA);
-- run transfer(CtoA, AtoB)
-- };
-- AtoB!err,0 /* start */
--}
-//GO.SYSIN DD p312
-echo p319 1>&2
-sed 's/.//' >p319 <<'//GO.SYSIN DD p319'
--#define true 1
--#define false 0
--
--bool busy[3];
--
--chan up[3] = [1] of { byte };
--chan down[3] = [1] of { byte };
--
--mtype = { start, attention, data, stop }
--
--proctype station(byte id; chan in, out)
--{ do
-- :: in?start ->
-- atomic { !busy[id] -> busy[id] = true };
-- out!attention;
-- do
-- :: in?data -> out!data
-- :: in?stop -> break
-- od;
-- out!stop;
-- busy[id] = false
-- :: atomic { !busy[id] -> busy[id] = true };
-- out!start;
-- in?attention;
-- do
-- :: out!data -> in?data
-- :: out!stop -> break
-- od;
-- in?stop;
-- busy[id] = false
-- od
--}
--
--init {
-- atomic {
-- run station(0, up[2], down[2]);
-- run station(1, up[0], down[0]);
-- run station(2, up[1], down[1]);
--
-- run station(0, down[0], up[0]);
-- run station(1, down[1], up[1]);
-- run station(2, down[2], up[2])
-- }
--}
-//GO.SYSIN DD p319
-echo p320 1>&2
-sed 's/.//' >p320 <<'//GO.SYSIN DD p320'
--#define true 1
--#define false 0
--#define Aturn false
--#define Bturn true
--
--bool x, y, t;
--bool ain, bin;
--
--proctype A()
--{ x = true;
-- t = Bturn;
-- (y == false || t == Aturn);
-- ain = true;
-- assert(bin == false); /* critical section */
-- ain = false;
-- x = false
--}
--
--proctype B()
--{ y = true;
-- t = Aturn;
-- (x == false || t == Bturn);
-- bin = true;
-- assert(ain == false); /* critical section */
-- bin = false;
-- y = false
--}
--
--init
--{ run A(); run B()
--}
-//GO.SYSIN DD p320
-echo p325.test 1>&2
-sed 's/.//' >p325.test <<'//GO.SYSIN DD p325.test'
--proctype test_sender(bit n)
--{ byte type, toggle;
--
-- ses_to_flow[n]!sync,toggle;
-- do
-- :: flow_to_ses[n]?sync_ack,type ->
-- if
-- :: (type != toggle)
-- :: (type == toggle) -> break
-- fi
-- :: timeout ->
-- ses_to_flow[n]!sync,toggle
-- od;
-- toggle = 1 - toggle;
--
-- do
-- :: ses_to_flow[n]!data,white
-- :: ses_to_flow[n]!data,red -> break
-- od;
-- do
-- :: ses_to_flow[n]!data,white
-- :: ses_to_flow[n]!data,blue -> break
-- od;
-- do
-- :: ses_to_flow[n]!data,white
-- :: break
-- od
--}
--proctype test_receiver(bit n)
--{
-- do
-- :: flow_to_ses[n]?data,white
-- :: flow_to_ses[n]?data,red -> break
-- od;
-- do
-- :: flow_to_ses[n]?data,white
-- :: flow_to_ses[n]?data,blue -> break
-- od;
--end: do
-- :: flow_to_ses[n]?data,white
-- od
--}
-//GO.SYSIN DD p325.test
-echo p327.upper 1>&2
-sed 's/.//' >p327.upper <<'//GO.SYSIN DD p327.upper'
--proctype upper()
--{ byte s_state, r_state;
-- byte type, toggle;
--
-- ses_to_flow[0]!sync,toggle;
-- do
-- :: flow_to_ses[0]?sync_ack,type ->
-- if
-- :: (type != toggle)
-- :: (type == toggle) -> break
-- fi
-- :: timeout ->
-- ses_to_flow[0]!sync,toggle
-- od;
-- toggle = 1 - toggle;
--
-- do
-- /* sender */
-- :: ses_to_flow[0]!white,0
-- :: atomic {
-- (s_state == 0 && len (ses_to_flow[0]) < QSZ) ->
-- ses_to_flow[0]!red,0 ->
-- s_state = 1
-- }
-- :: atomic {
-- (s_state == 1 && len (ses_to_flow[0]) < QSZ) ->
-- ses_to_flow[0]!blue,0 ->
-- s_state = 2
-- }
-- /* receiver */
-- :: flow_to_ses[1]?white,0
-- :: atomic {
-- (r_state == 0 && flow_to_ses[1]?[red]) ->
-- flow_to_ses[1]?red,0 ->
-- r_state = 1
-- }
-- :: atomic {
-- (r_state == 0 && flow_to_ses[1]?[blue]) ->
-- assert(0)
-- }
-- :: atomic {
-- (r_state == 1 && flow_to_ses[1]?[blue]) ->
-- flow_to_ses[1]?blue,0;
-- break
-- }
-- :: atomic {
-- (r_state == 1 && flow_to_ses[1]?[red]) ->
-- assert(0)
-- }
-- od;
--end:
-- do
-- :: flow_to_ses[1]?white,0
-- :: flow_to_ses[1]?red,0 -> assert(0)
-- :: flow_to_ses[1]?blue,0 -> assert(0)
-- od
--}
-//GO.SYSIN DD p327.upper
-echo p329 1>&2
-sed 's/.//' >p329 <<'//GO.SYSIN DD p329'
--/*
-- * PROMELA Validation Model
-- * FLOW CONTROL LAYER VALIDATION
-- */
--
--#define LOSS 0 /* message loss */
--#define DUPS 0 /* duplicate msgs */
--#define QSZ 2 /* queue size */
--
--mtype = {
-- red, white, blue,
-- abort, accept, ack, sync_ack, close, connect,
-- create, data, eof, open, reject, sync, transfer,
-- FATAL, NON_FATAL, COMPLETE
-- }
--
--chan ses_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_ses[2] = [QSZ] of { byte, byte };
--chan dll_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_dll[2];
--
--#include "App.F.flow_cl"
--#include "p327.upper"
--
--init
--{
-- atomic {
-- flow_to_dll[0] = dll_to_flow[1];
-- flow_to_dll[1] = dll_to_flow[0];
-- run fc(0); run fc(1);
-- run upper()
-- }
--}
-//GO.SYSIN DD p329
-echo p330 1>&2
-sed 's/.//' >p330 <<'//GO.SYSIN DD p330'
--/*
-- * PROMELA Validation Model
-- * FLOW CONTROL LAYER VALIDATION
-- */
--
--#define LOSS 0 /* message loss */
--#define DUPS 0 /* duplicate msgs */
--#define QSZ 2 /* queue size */
--
--mtype = {
-- red, white, blue,
-- abort, accept, ack, sync_ack, close, connect,
-- create, data, eof, open, reject, sync, transfer,
-- FATAL, NON_FATAL, COMPLETE
-- }
--
--chan ses_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_ses[2] = [QSZ] of { byte, byte };
--chan dll_to_flow[2] = [QSZ] of { byte, byte };
--chan flow_to_dll[2];
--
--#include "App.F.flow_cl"
--#include "p327.upper"
--
--init
--{
-- atomic {
-- flow_to_dll[0] = dll_to_flow[1];
-- flow_to_dll[1] = dll_to_flow[0];
-- run fc(0); run fc(1);
-- run upper()
-- }
--}
-//GO.SYSIN DD p330
-echo p337.defines2 1>&2
-sed 's/.//' >p337.defines2 <<'//GO.SYSIN DD p337.defines2'
--/*
-- * PROMELA Validation Model
-- * global definitions
-- */
--
--#define QSZ 2 /* queue size */
--
--mtype = {
-- red, white, blue,
-- abort, accept, ack, sync_ack, close, connect,
-- create, data, eof, open, reject, sync, transfer,
-- FATAL, NON_FATAL, COMPLETE
-- }
--
--chan use_to_pres[2] = [QSZ] of { mtype };
--chan pres_to_use[2] = [QSZ] of { mtype };
--chan pres_to_ses[2] = [QSZ] of { mtype };
--chan ses_to_pres[2] = [QSZ] of { mtype, byte };
--chan ses_to_flow[2] = [QSZ] of { mtype, byte };
--chan ses_to_fsrv[2] = [0] of { mtype };
--chan fsrv_to_ses[2] = [0] of { mtype };
--chan flow_to_ses[2];
-//GO.SYSIN DD p337.defines2
-echo p337.fserver 1>&2
-sed 's/.//' >p337.fserver <<'//GO.SYSIN DD p337.fserver'
--/*
-- * File Server Validation Model
-- */
--
--proctype fserver(bit n)
--{
--end: do
-- :: ses_to_fsrv[n]?create -> /* incoming */
-- if
-- :: fsrv_to_ses[n]!reject
-- :: fsrv_to_ses[n]!accept ->
-- do
-- :: ses_to_fsrv[n]?data
-- :: ses_to_fsrv[n]?eof -> break
-- :: ses_to_fsrv[n]?close -> break
-- od
-- fi
-- :: ses_to_fsrv[n]?open -> /* outgoing */
-- if
-- :: fsrv_to_ses[n]!reject
-- :: fsrv_to_ses[n]!accept ->
-- do
-- :: fsrv_to_ses[n]!data -> progress: skip
-- :: ses_to_fsrv[n]?close -> break
-- :: fsrv_to_ses[n]!eof -> break
-- od
-- fi
-- od
--}
-//GO.SYSIN DD p337.fserver
-echo p337.pftp.ses 1>&2
-sed 's/.//' >p337.pftp.ses <<'//GO.SYSIN DD p337.pftp.ses'
--/*
-- * PROMELA Validation Model
-- * Session Layer
-- */
--
--#include "p337.defines2"
--#include "p337.user"
--#include "App.F.present"
--#include "p337.session"
--#include "p337.fserver"
--
--init
--{ atomic {
-- run userprc(0); run userprc(1);
-- run present(0); run present(1);
-- run session(0); run session(1);
-- run fserver(0); run fserver(1);
-- flow_to_ses[0] = ses_to_flow[1];
-- flow_to_ses[1] = ses_to_flow[0]
-- }
--}
-//GO.SYSIN DD p337.pftp.ses
-echo p337.session 1>&2
-sed 's/.//' >p337.session <<'//GO.SYSIN DD p337.session'
--/*
-- * Session Layer Validation Model
-- */
--
--proctype session(bit n)
--{ bit toggle;
-- byte type, status;
--
--endIDLE:
-- do
-- :: pres_to_ses[n]?type ->
-- if
-- :: (type == transfer) ->
-- goto DATA_OUT
-- :: (type != transfer) /* ignore */
-- fi
-- :: flow_to_ses[n]?type,0 ->
-- if
-- :: (type == connect) ->
-- goto DATA_IN
-- :: (type != connect) /* ignore */
-- fi
-- od;
--
--DATA_IN: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!create;
-- do
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_flow[n]!reject,0;
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- ses_to_flow[n]!accept,0;
-- break
-- od;
-- /* 2. Receive the data, upto eof */
-- do
-- :: flow_to_ses[n]?data,0 ->
-- ses_to_fsrv[n]!data
-- :: flow_to_ses[n]?eof,0 ->
-- ses_to_fsrv[n]!eof;
-- break
-- :: pres_to_ses[n]?transfer ->
-- ses_to_pres[n]!reject(NON_FATAL)
-- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
-- ses_to_fsrv[n]!close;
-- break
-- :: timeout -> /* got disconnected */
-- ses_to_fsrv[n]!close;
-- goto endIDLE
-- od;
-- /* 3. Close the connection */
-- ses_to_flow[n]!close,0;
-- goto endIDLE;
--
--DATA_OUT: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!open;
-- if
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- skip
-- fi;
-- /* 2. initialize flow control *** disabled
-- ses_to_flow[n]!sync,toggle;
-- do
-- :: atomic {
-- flow_to_ses[n]?sync_ack,type ->
-- if
-- :: (type != toggle)
-- :: (type == toggle) -> break
-- fi
-- }
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- od;
-- toggle = 1 - toggle;
-- /* 3. prepare remote file fsrver */
-- ses_to_flow[n]!connect,0;
-- if
-- :: flow_to_ses[n]?reject,0 ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?connect,0 ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(NON_FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?accept,0 ->
-- skip
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- fi;
-- /* 4. Transmit the data, upto eof */
-- do
-- :: fsrv_to_ses[n]?data ->
-- ses_to_flow[n]!data,0
-- :: fsrv_to_ses[n]?eof ->
-- ses_to_flow[n]!eof,0;
-- status = COMPLETE;
-- break
-- :: pres_to_ses[n]?abort -> /* local user aborted */
-- ses_to_fsrv[n]!close;
-- ses_to_flow[n]!close,0;
-- status = FATAL;
-- break
-- od;
-- /* 5. Close the connection */
-- do
-- :: pres_to_ses[n]?abort /* ignore */
-- :: flow_to_ses[n]?close,0 ->
-- if
-- :: (status == COMPLETE) ->
-- ses_to_pres[n]!accept,0
-- :: (status != COMPLETE) ->
-- ses_to_pres[n]!reject(status)
-- fi;
-- break
-- :: timeout ->
-- ses_to_pres[n]!reject(FATAL);
-- break
-- od;
-- goto endIDLE
--}
-//GO.SYSIN DD p337.session
-echo p337.user 1>&2
-sed 's/.//' >p337.user <<'//GO.SYSIN DD p337.user'
--/*
-- * User Layer Validation Model
-- */
--
--proctype userprc(bit n)
--{
-- use_to_pres[n]!transfer;
-- if
-- :: pres_to_use[n]?accept -> goto Done
-- :: pres_to_use[n]?reject -> goto Done
-- :: use_to_pres[n]!abort -> goto Aborted
-- fi;
--Aborted:
-- if
-- :: pres_to_use[n]?accept -> goto Done
-- :: pres_to_use[n]?reject -> goto Done
-- fi;
--Done:
-- skip
--}
-//GO.SYSIN DD p337.user
-echo p342.pftp.ses1 1>&2
-sed 's/.//' >p342.pftp.ses1 <<'//GO.SYSIN DD p342.pftp.ses1'
--/*
-- * PROMELA Validation Model
-- * Session Layer
-- */
--
--#include "p337.defines2"
--#include "p337.user"
--#include "App.F.present"
--#include "p337.session"
--#include "p337.fserver"
--
--init
--{
-- atomic {
-- run userprc(0); run userprc(1);
-- run present(0); run present(1);
-- run session(0); run session(1);
-- run fserver(0); run fserver(1);
-- flow_to_ses[0] = ses_to_flow[1];
-- flow_to_ses[1] = ses_to_flow[0]
-- };
-- atomic {
-- byte any;
-- chan foo = [1] of { byte, byte };
-- ses_to_flow[0] = foo;
-- ses_to_flow[1] = foo
-- };
--end: do
-- :: foo?any,any
-- od
--}
-//GO.SYSIN DD p342.pftp.ses1
-echo p343.claim 1>&2
-sed 's/.//' >p343.claim <<'//GO.SYSIN DD p343.claim'
--never {
-- skip; /* match first step of init (spin version 2.0) */
-- do
-- :: !pres_to_ses[0]?[transfer]
-- && !flow_to_ses[0]?[connect]
-- :: pres_to_ses[0]?[transfer] ->
-- goto accept0
-- :: flow_to_ses[0]?[connect] ->
-- goto accept1
-- od;
--accept0:
-- do
-- :: !ses_to_pres[0]?[accept]
-- && !ses_to_pres[0]?[reject]
-- od;
--accept1:
-- do
-- :: !ses_to_pres[1]?[accept]
-- && !ses_to_pres[1]?[reject]
-- od
--}
-//GO.SYSIN DD p343.claim
-echo p347.pftp.ses5 1>&2
-sed 's/.//' >p347.pftp.ses5 <<'//GO.SYSIN DD p347.pftp.ses5'
--/*
-- * PROMELA Validation Model
-- * Session Layer
-- */
--
--#include "p337.defines2"
--#include "p347.pres.sim"
--#include "p347.session.prog"
--#include "p337.fserver"
--
--init
--{ atomic {
-- run present(0); run present(1);
-- run session(0); run session(1);
-- run fserver(0); run fserver(1);
-- flow_to_ses[0] = ses_to_flow[1];
-- flow_to_ses[1] = ses_to_flow[0]
-- }
--}
-//GO.SYSIN DD p347.pftp.ses5
-echo p347.pres.sim 1>&2
-sed 's/.//' >p347.pres.sim <<'//GO.SYSIN DD p347.pres.sim'
--/*
-- * PROMELA Validation Model
-- * Presentation & User Layer - combined and reduced
-- */
--
--proctype present(bit n)
--{ byte status;
--progress0:
-- pres_to_ses[n]!transfer ->
-- do
-- :: pres_to_ses[n]!abort;
--progress1: skip
-- :: ses_to_pres[n]?accept,status ->
-- break
-- :: ses_to_pres[n]?reject,status ->
-- if
-- :: (status == NON_FATAL) ->
-- goto progress0
-- :: (status != NON_FATAL) ->
-- break
-- fi
-- od
--}
-//GO.SYSIN DD p347.pres.sim
-echo p347.session.prog 1>&2
-sed 's/.//' >p347.session.prog <<'//GO.SYSIN DD p347.session.prog'
--/*
-- * Session Layer Validation Model
-- */
--
--proctype session(bit n)
--{ bit toggle;
-- byte type, status;
--
--endIDLE:
-- do
-- :: pres_to_ses[n]?type ->
-- if
-- :: (type == transfer) ->
-- goto progressDATA_OUT
-- :: (type != transfer) /* ignore */
-- fi
-- :: flow_to_ses[n]?type,0 ->
-- if
-- :: (type == connect) ->
-- goto progressDATA_IN
-- :: (type != connect) /* ignore */
-- fi
-- od;
--
--progressDATA_IN: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!create;
-- do
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_flow[n]!reject,0;
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- ses_to_flow[n]!accept,0;
-- break
-- od;
-- /* 2. Receive the data, upto eof */
-- do
-- :: flow_to_ses[n]?data,0 ->
--progress: ses_to_fsrv[n]!data
-- :: flow_to_ses[n]?eof,0 ->
-- ses_to_fsrv[n]!eof;
-- break
-- :: pres_to_ses[n]?transfer ->
-- ses_to_pres[n]!reject(NON_FATAL)
-- :: flow_to_ses[n]?close,0 -> /* remote user aborted */
-- ses_to_fsrv[n]!close;
-- break
-- :: timeout -> /* got disconnected */
-- ses_to_fsrv[n]!close;
-- goto endIDLE
-- od;
-- /* 3. Close the connection */
-- ses_to_flow[n]!close,0;
-- goto endIDLE;
--
--progressDATA_OUT: /* 1. prepare local file fsrver */
-- ses_to_fsrv[n]!open;
-- if
-- :: fsrv_to_ses[n]?reject ->
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: fsrv_to_ses[n]?accept ->
-- skip
-- fi;
-- /* 2. initialize flow control *** disabled
-- ses_to_flow[n]!sync,toggle;
-- do
-- :: atomic {
-- flow_to_ses[n]?sync_ack,type ->
-- if
-- :: (type != toggle)
-- :: (type == toggle) -> break
-- fi
-- }
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- od;
-- toggle = 1 - toggle;
-- /* 3. prepare remote file fsrver */
-- ses_to_flow[n]!connect,0;
-- if
-- :: flow_to_ses[n]?reject,status ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?connect,0 ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(NON_FATAL);
-- goto endIDLE
-- :: flow_to_ses[n]?accept,0 ->
-- skip
-- :: timeout ->
-- ses_to_fsrv[n]!close;
-- ses_to_pres[n]!reject(FATAL);
-- goto endIDLE
-- fi;
-- /* 4. Transmit the data, upto eof */
-- do
-- :: fsrv_to_ses[n]?data ->
-- ses_to_flow[n]!data,0
-- :: fsrv_to_ses[n]?eof ->
-- ses_to_flow[n]!eof,0;
-- status = COMPLETE;
-- break
-- :: pres_to_ses[n]?abort -> /* local user aborted */
-- ses_to_fsrv[n]!close;
-- ses_to_flow[n]!close,0;
-- status = FATAL;
-- break
-- od;
-- /* 5. Close the connection */
-- do
-- :: pres_to_ses[n]?abort /* ignore */
-- :: flow_to_ses[n]?close,0 ->
-- if
-- :: (status == COMPLETE) ->
-- ses_to_pres[n]!accept,0
-- :: (status != COMPLETE) ->
-- ses_to_pres[n]!reject(status)
-- fi;
-- break
-- :: timeout ->
-- ses_to_pres[n]!reject(FATAL);
-- break
-- od;
-- goto endIDLE
--}
-//GO.SYSIN DD p347.session.prog
-echo p94 1>&2
-sed 's/.//' >p94 <<'//GO.SYSIN DD p94'
--byte state = 2;
--
--proctype A() { (state == 1) -> state = 3 }
--
--proctype B() { state = state - 1 }
--
--/* added: */
--init { run A(); run B() }
-//GO.SYSIN DD p94
-echo p95.1 1>&2
-sed 's/.//' >p95.1 <<'//GO.SYSIN DD p95.1'
--init { printf("hello world\n") }
-//GO.SYSIN DD p95.1
-echo p95.2 1>&2
-sed 's/.//' >p95.2 <<'//GO.SYSIN DD p95.2'
--proctype A(byte state; short set)
--{ (state == 1) -> state = set
--}
--
--init { run A(1, 3) }
-//GO.SYSIN DD p95.2
-echo p96.1 1>&2
-sed 's/.//' >p96.1 <<'//GO.SYSIN DD p96.1'
--byte state = 1;
--
--proctype A() { (state == 1) -> state = state + 1 }
--
--proctype B() { (state == 1) -> state = state - 1 }
--
--init { run A(); run B() }
-//GO.SYSIN DD p96.1
-echo p96.2 1>&2
-sed 's/.//' >p96.2 <<'//GO.SYSIN DD p96.2'
--#define true 1
--#define false 0
--#define Aturn 1
--#define Bturn 0
--
--bool x, y, t;
--
--proctype A()
--{ x = true;
-- t = Bturn;
-- (y == false || t == Aturn);
-- /* critical section */
-- x = false
--}
--proctype B()
--{ y = true;
-- t = Aturn;
-- (x == false || t == Bturn);
-- /* critical section */
-- y = false
--}
--init { run A(); run B() }
-//GO.SYSIN DD p96.2
-echo p97.1 1>&2
-sed 's/.//' >p97.1 <<'//GO.SYSIN DD p97.1'
--byte state = 1;
--proctype A() { atomic { (state == 1) -> state = state + 1 } }
--proctype B() { atomic { (state == 1) -> state = state - 1 } }
--init { run A(); run B() }
-//GO.SYSIN DD p97.1
-echo p97.2 1>&2
-sed 's/.//' >p97.2 <<'//GO.SYSIN DD p97.2'
--proctype nr(short pid, a, b)
--{ int res;
--
--atomic { res = (a*a+b)/2*a;
-- printf("result %d: %d\n", pid, res)
-- }
--}
--init { run nr(1,1,1); run nr(1,2,2); run nr(1,3,2) }
-//GO.SYSIN DD p97.2
-echo p99 1>&2
-sed 's/.//' >p99 <<'//GO.SYSIN DD p99'
--proctype A(chan q1)
--{ chan q2;
--
-- q1?q2;
-- q2!123
--}
--
--proctype B(chan qforb)
--{ int x;
--
-- qforb?x;
-- printf("x = %d\n", x)
--}
--
--init
--{ chan qname[2] = [1] of { chan };
-- chan qforb = [1] of { int };
--
-- run A(qname[0]);
-- run B(qforb);
--
-- qname[0]!qforb
--}
-//GO.SYSIN DD p99
projects / lttv.git / blobdiff