Final Simulator for CML User Manual
Contents
1. points 1 Run This will simulate animate the model ignoring any breakpoints 2 Debug This will simulate animate the model and suspend execution at all en abled breakpoints 1 1 Creating a Launch Configuration To create a launch configuration you first click on the small arrow next to either the debug button or the run button depending on the desired mode as shown in Fig ure 1 Once clicked a drop down menu will appear with either Debug configurations or Run configurations depending on which button you clicked select the appropriate config urations option This will open a configurations dialog like the one shown in Figure 2 All of the existing CML launch configurations will appear under CML Model To create a new launch configuration you may double click on CML Model or on the New launch configuration button then an empty launch configuration will appear as shown in with the name New Configuration possibly followed by a number if this name is already used To edit an existing configuration click on the desired launch configuration name and the details will appear on the right side of the dialogue D32 2 Simulator for CML Public COMPASS JUJ OME DO LI1L FrOLES5 CMI LIVIL CUMIPdass FrOJECL USETS IU a pk 0a v bs E E ML Explorer 7 S0S csi C Componentl cml Process cml cs2 C Componentl cml o Component2 cml Componentl c2. P x Variable binding currently happens after communication so forms like c x x are not yet supported Guarded action e A 1f e is true behave like a otherwise behave like Stop Sequential compositio A B n behave like a until a terminates then behave like B External choice A B offer the environment the choice between a and B Internal choice A l7 B nondeterministically behave either like a or B Interrupt A B behave as a until sg takes control then behave like B Timed interrupt A _e_ B behave as a for e time units then behave as B Untimed timeout A gt B behave as a but nondeterministically change behaviour to B at any time Timeout A _e_ gt B offer a for e time units then offer B Abstraction A cs behave as a with the events in cs hidden Start deadline A startsby e Not implemented End deadline A endsby e Not implemented Channel renaming 1 A c lt nc Not implemented Recursion mu X F X explicit definition of a recursive action Mutual Recursion mu X Y F X Y G X Y Not implemented Table 1 Action constructors 15 PASS D32 2 Simulator for CML Public COMPASS Operator Syntax Comments Interleaving A ll nsi ns2 B execute A and B in parallel without synchro nising A can modify the state components in nsi and B can modify the state components in
3. Public COMPASS 1 The COMPASS CML Simulator This report explains how to simulate animate a CML model with the COMPASS tool The tool can be downloaded from SourceForge at http sf net projects compassresearch files Releases 0 2 0 where versions are available for several operating systems This document describes how to add and configure launch configurations and how the interpreter is launched and used First the basic modes of operation are explained The interpreter operates in two modes Run and Debug and within these modes there are two options Simulate and Animate The options control the level of user interaction and are described below 1 Simulate This option will interpret the model without any user interaction When faced with a choice of several observable events one will be chosen in a random but deterministic manner Thus the simulation will always make the same choices for every run of the same model This behavior is implemented by the use of a pseudo random number generator that has been initialised with a constant seed This random number generator is used to resolve the choice between events and will produce the same series of actions when presented with the same series of choices 2 Animate This option will interpret the model with user interaction All observ able events are selected by the user The modes of operation controls the interpreter s behaviour with respect to break
4. Sequence for loop for e in s doa for each expression e in the sequence s exe cute action a Set for loop for all e in set S do a Not implemented Index for loop for i el to e2 by e3 do a Not implemented While loop while e do a execute action a while the boolean expres sion e evaluates to true Table 5 Control statements 19 COMPASS D32 2 Simulator for CML Public COMPASS Operator Syntax Comments Sequential composition A B behave like a until a terminates then behave like B External choice A B offer the environment the choice between a and B Internal choice A l7 B nondeterministically behave either like a or B Generalised parallelism A I cs B execute A and 8 in parallel synchronising on the events in cs Alphabetised parallelism A csl cs2 B Not implemented Synchronous parallelism A IIB execute a and B in parallel synchronising on all events Interleaving A III B execute A and B in parallel without synchro nising Interrupt A B behave as a until B takes control then behave like B Timed interrupt A _e B Not implemented Untimed timeout A gt B offer a but may nondeterministically stop of fering a and offer sB at any time Timeout Al_e_ gt B offer a for e time units then offer B Abstraction Hiding A cs behave as a with the events in cs hidden Start deadli
5. for environment on tock b O tock 1 b al The environment picked b A tl observable step by C Observable trace of C init a init b Eval Status Skip Terminated with following state FINISHED The output contains the following information Waiting for environment on These are the events that are available to the environ ment before the next transition is taken If they include any observable events then the interpreter will await for user input The available events are listed to gether with an increasing number to the left of it To pick an event the user must enter the number to the left of the desired event and hit Enter and the animation will continue The environment picks lt event gt This shows the event that was chosen by the en vironment e g the user The system picks lt event gt This shows the silent transitions taken automatically by the interpreter Observable trace of lt processname gt This is the top level process trace including the event that happened in this step Eval Status This shows the current state of the top level process after the transition has been taken 13 D32 2 Simulator for CML Public COMPASS 3 Supported CML Constructs This section gives an overview of the CML constructs that are implemented As all of the expression types are implemented no detailed overview of them is given here The overview is divid
6. ns2 Interleaving no state A III B execute A and B in parallel without synchro nising Neither a nor sB change the state Synchronous parallelism A nsl ns2 B execute a and B in parallel synchronising on all events a can modify the state components in ns1 and sB can modify the state components in ns2 Synchronous parallelism no state A IIB execute a and B in parallel synchronising on all events Neither a nor a change the state Alphabetised parallelism A ns1 csl cs2 ns2 B Not implemented Alphabetised parallelism no state A esl cs2 B Not implemented Generalised parallelism A Insi cs ns2 B execute A and s in parallel synchronising on the events in cs A can modify the state com ponents in ns1 and B can modify the state components in ns2 Generalised parallelism no state A I cs B execute A and s in parallel synchronising on the events in cs Neither a nor B change the state Table 2 Parallel action constructors 16 D32 2 Simulator for CML Public COMPASS Operator Syntax Comments Replicated sequential composition i in seq e A i Not implemented Replicated external choice i in set e A i offer the environment the choice of all ac tions a i such that i is in the set e Replicated internal choice i in set e A i nondeterministically behave as a i for any i in the set e Replicated inte
7. process A 8 E Console tasks O a alele 0 A CML Model CML Debugger Eval Status c gt Skip Waiting for environment on tock c State for tock A 4 State for c A 4 Debug thread sending Status event to controller WAITING FOR ENVIRONMENT writable Insert 5 9 Figure 6 The a event has just occurred and the model interpretation is now currently offering c and tock D32 2 Simulator for CML Public COMPASS 1 3 2 Simulation Simulating without user interaction is achieved by choosing the Simulate option in the launch configuration This mode of operation will interpret the model by taking random decisions when faced with a choice of events However the same choices will always be taken if the model is interpreted multiple times In Figure 7 a simulate interpretation has completed Debug test test cml CML Compass Project my Riser EE TEE bas Q EML Debug Debug 2 G variables Breakpoints Observable Event History 2 o Y lt terminated gt A CML Model tock lt terminated gt CML Debug Target a wil lt terminated exit value 0 gt CML Debuager c gt test cml E E E outline F CML Event Options 23 SE channels a b process A begin a gt c gt Skip end process B begin b gt Skip end process A 8 E Console Tasks xx e earnen lt terminated gt A CML Model CML Debugger Debug thread sending Sta
8. the CML perspective To access this right click on a cml file to make the con text menu appear From here either choose Debug As CML Model or Run As gt CML Model After that two things can happen if the CML source file only contains one process then this process will be launched If however more than one process is defined then a process selection dialog appears with a list of possible processes This is shown in To launch a simulation a process must be chosen This is done by double clicking one of the process names in the list or selecting it and pressing OK This will launch a simulation with that process as the top level process If you launch via a shortcut then a launch configuration named Quick Launch or Quick Launch lt number gt if more exist will be created and launched D32 2 Simulator for CML Public COMPASS test2 cml test cml X channels a b c d process test begin e Process Selection 00 Select a process actions test a 2 amp a gt a a l a a 1 b gt Skip test2 l 1 4 c gt a a 2 a a 2 d gt Skip a 2 2 amp d gt a a 2 a a 2 d gt Skip process test2 begin actions INIT a gt b gt Skip INIT end L2 Cancel s Figure 4 Right after Run As gt CML Model has been clicked the context menu of the test cml file appears Since the file defines more than one process the proce
9. tock v 2 CML Debug Target gt y Process 99 Action cl 2 Action C off CML Debugger gt testcml B D 8 outline A CML Event Options 23 channels a b me process A 7 begin b o ac gt c gt Skip end process B begin end process A 8 E Console Tasks Sale a n 6 A CML Model CML Debugger waiting for environment on tock b al State for tock B 45 State for b B 5 State for a A 44 Debug thread sending Status event to controller WAITING FOR ENVIRONMENT writable Insert 10 4 Figure 5 A CML model animated in the debug perspective the selected event in the CML Event Options view To understand how the views work together a two step animation is shown in Figure 5 and Figure 6 In Figure 5 tock has happened once and a tock event is currently selected Since process A and B both offer tock they are both marked with gray in the Editor view In Figure 6 the a event has been double clicked and therefore just occurred Thus now the external choice has been resolved and only one part of the model is marked tiv sr E es a H Eome ds Debug Debug E Y Variables Breakpoints Observable Event History 2 SE 7 A CML Model tock CML Debug Target i y Action C sl CML Debugger testicml M B outline F cmt Event Options 28 p channels a b c tack process A c begin co gt Sp end process B begin 6 b gt Skip end
10. AReferenceProcess gt AActionProcess C The system picked tau AReferenceProcess gt AActionProcess C Waiting for environment on tau AActionProcess gt ACommunicationAction C The system picked tau AActionProcess gt ACommunicationAction C Waiting for environment on tock init 0 tock 1 init The environment picked init SRT SS observable step by C Observable trace of C init Eval Status 1 a gt Skip NA Waiting for environment on tock a O tock lla al The environment picked a a observable step by C Observable trace of C init a Eval Status Skip NA Waiting for environment on tau ASequentialCompositionProcess gt AReferenceProcess C The system picked tau ASequentialCompositionProcess gt AReferenceProcess C Waiting for environment on tau AReferenceProcess gt AActionProcess C The system picked tau AReferenceProcess gt AActionProcess C Waiting for environment on tau AActionProcess gt ACommunicationAction C 12 D32 2 Simulator for CML Public COMPASS The system picked tau AActionProcess gt ACommunicationAction C Waiting for environment on tock init 0 tock lJ init l The environment picked init observable step by C Observable trace of C init a init Eval Status b gt Skip Waiting
11. SEVENTH FRAMEWORK PROGRAMME Grant Agreement 287829 Comprehensive Modelling for Advanced Systems of Systems COMPASS Final Simulator for CML User Manual Technical Note Number D32 2 Version 0 7 Date September 2013 Public Document http www compass research eu D32 2 Simulator for CML Public COMPASS Contributors Joey W Coleman AU Anders Kaels Malmos AU Editors Joey Coleman AU Reviewers Marcel Oliveira UFPE Ken Pierce Newcastle Simon Foster York D32 2 Simulator for CML Public COMPASS Document History Ver Date Author Description 0 1 23 08 2013 AKM Initial document version 0 2 03 09 2013 AKM Supported CML constructs section added 0 3 04 09 2013 AKM Initial Cmdline section added 0 4 09 09 2013 JWC Editing 0 5 23 09 2013 AKM Editing based on internal review 0 6 25 09 2013 JWC Final Editing 0 7 27 09 2013 JWC Final version D32 2 Simulator for CML Public COMPASS Contents 1 The COMPASS CML Simulator 5 1 1 Creating a Launch Configuration 5 1 2 Launch Via Shortcut 2 2 ee ee 7 1 3 Interpretation i eb caes Bab a ghee OS e Mie a Ged re wR 8 2 Command line Interface 12 3 Supported CML Constructs 14 3T Actions oins s i Gs a Se Bi ae ee Se ae eR 14 32 PTOCESSES bb aeea ote sy bv ee wb he la eee de OR Soe ek 14 22 D32 2 Simulator for CML
12. ator has been used in the Bang amp Olufsen case study Theme 4 WP42 and this has guided the prioritisation of implementation of operators The remaining unimplemented operators will be fully completed for the third release of the tool in Month 32 Most of the operators will be complete by Month 26 however as many of the process operators have a corresponding action operators most of unimple mented statements have corresponding implementations in the Overture platform that may be reused The time based operators are also expected to be complete by Month 26 The remaining operators are channel renaming and mutual recursion and they are unlikely to have been completed until the Month 32 release 22
13. ed into two subsections actions and statements which is a sub group of actions and processes Each subsection contains a series of tables that group similar categories The first column of each table gives the name of the operator the second gives an informal syntax and the last is a short description that gives the oper ator s status If a construct is not supported entirely no or partial implementation of the semantics then the name of operator will be highlighted in red and a description of the issue will appear in the third column 3 1 Actions This section describes all of the supported and partially supported actions Where a and B are actions e is an expression P x is a predicate expression with x free c is a channel name cs is a channel set expression ns is a nameset expression 3 2 Processes This section describes all the supported and partially supported processes a and B are both processes e is an expression and cs is a channel expression 14 D32 2 Simulator for CML Public CoM Operator Syntax Comments Termination Skip terminate immediately Deadlock Stop only allows time to pass Chaos Chaos Not implemented Divergence Div runs without ever interacting in any observable event Delay Wait e does nothing for e time units and then terminates Prefixing c le x P x gt A offers the environment a choice of events of the form c e p Where p in set x x T
14. mi process A begin actions a Chaos b Skip Bb a end Figure 1 Screenshot of the toolbar of the COMPASS tool showing the debug button left and run button right highlighted Run Configurations Create manage and run configurations Project not set E Bx By a Y CML Model CA Eclipse Application El Java Applet El Java Application Ju JUnit J JUnit Plug in Test o Name New_configuration E Main Develop E Common Project Project Browse Top Process Process Search Animate Simulate Animate D Simulate m2 Maven Build OSGi Framework VDM PP Model I VDM RT Model E VDM SL Model Filter matched 13 of 13 items O Close Figure 2 The launch configuration dialog showing a newly created launch configura tion As seen in Figure 2 a project name and a process name need to be associated with a launch configuration along with the mode of operation as discussed in Section I When choosing a project you can either write the name or click on the browse button which shows a list of all the available projects and choose one from there The selection of the process name is identical The selected project must exist in the workspace and the process named must exist within it It will not be possible to launch if they do not In the left corner of a small red icon with an X and a message will indicate what is wrong In the figure it indicates that no project has been se
15. ml 23 Bl 5 outline channels a b c process A begin a gt c gt Skip end postcondition violated for init begin state a int Init gt Init 2 post BEEN Init b gt Skip end process C A B Figure 9 The interpreter has stopped because a post condition has been violated 11 D32 2 Simulator for CML Public COMPASS 2 Command line Interface The command line interface enables animation of CML models when invoked with the e option Since the CML model may have more than one process defined the e lt processId gt option must be supplied where lt processId gt is the name of the process that is to be animated If an unsupported CML construct is encountered the tool will raise an exception specifying the unsupported construct As an example of how this works consider the following CML model in a file called example cml channels init ab process A begin init gt a gt Skip end process B begin init gt b gt Skip end process C A B The following command will animate the process identified by C emic e C example cml This results in the following output being printed to the console COMPASS command line CML Checker CML M24 Parsing file example cml file s successfully parsed Starting analysis Running The CML Type Checker on example cml model types are ok Running on example cml Waiting for environment on tau
16. ne A startsby e Not implemented End deadline A endsby e Not implemented Process instantiation v T A e OF A e behaves as a where the formal parameters v are instantiated to e Channel renaming A c lt ne Not implemented Table 6 Process constructors 20 D32 2 Simulator for CML Public COMPASS Operator Syntax Comments Replicated sequential composition i in seq e A i Not implemented Replicated external choice i in set e A i Not implemented Replicated internal choice i in set e A i Not implemented Replicated generalised parallelism cs i in set e A i execute all processes a i for i in the set e in parallel synchronising on the events in cs Replicated alphabetised parallelism i in set e Not implemented cs i A i Replicated synchronous parallelism i in set e A i execute all processes a i in parallel syn chronising on all events Replicated interleaving i in set e A i execute all processes A i in parallel without synchronising on any events Table 7 Replicated process constructors 21 D32 2 Simulator for CML Public COMPASS 4 Conclusion At end of Month 24 the CML Simulator is not yet in its final form but it is nearly complete Section 3 provides a comprehensive list of the constructs that are supported and those that remain to be implemented As it stands now the simul
17. peration op of an object obj or 2 execute operation op the current object or process with the parameters p and assign the value returned by op to a variable Return return e OT return terminates the evaluation of an operation pos sibly yielding a value e Specification frame wr vl Tl rd v2 T2 pre P1 vl v2 post P2 v1 vl1l v2 v2 Not implemented New v new C instantiate a new object of class c and assign it to v Table 4 CML statements 18 COMPASS D32 2 Simulator for CML Public Operator Syntax Comments Nondeterministic if statement if el gt al e2 gt a2 end evaluate all guards ei If none are true then the statement diverges If one or more guards are true one of the associated actions is exe cuted nondeterministically If statement if el then al elseif e2 then a2 else an the boolean expressions ei are evaluated in order When the first ei is evaluated to true the associated action is executed If no ei evaluates to true the action an is executed Cases statement cases e pl gt al p2 gt al e others gt an end Not implemented Nondeterministic do statement do el gt al e2 gt a2 end if all guards ei evaluate to false terminate Otherwise choose nondeterministically one guard that evaluates to true execute the asso ciated action and repeat the do statement
18. rleaving i in set e execute all actions a i in parallel without ns i A i synchronising on any events Each action a i can only modify the state components in ns i Replicated generalised parallelism lcs i in set e execute all actions a i for i in the set e ns i A i in parallel synchronising on the events in cs Each action a i can only modify the state components in ns i Replicated alphabetised parallelism i in set e Not implemented ns i cs i A i Replicated synchronous parallelism i in set e execute all processes a i in parallel syn ns i A i chronising on all events Each action a i can only modify the state components in ns iy Table 3 Replicated action constructors 17 D32 2 Simulator for CML Public Operator Syntax Comments Let let p e ina evaluate the action a in the environment where p is associated to e Block del v T e a declare the local variable v of type T option ally initialised to e and evaluate action a in this context Assignment vise assign e to v Multiple assignment atomic v1 el Not implemented vn en Call execute operation op of an object obj 1 or 1 obj op p of the current object or process 2 with the a Se e parameters p 3 execute action a with pa A p rameters p Assignment call 1 v obj op p 2 v op p Il 1 execute o
19. ses 10 D32 2 Simulator for CML Public COMPASS Debug test test cml CML Compass Project AT Gay a Dom Debug Debug E 7 B variables e Breakpoints Observable Event History 23 el Quick Launch 1 CML Model 8 CML Debug Target vf CML Debugger test cml ES A E outline Fl CML Event Options 23 SE channels a bc process A begin Ga gt c gt Skip end process B begin state a int operations Init gt 0 e tmit E Init b gt Skipl end process C A 8 E Console H Tasks a S alele teem 85 Quick Launch 1 CML Model CML Debugger State for tock B 4 a undefined State for tau ASingleGeneralAssignnentStatenentaction gt AskipAction Child of B B 4 a undefined Debug thread sending Status event to controller WAITING FOR ENVIRONMENT The supervisor environment picks tau ASingLeGeneralassignnentStatementAction gt ASkipAction Child of B Debug thread sending Status event to controller SUSPENDED writable Insert 16 20 Figure 8 The interpreter is currently suspended because of a breakpoint hit marked with gray 1 3 4 Error reporting If an error occurs a dialog will appear with a message explaining the cause of the error Furthermore the location of the error will be marked in the editor view In Figure 9 a post condition has been violated This is described in the error dialog and a gray marking shows where in the model it happened test c
20. ss selection dialog is shown 1 3 Interpretation As mentioned at the start of Section T there are four possible ways to interpret a model each of them will be described 1 3 1 Animation Animating a model is achieved by choosing the Animate radio button in the launch configuration as described in the last section this is also the default behavior In this mode of operation the user has to pick every observable event before they can occur through the GUI In a small CML model is being animated in the debug perspective The fol lowing windows are depicted Observable Event History This window is located in the top right corner and shows the observable events that have been selected so far In only a tock event has occurred so far CML Event Options This shows the possible events that can occur in the current state of the model To make a particular event occur you must double click it Fur thermore to see the origin of a particular offered event you must click it and the location of every involved construct will be marked gray in the editor window Editor This shows the CML model source code with a twist As seen in parts of the model is marked with a gray background This marking is determined by D32 2 Simulator for CML Public COMPASS Debug test test cml CML Compass Project a ATINA eas a BH Dem Debug 35 Debug Y B variables e Breakpoints Observable Event History 3 Sate Y O A CML Model
21. t so this should be the first thing to do After setting the project name and process name the Apply button must be clicked to D32 2 Simulator for CML Public COMPASS save the changes to the launch configuration If the project exists is open and a process with the specified name exists in the project then the Run or Debug button will be active and it is possible to launch the simulation as shown in Figure 3 Furthermore the decision of whether to animate or simulate the model is decided by the two radio buttons in the buttom the default setting is to animate Run Configurations Create manage and run configurations Run CML Model Q CBx Bs Name Test Main Develop E Common Y CML Model PORE OA Project testi Browse New_configuration Eclipse Application Ed Java Applet E Java Application Animate Simulate Ju JUnit Animate D Simulate J JUnit Plug in Test m2 Maven Build 4 OSGi Framework VDM PP Model L VDM RT Model E VDM SL Model Top Process Process A Search Appl Re t Filter matched 13 of 13 items PPly ever Figure 3 The configuration dialog after a project and process has been selected This launch configuration will now appear in the drop down menu as described at the beginning of this section The actual interpretation will be described in Subsec 1 2 Launch Via Shortcut Another way to launch a simulation is through a shortcut in the COMPASS explorer view in
22. tus event to controller RUNNING observable step by C Observable trace of C tock a c Eval Status Skip Debug thread sending Status event to controller FINISHED Figure 7 The model has just been simulated 1 3 3 Run Debug In addition to the two modes of operation Animate and Simulate the standard modes Run and Debug also exist The Run mode will interpret the model with out ever breaking on any breakpoints The Debug however will stop on any enabled breakpoint in the model When a Debug configuration is launched the perspective changes to the Eclipse Debug Perspective however Run will stay on the perspective that is currently ac tive To create a new breakpoint you have to double click on the ruler to left in the editor view if created this will insert a small dot to the left ruler Breakpoints can be set on processes actions and expressions only Double clicking on a existing breakpoint dot will remove it In Figure 8 a debugging session is in progress Here a breakpoint on the body of the Init method has been hit and the interpreter has been suspended At this point the current state can be inspected in the variables view From here it is both possible to resume or stop the debugging session If the resume button is clicked the interpretation is resumed and the stop button stops it Note state inspection still has flaws and is not yet enabled in the development relea
Download Pdf Manuals
Related Search