User manual for Timed
Contents
1. Disable timed transitions Random Animation 10 Random Animation Random Timed Animation Find State Satisfying Predicate 2Y Find gt View Statespace D View gt Execute an Operation W Show Shortest Trace to Current State Show Current B State Figure 1 Activate deactivate the Timed CSP animation mode in ProB s menu 4 Timed CSP animation When the Timed CSP animation mode is activate the simulator supports automatic animation The animation strategy can be modified with respect to two parameters and three options Parameters Max steps maximal number of steps to animate Max time elapsed maximal time an integer or a rational number to animate Options Maximal progress if enabled the animator always select the longest timed transition If there is no upper bound on timed transition a random value of time is selected Events first if enable the animator always randomly select an event be fore any timed transition Time from beginning if enable the animator treats the Max time elapsed parameter as from the beginning To set an animation strategy users can select the menu item Random timed animation from the Animate menu The Random timed execu tion dialog will appear see Figure 2 Random Timed Execution Enter maximum nr of operations 100 Enter maximum elapsed time 300 Max time progress Always events before time evolutions Elapsed time from the b2. User manual for Timed CSP Simulator Hoang Nga Nguyen Markus Roggenbach Swansea University UK October 22 2012 1 Introduction Timed Csp Simulator is based on the presentation of Timed CspP in 4 For a brief discussion of the tool architecture see 1 2 The semantical questions regarding simulating Timed CsP are discussed in 3 2 Supported operators In addition to CSP M operators already defined in ProB Timed CSP Sim ulator supports several timed operators of Timed CSP ASCH Delay event prefix Timed event prefix WAIT d P a gt c d P aN c Table 1 Timed Operators in Timed CSP Simulators These extra operators are listed in Table 1 where e d denotes a time delay which is an arithmetic expression with the following syntax d i f d d d d dxd d d where i is an integer f t is a function call with terms t as parameters In runtime an arithmetic expression is evaluated to an integer or a simplest rational number e x denotes a timed variable e P Q are Timed CSP processes 3 Timed CSP mode In the Animate menu in the main menubar of ProB there is a new menu for activating and deactivating the Timed CSP animation mode see Fig ure 1 If the mode is activated timed transitions are allowed in the anima tion for simulating executing of Timed CSP processes When this mode is deactivated the animator disallows any timed transition hence working as usual with untimed CSP Animate Reset
3. eginning Run Cancel Figure 2 The Random Timed Execution dialog References 1 Marc Dragon Andy Gimblett and Markus Roggenbach A Simulator for Timed CSP In Jens Bendisposto Cliff Jones Michael Leuschel and Alexander Romanovsky editors AVoCS 11 Proceedings of the Eleventh International Workshop on Automated Verification of Critical Systems Newcastle University 2011 Marc Fontaine Andy Gimblett Faron Moller Hoang Nga Nguyen and Markus Roggenbach Timed CSP Simulator In Franco Mazzanti and Gianluca Trentanni editors iFM 2012 amp ABZ 2012 Proceedings of the Posters amp Tool demos Session CNR ISTI 2012 Faron Moller Hoang Nga Nguyen and Markus Roggenbach Theoret ical foundations for simulating Timed CSP Technical report Swansea University 3 2012 S Schneider Concurrent and real time systems the CSP approach Citeseer 2000
Download Pdf Manuals
Related Search