From 7c239331deb45092b634466f408bab4603aa6c64 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 15 Mar 2012 09:49:06 +0000 Subject: [PATCH] Change parameter names (K->COL, bmax->K) to align with MDP benchmark of same name. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4835 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/pta/csma/abst/auto | 8 ++++---- prism-examples/pta/csma/abst/csma.nm | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/prism-examples/pta/csma/abst/auto b/prism-examples/pta/csma/abst/auto index 61df4d1e..26af4be4 100755 --- a/prism-examples/pta/csma/abst/auto +++ b/prism-examples/pta/csma/abst/auto @@ -1,7 +1,7 @@ #!/bin/csh -prism csma.nm -const bmax=1 eventually.pctl -aroptions refine=all,nopre,opt +prism csma.nm -const K=1 eventually.pctl -aroptions refine=all,nopre,opt -prism csma.nm -const bmax=1 deadline.pctl -const T=1000 -aroptions refine=all,nopre,opt -prism csma.nm -const bmax=1 deadline.pctl -const T=2000 -aroptions refine=all,nopre,opt -prism csma.nm -const bmax=1 deadline.pctl -const T=3000 -aroptions refine=all,nopre,opt +prism csma.nm -const K=1 deadline.pctl -const T=1000 -aroptions refine=all,nopre,opt +prism csma.nm -const K=1 deadline.pctl -const T=2000 -aroptions refine=all,nopre,opt +prism csma.nm -const K=1 deadline.pctl -const T=3000 -aroptions refine=all,nopre,opt diff --git a/prism-examples/pta/csma/abst/csma.nm b/prism-examples/pta/csma/abst/csma.nm index 9f41ce98..07977d31 100644 --- a/prism-examples/pta/csma/abst/csma.nm +++ b/prism-examples/pta/csma/abst/csma.nm @@ -8,7 +8,7 @@ pta //---------------------------------------------------------------------------------------------------------------------------- // actual parameters -const int bmax; // exponential backoff limit +const int K; // exponential backoff limit (sometimes called bmax) const int slot=2*sigma; // length of slot const int sigma=26; const int lambda=808; @@ -65,7 +65,7 @@ module station1 // LOCAL CLOCK x1 : clock; // COLLISION COUNTER - cd1 : [0..bmax]; + cd1 : [0..K]; invariant (s1=0 => x1=0) & @@ -77,11 +77,11 @@ module station1 // start sending [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending - [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // detects channel is busy so go into backoff + [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff // transmitting [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished - [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // collision detected + [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected // set backoff (no time can pass in this state) // first retransmission @@ -121,7 +121,7 @@ module station1 // finished backoff [send1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=1) & (x1'=0); // channel free - [busy1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // channel busy + [busy1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy // once finished nothing matters [done] (s1=4) -> true;