From 40d2cadd45aea08d0ec4d43ac32d07d5b5115f36 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 20:59:34 +0000 Subject: [PATCH] Tidy PTA examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2165 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/pta/args-abovebelow | 14 --- prism-examples/pta/brp/README | 27 ------ prism-examples/pta/brp/auto | 7 -- prism-examples/pta/brp/brp.pctl | 22 ----- prism-examples/pta/brp/brp.pm | 150 ----------------------------- 5 files changed, 220 deletions(-) delete mode 100644 prism-examples/pta/args-abovebelow delete mode 100644 prism-examples/pta/brp/README delete mode 100755 prism-examples/pta/brp/auto delete mode 100644 prism-examples/pta/brp/brp.pctl delete mode 100644 prism-examples/pta/brp/brp.pm diff --git a/prism-examples/pta/args-abovebelow b/prism-examples/pta/args-abovebelow deleted file mode 100644 index 8f2547ad..00000000 --- a/prism-examples/pta/args-abovebelow +++ /dev/null @@ -1,14 +0,0 @@ -# no pre (or as little as poss) --aroptions nopre,noopt --aroptions nopre,opt --aroptions nopre,opt,above - --aroptions noprob1,noopt --aroptions noprob1,opt --aroptions noprob1,opt,above - -# pre --aroptions pre,noopt --aroptions pre,opt --aroptions pre,opt,above - diff --git a/prism-examples/pta/brp/README b/prism-examples/pta/brp/README deleted file mode 100644 index ef87bfc7..00000000 --- a/prism-examples/pta/brp/README +++ /dev/null @@ -1,27 +0,0 @@ -This case study is based on the bounded retransmission protocol (BRP) [HSV94], a variant of the alternating bit protocol. - -Its parameters are: - - N = number of chunks in a file - MAX = maximum number of retransmissions - TD = the transition delay - TIME_OUT = the time the sender waits before timing out - -TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD) - -For more information, see the untimed version: http://www.prismmodelchecker.org/casestudies/brp.php - -The PTA extension is based on that used in [HH09] - -===================================================================================== - -[HSV94] -L. Helmink, M. Sellink and F Vaandrager -Proof checking a data link protocol -In Proc. Types for Proofs and Programs (TYPES'93), LNCS 806, pp 127-165, Springer-Verlag, 1994 - -[HH09] -A. Hartmanns and H. Hermanns -A Modest Approach to Checking Probabilistic Timed Automata -Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009 - diff --git a/prism-examples/pta/brp/auto b/prism-examples/pta/brp/auto deleted file mode 100755 index 03503e01..00000000 --- a/prism-examples/pta/brp/auto +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/csh - -foreach N (16 32 64) - foreach MAX (2 3 4 5) - prism brp.pm brp.pctl -const N=$N,MAX=$MAX,TD=2,TIME_OUT=5 -fixdl - end -end diff --git a/prism-examples/pta/brp/brp.pctl b/prism-examples/pta/brp/brp.pctl deleted file mode 100644 index 44994b7e..00000000 --- a/prism-examples/pta/brp/brp.pctl +++ /dev/null @@ -1,22 +0,0 @@ -// properties taken from [D'AJJL01] - -// property A -P=? [ true U srep=1 & rrep=3 & recv ]; - -// property B -P=? [ true U srep=3 & !(rrep=3) & recv ]; - -// property 1 -P=? [ true U s=5 ]; - -// property 2 -P=? [ true U s=5 & srep=2 ]; - -// property 3 -P=? [ true U s=5 & srep=1 & i>8 ]; - -// property 4 -P=? [ true U !(srep=0) & !recv ]; - -// rewards -R=? [ F "deadlock" ]; diff --git a/prism-examples/pta/brp/brp.pm b/prism-examples/pta/brp/brp.pm deleted file mode 100644 index 09945670..00000000 --- a/prism-examples/pta/brp/brp.pm +++ /dev/null @@ -1,150 +0,0 @@ -// bounded retransmission protocol [D'AJJL01] -// gxn/dxp 23/05/2001 - -pta - -// number of chunks -const int N; -// maximum number of retransmissions -const int MAX; -// max time to send a message (transition delay) -const int TD; -// time out limit (greater than TD+TD - the max time to send a message and receive an ack) -const int TIME_OUT = 2*TD + 1; - -module sender - - // clock of the sender - x : clock; - - s : [0..6]; - // 0 idle - // 1 next_frame - // 2 wait_ack - // 3 retransmit - // 4 success - // 5 error - // 6 wait sync - srep : [0..3]; - // 0 bottom - // 1 not ok (nok) - // 2 do not know (dk) - // 3 ok (ok) - nrtr : [0..MAX]; - i : [0..N]; - bs : bool; - s_ab : bool; - fs : bool; - ls : bool; - - invariant - (s=2 => x<=TIME_OUT) // only wait until timeout - endinvariant - - // idle - [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); - // next_frame - [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0) & (x'=0); - // wait_ack - [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); - [] (s=2) & x=TIME_OUT -> (s'=3); // time out - // retransmit - [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1) & (x'=0); - [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); - [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); - // success - [] (s=4) & (i (s'=1) & (i'=i+1); - [] (s=4) & (i=N) -> (s'=0) & (srep'=3); - // error - [SyncWait] (s=5) -> (s'=6); - // wait sync - [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); - -endmodule - -module receiver - - r : [0..5]; - // 0 new_file - // 1 fst_safe - // 2 frame_received - // 3 frame_reported - // 4 idle - // 5 resync - rrep : [0..4]; - // 0 bottom - // 1 fst - // 2 inc - // 3 ok - // 4 nok - fr : bool; - lr : bool; - br : bool; - r_ab : bool; - recv : bool; - - - // new_file - [SyncWait] (r=0) -> (r'=0); - [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - // fst_safe_frame - [] (r=1) -> (r'=2) & (r_ab'=br); - // frame_received - [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); - [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); - [aA] (r=2) & !(r_ab=br) -> (r'=4); - // frame_reported - [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); - // idle - [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); - [SyncWait] (r=4) & (ls=true) -> (r'=5); - [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); - // resync - [SyncWait] (r=5) -> (r'=0) & (rrep'=0); - -endmodule - -module checker // prevents more than one frame being set - - T : bool; - - [NewFile] (T=false) -> (T'=true); - -endmodule - -module channelK - - xK : clock; - k : [0..1]; - - invariant - (k=1 => xK<=TD) - endinvariant - - // idle - [aF] (k=0) -> 0.98 : (k'=1) & (xK'=0) + 0.02 : (k'=0) & (xK'=0); - // sending - [aG] (k=1) & xK<=TD -> (k'=0) & (xK'=0); - -endmodule - -module channelL - - xL : clock; - l : [0..1]; - - invariant - (l=1 => xL<=TD) - endinvariant - - // idle - [aA] (l=0) -> 0.99 : (l'=1) & (xL'=0) + 0.02 : (l'=0) & (xL'=0); - // sending - [aB] (l=1) & xL<=TD -> (l'=0) & (xL'=0); - -endmodule - -rewards - [aF] i=1 : 1; -endrewards