Sphinx User Manual - School of Computer Science
Contents
1. Ex Packagelmport Ba pac im PackageMerge ix Dynamics Bg Structure 8 ET a is 5 Problems Javadoc Declaration EN mlt E 7 WorldConstraints gt 4 E UML Name WorldCo i2 IE lt gt Profile Visibility public arance z z pen ARRE Context Undefined eee np Specification XlIv0 g 0 cc 10 t el 141 36 Advanced us Constrained element 9 Q oP x Fd 3 3 MODEL SYSTEM DYNAMICS Now that we defined the structure of our system we can define its discrete and continuous dynamics Since system dynamics can become rather complicated we will model hierarchically We start with the overall system dynamics and will supply details in sub diagrams As cautious modelers we first define a safety condition before we model any behavior Le Define the safety condition select the tab UML of the properties view and scroll to the precondition and postcondition section Click the button on the postcondition to open the postcondition window and add a new Constraint eoo type filter text Postcondition DurationConstraint InteractionConstraint IntervalConstraint TimeConstraint w e lel lo Cancel OK On the constraint definition window name the constraint and optionally select the constrained element In our example of the bouncing ball the safety condition will demand that the ball s height is positive but no larger than its starting height thus we2. Select where to apply the geometric relevance filtering result Applicable open goals g gt 0 h gt 0 t gt 0 O lt c c lt 1 v 2 2 g H h Select All Deselect All Back Next gt Cane Beine Commit the changes to the source code repository or load the partial proof in KeYmaera to continue proving
3. 0 amp t gt 0 amp O lt c amp c 1 amp v 2 lt 2 g H h amp H gt 0 3 amp undefinedVariable e Code completion Nproblem initial state characterization g gt 9 amp h 0 amp t gt 0 amp B lt c amp c 1 amp v 2 lt 2 g H h amp H gt 9 re gt Zi XL 11E namics lE amp umping t und IE ick l gt t YA 2 lt gt ansitions M d E istcondition z e Keep overview with Code Folding using in vertical editor bar KRY bouncingball key 52 pu Hybrid model of a bouncing ball amp functions amp NprogramVariables amp Nproblem e Quick peek folded content as tooltip in vertical editor bar Open the quick outline using Ctrl O Windows Unix or Cmd O Mac Syntax and cross references are checked on the fly Get cross references to variables and other code completion help by pressing Ctrl Space Use code folding Hover the mouse over a folded code snippet to take a quick peek 8 TEXTUAL MODELING Kg bouncingball key 2 e t Hybrid model of a bouncing ball eE functions e Whenever you save a d textual model Spnx generates a ATEX representation of the model GRAPHICAL MODELING Abstract This chapter introduces the graphical modeling features of Spnx Spnx uses UML class diagrams to model the structure of a hybrid system and uMr activity diagrams to model their behavior G
4. Figure 2 2 The KeYmaera console ceo scr Open the quick outline Syntax checking fig textual codecompletion Code folding Quick peek into folded code Create a new UML model Create a new class Flag properties as constant or variable Define constraints using the d popup editor Add a new constraint Select the constrained element Specify a constraint as OpaqueExpression Enter d as constraint specification language Use d to specify a constraint body Use d to specify the continuous dynamics Hierarchically decompose behavior Overview of bouncing ball dynamics Add a new activity diagram Discrete dynamics of the bouncing ball example Create a new hyperlink Set a default hyperlink Transform a UML model into a textual d model Figure 4 1 Comparison of textual models Proof comparison Export an arithmetic goal Search an open goal Export file Select hiding suggestions Select applicable goals UI UY N CON NNN DO 10 11 11 12 12 12 13 13 14 14 15 15 16 16 17 17 17 19 20 21 21 22 25 25 INSTALLATION Abstract This chapter introduces the installation procedure of Spnx and the subsequent configuration steps to setup KeYmaera as hybrid verification tool Contents 123 Show Additional Views 1 2 4 Add Modeling Templates 131 Installation from Eclipse Update Site 1 12 ConUsSurdUO 53143939 0442093 Se iii 2 1 2 1 Install and Configure KeYma
5. jumping i e the discrete dynamics does nothing 1 In the Model Editor view add a New Activity Diagram to the DiscreteDynamics behavior created above using the context menu w _ veriry souncing sar J Validation gt New SysML Child gt E Export gt e u Import B Outline E Model Explor New Child gt Ma as Y Es Model New Table By Create a new Class Diagram 7 lt Package Import gt U m Delete Bo Y Create a new Communication Diagram n El Rename F3 amp Create a new Component Diagram gt t_ ownedRule 2 Create a new Composite Structure Diagram Y t ownedBehavior 1 Undo 36Z Y Create a new Deployment Diagram Redo 362 f Create a new Package Diagram gt L posteonidition 1 C ET Create a new Sequence Diagram precondition 1 ut gt t edge 6 Copy BC te Create a new StateMachine Diagram gt L node 6 Paste Create a new UseCase Diagram e Ol 2nhiancr Ball Enable write 2 Add an Initial Node to denote the start of the discrete dynamics 3 Connect the initial node to a decision node This is the start of the if condition 4 Add an Opaque Action to set the new velocity and another one to reset time Tag both with the stereotype Deterministic Assignment to define that they will set the value of variables in a deterministic manner Click the label of the action and set the values of velocity v c v and time t 0 5 Add a Merge Node an Activity Final Node and set the c
6. on the left side and add it by clicking the right pointing arrow eoo Language C C Java Natural language Fs selected elements D S E cancel EOS 3 Click into the body field and provide the constraint specification in d In our example we want the ball s height to be between o and its initial height H Click somewhere outside the body field e g reselect the name field to adopt the new body specification 13 Specify the constraint using a new OpaqueExpression Enter d as constraint specification language Specify the constraint body in d and confirm your definition by clicking outside the text field 14 GRAPHICAL MODELING eoo Create a new OpaqueExpression Name Valid Height Language i a oR x BO O lt h amp h lt H dL Visibility public Behavior Undefined E Type Undefined op r UML Profile Coe GE 4 Exit the constraint specification window the constraint window and the postcondition window by clicking OK on each Next we define the overall system dynamics These consist of the continuous dynamics the ball falls and jumps and discrete dynamics when it hits the ground the ball bounces back We want the ball fall and jump arbitrariliy often Thus discrete and continuous dynamics are repeated non deterministically many times in a loop 1 Add an Initial Node from the palette This node represents the start of
7. our system 2 Add a Merge Node from the palette This node represents the loop start 3 Connect the initial node and the merge node with a Control Flow The default condition for such a flow is true which means that it is executed unconditionally The condition can be hidden using Filter gt Manage Connector Labels from the context menu of the control flow 4 Add an OpaqueAction from the palette and connect the merge node with a control flow to the opaque action This action repre sents the continuous dynamics of our system On the properties view choose a descriptive name for the action e g Fall and Jump and add the stereotype Dynamics on the properties view The opaque action represents the continuous dynamics in our sys tem Click the Fall and Jump label to open the d popup editor Define the continuous and define the dynamics using a differential algebraic equation dynamics of a hybrid system as differential algebraic ftruel equation in the d popup editor of an OpaqueAction with true stereotype Dynamics dynamics h zv v z g t 1 h gt 0 5 Add a Behavior Call Action from the palette Although the discrete dynamics of the bouncing ball example is rather simple we want to have a separate activity diagram to demonstrate decomposition 3 3 MODEL SYSTEM DYNAMICS 15 We create a new behavior named DiscreteDynamics Use Call Behavior Actions to decompose eoo the dynamics and Create a new Ca
8. properties view or apply readOnly with the popup editor E Dynamics Bg Structure 23 y Problems Javadoc il Declaration E Console E Properties 3 Eg lied st 1114 IF1 Applied stereotypes Dl al X Profila gt El Constant from distatic Appearance Advanced 5 Model associations between your classes as appropriate Cur rently these are for documentation purposes only and do not influence code generation 6 Select Constraint from the palette to define conditions that must always be true In the bouncing ball example we add constraints on gravity must be strictly positive the damping coefficient must be positive and less than 1 time must be positive and the initial height of the ball must be positive The popup editor for constraints in d supports syntax highlighting and code com pletion You can confirm the constraint by pressing Ctrl Enter or leave the popup editor with Esc Define constraints using the d popup editor Add a new constraint as postcondition for a UML activity Select the constrained element 12 GRAPHICAL MODELING a system object World Ball 12 Constraint constant c Real 1 h Real 1 m DataType t Real 1 v Real 1 BallConstraints ES N constant g Real 1 H Real 1 dL H gt 0 1 DurationObse FE Enumeration I pe z i A InterfaceReali 0 980 ches LEO lt t Link t l t
9. ra EB ro rn Ej E n g y Gt m ax En Package K bouncingball key E bouncingball notati Ej Property HE bouncingball uml 3 Reception EB src gen system Ball di RedefinableT bm JRE System Library I25E li h Real 1 a n o v Real 1 Ge Edges E i H Real 1 E Task List 83 a p Abstr Ale a TEE x E K Association v Association Br Find k All Verify 3 AssociationCl Y Uncategorized CEL i Verify Bouncing Ball T Dynamics Pg Structure 2 Problem Decl Console E Properties 23 HE voc Ei Propertyl Applied stereot Tz Outline 52 D M ii el TX ume Profil Constant from distatic Appearance Advanced 2 On the properties view select the profile element Use System to flag the main system class and Object to flag other agents in the system 3 From the palette select Property and click on a class to add a new property We add three properties to the class World a clock t a damping coefficient c and gravity g 4 On the properties view you can apply stereotypes Constant or Variable to these properties to flag them as either being constant or variable By default all properties are variable Alternatively you can use the uMr tab to set a property read only or use the popup editor to add readOnly Flag properties as constant or variable using stereotypes or h Real 1 l c PrimitiveTypes Real readOnly setting readonly to true false on the UML tab of the
10. v42 lt 2 g H h H gt 0 gt forall R v O forall R h_0 forall Rt x Back Next gt Cancel Finish 4 Select or create a new file to export click Finish Select or create a new file to export 22 PROOF COLLABORATION eoo Create Open Goal File Create a new Open Goal File The selected goal will be exported into this file Enter or select the parent folder sphinxtutorial src proof A sphinxtutarial bin 2 META INF src model proof src gen File name invariant goal Advanced gt gt 9 lt Back Next gt Cancel 4 4 IMPORT GEOMETRIC RELEVANCE FILTERING RESULTS 1 Open the context menu of a proof and click Import 2 Select Sphinx Geometric Relevance Filtering Result 3 Select a file from the file system or from the Eclipse workspace 4 Select the hiding suggestions to import into the proof usually all Select hiding and click Next suggestions 4 4 IMPORT GEOMETRIC RELEVANCE FILTERING RESULTS 23 Geometric relevance filtering Select geometric relevance filtering result O frome sytem YB From workspace sphinxtutorial src proof invariant grf Browse Hide left 4 get 0 Select All lt c Mecel Deselect All gt Hide right Select All Deselect All Finish 5 Select the applicable goals usually all and click Finish Select applicable goals eoo Goal selection
11. SPHINX USER MANUAL STEFAN MITSCH Computer Science Department School of Computer Science Carnegie Mellon University Johannes Kepler University March 2013 Stefan Mitsch Sphinx User Manual March 2013 VERSION 1 0 0 CONTENTS 1 INSTALLATION 1 1 1 Installation from Eclipse Update Site 1 1 2 COMMSUTANON u 2 Oak Oe a ee piede 2 1 2 1 Install and Configure KeYmaera 2 122 Configure the Editors 5 4 59 aie xev edP aes 2 1 23 Show Additional Views 3 1 2 4 Add Modeling Templates 3 TEXTUAL MODELING 5 23 Create a mew Project por ee ei Pen ode le 5 2 2 Load a Model in KeYmaera 6 2 3 Refactor your Model 4 4 5 artos amp dee dace d bow de 0 7 2 4 Further Editor Features 0 7 GRAPHICAL MODELING 9 3 1 Create a new Graphical Model 9 3 2 Model System Structure 3 4 scd os a ERO 10 3 3 Model System Dynamics 12 3 4 Generate Textual Model 17 PROOF COLLABORATION 19 4 1 Share and Collaborate on Textual Models 19 4 2 Share and CollaborateonaProof 20 4 3 Export Open Goals of Partial Proofs 20 4 4 Import Geometric Relevance Filtering Results 22 uL LIST OF FIGURES KeYmaera configuration Configure d popup editors Create a new d project Figure 2 1 Run KeYmaera from the context menu of any key OL PLOO LUIS y e o Er ia ss
12. ble click on a diagram element Click Acceleo Model to Text gt Generate Differen tialDynamicLogic to generate a textual d model from a graphical UML model PROOF COLLABORATION Abstract This chapter introduces the proof collaboration features of Spnx Spnx uses Eclipse for model and proof versioning and is thus compatible with common versioning systems such as SVN and GIT Contents 4 31 Share and Collaborate on Textual Models 19 4 2 Share and Collaborate on a Proof 20 4 3 Export Open Goals of Partial Proofs 20 4 4 Import Geometric Relevance Filtering Results 22 4 1 SHARE AND COLLABORATE ON TEXTUAL MOD ELS Textual models in d just as ordinary source code can be versioned in a source code repository Differences between versions updates dele tions and conflicts can be compared and resolved using the standard Eclipse tools EP Compare 04c 1 1_robot_2D DynamicWindow key 589 and 575 2 El K Text Compare amp th 49 FA K 04c 1 1 robot 2D DynamicWindow key 589 K 04c 1 1 robot 2D DynamicWindow key 575 27 R cy rotation center y 28 R cy rotation center y Rr radius of curvature 29 Rr radius of curvature R ox position of obstacle 0 R ox position of obstacle R oy 31 R oy R odx direction and linear velocity of obstacle 32 R odx direction and linear velocity of obstacle R ody j R ody 3 Rt time 34 R t ti
13. constrain h Constrained element eoo type filter text Ez h Y Model PET Package Import UML Primiti do System SystemDynamics v H Ball Y t ownedAttribute 3 b Ez v b Ez H gt H System World 3 3 MODEL SYSTEM DYNAMICS 3 Exit the constrained element selection the constraint definition window and the postcondition window A new postcondition without specification has been added to the activity 4 Click on the postcondition to open the d popup editor Enter the postcondition and confirm with Ctrl Enter As an alternative to the popup editor constraint specifications can be added from the constraint editor continue from step 2 above 1 Add a constraint specification using the button next to the specification text field Specifications are always of kind Opaque Expression eoo Create a new Constraint Name Height Visibility public v e ESL Duration E text i sse 2 2 one ENDEN Pet Durationinterval P Constrained element Expression nie InstanceValue x Eg h Interval LiteralBoolean Literallnteger LiteralNull 1 LiteralReal s ado LiteralString G LiteralUnlimitedNatural OpaqueExpression Lok 1 StringExpression TimeExpression Timelnterval e Software released under the GNU GPL License 2 On the constraint specification window name the new specifi cation Click the button next to language to add d Type dL into the text field
14. d Undo 36Z j D Revert File Rg Save 36S R H Quick Outline 30 AprogramVa Open Declaration F3 sta O With Y Rh v Open Wit Show In X dW gt 2 Xproblem fe Y Cut ob X g gt 0 Copy C CH h amp H 0 gt M Paste eV Tee C Validate bing 1 Rename Element NR 4 sy Content Assist Space Toggle Comment 36 y Format DEF Lee ne x ca Quick Fix 9 1 kondition Shift Right Shift Left Find References HG Run As gt 1541 KeYmaera Proof Local Debug As gt Team gt Run Configurations Prohlems 2 Comnare With gt hes x Figure 2 1 Run KeYmaera from the context menu of any key or proof file Spnx will start KeYmaera as external application and show KeYmaera s information output in a console view If absolutely necessary you can stop KeYmaera from the console using the red stop button not encour aged Note that this will force quit KeYmaera without saving your work Problems Javadoc 2 Declaration El Console 2 Properties Library Java JavaVirtualMachines jdk1 7 0 1l Gaal 0 KeYmaera Prover Found CE HYPO loop inv box quan DISPROVABLE P Start Prune Proof BN Reuse Ep fa El inv lt v 2 2 g H Tasks y Inner Node HYPO loop inv box quan Env with no model 1 2 inv lt h gt v s2 g9 H M QO Proof closed D v 4 EZ D venis h v t Property proved We might have changed the o
15. d follow the steps below to apply the uMr profile for d 1 In the Properties View select the tab Profile and click the button Apply Registered Profile 2 Select Differential Dynamic Logic Structure and Differential Dynamic Logic Behavior and click OK 3 Check dldynamic and dlstatic and click OK 3 2 MODEL SYSTEM STRUCTURE In this section we discuss how to model the system structure with classes and properties We will use the stereotypes of the d UML profile to mark important parts of the model for code generation and subsequent verification 1 From the palette select Class and click on the editing area Al ternatively wait for the popup palette to appear in an empty part of the editing area We create two classes one represents the Create new classes by bouncing ball the other one the world dragging Class elements from the palette to the editing area 3 2 MODEL SYSTEM STRUCTURE 11 jeoo Java sphinxtutorial src model bouncingball di Eclipse Users smitsch Downloads eclipse workspace m Lu si HEBT BG a e H fm E ee ee De ero IE ei eee a eee Lucida Grande 3 E Te Wee Fa Quick Access y g Da H Package Explor X El 9 bouncingball di 3 m a ie V 4 Palette b Y 4 sphinxtutorial Raa Y src EE model oi Nodes 7 bouncingball di H B Sada Bj
16. era 2 1 2 2 Configure the Editors 2 3 3 1 1 INSTALLATION FROM ECLIPSE UPDATE SITE qnx comes with an Eclipse update site which automates installation and updates It assumes that Eclipse Juno Modeling Tools is already downloaded from http www eclipse org and installed To check for Spnx updates click Help Check for Updates 1 Start Eclipse Juno 2 Click Help Install new Software to open the Eclipse update manager 3 Click Add to add a new Papyrus update site Spnx installation retrieves its base graphical modeling libraries from this update site 4 Type the following into the location of the update site http download eclipse org modeling mdt papyrus updates releases juno 5 Click Add to add a new Spnx update site 6 Type the following into the location of the update site http www cis jku at sphinx updates releases to use the latest tool release If you want to use nightly builds use http www cis jku at sphinx updates nightly instead 7 Follow the screen instructions to complete the installation 1 http www eclipse org papyrus 2 1 2 1 2 1 1 Specify the locations of KeYmaera JAR libraries to enable KeYmaera startup from S pnx 4 INSTALLATION CONFIGURATION his section details the configuration of S nx once it is installed Spnx uses KeYmaera as hybrid verification tool Install and Configure KeYmaera Follow the instructions o
17. jar Browse b Key KeYmaera Local Installati ANTLR JAR Applications KeYmaera3 1 key ext jars antlr 3 4 complete jar Browse Term Team RecoderKEY JAR Applications KeYmaera3 1 key ext jars recoderKey jar Browse Log4J JAR Applications KeYmaera3 1 key ext jars log4j jar Browse JLink JAR Applications KeYmaera3 1 key ext jars JLink jar Browse Restore Defaults Apply Cae m0 If necessary supply the remaining JAR libraries manually using the respective Browse buttons 1 2 2 Configure the Editors Click Eclipse Preferences to open the Eclipse preferences dialog T Select DifferentialDynamicLogic Compiler to activate deactivate IATEX code generation and configure output directory and further code generation settings Select DifferentialDynamicLogic gt Syntax Coloring to change the coloring of terminal symbols comments and other syntactical elements of d Select DifferentialDynamicLogic Templates to change the existing templates or add new ones see Sect 1 2 4 for details Select DifferentialDynamicLogic Refactoring to change the default refactoring settings 2 http symbolaris com info KeYmaera html download 1 2 CONFIGURATION 3 5 Select Papyrus Embedded Editors to set the Spnx included d editors as default popup editors for the UML elements Constraint OpaqueAction and ControlFlow Set the d editors of S pnx as embedded eoo Preferences i o
18. ll Behavior Action create new Behavior nodes Create a new Behavior 2 Create behavior Behavior type Activity gt Behavior gt Name Element owner lt lt System gt gt lt Activity gt SystemDynamics rM Or assign an existing one _ Select behavior Behavior t Synchronous call 2 p D Came OK 6 Add a Decision Node from the palette This node represents the end of the loop body 7 Connect the decision node with the merge node using a Control Flow as back edge Select the stereotype Nondeterministic repeti tion for this control flow Then specify a loop invariant for the stereotype 8 Add an Activity Final Node and connect the decision node with a control flow This finalizes the overall system dynamics as follows Overview of bouncing ball 9 bouncingball di 3 dynamics 1 SystemDynamics PreCondition Init PostCondition Height dynamics Fall and Jump bounceback u 4 ti Dynamics 53 Bg Structure 16 Use the context menu to add a new activity diagram to a UML behavior The discrete dynamics of the bouncing ball example GRAPHICAL MODELING In the next step we will specify the discrete dynamics of the system The discrete dynamics of the bouncing ball is rather simple if the ball hits the ground it bounces back i e the discrete dynamics inverts the ball s velocity and reduces it according to the damping factor else it just keeps falling or
19. me A 35 5 3 6 problem 37 NschemaVariables v gt 0 8 term R trm amp Abs x ox gt v 2 2 b v V b j9 amp Abs y oy gt v 2 2 b v V b 10 amp r 0 11 Nrules amp dx 2 dyA2 1 42 absolute amp A 0 13 Nfind Abs trm amp b 14 Nreplacewith Nif trm 0 Nthen trm Nelse trm amp V 0 5 heuristics beta if comment then not used autor 15 8 Om gt 0 H T amp ep 0 v gt NL C 7 control obstacle 8 odx 3 19 ody 50 Nproblemi odx 2 ody 2 lt V 2 51 v gt 0 amp Abs x ox gt v 2 2 b v V b brake or remain stopped on your current curvatur 53 amp Abs y oy gt v 2 2 b v V b loa h 54 Rr vA E Properties E Console Error Log g Progress ji History X amp amp Ev a u trunk robix models map2d 04c 1 1_robot_2D DynamicWindow key in https cvs concert cs cmu edu multigoali Revision 7 Date Author Comment 589 1 31 13 5 28 PM smitsch Update to work with KeYmaera 3 1 575 1 30 13 8 20 PM smitsch Models and proofs with simpler invariants and preconditions Action Affected paths 4 Description Figure 4 1 Comparison of textual models 19 20 PROOF COLLABORATION 4 2 SHARE AND COLLABORATE ON A PROOF Just as for textual models Spnx supports any source code repository connected to Eclipse to version proofs You can compare changes be tween your local version of a proof and the latest version in the s
20. n the KeYmaera web site to download and install KeYmaera locally Note that Spnx does not yet work with the Webstart version Click Eclipse Preferences and select KeYmaera Local Installation from the tree view Click Browse on the KeYmaera Installation Directory line and select your local KeYmaera installation directory Spnx will try to figure out the library dependencies automatically Preferences jene type filter text KeYmaera Local Installation Or row P General 7 gt Ant Edit KeYmaera Settings PEDO n KeYmaera installation directory Applications KeYmaera3 1 Browse gt Ecore Tools Diagram y EMF Compare j A n n Orbital Extensions JAR Applications KeYmaera3 1 key ext jars orbital ext jar Browse P EMF Facet q gt Install Update Scala Library JAR Applications KeYmaera3 1 key ext jars scala library jar Browse P Java P Model Validation Orbital Core JAR Applications KeYmaera3 1 key ext jars orbital core jar Browse MoDisco P Mylyn KeYmaera JAR Applications KeYmaera3 1 key ext jars keymaera jar Browse POCL gt Papyrus e eme JMath Plot JAR Applications KeYmaera3 1 key ext jars jmathplot jar Browse b Plug in Development PPro C Cc AR licati Y 3 1 k j 1 4 j Brows P Run Debug ommons Compress JAR Applications KeYmaera3 L key ext jars commons compress 1 4 jar rOWSe YSphinx gt DifferentialDynamicLogic Java CC JAR Applications KeYmaera3 1 key ext jars javacc
21. nts 21 Create a new Project soseda soria aa ERR es 5 22 Load a Model in KeYmaera 6 23 Refactoryour Model ssa aus aaa sn bane aa 7 24 Further Editor Features 7 2 1 CREATE A NEW PROJECT 1 Click File 2New Other 2 Select Differential Dynamic Logic Project and click Next Create a new d project using the new CA project wizard Select a wizard mmc Wizards type filter text b Git b Java b gt Java Emitter Templates b MoDisco b Papyrus b Plug in Development Y Sphinx Ki Differential Dynamic Logic File 1 Differential Dynamic Logic Project gt SVN b Tasks User Assistance P Other Examples rT z Sr EEE cm O lt Back EEE cancel Finish 3 Enter the name of your new project and click Finish The project creation wizard creates a new project with a sample key file that shows the principal structure of a theorem in d including a hybrid program Details on d can be found on the KeYmaera web site including tutorials and cheat sheets Below we give a of a bouncing ball 1 http symbolaris com info KeYmaera html down load 6 TEXTUAL MODELING 2 2 LOAD A MODEL IN KEYMAERA Spnx uses KeYmaera to prove models in d You can start KeYmaera from the context menu of a key or key proof file in the package explorer or from the context menu of a textual editor Fir Hybrid hodel of a bouncina ball Se
22. odality split right gt Rule random ass box right gt Rule random ass box right gt Builtin Update Simplification gt Builtin Update Simplification gt Rule all right gt Rule all right Open Goal v_1 gt 0 dx D 2 dy_1 2 1 r1 0 Open Goal v_1 gt 0 dx 2 dy D A2 1 r_1 gt 0 Differences Properties Differences Properties 4 Use the buttons in the structural differences view header to copy changes between versions 4 3 EXPORT OPEN GOALS OF PARTIAL PROOFS 1 Open the context menu of a proof and click Export Export an arithmetic 2 Select Sphinx Export Arithmetic Goal and click Next goal via the export wizard 4 3 EXPORT OPEN GOALS OF PARTIAL PROOFS 21 Select an export destination type filter text General gt Install b Java b Papyrus b Plug in Development b Run Debug Y Sphinx Export Arithmetic Goal b Tasks gt Team gt Other lt Back Nex Cancel Finish 3 Search for and select the open goal to export click Next Search an open goal en u N ee ee Select goal Select an open goal to export Y Invariant Initially Valid g gt 0 h gt 0 t gt 0 0 lt c c lt 1 v42 lt 2 g H HhH H gt 0 gt h gt 04vA2 lt 2 g H h Y Use Case g gt 0 h gt 0 t gt 0 0 lt c c lt 1 v42 lt 2 g H h H gt 0 gt forall Rv 1 forall R h_1 forall Rt Y Body Preserves Invariant g gt 0 h gt 0 t gt 0 0 lt c c lt 1
23. ontrol flows to get the final dynamics as below 9 bouncingball di 3 DiscreteDynamics deterministicAssignment Bounce Back deterministicAssignment Reset Time ix Dynamics Bg Structure ix DiscreteDynamics 23 6 To set up navigation from the dynamics overview to the detailed discrete dynamics switch back to the tab Dynamics 7 Double click the behavior call action bounceback DiscreteDynamics to open the hyperlink configuration window 3 4 GENERATE TEXTUAL MODEL 8 Click the button on the tab View Hyperlinks to open the Edit Hyperlink Window 9 Click the button Search and select the DiscreteDynamics activity diagram 3 View hype rlinks Document hyperlinks Web hyperlinks Defa List of View hyperlinks leoo Editors list Tree View type filter text iz Dynamics B Structure iz DiscreteDynamics OK Cancel Edit Hyperlink View Tooltip text i Ok u Cancel e Bj be e 10 Switch to the tab Default Hyperlinks select the DiscreteDynamics hyperlink and press the right arrow button to add it as default 34 GENERATE TEXTUAL 1 Open the context menu of bouncingball uml in the package ex plorer 68098 HyperLinks L Le L Ok Cancel HyperLink View hyperlinks Document hyperlinks Web hyperlinks Defaults HyperLinks Hyperlink diagram with Heuristic Default Hyperlink
24. ource code repository as follows 1 Open the context menu of a proof and click Compare with Latest from Repository 2 Click Complete resource set s Proof comparison 3 Browse the proof comparison 3 PassiveSafety2 di EP Compare PassiveSafetyPartial key proof workspace and versions Structural differences ll gw Vv 13 change s in Branch Body Preserves Invariant v 1 change s in Open Goal v 12 0 dx_1 42 dy 1 A2 1 r1 gt 0 v1l 0 Abs x 1 ox 1 gt v1 2 2 b V v1 Il x Attribute goal EString in Open Goal v 12 0 dx 1 2 dy_l 42 1 r_1 gt 0 v1 0 Abs x 1 ox 1 gt 1 2 2 k Rule modality split right has been added t Rule random ass box right has been added g Builtin Update Simplification has been added e Rule all right has been added Visualization of Structural Differences ECRIRE Workspace file PassiveSafetyPartial key proof Repository file PassiveSafetyPartial key proof gt Rule and_left gt Rule hide_left gt Rule hide_left gt Rule hide left gt Rule hide left v nuie an 1igic gt Rule all right gt Rule imp right gt Rule and left gt Rule and left Rule and left gt Rule hide left Rule hide left gt Rule modality split right gt Rule hide left gt Rule random ass box right gt 4 Rule hide left gt Builtin Update Simplification gt Rule hide left gt 4 Rule all right gt Rule hide left gt 4 Rule m
25. pup editors for type filter text Embedded Editors qr rw P P P IM Papyrus UML models gt EMF Facet Elements to edit gt Help org eclipse uml2 uml Transition gt Install Update org eclipse uml2 uml State gt Java org eclipse uml2 uml Port d Model Validation org eclipse uml2 uml Property MoDisco org eclipse papyrus uml profile structure AppliedStereotypeProperty P Mylyn org eclipse uml2 uml Constraint OCL org eclipse uml2 uml OpagueAction Y Papyrus org eclipse uml2 uml CollaborationUse Connection Tools gt Diagrams Drag and drop b Embedded Editors org eclipse uml2 uml ControlFlow org eclipse uml2 uml Parameter org eclipse uml2 uml ConnectionPointReference Model loading Navigation Associated editor Papyrus Model Explorer Essential OCL constraint editor Default Pathmaps JAVA constraint E Printing Differential Dynamic Logic Default Editor Property view customizal Simple Direct Editor Property views A A O Cancel ER 1 2 3 Show Additional Views Click Window Show View Other then select the following views e Select General Properties e Select Papyrus Model Explorer 1 2 4 Add Modeling Templates TEXTUAL MODELING Abstract This chapter introduces the textual modeling features of 5onx These include project creation wizard loading d models to KeYmaera model refactoring syntax checking code completion outline and quick outline as well as code folding Conte
26. raphical models can be transformed into textual d models and then loaded to KeYmaera Contents 31 Create anew Graphical Model 9 3 2 Model System Structure ssas wx seo Res 10 33 Model System Dynamics esses 12 3 4 Generate Textual Model 17 3 1 CREATE A NEW GRAPHICAL MODEL 1 Click File New Other 2 Select Papyrus Model and click Next 3 Enter the name of your new model and click Next 4 Select uMr and click Next 5 Select UML Activity Diagram system dynamics and UML Class Diagram system structure then check A UML model with basic primitive types Create a new graphical model of a hybrid system describing structure and behavior 10 GRAPHICAL MODELING eoo New Papyrus Model Initialization information Select name and kind of the diagram Diagram Name BouncingBall Select a Diagram Kind Vf x UML Activity Diagram al Bg UML Class Diagram UML Communication Diagram UML Component Diagram 5d UML Composite Structure Diagram En UML Deployment Diagram n UML Package Diagram ET UML Sequence Diagram te UML StateMachine Diagram 28 UML UseCase Diagram You can load a template vi A UML model with basic primitive types ModelWithBasicTypes Remember current selection Back Next gt Cane Finish 6 Click Finish The editor pane now shows the graphical editor Switch to the class diagram structure an
27. riginal Proof K Statistics CEX Counterexample iii Proot Iree E 5 4 Found CE 1 gt r imply right lt Nodes 57 HYPO loop inv box quan DISPROVABLE 2 4l and left Branches 9 uc Nw 3 4l and left HYPO loop inv box quan 4 al and left fox inve h gt 08v42 lt 2 S al and left th a 6 4l and left V fh v 7 al and left We might have changed the original HYPO loop inv box quan PROVABLE inve h 0 amp v 2 lt 2 KRY Strategy Applied 49 rules 56 1 sec closed 9 goals 0 remaining h v t h v t Figure 2 2 The KeYmaera console 2 3 REFACTOR YOUR MODEL 2 3 REFACTOR YOUR MODEL Spnx has preliminary model refactoring support in the form of variable renaming Proofs are not yet adapted automatically 1 Right click a variable select Refactor Rename 2 4 FURTHER EDITOR FEATURES e Double click any tab to make it full screen e Open a searchable quick outline of your textual model from the context menu of a d textual model J AprogramVariables state varinhle derlaratinns Rh v Egv 2 Y Z bouncingball 2 Nproblem VIE Problem inita iz g gt 8 amp h lE amp gt vwiE amp AL YIIZ lt C VIZA h zw if Y dL Modality 2 v Y ix Box Modality a t Y Z Statimpl J i Y zStarlmpl J WIE StatReentrylmpl M C8 h Press Esc to exit the quick outline e Syntax checking initial state characterization g 0 amp h
28. s by double click Ex DiscreteDynamics DiscreteDynamics MODEL 2 Click Acceleo Model to Text Generate DifferentialDynamicLogic HE Package Explorer 52 m 9 bouncingball di 3 Li WS sphinxtutorial Y src P Y EE model New gt 9 bouncingball di Ki bouncingball key Open F3 E bouncingball nota Open With Show In Yew gt t 2 Copy 3C 5 E amp Copy Qualified Name 5 Paste eV X Delete po int id Show Filtered Children Alt click Fr e l DX 2 Remove from Context 0881 Find ball P ve Mark as Landmark x0301 Y c Uncategorized Build Path Verify Bouncing Ball Refactor XET gt ey Import 14 Export Tz Outline amp Model Explorer gt Refresh F5 IEA INIA gt d esu 2 Run As Y t ownedBehavior 1 Debug As Woe DiscreteDynamics Team x Diagram Disce Compare With v t edge 6 Replace With gt ControlFlow x Discovery gt 7 ControlFlow gt Z ControlFlow amp Paste b Z ControlFlow gt 7 ControlFlow 7 ControlFlow 73 Refactor Model Properties bouncingball uml sphinxtutorial s Assign Working Sets zr Acceleo Model to Text gt creteDynamics gt laration E Console Properties 52 lt vvvvy 31 v Value false true March 22 2 false JUsers smit bouncingba sphinxtutc 15 082 byt Generate DifferentialDynamicLogic 17 Create a new hyperlink Set a hyperlink as default action for dou
Download Pdf Manuals
Related Search