(************************************************************
 *                      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   : 2020/08/14
 *
 * IMITATOR version: 3
 ************************************************************)

property := #synth IM(
	(* IEEE VALUE *)
 	& lambda   = 808
 	& sigma    = 26
 	& timeslot = 52

	(* RESCALED PRISM VALUE *)
(*	& lambda   = 96
	& sigma    = 3
	& timeslot = 6*)
);