UML2Alloy Reference Manual
Contents
1. 117 person addConstraints ageSim 119 Finally add an assertion 120 Constraint anAssertion new ConstraintImpl anAssertion 121 context Person inv anAssertion Person allInstances gt 122 forAll p Person p wife notEmpty implies p wife husband p 123 anAssertion addStereotypes AssertionStereotype getInstance 124 person addConstraints anAssertion 7 2 Transforming To carry out the actual transformation the UML2Alloy Transformer class needs to be used For a detailed example please see the UML2Alloy website under the examples section Appendices Appendix A XMI Compatibility We use the KMF XMI parser so our parser is compatible with the XMI files the KMF parser can read We have tested UML2Alloy with a number of UML design CASE tools Table A 1 shows the results of our tests CASE TOOL VERSION SUCCESS ArgoUML 0 19 YES ArgoUML 0 22 YES Poseidon For UML 4 1 Community Edition YES MagicDraw 9 5 Community Edition YES MagicDraw Any Version gt 10 NO Table A 1 CASE Tools Support Appendix B Complete UML Model of Sudoku Puzzle Please note that the ArgoUML project the XMI file and the generated Alloy file of this example can be found on the UML2Alloy website under the examples section The following OCL statement constraints that the values of the cells to be in the range of one to six since it is a 6x6 puzzle context Cell inv value2. Similarly to simulation commands assertion commands can be used to check if a statement that depicts a property of the system is satisfed by the model In a class diagram an OCL statement can be used to depict an assertion The assertion stereotype can be used on OCL statements which will be transformed to Alloy assertions It is important to note that OCL constraints annotated with the simulation or assertion stereotypes cannot have any pre and post conditions 3 Transforming UML This section provides a brief informal overview of the transformation rules from UML to Alloy The rules are implemented in UML2Alloy This section also mentions any restrictions that might exist 3 1 Packages O A UML Package is transformed to an Alloy module Restrictions X Only one Package may be transformed to an Alloy module at a time X Package import is not supported 3 2 Classes Subclasses and Types O Translates Classes to Signatures If the class isAbstract it will be translated to an abstract Signa ture O Translates subclasses to subsignatures The default subclassing semantics is incomplete dis joint 8 p 72 O Enumerators are translated to abstract Signatures and Enumerator literals are translated to sub signatures with one element Singletons For more information see Section 3 3 O Custom data types We transform all Classes with the DataType stereotype to Signatures Currently custom data types are not treated any diff
3. 04 da GLS3 Classi Class2 c1 lass4 Class3 Class 03 Figure 6 1 Example UML model of two classes connected with two unidirectional and one bidirectional association 6 Examples 16 Wf unidirectional same as bidirectional zargo Class Diagram 1 ArgoUML File Edit View Create Arrange Generation Critique Tools Help 3 New Ctrl N M S DER DEBI amp Open Project Ctrl O Save Project Ctil S TE Save Project As Revert to Saved E or er B T Import XMI Import sources Classi Class2 amp Page Setup 01 E Print Ctrl P Save Graphics Export All Graphics Save Configuration test2 xmi I rT Figure 6 2 Exporting model to XMI using ArgoUML UML2Alloy 0 5 Beta Built on 31 0ct 2008 File Help Files Scopes Commands Transform and Execute areSame INVARIANT ASSERTION M Eu bidirectional INVARIANT ASSERTION i Figure 6 3 Selecting that the areSame and bidirectional statements are Assertions We now export the model to XMI format from within ArgoUML Figure 6 2 depicts a screenshot that shows how to achieve that in ArgoUML Next we invoke UML2Alloy In the first tab we select the path to the XMI file and the Alloy file we want to create We then click on the Parse XMI button In the next tab we sele
4. 63 64 66 67 68 69 7l 72 73 75 76 77 78 80 81 82 83 84 86 87 88 89 7 Developer API 23 lt analysis gt gt Example defaultScope 5 intScope 4 Figure 7 2 Example UML Model p addOwnedMember ptInt Add class Person make it abstract and add it to the package Class person new Class Impl Person person setIsAbstract true p addOwnedMember person Add class Man Class man new Class Impl Man p addOwnedMember man Add class Woman Also add the enforce stereotype to the woman Class woman new Class Impl Woman woman addStereotypes EnforceStereotype getInstance p addOwnedMember woman Add class Company Also add the scopedElement Stereotype Class company new Class Impl Company company addStereotypes new ScopedElementStereotype 2 p addOwnedMember company Add the generalization between Person and Man new GeneralizationImpl man person Add the generalization between Person and Woman new GeneralizationImpl woman person Add the age attribute of Person Property age new PropertyImpl age ptInt person addOwnedAttribute age Add the employer association end Property employer new PropertyImpl employer company employer setLower 0 Lower multiplicity of zero person addOwnedAttribute employer The non navigavle association end of the association bet
5. Currently this feature is compatible with Alloy Analyzer 4 1 9 which is also distributed with UML2Alloy The Alloy Analyzer works by translating the model into a boolean expression which is analysed by SAT solvers embedded within the Alloy Analyzer A user specified scope on the model elements bounds the domain making it possible to create finite boolean formulas for the evaluation by SAT solvers The Alloy Analyzer offers two analysis methods One is simulation and the other is assertion checking Simulation produces a random instance of the model that conforms to the constraints The absence of an instance implies that most probably the model is inconsistent It is possible from within the Analyser to narrow down the statements which produce the inconsistent model This functionality is called UnSat Core 9 Assertion checking checks whether an assertion which is a statement which should follow from the specification is satisfied by the model If it is not a counterexample is presented to the user A counterexample is an instance of the model which violates the assertion This manual contains some information for both Alloy and the Alloy Analyzer for people familiar with UML but unfamiliar with Alloy For more information on the Alloy Analyzer and the Alloy language the reader is refereed to 5 and 1 If the reader is interested in the transformation rules and the restrictions on the translation the reader is referenced to Chapt
6. Execute Logger Initialised Files CC XMI Path CMestxmi Browse XMI Alloy Path Citestals Browse Alloy Parse XMI Figure 5 1 Files Tab of UML2Alloy 5 UML2Alloy Usage Manual 12 UML2AIloy 0 5 Beta Built on 31 0ct 2008 File Help Files Scopes Commands Transform and Execute Default Scope Integer Values Range 2 1 E iv Enforce All Class Name Ee E ON Class1 1 x Enforce Class2 H1 x Enforce Class3 Hj v Enforce Class4 1 v Enforce Figure 5 2 Scopes Tab of UML2Alloy UML 2Alloy 0 5 Beta Built on 31 0ct 2008 File Help Files Scopes Commands Transform and Execute areSame INVARIANT ASSERTION 4 bidirectional INVARIANT ASSERTION m Figure 5 3 Commands Tab of UML2Alloy 5 2 2 Commands Tab In the Commands tab Figure 5 3 the user is presented with all the Invariants and Operations of the UML model The first column depicts the Operation or Invariant name Please note that by clicking on the name of Operation or Invariant you can see its original OCL specification The second column shows if the statement is an Invariant or Operation in the original UML model Finally the third column has a drop down menu which allows the user to select to what kind of Alloy statement the original UML
7. Using UML2Alloy Figure 5 1 shows the main screen UML2Alloy On the right hand side of the screen you can see the messages log In the first tab you need to enter the path to the XMI file that contains the UML model that will be transformed to Alloy You also need to specify the path of the Alloy text file that will be generated if the transformation is successful 5 2 1 Scopes Tab After you enter the path of the XMI file to parse and the Alloy file to generate you press the Parse XMTI button This will attempt to parse the XMI file If the parse completes successfully the other tabs in the user interface are enabled In the scopes tab you may specify the scopes of the elements Figure 5 2 depicts a screenshot of this tab On the top of the screen of the scopes tab the user may specify the default scope which is the scope that will be applied to all model elements This can be overridden for specific model elements if a value other than 1 exists in the scope box of a specific model element By checking the checkbox of the last column the user can enforce that a model element will have instances in the model For a concrete example on the usage of this function please refer to the examples in Chapter 6 1 ArgoUML 0 19 5 can be downloaded from http argouml downloads tigris org argouml 0 19 5 UML2Alloy 0 5 Beta Built on 31 0ct 2008 File Help ii Files Scopes Il Commands Transform and
8. stereotype gt lt lt stereotype gt gt lt stereotype gt stereotype stereotype gt lt lt stereotype gt gt analysis scopedElement singleton enforce simulation assertion dynamic oce A IO AAA defaultScope Integer 3 scope Integer intScope Integer 4 time Integer 3 Figure 2 1 UML Profile for Alloy Stereotypes 2 UML Profile for Alloy 3 2 3 Singleton A singleton stereotype can be applied to a class and is used to define the well known singleton design pattern 3 Classes annotated with this stereotype are restricted to have exactly one instance in the model 2 4 Enforce In general an instance of a UML class diagram may be partial i e some classes may not have any instances This stereotype is used on classes that are required to have at least one instance during the analysis 2 5 Simulation In Alloy a first order logic statement can be used to simulate a model This statement corresponds to the Alloy run command 5 Section 4 6 Similarly in a UML class diagram an OCL constraint can be used to simulate the model We use the simulation stereotype for this purpose More specifically an OCL statement stereotyped as simulation will be automatically transformed to an Alloy simulation run command An Alloy run command can be used with the Alloy Analyzer to create a random instance of the model that conforms to the statement and the constraints of the model 2 6 Assertion
9. 13 5 5 Selecting the Command to Execute 13 6 1 Example UML model of two classes connected with two unidirectional and one 6 2 Exporting model to XMI using ArgoUML 16 6 3 Selecting that the areSame and bidirectional statements are Assertions 16 6 4 Available Commands to Execute 17 0 5 Counterexample reas s gaada 28 RR URS 17 6 6 A Sample Sudoku Puzzle css san pia be a 18 6 7 A Class Diagram representing the Sudoku puzzle 18 6 8 Solution of the sample Puzzle of Figure 6 6 19 6 9 Man in the Middle Class Diagram Unprotected 19 6 10 Man in the Middle Class Diagram TLS 20 7 1 Package org uml2alloy umlmmsimplifiedprofile 22 7 2 Example UML Model 23 111 1 Introduction This document is the user manual of UML2Alloy version 0 52 2 The transformation rules are based on Alloy version 4 and UML version 2 0 UML2Alloy is the outcome of research which attempts to formalise UML using Alloy 5 UML2Alloy translates UML Class Diagrams enriched with OCL constraints to Alloy Alloy models can be au tomatically analysed using the Alloy Analyzer 1 The current version of UML2Alloy performs the transformation to the Alloy language and creates a text file with the Alloy model Since version 0 5 experimental support for executing the generated Alloy model from within UML2Alloy has been added This is possible by utilising the Alloy Analyzer API
10. AIO DEEE Lo qem cod FUOD aay A 4 11 Includes IncludesAll 4 12 Excludes ExcludesAll ANB Nob sa sms RR Revue Gude E UR EAD Ae ee e ee C 4 14 Variable Expressions o s escia ea naa ai Rm 415 Integer Expressions oa s omm m m o m Rm a a 4 16 ocllsEondOF i snes w Sue oye a 417 Boolean Literal 2 22x boe m mk om meg 5 UML2Alloy Usage Manual hu Installation ci a na v de deg Ro mom E E 5 2 Using UML2Alloy 2 2 64 8 6b ee a OA copas Tab ocd eue Se po ew 5 52 Commands Tab ss eis eomm ri RU 5 2 0 Transform and Execute corram hrs 6 Examples 6 1 Two Unidirectional vs One Bidirectional Associations 6 2 Precise UML for solving Sudoku 6 3 Man in the middle o Gol Unprotected i css 44665 44 6 4b ee es 632 TLS Protected 264464446 co pd RAE 7 Developer API 7 1 Defining a UML Model 0 4 o Lraustorm lp e 4 Uaec koe ee A A ee A XMI Compatibility B Complete UML Model of Sudoku Puzzle B 1 Generated Alloy Model References o o do o vc 10 10 11 11 11 11 12 12 15 17 18 19 19 21 21 24 26 27 28 33 il List of Figures 2 1 UML Profile for Alloy Stereotypes 2 5 1 Files Tab of UML2Alloy o ee 11 5 2 Scopes Tab of UML2Alloy 4 12 5 8 Commands Tab of UML2Aloy 12 5 4 Transform Tab of UML2Alloy
11. DRAFT Updated 04 May 2009 UML2Alloy Reference Manual UML2Alloy Version 0 52 Kyriakos Anastasakis The University of Birmingham School of Computer Science Please consider the environment before deciding to print this document Contents List DE IPAgHf S 2g ss ym BS aa Bw PE we e ded iii Introduction 1 1 1 Minimum Requirements ln 1 UML Profile for Alloy 2 ZL a las La eo xo dE Ga A ier x d 2 2 2 ScopodBlement crisis e RE Aes 2 23 Singleton o ios eai xa 4 oos de oben epe ed S CER 3 23 SIOE oou sik bor peg obo An 3 ES Ia iuo ES ED S meo ee e ees 3 20 JASSOFUONH ocn ce ye de odere epe e dod ke dk 3 Transforming UML 4 34 PAESE uuu RISO oque eMe WESS Rt ewe a 4 3 2 Classes Subclasses and Types 4 2 9 Enumerating socero oo cans e n e o Cap 5 SA JAsSOGLAUON s i x sa e ee ae el a aa 5 SUM Cies ADES zonae ks ek Hh ac A OS RU EOS 5 36 lass Methods lt er 4 cae E G4 ER OO C 6 Transforming OCL 7 Zl Wnvariants 22 2l so xo x baw be eee bee cR abe ne 7 2 3 DDBeraunS ucc AROS Sk ee A 7 43 OperationCallbaps 4 4 6 aca ee ne ee REG Remy s 8 AS AtidfOt ss aus Ge Bebb pee RR 8 432 DOb oy i Oe ok ee ee ee ee ed 8 r mE ae a eo er 8 A41 Tmplies 2 i205 Pa bo moe 8 4 5 Iterator Expressiols sds ao i ee we 8 16 motlmpty SEMP a xorgx x36 9 9x3 x whe ae 9 Of SWE ROB hha hb baa we bea ee Ae a 9 d L0 o9 a web ee ie ee pe ene d 9 19 Ingluling ExchidiBe ok e pers r ee ehh Se a 9
12. KeyType Nonce INonceType lencryptedCPublickey EncryptedPublicKeyType leoSessionKey SessionKeyType leclNonce INonceType lencryptedPublicKey EncryptedPublicKeyType lresultP age ResultPageType lloginAborted ResultType EName SNameType ImName SNameType j eceiveMsgFromAttacker Boolean jcheckAC2Q Boolean jcheckAC1Q Boolean labortLoginQ Boolean leceiveLoginP age Boolean Attacker laPublickey PublicKeyType lencryptedAPublickey EncryptedPublicKeyType lecSessionKey SessionKeyType tati Im feclNonce INonceType recCPublicKey PublicKeyType recEnenyptedCPublicKey EncryptedPublickeyType lencryptedPublicKey EneryptedPublicKeyType esultP age ResultPageType ImName SNameType l eceiveMsgFromSemer Boolean receiveLoginFromClient Boolean LoginManager esultP age ResultPageType essionKey SessionKeyType lencryptedPublicKey EncryptedPublicKeyType recPublickey PublicKeyType reciNonce INonceType ImName SNameType continueWithLoginQ Boolean leceiveLoginFromAttacker Boolean Datatype lt lt Datatype gt gt lt lt Datatype gt gt lt lt Enumerationi Enumeration PublicKeyType INonceTypd EncryptediNonceType SNameType e ResultPageType True void labortPage void lt lt Datatype gt gt lt lt Datatype gt gt lt lt Datatype gt gt omaPig red SessionKeyTyp EncryptedSNameType lomptedPublicKeyTyp
13. another class and back we end up with a different class Currently the results of the analysis are represented using the Alloy Analyzer representation form for example as a Tree as shown in Figure 6 5 In the future we plan to represent the results of the analysis in terms of UML i e object diagrams Checking the bidirectional assertion does not provide any counterexamples 6 2 Precise UML for solving Sudoku In this example we want to solve a simple sudoku puzzle using UML Figure 6 6 depicts a 6x6 sample sudoku puzzle It is a straight procedure to model this puzzle in UML Figure 6 7 shows the UML class diagram that represents the puzzle This puzzle consists of 36 cells Each cell has a row ndex which represents the row of the cell a columnIndez which represents the column of the cell and a value which represents the contents of the cell Finally a cell belongs to a region and each region is represented by an integer number 1 The sample puzzle of Figure 6 6 has 6 regions The region borders are designated by the bold lines 6 Examples 18 Figure 6 7 A Class Diagram representing the Sudoku puzzle OCL is used to specify the constraints of the puzzle and the numbers that exist already in the puzzle The following OCL statement depicts the rules of the puzzle context Cell inv rules Cell allInstances gt forAll ci c2 Cell C ci rowIndex c2 rowIndex or ci columnIndex c2 columnIndex o
14. command java jar Xmz256m umlZalloy jar 6 Examples 19 Figure 6 8 Solution of the sample Puzzle of Figure 6 6 6 3 1 Unprotected Figure 6 9 shows the class diagram of the unprotected man in the middle attack The Client is connected through an Attacker to the LoginManager The Client uses a username and a password to login to the LoginManager If the correct username and password are supplied the Client has access to the personalised homePage otherwise he has access to a visitorPage ActiveClient LoginManager Attacker name NameType name NameType name NameType pis a word PasswordType pword PasswordType lpword PasswordType P SEE VARA TIA lauth AuthenticationResultType ati m fprot Profiletype tact tat FesunP age s ResuPageType result age ResultPageType lresultP age ResultPageType rec eiveResult Boolean receiveLoginFromClient Boolean receiveLoginFromAttacker Boolean leceiveAuthFromUAMO Boolean bendResult Boolean eceiveResultFromLoginManagerQ Boolean UProfileManager prof ProfileType UAcctManager name NameType name NameType lgetP rofileQ Boolean buoni PasseirdType auth AuthenticationResultTyp erifyQ Boolean lt lt Enumeration gt gt lt lt Enumeration gt gt lt lt Enumeration gt gt lt lt Enumeration gt gt lt lt Enumeration gt gt lt l
15. ct the scopes for each model element Figure 5 2 We specify a default scope of 2 This means that the Alloy Analyzer will probe to find a counterexample to the assertion using up to two atoms i e instances for each class We also check the enforce checkbox on all classes to enforce that at least one instance of each class will exist in the solution Finally we do not change the Integer Values Range combobox because our model does not use any integers In the Commands tab Figure 5 3 we specify how each OCL statement will be mapped to Alloy We want to check if both the areSame and bidirectional OCL statements are satisfied They therefore need to be transformed to assertions This is specified by selecting in the drop down menus that we want the original OCL invariants to be transformed to assertions indicated by the red arrows in Figure 6 3 We now move to the Transform and Execute tab and click on the Transform2Alloy button Once the transformation is successful the Command2Execute drop down menu will be populated with the available commands to execute as in Figure 6 4 In this case the available commands are the areSame and bidirectional assertions Moreover by default a simulation command is available to execute run for in the drop down menu The simulation command will attempt to find an instance of the model that conforms the constraints Next to the name of each command are the scopes For this example th
16. e Alloy Analyzer will attempt to find a counterexample to the assertions for 4 elements but for a bitwidth of 2 for integer numbers We first select from the drop down menu the areSame assertion and press on Execute The Alloy Ana lyzer produces a counterexample The counterexample in XML format can be seen in the Alloy Execution Log part of the screen We can click on the View Execution Result Graph to view the counterexam ple using Alloy Analyzer s visualisation engine The counterexample using Alloy s visualisation engine is depicted in Figure 6 5 From a closer examination of the instance we can see that there is a class Class1_0 related to Class2_0 6 Examples 17 UML2Alloy 0 5 Beta Built on 31 0ct 2008 File Help Files Scopes Commands Transform and Execute Transform Transform2Alloy xecute Experimental Feature Command2Execute chr Alloy Execution Log Figure 6 4 Available Commands to Execute Msgs Mir Ii amp E E Layout Viz Tree Tables Te E Ii X M areSame_counterexample_08 a x 3 Solution gt univ o Gj Class2 gt Ei Class3 o 5 Class4 o 5 Classi CH areSame cl E Classi_0 e de C Class2 0 det CH Class1_1 dez CH Class2 0 ea o 5 Class1_1 Figure 6 5 Counterexample which in turn is related to Class1_1 The assertion therefore fails because navigating from a class to
17. e f False void isitorP age void Figure 6 10 Man in the Middle Class Diagram TLS This example was analysed for a scope of 8 The Alloy Analyzer produced an instance of the model where the Attacker can view the homePage For a close inspection of the instance it became apparent that this happens if the Attacker has access to the encrypted public key of the client In practice this can only happen if the Attacker has access to the Client s private key Assuming that the Client keeps his private key safe we added the following invariant in the model context ActiveClient inv ActiveClient allInstances gt forAll ac ActiveClient ac at encryptedAPublicKey lt gt ac encryptedCPublicKey After the invariant was added to the model using a scope of 20 the Alloy Analyzer did not produce any counterexample 10 TX 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 31 33 34 35 36 37 38 39 41 42 7 Developer API This section contains information on how to use the developer API of UML2Alloy to carry out an automated transformation of a UML model that conforms to the UML profile for Alloy into Alloy UML2Alloy comes with a simplified version of the UML metamodel The classes of this metamodel can be found in the package org uml2alloy umlmmsimplifiedprofile Figure 7 1 depicts a UML model of the classes of the package In order to carry out the transformation first we need to us
18. e the classes in the package to define a UML model The following section shows how this is achieved 7 1 Defining a UML Model Assume the UML model of Figure 7 2 The model has the following constraints context Person inv ageInv self age gt 0 The following constraint is stereotyped as simulation context Person inv adultSimulation Person allInstances forAll p Person p age gt 18 The following constraint is stereotyped as assertion context Person inv anAssertion Person allInstances gt forAll p Person p wife gt notEmpty implies p wife husband p This model can be represented with the following Java code Imports package org uml2alloy tests import java io FileNotFoundException import java io IOException import org uml2alloy AbstractUML2AlloyTransformer import org uml2alloy UML2AlloyTransformer import org uml2alloy alloy4 AlloyModel import org uml2alloy sitra4uml2alloy RuleNotFoundException import org uml2alloy transformer exceptions UML2AlloyTransformationException import org uml2alloy umlmmsimplifiedprofile Association import org uml2alloy umlmmsimplifiedprofile AssociationImpl import org uml2alloy umlmmsimplifiedprofile Class_ import org uml2alloy umlmmsimplifiedprofile Class Impl import org uml2alloy umlmmsimplifiedprofile Constraint import org uml2alloy umlmmsimplifiedprofile ConstraintImpl import org uml2alloy umlmmsimplifiedprofile GeneralizationImp
19. ect Operationcall is transformed to an Alloy ComprehensionEzpr 4 11 Includes IncludesAll O OCL includes and includesAll Operationcalls are transformed to an Alloy Formula with a subsets compare operation According to Table A 3 of OCL 2 0 specification 6 includes and includesAll set theoretic interpretation is that of the subsets set theoretic operation 4 12 Excludes ExcludesAIl O OCL excludes and excludesAll Operationcalls are transformed to an Alloy Formula with a negation of the subsets compare operation According to Table A 3 of OCL 2 0 specification 6 excludes and excludesAll set theoretic interpretation is that of the the negation of the subsets set theoretic operation 4 13 Not O OCL not expressions expressions with a negation are directly transformed to Alloy Negation Formulas NegFormula 4 14 Variable Expressions O OCL Variable Expressions for example in the expression self name self is a Variable Expression are transformed to Alloy Variable Expressions VariableExpr 4 Transforming OCL 10 4 15 Integer Expressions O UML Class attributes of type integer are transformed to fields of type Int O OCL LiteralIntegers 7 p 60 are transformed to Alloy LiteralIntExprs Restrictions X Currently version 0 5 do not support operations i e addition subtraction multiplication divi sion over integer values 4 16 oclIsKindOf An ocllsKindOf OCL statement is transformed to Alloy us
20. elf self self self self self self self self self self self self self self self rowIndex 5 amp amp columnIndex 1 value 5 rowIndex 5 amp amp columnIndex 5 value 3 rowIndex 5 amp amp columnIndex 6 value 1 rowIndex 6 amp amp columnIndex 1 value 1 rowlIndex 6 amp amp columnIndex 3 value 2 rowIndex 6 amp amp columnIndex 4 value 4 Appendix B Complete UML Model of Sudoku Puzzle 32 all cl c2 Cell cl rowIndex c2 rowIndex amp amp cl columnIndex c2 columnIndex gt cl c2 pred Cell rules self Cell all cli c2 Cell cl rowIndex c2 rowIndex cl columnIndex c2 columnIndex cl region c2 region amp amp cl c2 gt cl value c2 value pred Cell puzzleSize self Cell COLETTI int self rowIndex gt 0 amp amp int self rowIndex lt 7 amp amp int self columnIndex 7 amp amp int self columnIndex 0 amp amp int self value 7 amp amp int self value 0 amp amp int self region 0 amp amp int self region 7 pred Cell differentCells self Cell run for 4 but 7 int 36 Cell 1 Puzzle Bibliography 1 Alloy Analyzer website http alloy mit edu Accessed April 2008 1 2 UML2Alloy webs
21. erent than any other Class In the future we will extend the transformation to support the notion of Datatypes according to the UML standard In particular the UML standard specifies that Datatypes are identified by their value rather than their object id Restrictions X The only primitive types supported are Integers X Multiple packages are not supported Translation of the classes of one package at a time takes place X Multiple inheritance is not allowed It is possible to express diamond multiple inheritance in the future X Only subclasses with incomplete disjoint semantics are allowed Again the rules for the rest of the cases have been defined but we haven t implemented them X Subclasses can not redefine attributes operations Thus attribute and operation names can not have the same name as the attribute and operation names of the superclasses X The NameSpace to which Classes can belong to is not restricted by the UML specification Thus a Class can belong to the NameSpace of another Class inner Classes Our rules only support Classes which belong to the NameSpace of a Package 3 Transforming UML 5 3 3 Enumerations O Enumerations are transformed to abstract Signatures O Enumeration literals are translated to Subsignatures which extend the abstract Signature of the Enumeration Since each enumeration literal represents only one value it is declared as a Signature represented by one atom in Alloy Restrictio
22. ers 3 and 4 If the reader wants to learn details on how to use UML2Alloy s he is referenced to Chapter 5 Finally Chapter 6 presents a number of examples to demonstrate how UML2Alloy can be used 1 4 Minimum Requirements UML2Alloy requires Sun Java 1 5 All the required third party libraries are distributed with UML2Alloy 2 UML Profile for Alloy In order to facilitate fully automated analysis of UML class diagrams enriched with OCL constraints a UML profile for Alloy was developed The purpose of the profile is two fold First it does not allow the definition of UML models that can not be represented in Alloy for example the UML standard allows for named elements i e the NamedElement metaelement without a name Consequently it is possible to have an operation parameter without a name On the other hand Alloy requires that all predicate the concept that maps to UML operations parameters have a unique name Moreover the Alloy language has notions such as the scope simulation and assertion commands which allow fully automated analysis of Alloy models On the other hand the UML does not have such concepts As a result in order to achieve fully automated of UML models through Alloy the UML profile for Alloy extends the UML with stereotypes and tagged values Figure 2 1 depicts the stereotypes and the tagged values that may be specified In the following we explain briefly the meaning of each stereotype 2 1 Analysis The analysis
23. f rowIndex 3 and self columnIndex 6 implies self value 3 and self rowIndex 4 and self columnIndex 1 implies self value 2 and self rowIndex 4 and self columnIndex 2 implies self value 5 and self rowIndex 5 and self columnIndex 1 implies self value 5 and self rowIndex 5 and self columnIndex 5 implies self value 3 and self rowIndex 5 and self columnIndex 6 implies self value 1 and self rowIndex 6 and self columnIndex 1 implies self value 1 and self rowIndex 6 and self columnIndex 3 implies self value 2 and self rowIndex 6 and self columnIndex 4 implies self value 4 The following OCL statement defines that all cells have different row and column indexes if two cells have the same row and column index then they are the same cell context Cell inv differentCells Cell allInstances gt forAll cl c2 Cell cl rowIndex c2 rowIndex and cl columnIndex c2 columnIndex implies cl c2 The following OCL fragment illustrates the rules of the puzzle More specifically if two different cells belongs to the same row or column or region they have to have a different value Appendix B Complete UML Model of Sudoku Puzzle 28 context Cell inv rules Cell allInstances gt forAll cl c2 Cell cl rowIndex c2 rowIndex or cl columnIndex c2 columnIndex or cl region c2 region and cl lt gt c2 imp
24. hat the OCL else clause is translated to 4 4 1 Implies O Implies OperationCalls are directly transformed to an Alloy implies formula ImplicationFormula 4 5 Iterator Expressions An OCL Iterator Expression is transformed to an Alloy Quantified Formula Restrictions X Currently only the forAll and exists Iterator Expressions are supported 4 Transforming OCL 9 4 6 notEmpty isEmpty O An OCL notEmpty expression is transformed to an Alloy QuantifiedExpr with the some quan tifier In particular it is transformed to an Alloy Formula which enforces the existence of some elements O Similarly an OCL isEmpty expression is transformed to an Alloy QuantifiedExpr with the no quantifier 4 7 size An OCL size Operationcall is transformed to an Alloy CardinalityExpr 4 8 union An OCL union Operationcall is transformed to an Alloy BinaryExpr with a union operation 4 9 Including Excluding An OCL including Operationcall is transformed to an Alloy BinaryExpr with a union operation according to Table A 4 of OCL 2 0 specification 6 the including set theoretic interpretation is the same as the union set theoretic operation O An OCL ezcluding Operationcall is transformed to an Alloy BinaryExpr with a set difference operation according to Table A 4 of OCL 2 0 specification 6 the excluding set theoretic interpre tation is that of the set difference set theoretic opearation 4 10 Select An OCL sel
25. ing the set containment operator Restrictions X The oclIsKindOf can only be applied on user defined classes It cannot be applied on UML predefined types i e 10 oclIsTypeOf Integer is not allowed 4 17 Boolean Literal O The Boolean literal true is transformed to an Alloy expression that always evaluates to true for example 1 1 Similarly the Boolean literal false is transformed to an Alloy expression that always evaluates to false for example 1 1 5 UML2Alloy Usage Manual This chapter is a brief guide on how to use UML2Alloy It is suggested that ArgoUML version 0 19 5 is used to develop any models The reason for this is that ArgoUML provides syntax checking for OCL statements Please note that apparently some versions since ArgoUML version 0 20 have a bug in the OCL syntax checker and as a result it is strongly recommended to use version 0 19 5 5 1 Installation Download the zip file of the distribution and unpack it on your local storage ensuring the directory structure of the contents of the zip file is preserved In the command prompt navigate to the directory where UML2Alloy was unzipped and use the run bat if you are on windows or the run sh file if you are using nix If you are on a nix operating system you will have to give execution rights to the file run sh Please run UML2Alloy from the command prompt because for the time being a number of error messages and warnings print to the console 5 2
26. instance of the Signature on which the specification of the Predicate is applied is passed as a parameter to the Class Therefore all references to the self keyword used in OCL are transformed to the parameter passed in the Predicate For a detailed example please see Section 6 3 Restrictions X The current implementation supports one OCL expression as specification to the Operation X Pre and Post conditions have to have a name X Operations can be of either Boolean or Void type X Currently Operations can not have any parameters 4 3 OperationCallExps In OCL a large number of expressions are OperationCall expressions For example equality implies and or etc expressions are considered to be OperationCall expressions The following shows how those OperationCall expressions are transformed into Alloy 4 3 1 And Or O An OCL and OperationCall is transformed to an Alloy binary formula BinaryFormula with an AND Logical operator O Similarly an OCL or OperationCall is transformed to an Alloy binary formula with an OR Logical operator 4 3 2 Dot Dot OperationCall expressions in OCL are navigation expressions which use the navigation dot O An OCL Dot OperationCall is transformed to an Alloy binary expression BinaryExpr with a JOIN DOT binary expression Operation 4 4 If O An OCL Tf Expression is transformed to an Alloy implies formula ImplicationFormula In Alloy an ImplicationFormula can have an else clause which is w
27. ite http www cs bham ac uk bxb UML2Alloy index php 1 3 Erich Gamma Richard Helm Ralph Johnson and John Vlissides Design patterns elements of ES 10 reusable object oriented software Addison Wesley Professional Computing Addison Wesley Boston MA USA 1995 ISBN 0 201 63361 2 2 3 Martin Gogolla and Mark Richters Transformation rules for UML class diagrams In UML 98 Selected papers from the First International Workshop on The Unified Modeling Language UML 98 pages 92 106 London UK 1999 Springer Verlag ISBN 3 540 66252 9 3 4 Daniel Jackson Software Abstractions Logic Language and Analysis The MIT Press London England 2006 1 2 5 OMG OCL Version 2 0 Document id formal 06 05 01 http www omg org 4 9 4 11 4 12 OMG UML Infrastructure Document formal 05 07 05 http www omg org 4 15 OMG UML Superstructure Version 2 0 Document id formal 05 07 04 http www omg org 3 2 3 4 Ilya Shlyakhter Robert Seater Daniel Jackson Manu Sridharan and Mana Taghdiri Debugging overconstrained declarative models using unsatisfiable cores In Proceedings of the 18th IEEE Inter national Conference on Automated Software Engineering Montreal Canada pages 94 105 IEEE Computer Society 2003 1 Emina Torlak Marten van Dijk Blaise Gassend Daniel Jackson and Srinivas Devadas Knowledge flow analysis for security protocols Technical Report MIT CSAIL TR 2005 066 Computer Scie
28. l import org uml2alloy umlmmsimplifiedprofile PackageImpl import org uml2alloy umlmmsimplifiedprofile Package import org uml2alloy umlmmsimplifiedprofile PrimitiveType import org uml2alloy umlmmsimplifiedprofile PrimitiveTypeImpl import org uml2alloy umlmmsimplifiedprofile Property import org uml2alloy umlmmsimplifiedprofile PropertyImpl import org uml2alloy umlmmsimplifiedprofile stereotypes AnalysisStereotype import org uml2alloy umlmmsimplifiedprofile stereotypes AssertionStereotype import org uml2alloy umlmmsimplifiedprofile stereotypes EnforceStereotype import org uml2alloy umlmmsimplifiedprofile stereotypes ScopedElementStereotype import org uml2alloy umlmmsimplifiedprofile stereotypes SimulationStereotype CODE Define the package called Example Package p new PackageImpl Example The package is stereotyped as analysis Set the tagged values and add an instance of the stereotype to the package AnalysisStereotype setDefaultScope 4 AnalysisStereotype setIntScope 6 p addStereotypes AnalysisStereotype getInstance Add the integer primitive type and add it to the package PrimitiveType ptInt PrimitiveTypeImpl buildIntegerPrimitiveType package uml2alloy pwnedOperation ownedParameter Figure 7 1 Package org uml2alloy umlmmsimplifiedprofile IdV Jodojosog 4 GG 43 45 46 47 48 50 51 52 54 55 56 57 58 60 61 62
29. lean expression with v Do NOT use collection forAll boolean expression Use self attribute Do NOT use attribute 4 1 Invariants Please NOTE Invariants stereotyped as Simulation or Assertion cannot reference the special variable self For simulation and assertion commands the expanded form of in variants should be used For example instead of the statement context C1 self attribute value the statement context C1 C1 allInstances forAll v1 C1 v1 attribute value should be used O Class invariants are generally transformed to Alloy facts They can also be transformed to Sim ulation or Assertions commands This is defined during the transformation process For more information please see the usage manual in Chapter 5 O Each invariant is translated to a predicate and then a fact statement which references the predicate is added Restrictions X Only Class invariants defined in the namespace of a Class are supported i e Class invariants X Invariants have to have a name The name of each invariant needs to be unique throughout the model 4 2 Operations The effects of Operations is defined using OCL pre and post conditions NOTE The current version of the implementation only supports postconditions 4 Transforming OCL 8 O Operations are transformed to Alloy Predicates Operations are defined in the context of a Class Because in Alloy Predicates belong to the NameSpace of the model an
30. lies cl value lt gt c2 value B 1 Generated Alloy Model The following listing is the Alloy code generated by the application of UML2Alloy on the UML model presented in the previous section module sudoku puzzle some sig Cell rowIndex one Int columnIndex one Int value one Int region one Int some sig Puzzle cells set Cell fact Cell regions fact all self Cell Cell regions self fact Cell rules fact all self Cell Cell rules self fact Cell puzzleSize fact all self Cell Cell puzzleSize fact Asso Puzzle puzzle cells Cell Puzzle cells in Pu fact AssoCustom Puzzle puzzle cells Cell all var Puzzle pred Cell regions self Cell COCCO int self rowIndex lt 2 amp amp int self columnIndex lt 3 gt int self region 1 int self rowIndex lt 2 amp amp int self columnIndex gt 3 int self region 2 int self rowIndex gt 2 amp amp int self rowIndex lt 4 amp amp int self columnIndex lt 3 int self region 3 int self rowIndex gt 2 amp amp int self rowIndex lt 4 amp amp int self columnIndex gt 3 13 fact Cell numbers exist fact all self Cell Cell numbers exist fact Cell differentCells fact all self Cell Cell differentCells self self zzle var self one gt set cells Cell 36 Appe
31. nce and Artificial Intelligence Laboratory MIT October 2005 6 3
32. ndix B Complete UML Model of Sudoku Puzzle 29 int self region 4 int self rowIndex gt 4 amp amp int self region 5 int self rowIndex 4 amp amp int self columnIndex 3 int self region 6 CERES OCA int self rowIndex 1 amp amp int self columnIndex 3 int self value 6 int self rowIndex 1 amp amp int self columnIndex 4 int self value 3 int self rowIndex 1 amp amp int self columnIndex 6 int self value 2 amp amp int self rowIndex 2 amp amp int self columnIndex 1 gt int self columnIndex lt 3 pred Cell numbers exist self Cell Appendix B Complete UML Model of Sudoku Puzzle 30 int self int self int self int self int self int self int self int self int self int self int self int self int self int self int self int self int self int self int self value 3 rowIndex 2 amp amp columnIndex 2 value 2 rowIndex 2 amp amp columnIndex 6 value 6 rowIndex 3 amp amp columnIndex 5 value 2 rowlIndex 3 amp amp columnIndex 6 value 3 rowIndex 4 amp amp columnIndex 1 value 2 rowIndex 4 amp amp columnIndex 2 value 5 Appendix B Complete UML Model of Sudoku Puzzle 31 self self s
33. ns X Enumerations have to be defined in the UML class diagram as Classes with an enumeration stereotype Enumeration literals have to be defined as attributes of the Class Attributes have to be of void type 3 4 Associations Please note that in this section the term Association End is used to reference the ends of an association Even though this term is used in the UML specification for example see 8 p 14 or 8 p 40 the UML metamodel refers to Association Ends as Properties 8 p 29 All association ends have to have names Association end names have to be unique O Unidirectional Associations The navigable Association End appears as a field in the Signature to which the original Class the association belonged to was translated O Bidirectional Associations Association Ends appear as fields in both the Signatures that partic ipate in the relation An additional fact is added to the model to denote that the relations are symmetric O Multiplicities Depending on the multiplicity of the Association Ends the necessary multiplicity facts will be added to the model O Custom multiplicities are supported Restrictions X Association End names have to be unique throughout the model i e all Association Ends have to have unique names in contrast with the UML specification which allows two separate Association Ends to have the same name as long as they belong to different Classes X Association End annotation
34. r ci region c2 region and c1 lt gt c2 implies ci value lt gt c2 value The OCL statement requires that for every two cells ci and c2 if they belong to the same row or column or region and they are not the same cell then the numbers of c1 and c2 are different The complete UML model and OCL constraints of this puzzle and the generated Alloy model can be found in appendix B UML2Alloy was used to transform the UML representation of the puzzle to Alloy The Analyzer provided a solution to the puzzle 2 The solution the Analyzer found is illustrated in Figure 6 8 6 3 Man in the middle This section presents an example of how the man in the middle attack can be analysed using Alloy through UML2Alloy Please note that in these example we do not care about the order of the messages exchanged between the parties involved but only about which party has access to which information This is similar to the approach taken by Torlak et al 10 Since no attribute or association end is stereotyped as dynamic the analysis is carried out over a single state i e the operation pre and post conditions are dealt as invariants First the unprotected plaintext version of the attack is presented in the next section 2 Please note that executing this puzzle requires additional memory As a result when launching UML2Alloy from the command prompt use the Xmz java switch to provide additional memory to the Java VM For example use the
35. s self value gt 0 and self value lt 6 The following OCL excerpt illustrates the constraints that define which cells belongs to which region notice the puzzle is split up in six regions as indicated by the bold lines in Figure 6 6 context Cell inv regions self rowIndex lt 2 and self columnIndex 3 implies self region 1 and self rowIndex lt 2 and self columnIndex gt 3 implies self region 2 and self rowIndex gt 2 and self rowIndex lt 4 and self columnIndex lt 3 implies self region 3 and self rowIndex gt 2 and self rowIndex lt 4 and self columnIndex gt 3 implies self region 4 and self rowIndex gt 4 and self columnIndex lt 3 implies self region 5 and The following OCL fragment depicts specifies the existing numbers in the puzzle for example the cell whose row is 1 and column is 3 has a value of 6 context Cell inv numbers_exist self rowIndex 1 and self columnIndex 3 implies self value 6 and self rowIndex 1 and self columnIndex 4 implies self value 3 and self rowIndex 1 and self columnIndex 6 implies self value 2 and self rowIndex 2 and self columnIndex 1 implies self value 3 and self rowIndex 2 and self columnIndex 2 implies self value 2 and self rowIndex 2 and self columnIndex 6 implies self value 6 and self rowIndex 3 and self columnIndex 5 implies self value 2 and sel
36. s are not currently supported e g subsets ordered etc PS Only binary associations are supported in the current version of the implementation X The UML specification allows for unspecified navigability 8 p 41 In UML2Alloy an Association End needs to be either navigable or non navigable X Aggregation and Composition are not supported Associations with composition or aggregation have to be refactored using the method defined by Gogolla and Richters 4 X Association Classes are not currently supported 3 5 Class Attributes O Class attributes are translated to Signature fields 3 Transforming UML 6 Restrictions X Attributes have to be of a specific type ie not void This restriction does not apply for enumeration literals see Section 3 3 X Only attributes with multiplicity of 1 are supported 3 6 Class Methods O Class methods are transformed to Alloy predicates For more information see Section 4 2 Restrictions X Class methods can not return any type other than Boolean or Void X Operations in UML may raise exceptions UML2Alloy does not deal with the exceptions 4 Transforming OCL This section presents the details on the translation of OCL statements invariants and pre and postcon ditions to Alloy IMPORTANT NOTE NO shorthand notation is supported for OCL expressions For ex ample Use collection forAll v Type boolean expression with v Do NOT use collection forAll v boo
37. statement will be transformed The drop down menu with the selections is populated with the following rules An OCL Invariant can be translated to an Invariant Fact in Alloy terms Assertion or Simulation statement 5 2 3 Transform and Execute Figure 5 4 shows a screenshot of the Transform and Execute tab Once the user has set the desired parameters in the previous tabs s he can press the Transform2Alloy button that will carry out the actual transformation of the UML model into Alloy If the transformation is successful the Alloy model will be generated in the path that was specified by the use in the Files tab When the transformation to Alloy is finished it is possible to select the command to execute and execute it from within UML2Alloy using the Alloy Analyzer API In particular the Command2Ezecute drop down box will be populated with the commands in the generated Alloy model as shown in Figure 5 5 The user can select the command to execute from the drop down menu and hit the Execute button If the execution is successful the result will be displayed in the Alloy execution log If the execution returns an instance a random instance in the case of simulation or a counterexample in the case of assertions the XML output of the instance will be displayed in the Alloy execution log It is also possible to click on the View Execution Result Graph button that will show the instance using 5 UML2Alloy Usage Man
38. stereotype is used on UML packages that are going to be analysed using our method A UML class diagram is required to have exactly one package stereotyped as analysis The analysis stereotype defines three attributes also called tagged values the defaultScope intScope and time These tagged values are used during the transformation to set the default Alloy scope the scope for integer numbers and the scope for the time respectively The defaultScope intScope and time are positive integer numbers Following Alloy s approach if no defaultScope tagged value has been defined in the model the default value is 3 Similarly if no default tagged value has been defined in the model for integer values the scope for integer numbers is set to 4 and if no scope for the time has been defined the scope for time is set to 3 2 2 ScopedElement Each class in a class diagram can be stereotyped as a scopedElement The scopedElement stereotype defines a tagged value scope which is used to limit the number of instances of an element when a system instance is being checked by the SAT solver This is used to override the defaultScope attribute of the analysis stereotype in order to define a different scope for the particular class on which the stereotype is applied 1 The scope for time is used only when modelling dynamic systems lt lt profile gt gt metaclass gt lt lt metaclass gt gt Class Constraint lt lt stereotype gt gt
39. t Enumeration gt gt NameType PasswordType ResultPageType AuthenticationResultTypd AttackSuccessType ProfileType loName void lcpword void homePage void jauthenticated void uccess void IcProfile void jaName void japword void isitorPage void notAuth void failure void InullProfile void Figure 6 9 Man in the Middle Class Diagram Unprotected In this example we check that if the Attacker eavesdrops on the communication whether s he can have access to the homepage This model has one invariant called exec main This invariant is used to simulate the model Also there are two assertions assert and assert2 which need to be transformed to Alloy assertions The specification of Assert1 is the following all a ActiveClient a at resultPage visitorPage Asserti asks whether all Attackers in the system will have access to the visitorPage i e no Attacker has access to the homePage Alloy presents a counterexample with an Attacker having access to the homePage using the credentials of the ActiveClient 6 3 2 TLS Protected Figure 6 10 shows the class diagram of the man in the middle attack over the TLS protocol In this case no username or password is used by the client to gain access to the homepage Instead the TLS protocol utilises asymmetric cryptography which means that the server needs to have a certificate signed by an authority 6 Examples 20 ActiveClient cPublicKey Public
40. tion statements can be acquired and how the UnSat Core of assertions can be interpreted 6 1 Two Unidirectional vs One Bidirectional Associations In this example we want to assert if two unidirectional associations between two classes have the same meaning as one bidirectional association To do so we generate the model depicted in Figure 6 1 The model was developed using ArgoUML version 0 19 5 The model does not have any constraints We want to assert that the two unidirectional associations between Classl and Class2 have the same effect on the model as the bidirectional association between Class3 and Class4 The assertion we use is stated in OCL We call this statement areSame context Classl inv areSame Classi allInstances gt forAll cll Classi cll c2 cl cll This assertion states that for each Class1 if we navigate to Class2 and come back we will end up in the same object as where we started In ArgoUML we define this assertion as an Invariant and when we use UML2Alloy in the Commands tab we define that we want to transform it as an assertion i e a statement to check Another option would be to stereotype the statement as assertion Similarly we formulate the following OCL statement to reason about the association between Class3 and Class4 We call this statement bidirectional context Class3 inv bidirectiional Class3 allInstances gt forAll cl3 3 Class3 cls
41. ual 13 UML2Alloy 0 5 Beta Built on 31 0ct 2008 xecute Experimental Feature comme Alloy Execution Log View Execution Result Graph Figure 5 4 Transform Tab of UML2Aloy UML2AIloy 0 5 Beta Built on 31 0ct 2008 File Help Files Scopes Commands Transform and Execute Transform Execute Experimental Feature Command2Execute check Class1 areSame for 2 but 2 int Alloy Execution Log check Class3 hidirectional for 2 but 2 int un for 2 but 2 int View Execution Result Graph Figure 5 5 Selecting the Command to Execute 5 UML2Alloy Usage Manual 14 Alloy s graphical engine In a future release of UML2Alloy the instance will be shown as a UML object diagram If an instance cannot be found the UnSat Core will be queried and the original UML and OCL elements responsible for the inconsistency will be displayed Please note that in the case of an assertion not pro ducing a counterexample the UnSat core can represent the original UML and OCL elements responsible for the validity of the assertion 6 Examples This chapter presents a number of simple examples to demonstrate the usage of UML2Alloy Please note the ArgoUML project files as well as the generated Alloy models can be found under the Examples section of the UML2Alloy website Section 6 1 describes a very simple example which demonstrates how counterexamples to asser
42. ween Person and Company Property person non navigable new PropertyImpl person non navigable person person non navigable setLower 0 person non navigable setUpper 1 Association between Person Company Association asso person company new AssociationImpl employer person non navigable Person non navigable association end is not navigable therefore it belongs to the association rather than a class 7 Developer API 24 90 asso person company addOwnedEnd person non navigable 92 Add association to the package owned elements 93 p addOwnedMember asso person company 95 The wife association end 96 Property wife new PropertyImpl wife woman 0 1 97 man addOwnedAttribute wife 99 The husband association end 100 Property husband new PropertyImpl husband man 0 1 101 woman addOwnedAttribute husband 103 Pi Association between Man Woman 104 Association asso man woman new AssociationImpl wife husband 106 p addOwnedMember asso man woman 108 Also add invariants 109 Constraint ageInv new ConstraintImpl ageInv 110 context Person inv ageInv self age 0 111 person addConstraints ageInv 113 Also add the ageSim Simulation Invariant 114 Constraint ageSim new ConstraintImpl ageSim 115 context Person inv ageSim Person allInstances gt forAll p Person p age gt 18 116 ageSim addStereotypes SimulationStereotype getInstance
Download Pdf Manuals
Related Search