s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3668 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Tree: bb86d1c14b
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'bb86d1c14b'
${ noResults }
prism-accumulation/prism-examples/mdps/wlan
Dave Parker bb86d1c14b
Group examples subdirectories by model type. 		7 years ago
..
README.txt Group examples subdirectories by model type. 7 years ago
auto Group examples subdirectories by model type. 7 years ago
wlan.pctl Group examples subdirectories by model type. 7 years ago
wlan0.nm Group examples subdirectories by model type. 7 years ago
wlan0_collide.nm Group examples subdirectories by model type. 7 years ago
wlan0_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan1.nm Group examples subdirectories by model type. 7 years ago
wlan1_collide.nm Group examples subdirectories by model type. 7 years ago
wlan1_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan2.nm Group examples subdirectories by model type. 7 years ago
wlan2_collide.nm Group examples subdirectories by model type. 7 years ago
wlan2_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan3.nm Group examples subdirectories by model type. 7 years ago
wlan3_collide.nm Group examples subdirectories by model type. 7 years ago
wlan3_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan4.nm Group examples subdirectories by model type. 7 years ago
wlan4_collide.nm Group examples subdirectories by model type. 7 years ago
wlan4_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan5.nm Group examples subdirectories by model type. 7 years ago
wlan5_collide.nm Group examples subdirectories by model type. 7 years ago
wlan5_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan6.nm Group examples subdirectories by model type. 7 years ago
wlan6_collide.nm Group examples subdirectories by model type. 7 years ago
wlan6_time_bounded.nm Group examples subdirectories by model type. 7 years ago
wlan_collide.pctl Group examples subdirectories by model type. 7 years ago
wlan_time_bounded.pctl Group examples subdirectories by model type. 7 years ago

README.txt 

This case study concerns the IEEE 802.11 Wireless LAN

We consider the scenario where two stations trying to send packets simultaneously.

The PRISM model is taken from [KNS02a] using the integer semantics given in [KNS06]. In the model one time unit
corresponds to 50μs and to ensure integer bounds, where neccessary, scaling lower bound constraints down and
upper bound constraints up to sensure a sound abstraction.


For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/wlan.php

PARAMETERS

wlanK.nm - K is the maximum value of a stations backoff counter where 6 is specified in the standard
TRANS_TIME_MAX - maximum time to send a packet where (after scaling) 315 specified in the standard
COL=2: in collosion model to count number collisions (parameter k in the property files must be less than or equal to COL)
DEADLINE: in time_bounded model is the deadline

=====================================================================================

[KNS02a]
M. Kw