(************************************************************ * IMITATOR MODEL * * CSMA/CD Protocol * * Description : CSMA/CD Protocol * Correctness : TODO * Source : 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 * Author : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. * Modeling : M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. * Input by : Laurent Fribourg and Etienne Andre * * Created : 2007 * Last modified : 2015/07/30 * * IMITATOR version: 2.7.1 ************************************************************) ---IEEE VALUE--- & lambda = 808 & sigma = 26 & timeslot = 52 ---RESCALED PRISM VALUE--- -- & lambda = 96 -- & sigma = 3 -- & timeslot = 6