CoreASM Editor & Debugger — Manual
Contents
1. 21 22 function controlled leftChop Agents gt CHOPSTICK 23 function controlled rightChop Agents gt CHOPSTICK 25 function controlled name Agents gt String 27 derived CanPickBothChopsticks chopOwner leftChop self undef and chopOwner rightChop self undef 29 init initrule 31 main program of every philosopher 32rule Philosopher par if hungry self and not eating self then if CanPickBothChopsticks then StartEating else print name self is hungry but can t eat if not hungry self and eating self then 41 StopEating 43 hungry self flip 44 endpar 47 starts eating 48rule StartEating 9 par 50 chopOwner LeftChop self self 51 chopOwner rightChop self self 52 eating self true 3 print name self starts eating 54 endpar lt gt instance in plug in EI Java Debug DiningPhilosophers v Used Plugins StandardPlugins 8 OptionsPlugin 8 MathPlugin v Signatures CHOPSTICK PHILOSOPHERS eating chopOwner hungry leFtChop rightChop name CanPickBothChopsticks S initRule Rule Definitions Philosopher StartEating StopEating gt Flip initRule E CoreASM AST Tree View m Figure 1 Overview of the Eclipse IDE showing the CoreASM editor and its outline view The editor offers a lot of features to support the user to create examine and correct or revise specifica2. highlighted by a green symbol interpreter Compare View Shows the state of the Core All selected steps in the Debug view ASM execution for specific are shown for comparison Optionally steps just differences are presented 4 2 Adding Removing Breakpoints A breakpoint can be set from within the source editor by double clicking on the ruler or right clicking it and selecting see Fig 5 48rule StartEating 49 par 50 chopOwner LeftChop self self 51 chopOwner rightChop self self ec a en E a om Toggle Breakpoint Double Click ts eating Disable Breakpoint Shift Double Click Figure 5 Line breakpoint set at line 52 of the DiningPhilosophers specification There are three different types of breakpoints see Fig 6 e Watchpoints They will be added if the selected line starts with function or uni verse They will suspend the execution whenever the value of a function universe changes or is being read 10 4 Debugging a Specification e Method breakpoints They will be added if the selected line starts with rule They will suspend whenever an update occurs from a line within the selected rule s body e Line breakpoints They will be added if none of the above breakpoints can be added They will suspend whenever an update occurs from the selected line DiningPhilosophers coreasm line 36 DiningPhilosophers coreasm lines 26 38 PhilosopherProgram 5 DiningPhilosop
3. 10 S Verbosity Log messages with at least the Following severity level Fatal v Dump updates after each step Dump entire state after each step Dump final report at termination Mark the end of each step Print the selected set of agents after each step qee F Filter matched 10 of 10 items D Run Close Figure 3 Default Run Configuration for the DiningPhilosophers specification 4 Debugging a Specification A CoreASM specification can be started for debugging by either using the debug button of the toolbar see fig 2 a or by selecting a Debug Configuration via the down arrow beside this button Another option is using the eclipse menu Run Y Debug Configurations If the specification has been paused by using one ot the pause buttons or a break point has been reached Eclipse asks the user to switch to the debug perspective Confirming this question the user will be shown a screen similar to fig 4 This debug perspective contains the views from top left to bottom right described in table 4 on page 9 The debbuging of CoreASM specifications is described in detail in the following sections 8 4 Debugging a Specification 8 WS Debug SampleSpecs DiningPhilosophers casm Eclipse SDK yw YY B amp W File Edit Navigate Search Project CoreASM Run Window Help we oh amp b gt ial Sahn amp rYO Q SS Vv v
4. chopowner Only show updates From agent Herbert chopOwner c5 Albert _ Albert eating Herbert False False eating Albert true true eating Sina False False a The filter of the Update view helps the user to b The Compare view shows the functions for dif concentrate on the updates of a specific agent ferent states side by side To focus on the changes between those states the filter can be used to hide functions with equal values Figure 11 Both the Update and the Compare view offer filters to focus on certain aspects A multi line comment for the HelloWorld specification Fach specification has to start with CoreASM lt name gt CoreASM HelloWorld A single line comment previous to the block of used plugins use Standard use Modularity the initial rule definition init HelloWorld The path to an included CoreASM module has to be gtven within double quotes include PrintHelloWorld casm rule HelloWorld seq print we proudly present next PrintHelloWorld IIm ow WW Fe 14 References The module S amp PrintHelloWorld casm implements the output of Hello World In differ ence to a main specification its header starts with CoreModule lt module name gt and an init rule is not allowed here modules can be included in CoreASM specifications CoreModule PrintHelloWorld use Standard rule PrintHelloWorld print Hello World Further exam
5. the Breakpoints view where all steps are listed Multiple steps can be selected while holding for single selection or holding f to mark a range of steps Steps which are marked by a are intermediate steps resulting from sequential steps To clear up the Compare view the filter option can be used which results in hiding all corresponding functions with equal values see fig 11 b p 13 7 Excursus Modules in CoreASM Hello World The following specification Gj HelloWorld casm implements an extended Hello World This specification itself specifies the output of we proudly present It further demonstrates the use of modules by including the module G amp PrintHelloWorld casm which implements the output of Hello World As a result the rule PrintHelloWorld can be called from the initial rule of the main specification HelloWorld O ON onow trewhnd Fe N wmO Nw NY FR KF BPR RF BP rR Fe WoNnNnNrr OVO AN DOK WN F CO 13 7 Excursus Modules in CoreASM Hello World CoreAsM Update View 53 5 CoreASM Compare View 3 ial lia hungry sina v Show updates from all agents Name Step 14 i Show differences only D chopOwner e name Herbert Herbert e Only show updates From agent Fredrich i i D hungry Albert name Albert Albert Albert hungry Juan Only show updates from agent Albert eating Albert Only show updates From agent Juan chopOwner c1 Albert Albert
6. CoreASM Editor amp Debugger Manual An advanced Editor and Debugger for CoreASM http uni ulm de in pm projects coreasm https github com CoreASM http coreasm org Marcel Dausend Markus Muller and Michael Stegmaier marcel dausend markus mueller michael 1 stegmaier uni ulm de Version 1 7 0 SNAPSHOT March 2013 1 Introducing Notes The CoreASM Eclipse plugin extends the Eclipse IDE for editing debugging and executing CoreASM specifications This version is a major upgrade from the latest version 0 6 8 beta It offers a reimplemented and enhanced editor which integrates the latest jparsec parser This new editor performs noticeably better than the old one and introduces some valuable features to revise specifications like quick fixes and syntax checks Furthermore CoreASM specifications can be investigated in an intuitive as well as comprehensive manner with the new debugger which makes use of the regular Eclipse debugging components The reimplementation and enhancement of the editor component has been implemented by Markus M ller during his diploma thesis 3 The debugger has been implemented as part of a bachelor thesis by Michael Stegmaier 5 and has been introduced on the ABZ conference 2012 in Pisa 2 Both theses have been supervised by Prof Dr Helmuth A Partsch head of the institute of Software Engineering and Compiler Construction at the University of Ulm The work has been initiated and mentored by Marce
7. difying their values To keep an eye on a specific function for a given location a corresponding entry in the Expressions view see fig 8 a can be created by right clicking on the desired entry and selecting from the menu see Fig 7 b Additional expressions can be added to the Expressions view by pressing 444 new expression and entering either a universe name or function name and its location see fig 8 b En tering a function name without its location e g hungry will result in showing a container 11 6S Expressions IN hungn Sina hunagny Fredrich hungry Juan hungrylAlbert hungry Herbert SP Add new expression a A function and its values for each location Sina Fredrich Juan Albert Herbert False False true true true 4 Debugging a Specification 6S Expressions xa i p w O P w yY Name Value xay hungry Sina False xay hungrylAlbert true EM hungry Sina or hungry Albert true zay eating Albert False xay leftChop Fredrich c3 P Add new expression i b Some functions of specific locations and their values The marked entry shows a user defined expression and its value Figure 8 The Expressions view shows user selected universes functions for either all or one specific location and evaluates user defined expressions depending on the current state of all it s locations and values see Fig 8 a E
8. e and press or click on the Finish button A CoreASM specification can be created in at least two ways One way is creating a new text file with a name ending on casm or coreasm within the project of choice An alternative is the new wizard 1 Choose from the Eclipse menu or press Ctrl N 2 In the appearing New dialog select and press or click on the Neazt button 3 Preferably select a project from the workspace as a container for the specification This can be done by either using the file selection dialog or manually entering the project s name 4 Give the new specification file a name ending with amp casm or S coreasm and press or click on the Finish button The structure of a CoreASM specification and the CoreASM language are described in CoreASM Language User Manual 4 p 7 A Hello World example is given in section 7 Shttp coreasm svn sourceforge net viewvc coreasm engine carma trunk doc user_manual CoreASM UserManual pdf 6 3 General Introduction to CoreASM and its Editor 3 2 Executing a Specification A CoreASM specification can be executed using Carma 4 p 4 or the CoreASM Eclipse plugin There are two ways to execute a CoreASM specification in Eclipse The easiest way to run the specification of the currently selected editor component is to click on the green run button of the eclipse toolbar see fig 2 a and fig 2 b As a result the selected specification
9. ent step Each update is a triple consisting of the function and its location the value and the type of action The action type is an internal CoreASM specific value By double clicking on an update entry the source of this update inside the specification is presented to the user Updates that correspond to an active breakpoint are marked by a green symbol To focus on the updates of a specific agent a filter option can be applied see fig 11 a E dle E EER i io Outline j E CoreASM Update View sg i 7 45 par a Sin chopOwner c1 Albert updateAction alg es eal Le eatin Albert true updateAction 51 chopOwner rightChop seLf self a ut e 52 eating self true A chopOwner c5 Albert updateAction 53 print name self starts eating GD output Albert starts eating printAction 54 endpar 57 stops eating 58 rule StopEating 29 par SC chopOwner LeftCchop seLf undef 61 chopOwner rightchop self undef a Figure 10 The Editor left and Update view right The statement in the specification causing the marked update is highlighted It is located in a line with an active breakpoint 6 What has been changed The Compare view enables analyzing the state of the machine over the time Therefore the view shows all functions and their values for selected steps of the machine side by side The selection has to be performed within
10. gin is developed with Eclipse Juno on Windows and Linux 6 bit Systems with Oracle Java SE 1 7 installed The following infras tructure is required for the CoreASM Eclipse plugin e Java SE Runtime Environment 7 http www oracle com technetwork java javase downloads index html e Eclipse IDE for Java Developers version Juno suggested http www eclipse org downloads e A program to unzip the CoreASM distributable e g 7 Zip http www 7 zip org The installation requires the following steps 1 Check if the required software see above is already installed on the target machine and if not install the software 2 Extract the CoreASM Eclipse plugin SG org coreasm eclipse_ lt version gt zip to the plugin folder of your eclipse installation For example on a 32bit Windows system the standard destination would be SC gt Program Files gt eclipse gt plugins On a linux system the destination depends on the distribution and installation method e g on an Ubuntu system the eclipse folder would be Gusr gt lib gt eclipse gt plugins if it has been installed from the ubuntu s standard software repository In this case super user privileges are needed to access the folder For people without super user privileges Download a version of the Eclipse IDE from the above mentioned website and extract it to a user accessible destination 3 Check if the CoreASM plugin has been extracted to the plugin destination There should be a d
11. hers coreasm access and modification eating Figure 6 Three different kinds of breakpoints listed in the Breakpoints view A breakpoint can be disabled by choosing from context menu of the ruler or by un checking the box in front of its entry in the Breakpoints view By enabling the Skip All Breakpoints toggle switch gt all breakpoints are discounted during an execution without the need of changing the set of active breakpoints 4 3 Watching Functions and Expressions The Variables view see Fig 7 a allows to watch and examine the values of all available functions of the machine s state All values that have been changed due to the last update set are highlighted in yellow color The value of a function at a specific location can be changed by clicking on its value entry changing the value by modifying the text and pressing Enter This modification is applied directly to the state of the machine and will not induce an extra update this feature has to be used with caution G variables 25 S Breakpoints trick select All Cria 2 i A al R3 Copy Variables Ctrl C 5 ame alue l ER 4 Find Ctrl F 3 p ert a Change Value el Last Selected Agents InitAgent A _ P fal rightChoplFredrich 0 B M Eat a The Variables view shows all functions at its loca b Context menu of the Vari tion their value definition type and current type ables view Figure 7 The Variables view for inspecting function and mo
12. irectory likeG eclipse gt plugins gt org coreasm eclipse_ lt version gt 4 Start eclipse by executing the file eclipse in the directory G eclipse 2please send a request by e mail to marcel dausend uni ulm de 4 3 General Introduction to CoreASM and its Editor 3 General Introduction to CoreASM and its Editor The CoreASM plugin for Eclipse offers two components which are designed to support writing CoreASM specifications The redesigned editor see fig 1 middle and an outline view of the currently open CoreASM specification see fig 1 right Moreover a view showing the AST of the current specification is provided to assist for development JO Java SampleSpecs DiningPhilosophers casm Eclipse File Edit Navigate Search Project CoreASM Run Window Help riv mv oe ey Ov Qv Gv amp o vy liv ivt ov j Package Explorer 53 A DiningPhilosophers casm 38 Ss 5 n A AS 9 CoreASM DiningPhilosophers v E SampleSpecs o luse StandardPlugins o 2use OptionsPlugin 68 DiningPhilosophers casm 2use MathPLugin 6S ListsAndMaps coreasm 4 PlotterExample coreasm Senum CHOPSTICK cl c2 c3 c4 c5 p a 6enum PHILOSOPHERS Albert Herbert Fredrich Sina Juan 6S RailroadCrossing coreasm m Reattore coreasm 8function controlled eating Agents gt BOOLEAN VendingMachine coreasm E 9 function controlled chopOwner CHOPSTICK gt Agents 20 function controlled hungry Agents gt BOOLEAN
13. is executed by the CoreASM engine and the output is shown inside the Console view of Eclipse see fig 2 e Running a specification the first time EAA ER DA C oO vv ophers casn G8 1 DiningPhilosophers casm ares Ma Run As gt 1g Philos 1 Project D CoreASM Run Wi ts g ol g g g G v g B ted on Au Run Configurations Organize Favorites cS By a ff t v Ov ophers casl Run DiningPhilosophers casm sed by Ra a Relevant excerpt of b Running the Dining c by selecting its Run Con the Eclipse tool bar Philosophers specification figuration Javadoc Er Problems E Declaration E Console 53 S Coresi DiningPhilosophers TABLE cl Herbert c2 Fredrich c3 Sina 1 Project CoreASM Run Wir Fredrich starts eating Herbert is hungry but can t eat l Sina 1s hungry but can t eat Sina 1s hungry but can t eat Fredrich stops eating Juan starts eating E p Ls W 9 BD About CoreasM B G39 CoreASM Help E 4 Ce a t Pause Engine d The CoreASM menu e The output of the DiningPhilosophers specification Figure 2 Running a CoreASM specification automatically creates a Run Configuration which specifies some options for the execution of the related CoreASM specification Fig 3 on page 7 shows the default Run Configuration for the DiningPhilosophers specification The different options for a certain specification configure the termination condition f
14. k Philosopher Philosopher 62 eating self false i i eating Herbert false updateActi on right Chop Herbe c1 ied Sd prm name self stops eat ng hungry Herbert False updateAction rightChop Albert c5 i c5 6 endpar i i 5 j rightChop Sina i c3 i c3 rightChop Fredri c2 c2 57 right Chop Juan c4 c4 68 return a random BOOLEAN hungrylalbert False False 69rule flip z E i iz za return bin ungry Fredric rue rue 71 choose c in BOOLEAN do hungry Sina true true l 72 b i 6 e i a lt gt 2 OO L I L J El console X Ex be we FS mS o CoreASM DiningPhilosophers TABLE cl Herbert c2 Fredrich c3 Sina c4 Juan cS Albert cl Figure 4 Overview of the Debugger 4 1 Stepping Through a Specification Once the execution of a specification in debug mode is paused one can analyze a specification step by step There are three different kinds of stepping which can be forced by pressing the related buttons in the toolbar of the debug perspective or use a keyboard shortcut e E Step Return Executing all statements and stopping at the next sequential block o Q Step Over Executing a single step of the machine E Step Into Executing a single step which can also be a step inside a sequential block Debugging of imperative languages differs in many points from debugging Abstract State Machines One difference is that in a CoreASM specification without sequential
15. l Dausend Meanwhile the project has been merged with the official CoreASM development project www coreasm org and is provided as open source via github 1 ljparsec 2 0 1 http jparsec codehaus org 2 Contents 1 Introducing Notes 2 6 7 Installing the CoreASM Eclipse Plugin 2 1 System Requirements 2 2 0 00008 es General Introduction to CoreASM and its Editor 3 1 Creating a Specification 2 0 020080 G 3 2 Executing a Specification 2 000004 Debugging a Specification 4 1 Stepping Through a Specification 4 2 Adding Removing Breakpoints 4 3 Watching Functions and Expressions Taking Care of Updates What has been changed Excursus Modules in CoreASM Hello World References Contents ee ee ee 10 12 12 12 14 3 2 Installing the CoreASM Eclipse Plugin 2 Installing the CoreASM Eclipse Plugin The daily version of the CoreASM Eclipse plugin can be received via 1 github A guide for building and executing the development version can be found on the referred website too This installation guide refers to a S org coreasm eclipse_ lt version gt zip distributable which enables non developers to easily try out the latest version of the CoreASM Eclipse plugin by themselves Such a distributable can be directly received from the authors 2 1 System Requirements The current version of the CoreASM Eclipse plu
16. o ve Gy amp EY Java HF Debug Debug X Y Breakpoin X m 69 Variables x gt H amp f Expressions X O p Xx 3g o m DiningPhilosophers casm ASM Specific x P ox A e S Name e S DiningPhilosophers casm ASM Specific Name Value oe ay eating Albert Gf SampleSpecs iba ht kf eccehence chopOwner aP Thread main Suspended I DiningPhilosophers casr chopownertcz Herbert SY hungan DiningPhilosophers casm Philos v Z DiningPhilosophers casr eating Fredrich False Ub Add nw ERER l DiningPhilosophers casm StopE eating Sina true DiningPhilosophers casm Philos eating Albert False DiningPhilosophers casmPhilos estingterber true DiningPhilosophers casm Philos r 2 ____ _ False Je DiningPhilosophers casm Philos lt C EEE lt gt DiningPhilosophers casm Philos f E at Phil No details to display For the F DiningPhilosophers casm Philos current selection DiningPhilosophers casm initRu Bs 9 CD lt gt E i S DiningPhilosophers casm z 3 6 outline CoreASM Update View 58 moeng CoreASM Compare View aa 7 57 _ stops eati ng output Herbert stops eating printAction Name Step 4 Step 2 cq ig a chopOwner c2 undef updateAction 50 chopOwner LeftChop self undef chopowner ct undef updateAction 61 chopOwner rightChop self undef b False updateAction Callstac
17. or a CoreASM execution and the verbosity of its output The second option to start a specification is to use a Run Configuration If a Run Configuration for a specification exists or after it has been created its specification can be executed by selecting it The down arrow on the right hand side of the Run button or the Run Configuration menu can be used to open a selection list see fig 2 c To access a Run Configuration via the Eclipse menu select Run X Run Configurations The execution of a specification can be paused resumed and stopped by clicking one of the buttons see fig 2 a located under the CoreASM menu or selecting an entry from that menu see fig 2 d 4Carma can be received at www coreasm org download T 4 Debugging a Specification S gt Run Configurations v a Bs Create manage and run configurations Q C B Xx E Name DiningPhilosophers casm v G8 ASM Specification Source E DiningPhilosophers c Eclipse Application Project SampleSpecs Browse E5 Java Applet Specification DiningPhilosophers casm Browse Java Application Ju JUnit Termination condition JG JUnit Plug in Test v Upon errors wv Upon Failed updates m2 Maven Build When a step returns an empty set of updates A Mwe2 Launch OSGi Framework _ When a step returns the same set of updates as the previous one v When there is no agent with a defined program After this many steps have been performed
18. parts all different step actions result in collecting and aggregating all updates of the current step The execution will stop again before the first statement of the next step will be computed so that one can examine the update set before the state of the machine is updated To continue the execution of the interpreter click on one of the resume buttons 9 4 Debugging a Specification Table 1 Overview of the debugging components in fig 4 View Interaction Debug Shows the currently executed pierastion ae steps are taken into account bean eer bad ep Breakpoints Lists all Breakpoints of the Breakpoint s can be disabled or re workspace enabled eh deleted exported imported and used to navigate to its related source destination Variables Shows the state of the Core The state of the CoreASM execution ASM engine can be investigated and manipulated Expressions Shows user defined CoreASM User defined expressions are passed to expressions and their values the interpreter and evaluated based on the current state of the execution Editor Shows the statement to be Changes to the specification during evaluated next debugging do not influence the cur rent execution Update View Shows all updates optionally An update can be used to navigate to restricted to a specific agent the statement of its origin Updates which are collected up to now which correspond to a breakpoint are during the current step of the
19. ple specifications e g the DiningPhilosophers specification are part of the distributable and can be found in the folder GsampleSpecs References 1 M Dausend R Farahbod M M ller A Raschke and M Stegmaier The CoreASM Project https github com CoreASM coreasm core 2012 2 M Dausend M Stegmaier and A Raschke Debugging Abstract State Machine Specifi cations An Extension of CoreASM In Proceedings of the Posters amp Tool demos Session iFM 2012 amp ABZ 2012 2012 3 M M ller Entwicklung eines Editors f r CoreASM Redesign nach Software Engi neering Methoden Diplomathesis University of Ulm 2012 4 R Rarahbod CoreASM Language User Manual engine version 1 5 beta edition 2011 5 M Stegmaier Entwurf und Implementierung eines Debuggers fiir Abstract State Ma chines in CoreASM Bachelorthesis University of Ulm 2012
20. tions e syntax highlighting e syntax checking e warning and error markers which are also shown in the eclipse problems view e quick fixes for several issues e tooltips showing parser information e bracket highlighting 5 3 General Introduction to CoreASM and its Editor The outline view shows an overview of the specification corresponding to the currently open editor The user can decide if the entries should be shown in a structured way where use statements signatures and rules are grouped or in a flat representation Also the user can decide if the entries should be ordered alphabetically or in textual order of the specification The buttons at the top of the outline view can be used to toggle between those configurations Moreover entries in the outline view can be used to navigate to their corresponding definition inside the specification by simply clicking on the desired entry If the current specification cannot be parsed correctly the outline view is marked as outdated In this case the user is advised to correct the specification before he can continue to use the outline view 3 1 Creating a Specification To create a CoreASM specification an existing project in the current eclipse workspace is required as a container for the new specification A new project can be created in three steps 1 Choose from the Eclipse menu or press Ctrl N 2 Choose from the New Project dialog 3 Give the new project a nam
21. xpressions can be removed by selecting at least one entry and pressing Del or using the buttons Another way to inspect expressions on the fly is marking an expression inside the Editor view or moving the mouse over a single statement By doing so a tooltip will be presented that shows the result of the evaluation of the marked expression based on the current context of the machine s evaluation i e the global state and the current computation context Two examples are given in fig 9 31 main program ot every philosopher 32 rule Philosopher par 34 if MOACASA E EA then false hrtEating else pPickBothChopsticks then 38 print name self is hungry but can t eat a The expression at the line breakpoint is eval uated on the fly 32 rule Philosopher par 34 if hungry self and not eating self then 35 if CanPickBothChopsticks then 36 StartEating f a7 alae Derived Function CanPickBothChopsticks true print name self is hungry but can t eat b The result of the derived function CanPickBothChopsticks is presented as a tooltip when the mouse cursor hovers over its calling statement Figure 9 During debugging expressions can be marked inside the Editor view so that the result will be shown as a tooltip 12 7 Excursus Modules in CoreASM Hello World 5 Taking Care of Updates The Update view see fig 10 lists all updates which have been computed during the curr
Download Pdf Manuals
Related Search