1		package(load_event_b_project([event_b_model(none,'CB3FSMM',[sees(none,['CB3FSMC']),variables(none,[identifier(none,'BUSpriority'),identifier(none,'BUSvalue'),identifier(none,'BUSwrite'),identifier(none,'T1_state'),identifier(none,'T1_timer'),identifier(none,'T1_writevalue'),identifier(none,'T2_mode'),identifier(none,'T2_readpriority'),identifier(none,'T2_readvalue'),identifier(none,'T2_state'),identifier(none,'T2_timer'),identifier(none,'T2_writevalue'),identifier(none,'T2v'),identifier(none,'T3_enabled'),identifier(none,'T3_evaluated'),identifier(none,'T3_readpriority'),identifier(none,'T3_readvalue'),identifier(none,'T3_state')]),invariant(none,[member(rodinpos('CB3FSMM',inv1,'_mpY_kiJnEeK2gagIYXFA3g'),identifier(none,'T2v'),integer_set(none)),member(rodinpos('CB3FSMM',inv34,'_mpZmoCJnEeK2gagIYXFA3g'),identifier(none,'T3_evaluated'),bool_set(none)),member(rodinpos('CB3FSMM',inv35,'_mpaNsCJnEeK2gagIYXFA3g'),identifier(none,'T3_enabled'),bool_set(none)),member(rodinpos('CB3FSMM',inv4,'_mpaNsSJnEeK2gagIYXFA3g'),identifier(none,'T1_state'),identifier(none,'T1state')),member(rodinpos('CB3FSMM',inv5,'_mpaNsiJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2state')),member(rodinpos('CB3FSMM',inv56,'_mpa0wCJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3state')),member(rodinpos('CB3FSMM',inv6,'_mpa0wSJnEeK2gagIYXFA3g'),identifier(none,'T1_writevalue'),integer_set(none)),member(rodinpos('CB3FSMM',inv7,'_mpa0wiJnEeK2gagIYXFA3g'),identifier(none,'T2_writevalue'),integer_set(none)),member(rodinpos('CB3FSMM',inv8,'_mpbb0CJnEeK2gagIYXFA3g'),identifier(none,'T2_readvalue'),integer_set(none)),member(rodinpos('CB3FSMM',inv9,'_mpbb0SJnEeK2gagIYXFA3g'),identifier(none,'T2_readpriority'),natural_set(none)),member(rodinpos('CB3FSMM',inv87,'_mpcC4CJnEeK2gagIYXFA3g'),identifier(none,'T3_readvalue'),integer_set(none)),member(rodinpos('CB3FSMM',inv98,'_mpcC4SJnEeK2gagIYXFA3g'),identifier(none,'T3_readpriority'),natural_set(none)),member(rodinpos('CB3FSMM',inv10,'_mpcC4iJnEeK2gagIYXFA3g'),identifier(none,'T1_timer'),natural_set(none)),member(rodinpos('CB3FSMM',inv11,'_mpcp8CJnEeK2gagIYXFA3g'),identifier(none,'T2_timer'),natural_set(none)),member(rodinpos('CB3FSMM',inv14,'_mpcp8SJnEeK2gagIYXFA3g'),identifier(none,'BUSwrite'),partial_function(none,natural_set(none),integer_set(none))),member(rodinpos('CB3FSMM',inv15,'_mpdRACJnEeK2gagIYXFA3g'),identifier(none,'BUSvalue'),integer_set(none)),member(rodinpos('CB3FSMM',inv16,'_mpdRASJnEeK2gagIYXFA3g'),identifier(none,'BUSpriority'),natural_set(none)),
2		finite(rodinpos('CB3FSMM',inv19,'_mpd4ECJnEeK2gagIYXFA3g'),identifier(none,'BUSwrite')),
3		not_equal(rodinpos('CB3FSMM',inv24,'_mpd4ESJnEeK2gagIYXFA3g'),identifier(none,'BUSwrite'),empty_set(none)),
4		member(rodinpos('CB3FSMM',inv25,'_mpefICJnEeK2gagIYXFA3g'),integer(none,0),domain(none,identifier(none,'BUSwrite'))),member(rodinpos('CB3FSMM',inv26,'_L49B8CJyEeK2gagIYXFA3g'),identifier(none,'T2_mode'),identifier(none,'T2mode'))]),theorems(none,[]),events(none,[event(rodinpos('CB3FSMM','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('CB3FSMM',act1,'_mpfGMCJnEeK2gagIYXFA3g'),[identifier(none,'T2v')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act34,'_mpfGMSJnEeK2gagIYXFA3g'),[identifier(none,'T3_evaluated')],[boolean_true(none)]),assign(rodinpos('CB3FSMM',act35,'_mpfGMiJnEeK2gagIYXFA3g'),[identifier(none,'T3_enabled')],[boolean_true(none)]),assign(rodinpos('CB3FSMM',act4,'_mpfGMyJnEeK2gagIYXFA3g'),[identifier(none,'T1_state')],[identifier(none,'T1_EN')]),assign(rodinpos('CB3FSMM',act5,'_mpftQCJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_EN')]),assign(rodinpos('CB3FSMM',act56,'_mpftQSJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_READY')]),assign(rodinpos('CB3FSMM',act6,'_mpftQiJnEeK2gagIYXFA3g'),[identifier(none,'T1_writevalue')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act7,'_mpftQyJnEeK2gagIYXFA3g'),[identifier(none,'T2_writevalue')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act8,'_mpgUUCJnEeK2gagIYXFA3g'),[identifier(none,'T2_readvalue')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act9,'_mpgUUSJnEeK2gagIYXFA3g'),[identifier(none,'T2_readpriority')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act87,'_mpgUUiJnEeK2gagIYXFA3g'),[identifier(none,'T3_readvalue')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act98,'_mpgUUyJnEeK2gagIYXFA3g'),[identifier(none,'T3_readpriority')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act10,'_mpg7YCJnEeK2gagIYXFA3g'),[identifier(none,'T1_timer')],[integer(none,2)]),assign(rodinpos('CB3FSMM',act11,'_mpg7YSJnEeK2gagIYXFA3g'),[identifier(none,'T2_timer')],[integer(none,3)]),assign(rodinpos('CB3FSMM',act14,'_mphicCJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])]),assign(rodinpos('CB3FSMM',act15,'_mphicSJnEeK2gagIYXFA3g'),[identifier(none,'BUSvalue')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act16,'_mphiciJnEeK2gagIYXFA3g'),[identifier(none,'BUSpriority')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act17,'_QlCWkCJyEeK2gagIYXFA3g'),[identifier(none,'T2_mode')],[identifier(none,'T2MODE_SENSE')])],[]),event(rodinpos('CB3FSMM','T1Evaluate','_mpiJgCJnEeK2gagIYXFA3g'),'T1Evaluate',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mpiwkCJnEeK2gagIYXFA3g'),identifier(none,'T1_timer'),integer(none,0)),equal(rodinpos('CB3FSMM',grd3,'_mpiwkSJnEeK2gagIYXFA3g'),identifier(none,'T1_state'),identifier(none,'T1_EN'))],[],[assign(rodinpos('CB3FSMM',act2,'_mpiwkiJnEeK2gagIYXFA3g'),[identifier(none,'T1_timer')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act3,'_mpjXoCJnEeK2gagIYXFA3g'),[identifier(none,'T1_state')],[identifier(none,'T1_CALC')])],[]),event(rodinpos('CB3FSMM','T1Calculate','_mpjXoSJnEeK2gagIYXFA3g'),'T1Calculate',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpjXoiJnEeK2gagIYXFA3g'),p)],[member(rodinpos('CB3FSMM',grd1,'_mpj-sCJnEeK2gagIYXFA3g'),identifier(none,p),integer_set(none)),equal(rodinpos('CB3FSMM',grd2,'_mpj-sSJnEeK2gagIYXFA3g'),identifier(none,'T1_state'),identifier(none,'T1_CALC'))],[],[assign(rodinpos('CB3FSMM',act1,'_mpj-siJnEeK2gagIYXFA3g'),[identifier(none,'T1_writevalue')],[identifier(none,p)]),assign(rodinpos('CB3FSMM',act2,'_mpklwCJnEeK2gagIYXFA3g'),[identifier(none,'T1_state')],[identifier(none,'T1_SEND')])],[]),event(rodinpos('CB3FSMM','T1SendResult','_mpklwSJnEeK2gagIYXFA3g'),'T1SendResult',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mplM0CJnEeK2gagIYXFA3g'),ppriority),identifier(rodinpos('CB3FSMM',[],'_mpklwiJnEeK2gagIYXFA3g'),pv)],[equal(rodinpos('CB3FSMM',grd1,'_mplM0SJnEeK2gagIYXFA3g'),identifier(none,pv),identifier(none,'T1_writevalue')),equal(rodinpos('CB3FSMM',grd2,'_mplM0iJnEeK2gagIYXFA3g'),identifier(none,ppriority),integer(none,3)),equal(rodinpos('CB3FSMM',grd3,'_mplM0yJnEeK2gagIYXFA3g'),identifier(none,'T1_state'),identifier(none,'T1_SEND'))],[],[assign(rodinpos('CB3FSMM',act1,'_mplz4CJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[overwrite(none,identifier(none,'BUSwrite'),set_extension(none,[couple(none,[identifier(none,ppriority),identifier(none,pv)])]))]),assign(rodinpos('CB3FSMM',act2,'_mplz4SJnEeK2gagIYXFA3g'),[identifier(none,'T1_state')],[identifier(none,'T1_WAIT')])],[]),event(rodinpos('CB3FSMM','T1Wait','_mplz4iJnEeK2gagIYXFA3g'),'T1Wait',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpma8CJnEeK2gagIYXFA3g'),pt)],[equal(rodinpos('CB3FSMM',grd1,'_mpma8SJnEeK2gagIYXFA3g'),identifier(none,pt),integer(none,2)),equal(rodinpos('CB3FSMM',grd2,'_mpma8iJnEeK2gagIYXFA3g'),identifier(none,'T1_state'),identifier(none,'T1_WAIT'))],[],[assign(rodinpos('CB3FSMM',act1,'_mpnCACJnEeK2gagIYXFA3g'),[identifier(none,'T1_timer')],[identifier(none,pt)]),assign(rodinpos('CB3FSMM',act2,'_mpnCASJnEeK2gagIYXFA3g'),[identifier(none,'T1_state')],[identifier(none,'T1_EN')])],[]),event(rodinpos('CB3FSMM','T2Evaluate','_mpnCAiJnEeK2gagIYXFA3g'),'T2Evaluate',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mpnpECJnEeK2gagIYXFA3g'),identifier(none,'T2_timer'),integer(none,0)),equal(rodinpos('CB3FSMM',grd3,'_mpnpESJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_EN'))],[],[assign(rodinpos('CB3FSMM',act2,'_mpoQICJnEeK2gagIYXFA3g'),[identifier(none,'T2_timer')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act3,'_mpoQISJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_RCV')])],[]),event(rodinpos('CB3FSMM','T2ReadBus','_mpoQIiJnEeK2gagIYXFA3g'),'T2ReadBus',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpo3MSJnEeK2gagIYXFA3g'),ppriority),identifier(rodinpos('CB3FSMM',[],'_mpo3MCJnEeK2gagIYXFA3g'),pv)],[equal(rodinpos('CB3FSMM',grd1,'_mpo3MiJnEeK2gagIYXFA3g'),identifier(none,pv),identifier(none,'BUSvalue')),equal(rodinpos('CB3FSMM',grd2,'_mpo3MyJnEeK2gagIYXFA3g'),identifier(none,ppriority),identifier(none,'BUSpriority')),equal(rodinpos('CB3FSMM',grd3,'_mppeQCJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_RCV'))],[],[assign(rodinpos('CB3FSMM',act1,'_mppeQSJnEeK2gagIYXFA3g'),[identifier(none,'T2_readvalue')],[identifier(none,pv)]),assign(rodinpos('CB3FSMM',act2,'_mppeQiJnEeK2gagIYXFA3g'),[identifier(none,'T2_readpriority')],[identifier(none,ppriority)]),assign(rodinpos('CB3FSMM',act4,'_mpqFUCJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_PROC')])],[]),event(rodinpos('CB3FSMM','T2Reset','_mpqFUSJnEeK2gagIYXFA3g'),'T2Reset',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mpqsYCJnEeK2gagIYXFA3g'),identifier(none,'T2_readpriority'),integer(none,4)),equal(rodinpos('CB3FSMM',grd2,'_mpqsYSJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_PROC'))],[],[assign(rodinpos('CB3FSMM',act1,'_mprTcCJnEeK2gagIYXFA3g'),[identifier(none,'T2_writevalue')],[identifier(none,'T2v')]),assign(rodinpos('CB3FSMM',act2,'_mprTcSJnEeK2gagIYXFA3g'),[identifier(none,'T2v')],[integer(none,0)]),assign(rodinpos('CB3FSMM',act3,'_mpr6gCJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_SEND')]),assign(rodinpos('CB3FSMM',act4,'_LUT1ECJ4EeK2gagIYXFA3g'),[identifier(none,'T2_mode')],[identifier(none,'T2MODE_TRANSMIT')])],[]),event(rodinpos('CB3FSMM','T2Complete','_6pZTsCM3EeK2gagIYXFA3g'),'T2Complete',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_6pZTsSM3EeK2gagIYXFA3g'),identifier(none,'T2_readpriority'),integer(none,5)),equal(rodinpos('CB3FSMM',grd2,'_6pZ6wCM3EeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_PROC')),equal(rodinpos('CB3FSMM',grd3,'_6pZ6wSM3EeK2gagIYXFA3g'),identifier(none,'T2_mode'),identifier(none,'T2MODE_TRANSMIT'))],[],[assign(rodinpos('CB3FSMM',act1,'_6pZ6wiM3EeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_RELEASE')]),assign(rodinpos('CB3FSMM',act2,'_6pZ6wyM3EeK2gagIYXFA3g'),[identifier(none,'T2_mode')],[identifier(none,'T2MODE_SENSE')])],[]),event(rodinpos('CB3FSMM','T2ReleaseBus','_mpr6gSJnEeK2gagIYXFA3g'),'T2ReleaseBus',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpshkCJnEeK2gagIYXFA3g'),ppriority)],[equal(rodinpos('CB3FSMM',grd1,'_mpshkSJnEeK2gagIYXFA3g'),identifier(none,ppriority),identifier(none,'T2_readpriority')),member(rodinpos('CB3FSMM',grd3,'_mptIoSJnEeK2gagIYXFA3g'),identifier(none,ppriority),domain(none,identifier(none,'BUSwrite'))),equal(rodinpos('CB3FSMM',grd4,'_mptvsCJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_RELEASE'))],[],[assign(rodinpos('CB3FSMM',act1,'_mptvsSJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[domain_subtraction(none,set_extension(none,[identifier(none,ppriority)]),identifier(none,'BUSwrite'))]),assign(rodinpos('CB3FSMM',act2,'_mpuWwCJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_WAIT')])],[]),event(rodinpos('CB3FSMM','T2Calculate','_mpuWwSJnEeK2gagIYXFA3g'),'T2Calculate',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mpu90CJnEeK2gagIYXFA3g'),identifier(none,'T2_readpriority'),integer(none,3)),equal(rodinpos('CB3FSMM',grd2,'_mpu90SJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_PROC'))],[],[assign(rodinpos('CB3FSMM',act1,'_mpvk4CJnEeK2gagIYXFA3g'),[identifier(none,'T2v')],[identifier(none,'T2_readvalue')]),assign(rodinpos('CB3FSMM',act2,'_mpvk4SJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_WAIT')])],[]),event(rodinpos('CB3FSMM','T2WriteBus','_mpwL8CJnEeK2gagIYXFA3g'),'T2WriteBus',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpwzASJnEeK2gagIYXFA3g'),ppriority),identifier(rodinpos('CB3FSMM',[],'_mpwzACJnEeK2gagIYXFA3g'),pv)],[equal(rodinpos('CB3FSMM',grd1,'_mpwzAiJnEeK2gagIYXFA3g'),identifier(none,pv),identifier(none,'T2_writevalue')),equal(rodinpos('CB3FSMM',grd2,'_mpxaECJnEeK2gagIYXFA3g'),identifier(none,ppriority),integer(none,5)),equal(rodinpos('CB3FSMM',grd3,'_mpxaESJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_SEND'))],[],[assign(rodinpos('CB3FSMM',act1,'_mpyBICJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[overwrite(none,identifier(none,'BUSwrite'),set_extension(none,[couple(none,[identifier(none,ppriority),identifier(none,pv)])]))]),assign(rodinpos('CB3FSMM',act2,'_mpyBISJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_WAIT')])],[]),event(rodinpos('CB3FSMM','T2Wait','_mpyBIiJnEeK2gagIYXFA3g'),'T2Wait',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mpyoMCJnEeK2gagIYXFA3g'),pt)],[equal(rodinpos('CB3FSMM',grd1,'_mpzPQCJnEeK2gagIYXFA3g'),identifier(none,pt),integer(none,3)),equal(rodinpos('CB3FSMM',grd2,'_mpzPQSJnEeK2gagIYXFA3g'),identifier(none,'T2_state'),identifier(none,'T2_WAIT'))],[],[assign(rodinpos('CB3FSMM',act2,'_mpz2UCJnEeK2gagIYXFA3g'),[identifier(none,'T2_timer')],[identifier(none,pt)]),assign(rodinpos('CB3FSMM',act3,'_mpz2USJnEeK2gagIYXFA3g'),[identifier(none,'T2_state')],[identifier(none,'T2_EN')])],[]),event(rodinpos('CB3FSMM','T3Initiate','_mp0dYCJnEeK2gagIYXFA3g'),'T3Initiate',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mp0dYSJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_READY')),equal(rodinpos('CB3FSMM',grd2,'_mp1EcCJnEeK2gagIYXFA3g'),identifier(none,'T3_evaluated'),boolean_false(none)),equal(rodinpos('CB3FSMM',grd3,'_mp1EcSJnEeK2gagIYXFA3g'),identifier(none,'T3_enabled'),boolean_true(none))],[],[assign(rodinpos('CB3FSMM',act1,'_mp1rgCJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_WRITE')]),assign(rodinpos('CB3FSMM',act2,'_mp1rgSJnEeK2gagIYXFA3g'),[identifier(none,'T3_enabled')],[boolean_false(none)])],[]),event(rodinpos('CB3FSMM','T3Evaluate','_mp2SkCJnEeK2gagIYXFA3g'),'T3Evaluate',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mp2SkSJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_READY')),equal(rodinpos('CB3FSMM',grd2,'_mp25oCJnEeK2gagIYXFA3g'),identifier(none,'T3_evaluated'),boolean_false(none)),equal(rodinpos('CB3FSMM',grd3,'_mp25oSJnEeK2gagIYXFA3g'),identifier(none,'T3_enabled'),boolean_false(none))],[],[assign(rodinpos('CB3FSMM',act1,'_mp25oiJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_READ')])],[]),event(rodinpos('CB3FSMM','T3writebus','_mp3gsCJnEeK2gagIYXFA3g'),'T3writebus',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mp3gsiJnEeK2gagIYXFA3g'),ppriority),identifier(rodinpos('CB3FSMM',[],'_mp3gsSJnEeK2gagIYXFA3g'),pv)],[equal(rodinpos('CB3FSMM',grd1,'_mp4HwCJnEeK2gagIYXFA3g'),identifier(none,pv),integer(none,0)),equal(rodinpos('CB3FSMM',grd2,'_mp4HwSJnEeK2gagIYXFA3g'),identifier(none,ppriority),integer(none,4)),equal(rodinpos('CB3FSMM',grd3,'_mp4u0CJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_WRITE'))],[],[assign(rodinpos('CB3FSMM',act1,'_mp4u0SJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[overwrite(none,identifier(none,'BUSwrite'),set_extension(none,[couple(none,[identifier(none,ppriority),identifier(none,pv)])]))]),assign(rodinpos('CB3FSMM',act2,'_mp4u0iJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_WAIT')])],[]),event(rodinpos('CB3FSMM','T3Read','_mp5V4CJnEeK2gagIYXFA3g'),'T3Read',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mp588SJnEeK2gagIYXFA3g'),ppriority),identifier(rodinpos('CB3FSMM',[],'_mp588CJnEeK2gagIYXFA3g'),pv)],[equal(rodinpos('CB3FSMM',grd1,'_mp6kACJnEeK2gagIYXFA3g'),identifier(none,pv),identifier(none,'BUSvalue')),equal(rodinpos('CB3FSMM',grd2,'_mp6kASJnEeK2gagIYXFA3g'),identifier(none,ppriority),identifier(none,'BUSpriority')),equal(rodinpos('CB3FSMM',grd4,'_mp7LECJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_READ'))],[],[assign(rodinpos('CB3FSMM',act1,'_mp7LESJnEeK2gagIYXFA3g'),[identifier(none,'T3_readvalue')],[identifier(none,pv)]),assign(rodinpos('CB3FSMM',act2,'_mp7yICJnEeK2gagIYXFA3g'),[identifier(none,'T3_readpriority')],[identifier(none,ppriority)]),assign(rodinpos('CB3FSMM',act3,'_mp7yISJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_PROC')])],[]),event(rodinpos('CB3FSMM','T3Poll','_mp7yIiJnEeK2gagIYXFA3g'),'T3Poll',ordinary(none),[],[],[less(rodinpos('CB3FSMM',grd1,'_mp8ZMCJnEeK2gagIYXFA3g'),identifier(none,'T3_readpriority'),integer(none,5)),equal(rodinpos('CB3FSMM',grd2,'_mp9AQCJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_PROC'))],[],[assign(rodinpos('CB3FSMM',act1,'_mp9AQSJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_WAIT')])],[]),event(rodinpos('CB3FSMM','T3ReleaseBus','_mp9AQiJnEeK2gagIYXFA3g'),'T3ReleaseBus',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mp9nUCJnEeK2gagIYXFA3g'),ppriority)],[equal(rodinpos('CB3FSMM',grd1,'_mp-OYCJnEeK2gagIYXFA3g'),identifier(none,ppriority),integer(none,4)),equal(rodinpos('CB3FSMM',grd2,'_mp-OYSJnEeK2gagIYXFA3g'),identifier(none,'T3_readpriority'),integer(none,5)),equal(rodinpos('CB3FSMM',grd3,'_mp-1cCJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_PROC'))],[],[assign(rodinpos('CB3FSMM',act1,'_mp-1cSJnEeK2gagIYXFA3g'),[identifier(none,'BUSwrite')],[domain_subtraction(none,set_extension(none,[identifier(none,ppriority)]),identifier(none,'BUSwrite'))]),assign(rodinpos('CB3FSMM',act2,'_mp_cgCJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_RELEASE')])],[]),event(rodinpos('CB3FSMM','T3Wait','_mp_cgSJnEeK2gagIYXFA3g'),'T3Wait',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mqADkCJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_WAIT'))],[],[assign(rodinpos('CB3FSMM',act1,'_mqADkSJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_READY')]),assign(rodinpos('CB3FSMM',act2,'_mqAqoCJnEeK2gagIYXFA3g'),[identifier(none,'T3_evaluated')],[boolean_true(none)])],[]),event(rodinpos('CB3FSMM','T3ReEnableWait','_mqAqoSJnEeK2gagIYXFA3g'),'T3ReEnableWait',ordinary(none),[],[],[equal(rodinpos('CB3FSMM',grd1,'_mqBRsCJnEeK2gagIYXFA3g'),identifier(none,'T3_state'),identifier(none,'T3_RELEASE'))],[],[assign(rodinpos('CB3FSMM',act1,'_mqBRsSJnEeK2gagIYXFA3g'),[identifier(none,'T3_state')],[identifier(none,'T3_READY')]),assign(rodinpos('CB3FSMM',act2,'_mqBRsiJnEeK2gagIYXFA3g'),[identifier(none,'T3_evaluated')],[boolean_true(none)]),assign(rodinpos('CB3FSMM',act3,'_mqBRsyJnEeK2gagIYXFA3g'),[identifier(none,'T3_enabled')],[boolean_true(none)])],[]),event(rodinpos('CB3FSMM','Update','_mqB4wCJnEeK2gagIYXFA3g'),'Update',ordinary(none),[],[identifier(rodinpos('CB3FSMM',[],'_mqB4wSJnEeK2gagIYXFA3g'),pmax)],[equal(rodinpos('CB3FSMM',grd1,'_mqB4wiJnEeK2gagIYXFA3g'),identifier(none,pmax),max(none,domain(none,identifier(none,'BUSwrite')))),greater(rodinpos('CB3FSMM',grd2,'_mqB4wyJnEeK2gagIYXFA3g'),identifier(none,'T1_timer'),integer(none,0)),greater(rodinpos('CB3FSMM',grd3,'_mqCf0CJnEeK2gagIYXFA3g'),identifier(none,'T2_timer'),integer(none,0)),disjunct(rodinpos('CB3FSMM',grd4,'_mqCf0SJnEeK2gagIYXFA3g'),equal(none,identifier(none,'T3_enabled'),boolean_true(none)),equal(none,identifier(none,'T3_evaluated'),boolean_true(none)))],[],[assign(rodinpos('CB3FSMM',act1,'_mqCf0iJnEeK2gagIYXFA3g'),[identifier(none,'BUSvalue')],[function(none,identifier(none,'BUSwrite'),[identifier(none,pmax)])]),assign(rodinpos('CB3FSMM',act2,'_mqCf0yJnEeK2gagIYXFA3g'),[identifier(none,'BUSpriority')],[identifier(none,pmax)]),assign(rodinpos('CB3FSMM',act3,'_mqDG4CJnEeK2gagIYXFA3g'),[identifier(none,'T1_timer')],[minus(none,identifier(none,'T1_timer'),integer(none,1))]),assign(rodinpos('CB3FSMM',act4,'_mqDG4SJnEeK2gagIYXFA3g'),[identifier(none,'T2_timer')],[minus(none,identifier(none,'T2_timer'),integer(none,1))]),assign(rodinpos('CB3FSMM',act7,'_mqDG4iJnEeK2gagIYXFA3g'),[identifier(none,'T3_evaluated')],[boolean_false(none)])],[])])])],[event_b_context(none,'CB3FSMC',[extends(none,[]),constants(none,[identifier(none,'T1_CALC'),identifier(none,'T1_EN'),identifier(none,'T1_SEND'),identifier(none,'T1_WAIT'),identifier(none,'T2MODE_RELEASE'),identifier(none,'T2MODE_SENSE'),identifier(none,'T2MODE_TRANSMIT'),identifier(none,'T2_CALC'),identifier(none,'T2_EN'),identifier(none,'T2_PROC'),identifier(none,'T2_RCV'),identifier(none,'T2_RELEASE'),identifier(none,'T2_SEND'),identifier(none,'T2_WAIT'),identifier(none,'T3_PROC'),identifier(none,'T3_READ'),identifier(none,'T3_READY'),identifier(none,'T3_RELEASE'),identifier(none,'T3_WAIT'),identifier(none,'T3_WRITE')]),axioms(none,[partition(rodinpos('CB3FSMC',axm1,'_brH6OCJyEeK2gagIYXFA3g'),identifier(none,'T1state'),[set_extension(none,[identifier(none,'T1_EN')]),set_extension(none,[identifier(none,'T1_CALC')]),set_extension(none,[identifier(none,'T1_SEND')]),set_extension(none,[identifier(none,'T1_WAIT')])]),partition(rodinpos('CB3FSMC',axm2,'_brIhQCJyEeK2gagIYXFA3g'),identifier(none,'T2state'),[set_extension(none,[identifier(none,'T2_EN')]),set_extension(none,[identifier(none,'T2_RCV')]),set_extension(none,[identifier(none,'T2_PROC')]),set_extension(none,[identifier(none,'T2_CALC')]),set_extension(none,[identifier(none,'T2_SEND')]),set_extension(none,[identifier(none,'T2_WAIT')]),set_extension(none,[identifier(none,'T2_RELEASE')])]),partition(rodinpos('CB3FSMC',axm3,'_brIhQSJyEeK2gagIYXFA3g'),identifier(none,'T3state'),[set_extension(none,[identifier(none,'T3_READY')]),set_extension(none,[identifier(none,'T3_WRITE')]),set_extension(none,[identifier(none,'T3_RELEASE')]),set_extension(none,[identifier(none,'T3_READ')]),set_extension(none,[identifier(none,'T3_PROC')]),set_extension(none,[identifier(none,'T3_WAIT')])]),partition(rodinpos('CB3FSMC',axm4,'_brIhQSJyEeK2gagIYXFA3l'),identifier(none,'T2mode'),[set_extension(none,[identifier(none,'T2MODE_SENSE')]),set_extension(none,[identifier(none,'T2MODE_TRANSMIT')]),set_extension(none,[identifier(none,'T2MODE_RELEASE')])])]),theorems(none,[]),sets(none,[deferred_set(none,'T1state'),deferred_set(none,'T2mode'),deferred_set(none,'T2state'),deferred_set(none,'T3state')])])],[discharged('CB3FSMM','INITIALISATION',inv9),discharged('CB3FSMM','INITIALISATION',inv98),discharged('CB3FSMM','INITIALISATION',inv10),discharged('CB3FSMM','INITIALISATION',inv11),discharged('CB3FSMM','INITIALISATION',inv16),discharged('CB3FSMM','INITIALISATION',inv19),discharged('CB3FSMM','INITIALISATION',inv25),discharged('CB3FSMM','T1Evaluate',inv10),discharged('CB3FSMM','T1Wait',inv10),discharged('CB3FSMM','T2Evaluate',inv11),discharged('CB3FSMM','T2ReadBus',inv9),discharged('CB3FSMM','T2ReleaseBus',inv14),discharged('CB3FSMM','T2WriteBus',inv14),discharged('CB3FSMM','T2WriteBus',inv24),discharged('CB3FSMM','T2WriteBus',inv25),discharged('CB3FSMM','T2Wait',inv11),discharged('CB3FSMM','T3writebus',inv14),discharged('CB3FSMM','T3writebus',inv24),discharged('CB3FSMM','T3writebus',inv25),discharged('CB3FSMM','T3Read',inv98),discharged('CB3FSMM','T3ReleaseBus',inv14),discharged('CB3FSMM','T3ReleaseBus',inv25),discharged('CB3FSMM','Update',inv10),discharged('CB3FSMM','Update',inv11),discharged('CB3FSMM','Update',inv16)],_Error)).
5