# 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 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]) - 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