(************************************************************ * IMITATOR MODEL * * BRP (Bounded Retransmission Protocol) * * Description : Bounded Retransmission Protocol [version slightly modified] * Correctness : V[] ((S.error ^ x = SYNC) => R.new_file) V [] (R.firstsafe_frame => rb1 = 1) * Source : "The Bounded Retransmission Protocol Must Be on Time!" * Author : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans * Modeling : ?? and Laurent Fribourg * Input by : ?? and Etienne Andre * * Created : ? (< 09/2007) * Last modified : 2015/07/19 * * IMITATOR version: 2.7.1 ************************************************************) ---START PI0--- (* & MAX = 2 & N = 2 *) & TD = 1 & T1 = 3 & TR = 16 & SYNC = 17 ---END PI0---