Benchmark wlan.5-0

Download
model.prism (0.01 MB)
property.props (0.01 MB)
model.jani (0.40 MB)
Origin
Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.

Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
Contents of file: model.prism
// WLAN PROTOCOL (two stations)
// discrete time model
// gxn/jzs 20/02/02

mdp

// COLLISIONS
const int COL=0; // maximum number of collisions

// TIMING CONSTRAINTS
// we have used the FHSS parameters
// then scaled by the value of ASLOTTIME
const int ASLOTTIME = 1;
const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice
const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
const int TRANS_TIME_MAX = 10; // scaling up
const int TRANS_TIME_MIN = 4; // scaling down
const int ACK_TO = 6;
const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice
const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
// maximum constant used in timing constraints + 1
const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1;

// CONTENTION WINDOW
// CWMIN =15 & CWMAX =511
// this means that MAX_BACKOFF IS 5
const int MAX_BACKOFF = 5;

//-----------------------------------------------------------------//
// THE MEDIUM/CHANNEL

// FORMULAE FOR THE CHANNEL
// channel is busy
formula busy = c1>0 | c2>0;
// channel is free
formula free = c1=0 & c2=0;

module medium
	
	// number of collisions
	col : [0..COL+1];
	
	// medium status 
	c1 : [0..2];
	c2 : [0..2];
	// ci corresponds to messages associated with station i
	// 0 nothing being sent
	// 1 being sent correctly
	// 2 being sent garbled	  
	
	// begin sending message and nothing else currently being sent
	[send1] c1=0 & c2=0 -> (c1'=1);
	[send2] c2=0 & c1=0 -> (c2'=1);
	
	// begin sending message and  something is already being sent
	// in this case both messages become garbled
	[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
	[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
	
	// finish sending message
	[finish1] c1>0 -> (c1'=0);
	[finish2] c2>0 -> (c2'=0);

endmodule

//-----------------------------------------------------------------//
// STATION 1
module station1
	// clock for station 1
	x1 : [0..TIME_MAX];
	
	// local state
	s1 : [1..12];
	// 1 sense
	// 2 wait until free before setting backoff
	// 3 wait for DIFS then set slot
	// 4 set backoff 
	// 5 backoff
	// 6 wait until free in backoff
	// 7 wait for DIFS then resume backoff
	// 8 vulnerable 
	// 9 transmit
	// 11 wait for SIFS and then ACK
	// 10 wait for ACT_TO 
	// 12 done
	// BACKOFF
	// separate into slots
	slot1 : [0..31]; 
	backoff1 : [0..15];
	
	// BACKOFF COUNTER
	bc1 : [0..MAX_BACKOFF];
	// SENSE
	// let time pass
	[time] s1=1 & x1 (x1'=min(x1+1,TIME_MAX));
	// ready to transmit
	[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
	// found channel busy so wait until free
	[] s1=1 & busy -> (s1'=2) & (x1'=0);
	// WAIT UNTIL FREE BEFORE SETTING BACKOFF
	// let time pass (no need for the clock x1 to change)
	[time] s1=2 & busy -> (s1'=2);
	// find that channel is free so check its free for DIFS before setting backoff
	[] s1=2 & free -> (s1'=3);
	// WAIT FOR DIFS THEN SET BACKOFF
	// let time pass
	[time] s1=3 & x1 (x1'=min(x1+1,TIME_MAX));
	// found channel busy so wait until free
	[] s1=3 & busy -> (s1'=2) & (x1'=0);
	// start backoff  first uniformly choose slot
	// backoff counter 0
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF));
	// backoff counter 1
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF));
	// backoff counter 2
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF));
	// backoff counter 3
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF));
	// backoff counter 4
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF));
	// backoff counter 5
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 -> 1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF))
	                                         + 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,MAX_BACKOFF));
																					 
	// SET BACKOFF (no time can pass)
	// chosen slot now set backoff
	[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 )
	         + 1/16 : (s1'=5) & (backoff1'=1 )
	         + 1/16 : (s1'=5) & (backoff1'=2 )
	         + 1/16 : (s1'=5) & (backoff1'=3 )
	         + 1/16 : (s1'=5) & (backoff1'=4 )
	         + 1/16 : (s1'=5) & (backoff1'=5 )
	         + 1/16 : (s1'=5) & (backoff1'=6 )
	         + 1/16 : (s1'=5) & (backoff1'=7 )
	         + 1/16 : (s1'=5) & (backoff1'=8 )
	         + 1/16 : (s1'=5) & (backoff1'=9 )
	         + 1/16 : (s1'=5) & (backoff1'=10)
	         + 1/16 : (s1'=5) & (backoff1'=11)
	         + 1/16 : (s1'=5) & (backoff1'=12)
	         + 1/16 : (s1'=5) & (backoff1'=13)
	         + 1/16 : (s1'=5) & (backoff1'=14)
	         + 1/16 : (s1'=5) & (backoff1'=15);
	// BACKOFF
	// let time pass
	[time] s1=5 & x1 (x1'=min(x1+1,TIME_MAX));
	// decrement backoff
	[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);	
	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);	
	// finish backoff 
	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
	// found channel busy
	[] s1=5 & busy -> (s1'=6) & (x1'=0);
	// WAIT UNTIL FREE IN BACKOFF
	// let time pass (no need for the clock x1 to change)
	[time] s1=6 & busy -> (s1'=6);
	// find that channel is free
	[] s1=6 & free -> (s1'=7);
	
	// WAIT FOR DIFS THEN RESUME BACKOFF
	// let time pass
	[time] s1=7 & x1 (x1'=min(x1+1,TIME_MAX));
	// resume backoff (start again from previous backoff)
	[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
	// found channel busy
	[] s1=7 & busy -> (s1'=6) & (x1'=0);
	
	// VULNERABLE
	// let time pass
	[time] s1=8 & x1 (x1'=min(x1+1,TIME_MAX));
	// move to transmit
	[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
	// TRANSMIT
	// let time pass
	[time] s1=9 & x1 (x1'=min(x1+1,TIME_MAX));
	// finish transmission successful	
	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
	// finish transmission garbled
	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
	// WAIT FOR SIFS THEN WAIT FOR ACK
	
	// WAIT FOR SIFS i.e. c1=0
	// check channel and busy: go into backoff
	[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
	// check channel and free: let time pass
	[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
	// let time pass
	// following guard is always false as SIFS=1
	// [time] s1=10 & c1=0 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX));
	// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
	[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
	
	// WAIT FOR ACK i.e. c1=1
	// let time pass
	[time] s1=10 & c1=1 & x1 (x1'=min(x1+1,TIME_MAX));
	// get acknowledgement so packet sent correctly and move to done
	[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
	
	// WAIT FOR ACK_TO
	// check channel and busy: go into backoff
	[] s1=11 & x1=0 & busy -> (s1'=2);
	// check channel and free: let time pass
	[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
	// let time pass
	[time] s1=11 & x1>0 & x1 (x1'=min(x1+1,TIME_MAX));
	// no acknowledgement (go to backoff waiting DIFS first)
	[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
		
	// DONE
	[time] s1=12 -> (s1'=12);
endmodule	

// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module 
station2=station1[x1=x2, 
                  s1=s2,
				  s2=s1,
				  c1=c2,
				  c2=c1, 
				  slot1=slot2, 
				  backoff1=backoff2, 
				  bc1=bc2, 
				  send1=send2, 
				  finish1=finish2] 
endmodule
// ---------------------------------------------------------------------------- //

label "target" = s1=12 & s2=12;
Contents of file: property.props
"sent": P>=1 [ F "target" ];
Contents of file: model.jani
File too large to display (size: 0.40 MB).