UML2Alloy Reference Manual - Computer Science
Contents
1. X Multiple inheritance is not allowed the transformation rules have been defined but not imple mented in the tool 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 2 2 Enumerations O Enumerations are translated to abstract Signatures 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 Restrictions 2 Translating UML 3 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 2 3 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 7 p 14 or 72. and press on Execute The Alloy Analyzer produces a countererample This is an instance of the model that violates the assertion This instance is depicted in Figure 5 5 From a closer examination of the instance we can see that there is a class Class1_0 related to Class2 0 5 Examples 12 Alloy Analyzer File Edit View Tools Window Help la chk areSame 4 x a P New Open Save Prefs Build Execute ayout iz Tree test2 als Welcome to Alloy Compiling test2 a INFO Performed INFO Performed Compilation succ module untitledModel set sig Class 1 c2 one Class2 set sig Class2 c1 one Class Figure 5 4 Selecting the statement we want to check which in turn is related to Class1_1 The assertion therefore fails because navigating from a class to another class and back we end up with 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 5 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 For more information on the Alloy Analyzer please consult the Alloy website 1 5 2 Using UML2Alloy in a model with integer expressions This section presents a simple example where a UML model with integer expressions is transformed to Alloy 5 2 1 The
3. field marry E Adulto field age 4 18 field marry amp C Adulti 1 DD Figure 5 10 A counterexample to the assertion 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 UML2Alloy Manual Document Changelog This page provides an overview of the changes of this manual document not UML2Alloy e Sections 3 9 and 5 2 which provide information on the support for Integer Expressions e Appendix C on the changelog of the UML2Alloy application Appendix C UML2Alloy Application Changelog RELEASE OF VERSION 0 26 Beta support for XMI 2 1 XMI produced by the UML plugin of eclipse It does not support packages Only supports classes defined in the namespace of the Model Also only supports OCL expressions defined as OpaqueExpressions 09 Aug 2007 Beta support for integer types and expressions 08 Aug 2007 If an attribute whose type is not supporte
4. p 41 Such cases are not supported X The UML specification allows for binary associations with both ends non navigable Again such cases are not supported X This version of UML2Alloy has not implemented our rules for aggregation and composition Asso ciations with composition or aggregation have to be refactored using the method defined by Gogolla and Richters 3 X Association Classes are not currently supported 2 4 Class Attributes Q Class attributes are translated to Signature fields Restrictions X Attributes have to be of a specific type i e not void This restriction does not apply for enumeration literals see Section 2 2 X Only attributes with multiplicity of 1 are supported 2 Translating UML 2 5 Class Methods O Class methods are translated to Alloy predicates For more information see Section 3 2 Restrictions X Class method can not return any type other than Boolean or Void X Operations in UML may raise exceptions UML2Alloy does not deal with such cases 3 Translating 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 boolean expression with v Do NOT use collection forAll boolean expression Use self attribute Do NOT
5. translated to an Alloy binary expression BinaryExpr with a JOIN DOT binary expression Operation 3 4 If O An OCL f Expression is transformed to an Alloy implies formula ImplicationFormula In Alloy an ImplicationFormula can have an else clause which is what the OCL else clause is translated to 3 Translating OCL 7 3 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 X Can only translate Iterator Expressions of the form Class allInstances forAll or Class allInstances exists X Do not currently support nested Iterator Expressions 3 6 notEmpty An OCL notEmpty expression is transformed to an Alloy ElemIntFormula In particular it is translated to an Alloy Formula which enforces the size of the Expression to be greater than zero For an example please refer to Chapter 5 Restrictions X The notEmpty operator has to be applied to a simple navigation expressions such as Per son allInstances rightarrow exists p Person p wife gt notEmpty Currently UML2Alloy does not support the application of notEmpty to more complicated expressions such as Iterator Ex pressions 3 7 Not O OCL not expressions expressions with a negation are directly transformed to Alloy Negation Formulas NegFormula 3 8 Variable Expressions O OCL Variable Expressions for example in the expr
6. DRAFT Updated 12 Aug 2007 UML2Alloy Reference Manual Version 0 26 Date Monday 10 September 2007 Kyriakos Anastasakis The University of Birmingham School of Computer Science Contents List Of Figures 4 os a csaa mm a ok os EUR ESOS iii Introduction 1 11 Minimum Requirements lees 1 Translating UML 2 2 1 Classes Subclasses and Types 2 2 24 En merations corras a 2 2 9 Associations ce a eee ee 3 2 4 Class Attributes 3 2 5 Class Methods ees 4 Translating OCL 5 Sel Invariants usas ssa ms go ok Ro RR RR e RR 5 3 2 Operations 4222942295999 bee 6 3 8 OperationCallExps ens 6 33 1 Impli 8 assess Roa GAR SSD E ME aw Be 6 33 20 ANA uova wea PR iid 6 33 3 DOG A 6 n NM PLC a A A e Bean A 6 3 5 Iterator Expressions e 7 JO mnotEmpiy ss ssa a rra 7 dl Noli AA ada 7 3 8 Variable Expressions less 7 3 9 Integer Expressions llle 7 UML2Alloy Usage Manual 8 4 l Installation 22 22 2 44 A ED a RUE EU a 8 4 2 Using UML2Alloy o 8 ADT Step Loo aa a 8 42D USED 2 euo a A qtue 8 4 23 OD d sem o A AE AAA RR RO 9 Examples 5 1 Two Unidirectional vs One Bidirectional Associations 5 2 Using UML2Alloy in a model with integer expressions 5 2 1 The UML model less 5 2 2 Transformation lees Do Results a se a bs ea B Bowed XMI Compatibility UML2Alloy Manual Document Chang
7. T m jadultinv INVARIANT INVARIANT r assertion INVARIANT ASSERTION A AAA Proceed Figure 5 7 Screenshot of the second step of the transformation process ad Adult ad marry age gt 18 We now export this model from our UML modelling environment to XMI format and use UML2Alloy to transform it to Alloy 5 2 2 Transformation In the first step of the transformation process we provide the path to the XMI file that contains the UML model we presented in the previous section We also specify the path of the Alloy file that will be created In the second step of the transformation process we specify how invariants and operations of the UML model map in Alloy Figure 5 7 presents a screenshot This shows that the ageInv and adultInv will be transformed into Invariants i e Facts in Alloy while the assertion statement will be transformed to an assertion in Alloy The next step in the transformation process is to specify the scopes As depicted in Figure 5 8 when defining the scope we now have another option the Integer Values Range which is a drop down menu Like all elements in Alloy we need to specify a scope for integer expressions The user can select from the drop down menu the range of integer expressions for which the model will be probed for a solution or a counterexample In this case we have selected a range of 32 31 So the largest negative integer in the model is 32 while the largest pos
8. This obviously produces a counterexample This small UML example was used as a simple example to show how integer expressions in OCL can be transformed in Alloy The Alloy counterexample also showed that the Adult Adult married Adult0 and Adult0 is married to Adult Exercise In this counterexample Adult0 is married to Adulti and Adult1 is married to Adult0 Is this always the case Can an Adult1 be married to Adult2 while Adult2 is married to a third person Adult3 5 Examples 16 module untitledModel some sig Person age one Int some sig Adult extends Person marry lone Adult fact My11To01 marry Adult Adult pred My11To01 r univ gt univ t set univ u set univ all x t lone y ulx r y all y ulone x t x r y fact ageInv fact i adultInv pred adultInv all ad Adult int ad age gt 18 pred ageInv all p Person int p age gt 0 assert assertion all ad Adult int ad marry age gt 18 check assertion for 4 but 8 Person 6 int Figure 5 9 Alloy model of example with integer expressions 5 Examples example Check assertion for 4 but 6 int 5 Person Eile Instance Theme Window Arze HE Viz Dot XML Tree Evaluator Next J example Check assertion for 4 but 6 int 5 Person 3 sig Adult 0 Adulto C Adulti 4 07 sig Int 3 3 sig Person a Adulto 03 Adulti CJ sig univ sig seg int set ad 3 Adulti 2 3 field age t e 29
9. UML model Figure 5 6 depicts a simple UML model There two classes A Person class and an Adult class which extends the Person class The Person class has an attribute age of type Integer An Adult can marry another Adult There are some OCL constraints related to integer values attached to the model The constraints of the Person class are context Person inv ageInv Person allInstances gt forAll p Person p age gt 0 The constraints of the Adult class are context Adult inv adultInv Adult allInstances gt forAll ad Adult ad age gt 18 We need to check that in such a model a Person over 18 can only marry only another Person whose age is over 18 This assertion can be formulated in OCL context Adult inv assertion Adult allInstances gt forAll 5 Examples 13 4 E E Layout Viz Tree Tables Te lir Mr E Il Msgs a x M areSame counterexample 08 l x 3 Solution gt 3 univ o 5 Class2 gt CY Class3 o 5 Class4 o EJ Classi CY areSame cH 5 Classi 0 9 3 c2 E Class2 0 e Edo CH Classi 1 Y ma c2 9 Ei Class2 0 e t o I Class1_1 Figure 5 5 Counterexample Figure 5 6 UML model of example 5 Examples 14 Functions of the model Please select whether the items in the model are facts or predicates For more information please consult the UML2Alloy manual lagelnv INVARIANT INVARIAN
10. d is found we raise a fatal exception 08 Aug 2007 If a fatal error occurs the transformation procedure will stop 31 Jul 2007 Compatibility with Alloy v4 25 Jul 2007 If an Association End name has not been specified by default it will be given the name of the Class converted to lowercase which the Association End connects Bibliography 1 Alloy Analyzer website http alloy mit edu beta faq php cited April 2005 2 UML2Alloy website http www cs bham ac uk bxb UML2A11oy index php 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 4 Daniel Jackson Software Abstractions Logic Language and Analysis The MIT Press London England 2006 5 OMG OCL Version 2 0 Document id formal 06 05 01 http www omg org 6 OMG UML Infrastructure Document formal 05 07 05 http www omg org 7 OMG UML Superstructure Version 2 0 URL http www omg org cgi bin doc formal 05 07 04 Document id formal 05 07 04 http www omg org
11. elog UML2Alloy Application Changelog References es 10 10 12 12 14 14 19 20 21 List of Figures 4 1 4 2 4 3 5 1 5 2 5 3 5 4 5 5 5 6 5 7 5 8 5 9 First Screen of UML2Alloy leen 8 Second Screen of UML2Alloy sen 9 Final Screen of UML2Aloy s 9 Example UML model of two classes connected with two unidirectional and one bidirectional association 10 Exporting model to XMI using ArgoUML 11 Selecting the mapping 0 0 11 Selecting the statement we want to check 12 Counterexample LL 13 UML model of example 13 Screenshot of the second step of the transformation process 14 Providing the scope sns 15 Alloy model of example with integer expressions 16 5 10 A counterexample to the assertion 17 iii 1 Introduction This document is the user manual of UML2Alloy version 0 26 alpha 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 4 UML2Alloy translates UML Class Diagrams enriched with OCL constraints to Alloy Alloy models can be automati cally analysed using the Alloy Analyzer 1 The current version of UML2Alloy performs the translation to the Alloy language and creates a text file with the Alloy model The user needs to use the Alloy Analyzer to open
12. ession self name self is a Variable Expression are transformed to Alloy Variable Expressions VariableExpr 3 9 Integer Expressions O UML Class attributes of type integer are transformed to fields of type Int OCL integer OperationCall expressions that match the pattern expression IntCompOp LiteralIn teger where expression is an expression IntCompOp is an integer comparison operation i e lt gt gt lt and a LiteralInteger is an expression that denotes to an integer value i e 3 0 1 etc are transformed to Alloy ElemIntFormulas O OCL LiteralIntegers 6 p 60 are transformed to Alloy LiteralIntEzprs Restrictions X Currently version 0 3 do not support operations i e addition subtraction multiplication divi sion over integer values X Currently version 0 3 only support OCL expressions that follow the pattern expression Int CompOp LiteralInteger where expression is an expression IntCompOp is an integer comparison operation i e lt gt gt lt and a LiteralInteger is an expression that denotes to an integer value i e 3 0 1 etc 4 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 greater than 0 19 5 have a bug in the OCL syntax checker 4 1 I
13. he association between Class3 and Class4 We call this statement bidirectional context Class3 inv bidirectiional Class3 allInstances gt forAll cl3 Class3 c13 c4 c3 c13 We now export the model to XMI format from within ArgoUML Figure 5 2 depicts a screenshot that shows how to achieve that in ArgoUML Next we invoke UML2Alloy In the first step of the transformation process we select the path to the XMI file and the Alloy file we want to create In the next step we select what each OCL statement maps Class Class2 Class3 Class4 03 Figure 5 1 Example UML model of two classes connected with two unidirectional and one bidirectional association 5 Examples 11 W unidirectional same as bidirectional zargo Class Diagram 1 ArgoUML File Edit View Create Arrange Generation Critique Tools Help 3 New Cti N ry e E BB 3 Open Project Ctrl O mI o ec Be 1 Save Project Ctrl S E Save Project As Revert to Saved Import XMI amp Import sources amp Page Setup DD amp Print Ctr P Save Graphics Export All Graphics EM a Save Configuration test2 xmi La o Figure 5 2 Exporting model to XMI using ArgoUML Functions of the model Please select whether the items in the model are facts or predicates For more information please consult the UML2Allo
14. itive integer is 31 The scope of integer values can be chosen according to the biggest positive negative value we expect in tegers expressions to have to in the model For example in our example we care about integer expressions of scope 18 and over This is why we chose a scope of 32 31 for this example Figure 5 8 also shows that we have enforced that there will be instances of Persons and Adults in the model We have also specified a default scope of 4 but defined a specific scope of 8 Persons 5 2 3 Results The Alloy model that was produced by UML2Alloy is depicted in Figure 5 9 Executing this Alloy model provides a counterexample The counterexample is depicted in Figure 5 10 5 Examples 15 CA x PLEASE SELECT THE SCOPE OF THE ELEMENTS IN THE MODEL Default Scope 4 Integer Values Range 32 31 Ka Class Name Scope Enforce Instance Person 8 y Enforce Adult 1 v Enforce Figure 5 8 Providing the scope The counterexample shows an Adult Adult0 married to an Adult Adult1 whose age is exactly 18 years old This counterexample is produced because according to our OCL invariant an Adult is someone who is 18 years old or older someone 18 years old is considered to be an Adult while our assertion checks for people over the age of 18 More specifically the assertion asserts that all Adults i e People 18 years or older will marry another Adult whose age is over 18 years old
15. mulation statement An Operation UML2Alloy a x File Help Path of the XMI file to translate Browse XMI File if Path of the Alloy file to translate to Browse Alloy File Figure 4 1 First Screen of UML2Alloy 4 UML2Alloy Usage Manual 9 Functions of the model Please select whether the items in the model are facts or predicates For more information please consult the UML2Alloy manual husband wife INVARIANT INVARIANT noHusbandAndWife INVARIANT main PREDICATE PREDICATE a v Proceed Figure 4 2 Second Screen of UML2Alloy Select Scope PLEASE SELECT THE SCOPE OF THE ELEMENTS IN THE MODEL Default Scope b Class Name Scope Enforce Instance Person 1 Enforce Company 1 Enforce String 1 _ Enforce Branch 1 Enforce Figure 4 3 Final Screen of UML2Alloy can be translated to a Predicate Simulation or Invariant An Operation with an OCL statement which uses the self keyword can only be transformed to a Predicate 4 2 3 Step 3 The last step towards the translation of UML to Alloy requires the user to specify the Scope Figure 4 3 depicts a screenshot of this last step The user can 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 exist
16. nd post conditions NOTE The current version of the implementation only supports postconditions 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 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 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 3 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 translated to Alloy 3 3 1 Implies Implies OperationCalls are directly translated to an Alloy implies formula ImplicationFormula 3 3 2 And O An OCL and OperationCall is translated to an Alloy binary formula BinaryFormula with a AND Logical operator 3 3 3 Dot Dot OperationCall expressions in OCL are navigation expressions which use the navigation dot O An OCL Dot OperationCall is
17. ns on the translation the reader is referenced to Chapters 2 and 3 If the reader wants to learn details on how to use UML2Alloy s he is referenced to Chapter 4 Finally Chapter 5 presents a number of simple examples to demonstrate how UML2Alloy can be used 1 1 Minimum Requirements UML2Alloy requires Sun Java 1 5 2 Translating 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 2 1 Classes Subclasses and Types 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 7 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 2 2 O Custom data types We translate all Classes with the DataType stereotype to Signatures In principle Custom data types are not treated any different than any other Class Restrictions X No primitive data types as defined in the UML standard are currently supported by the implemen tation Since UML2Alloy 0 3 rudimentary support for integer expressions has been introduced X Multiple packages are not supported Translation of the classes of one package at a time takes place
18. nstallation Unpack the compressed file of the distribution to a directory Depending on the platform edit the run_windows bat or run_linux sh files and make the necessary changes to the path variables The program can be started by executing the run windows or run linux files respectively 4 2 Using UML2Alloy 4 2 1 Step 1 Figure 4 1 depicts the first screen that prompts the user to select the path to the XMI file of the UML model For a table of the XMI files currently supported by UML2Alloy please refer to Appendix A The user then needs to select the path to the Alloy file text file with an als extension that will be generated if the transformation is successful The user then needs to click on Parse This starts the parsing method Messages on the progress appear on the console T he next screen that will be presented to the user is depicted in Figure 4 2 4 2 2 Step 2 In this screen the user is presented with all the Invariants and Operations of the UML models The first column depicts the Operation or Invariant name 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 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 Si
19. p 40 the UML metamodel reffers to Association Ends as Properties 7 p 29 O All association ends have to have names Role names have to be unique Since UML2Alloy 0 3 this is not a requirements If an Association End does not have a name it will be assigned the name of the 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 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 annotations are not supported e g subsets ordered etc x Only binary associations are supported in the current version of the implementation X Custom multiplicities are not currently supported by the implementation Only the predefined 1 0 1 1 and 0 multiplicities are supported X The UML specification allows for unspecified navigability 7
20. s 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 5 5 Examples This chapter presents a number of simple examples to demonstrate the usage of UML2Alloy 5 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 5 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 Classi inv areSame Classi allInstances gt forAll cli Classi cli c2 c1 cli This assertion states that for each Classl 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 Step 2 we define that we want to translate it as an assertion i e a statement to check Similarly we formulate the following OCL statement to reason about t
21. the text file and perform the analysis using Alloy Analyzer In the future we endeavour to use Alloy Analyzer as a library to incorporate its functionality in 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 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 4 and 1 If the reader is interested in the transformation rules and the restrictio
22. use attribute OCL expressions which reference the Boolean values rue or false directly are not supported For example an expression like if condition then expression else false endif is not currently supported Instead an expression which always evaluates to false could be used in the else branch of the above statement 3 1 Invariants Please NOTE The UML standard specifies that invariants are implicitly qualified over all of the instances of the context 5 A 3 1 5 So for example an invariant context C1 inv test self attribute value is implicitly transformed to context C1 C1 allInstances forAll v1 C1 v1 attribute value UML2Alloy currently supports only the second expanded form i e with the explicit quan tification using allInstances and forAll NOT the first form Support for the first form will be provided in the future O Class invariants are generally translated to Alloy facts They can also be translated to Assertions This is defined during the transformation process For more information please see the examples in Section 4 2 2 Each invariant is translated to a predicate and then a fact statement which references the predicate is added Restrictions 3 Translating OCL 6 X Only Class invariants defined in the namespace of a Class are supported i e Class invariants X Invariants have to have a name 3 2 Operations The effects of Operations is defined using OCL pre a
23. y manual areSame INVARIANT ASSERTION Y bidirectiional INVARIANT Proceed Figure 5 3 Selecting the mapping toin Alloy This step is depicted in Figure 5 3 The areSame and bidirectional are the two invariants we specified in ArgoUML By default the statements specified as invariants in the original UML model are translated to invariants in Alloy facts according to the Alloy terminology We want to check if these statements are satisfied They therefore need to be transformed to assertions not invariants We specify that by selecting in the drop down menus that the original OCL invariants are transformed to assertions indicated by the red arrows in Figure 5 3 We then click on the proceed button Finally in the last step we specify a default scope of 3 We do not need to change any other parameters in the last screen The transformation process has finished without an error and the Alloy file has been generated in the path we specified in the first step We now need to invoke the Alloy Analyzer to conduct the analysis On the main Alloy Analyzer window we Open the Alloy file generated by UML2Alloy We first have to Build the file Then we need to select from the drop down menu indicated by the red arrow in Figure 5 4 the statement we want to simulate or check In this case our model has only two assertions areSame and bidirectional We first select from the drop down menu the areSame assertion
Download Pdf Manuals
Related Search