--****************************************************-- --****************************************************-- -- CSMA/CD Protocol -- -- Non-probabilistic model deduced from the probabilistic model in -- "Symbolic Model Checking for Probabilistic Timed Automata" -- (M. Kwiatkowska, G. Norman, J. Sproston and F. Wang., FORMATS/FTRTFT'2004) -- -- See figures on http://www.prismmodelchecker.org/casestudies/csma.php -- -- Modeling by Laurent Fribourg and Etienne Andre (LSV) -- -- Created : 2009 -- Last modified : 2010/04/28 --****************************************************-- --****************************************************-- ---IEEE VALUE--- & lambda = 808 & sigma = 26 & timeslot = 52 ---RESCALED PRISM VALUE--- -- & lambda = 96 -- & sigma = 3 -- & timeslot = 6