CGMTool User Manual
Contents
1. Graphically it is represented as rounded rectangle and can be created using Require ment tool located in the palette keguriement Figure 14 Requirement Node II Goal Goals Figure are intermediate goals in a constrained goal model and can only be refined into other intermediate goal nodes tasks and domain assumptions in the model They are graphically represented as Oval and can be created using Goal tool located in the palette 10 III IV Figure 15 Goal Node Task Tasks Figure are leaf goal in a constrained goal model and can only be refined into other tasks in the model Graphically they are represented as Hexagon and can be created using Task tool located in the tool palette Figure 16 Task Node Domain Assumption Node Domain Assumption Figure are propositional nodes and can only be refined into other domain assumption nodes in the model Graphically Domain Assumption nodes are represented as Rectangle and can be created using Domain Assumption tool located in the CGM Tool palette DAN Figure 17 Domain Assumption Node Refinement Refinements are represented as a small dark circle and works as a merging point for the edges connecting a group of source nodes to a target node in a refinement relation It can be created by using Refinement tool located in the CGM Tool palette 11 Note e If th2. Figure 11 Rename dialog box The selection of rename command will be followed by a dialog box Figure 11 that will let you choose the new name When done press Ok to confirm or Cancel to abort the operation Delete Project Folder and Files To delete a project a folder or a file left click on it and press Del on the keyboard or right click on it and select Delete command from the context menu amp Delete Resources E Delete project contents on disk cannot be undone Figure 13 Delete project dialog box The selection of delete command will be followed by a dialog box Figure 13 that will require your confirmation for the deletion of the file T he confirmation dialog box is slightly different for project deletion Figure 12 Which has a check box that provides option to physically delete the project from the file system If not checked the project will only be removed from the project explorer view and will be recoverable later but 1t will not be possible to create a new project with the same name in the project structure Select Ok to confirm the deletion of the file otherwise press Cancel to abort the operation Note e Some default folders in CGM Tool can not be Deleted or Renamed TI Outline View This view displays the contents of the active editor as list of structural elements It helps the modeler to easily navigate through the model and to see the overall pi
3. 35 35 37 1 Getting Started CGM Tool is a modeling and reasoning tool support for constrained goal models 1 It enables diagrammatic modeling of constrained goals with automated well formedness anal ysis and multi objective lexicographical reasoning CGM Tool utilizes OptiMathSAT SMT solver 2 as a back end engine for its reasoning functionality To start using CGM Tool first extract the contents of the downloaded archive file into any directory of your computer Since the reasoning functionality of the tool principally relies on OptiMathSAT solver installation of OptiMathSAT is required For this you need to download OptiMathSAT solver from http optimathsat disi unitn it and extract its content into OptiMathSAT folder of the extracted tool After that run the launcher CGM Tool consequently a splash screen with the logo and version of the tool will appear in the middle of your screen indicating that the program is loading Figure 1 pe eg ma i LIMIWERSITY Loading Workbench aap ny EEF Figure 1 CGM Tool splash screen Subsequently you will be asked to read and accept the terms of use To start using the tool select the license agreement checkbox on the bottom of the page and press I Agree button you can also click on Decline button in order to turn down the license agreement and exit from the program After you agree with the license the tool will open a change log window Figure 2 and present you list
4. Goal Model Tool File Edit Model Analysis Window MENU BAR A SMT Variable Global Constraint Check well formedness Generate Scenario Launch reasoner tS Project Navi O 8 CGMModel cgm 3 Lo ass amp amp 100 i mA i CGMProject TOOL Models CURRENT ACTIVE BAR Optimathsat MODEL EDITOR 2 Scenarios PROJECT e EDITOR AREA NAVIGATION AREA ODE MODEL Py OUTLINE VIEW PROPERTY ANALYSIS VARIABLE VARIABLE VIEW REPORT VIEW VIEW Bl mr az Outline Goal Md PALETTE REASONING RESULT VIEW CI Properties Analysis Report CI Node Variable CI Model Variable DI Reasoning Result Property Value Name IE CGMModel Description Further Figure 3 CGM Tool Overview 2 1 CGM Tool GUI lt e Palette gt h 2 Nodes do O Requirement O Goal Task O Domain Assemption Relations 45 A Refinement 4 Conflict E Contribution A Bl Contribution a An The graphical user interface of CGM Tool is composed of menus editor area palette and several different views T he following sub sections will explain parts of the GUl one by one 2 1 1 Menus Commands which are scattered over the tool menu bar and tool bar are the main interfaces to access the primary functions of CGM Tool The succeeding sub sections will introduce these commands and their use File Edit Model Analysis Window Figure 4 CGM Tool menu bar I Menu Bar CGM T
5. can see that the node is added in the required location with its default name The automatically assigned default name can be change into any other name by simply type the desired name while the node is active selected To return to selection tool click outside of element Note e Names of nodes should be unique in the model 6 Tip e While creating a node you can press the Ctrl or Apple in case of Macintosh key on the keyboard to create sequence of nodes with the same type without the need to select the node creation tool repeatedly 15 P New CGM Model bla Enter or select the parent folder CGMProjectModels d CGMProject gt Models Optimathsat 2 Scenarios File name CGMMode cgm Cancel Figure 21 Creating new CGM Model wizard 2 Nodes O Requirement IMI _ Requirement a Create a new requirement Figure 22 Adding CGM node into the model 4 4 Adding Relations CGM relations are links between two CGM nodes as a result in order to create a relation you need to have at least two nodes in the model which will work as a source and target node of the relation The following two steps shows how to create relation between nodes Figure 23 III Select the required relation from the palette area and then click on the top of the desired source node 16 II While keeping the mouse not pressed move the mouse cursor into the target eleme
6. objective reasoning with unsat core extraction This feature enables modelers to reason on the model and examine whether the underlying model is realizable or not To provide this functionality CGM Tool utilized OptiMathSAT SMT Solver 5 3 1 Launch Reasoner To launch reasoner wizard on a CGM model select Launch Reasoner command from Analysis menu alternatively it can be launched by Launch Reasoner icon of the toolbar Launching reasoner command will automatically initiate well formedness check on the model If the check does not discover any problem the tool will encode the graphical model into SMT2 formula then it will call OptiMathSAT solver on the top of it After that the reasoning result file which is generated by OptiMathSAT solver will be parsed If the model is realizable satisfied then the results will be presented in the following format e Highlight parts of the model in blue which are realizable satisfied Figure 39 e Generate a pdf report for the reasoning result which contains the diagrammatic result encoded smt2 file and the OptiMathSAT output file e And tabular result Figure 40 that is filled with the calculated values of all non zero SMT variables and the total reasoning time ol Schedule ScheduleAutom Figure 39 Highlighted Satisfied Nodes FI Properties Ta Analysis Report DI Reasoning Result 7 Model Variable CI Node Va Name Value 4 Reasoning Resul
7. of constrained goal model will be discussed on section 3 and creation of nodes and relation will be covered on section 2 1 3 Views CGM Tool allows its users to navigate and modify model data through its views These views can be freely moved and positioned across the tool GUI This section discusses some of the main views and basic operations on them where as other views such as Property Analysis Report Reasoning Result Node Variable and Model Variable of the tool will be presented in detail later in this document I Project Explorer View It enables to view CGM Projects and its contents hierarchically Furthermore it allows modelers to perform the following operation a Open File A file in project explorer can be opened by double clicking on it It is also possible to open a file by selecting it with the mouse and pressing enter on the keyboard alternatively you can right click on the file and select open from the context menu Figure 10 4 13 CGMProject a 2 Models CGMModel cgr iis Optimathsat Scenarios Open Open With Figure 10 Open file b Rename Project Folder and Files To rename a project a folder or a file just select it with the mouse and press F2 on the keyboard or use the Edit menu and then select Rename command Renaming can be also performed by right click on the file and select Rename in the context menu GS Rename Resource New name MO
8. B Undeclared SMT Variable costCall in Global constraint Undeclared Variable B Undeclared SMT Variable cost in Global constraint Undeclared Variable Undeclared SMT Variable scheduleTime in Global constraint Undeclared Variable i Goal Element Goal should be a Requirement node Invalid Goal Node il mr Description Figure 34 Analysis report table 5 2 Scenario Generation Scenario models are well formed and valid copies of the original model their purpose is to provide a possibility to model a small scenario of a very complex system and to perform reasoning on it It enhances the reasoning process by providing the copy of the model for the user to play with by changing and modifying the scenario model until the desired result achieved while keeping the original model unmodified 5 2 1 Generate Scenario Model The scenario generation wizard can be launched by choosing Generate scenario com mand from Analysis menu alternatively it can also be launched by Generate sce nario icon of the tool bar Once you choose Generate scenario command an automatic well formedness check will be performed on the model and if the model contain severe errors such as invalid refinement node and or undeclared SMT variable it will notify the modeler to correct these problems Figure 35 and will halt the scenario generation process However if the automatic well formedness analysis identify only less severe error w
9. CONSTRAINED GOAL MODELING AND REASONING TOOL USER MANUAL revision 1 0 1 For CGM Tool Version 1 0 0 http www cgm tool eu Contents 1 Getting Started 2 GUI and Working Environment 21 CGM Tool GUI L Dal Vici amp ake eee eee eee ee hee ee ee ee 2 1 2 Editor Area and Palette 0 0 0 00 00 0200 a Dil VICON tee eo ee Cee Oe eee eee ee Y 3 CGM Nodes and Relations 3 1 CGM Nodes 0 0 00000 2 3 2 CGM Relations 4258465864 6 e825R86R8ER AAA 4 1 Creating New CGM Projectj 0000 4 2 Creating New CGM Modelj 0 0 0 0 200000000084 4 3 Adding Node 24 ee eee se eee e ee edee eed ads 4 4 Adding Relationsj 20000 4 5 Force True and Force False Operations 4 6 Global and Local Constraints 0 0 0 0 0 0 0000004 4 6 1 Defining Local Constraints 0 0 0 2 2084 AE A SNE ii DIE a ae mia e rd 4 1 1 Variable Declaration ee 4 7 2 Variable Naming sos ae aa A AAA a rre arpas KO AP ee sees pe ee ee eee ee ee eee pen ehue eee EL ET ne ee Ae ee eee eek as Dm OW WO W 5 Well formedness Analysis Scenario Generation and Reasoning 5 1 Well formedness Check 5 1 1 Launch Well formedness Analysis 0 4 52 Scenario Generation 5 2 1 Generate Scenario Model 5 3 Reasoning on the Model 5 3 1 Launch Reasoner 6 Acknowledgment Appendices A BNE of SMT Formulas 27 2r 28 29 29 dl l 34
10. M MONOMIAL MONOMIAL MONOMIAL MONOMIAL MONOMIAL MONOMIAL NUMBER VARIABLE NUMBER VARIABLE NUMBER INTEGER NUMBER REAL NUMBER INTEGER NUMBER 0 9 REAL NUMBER INTEGER NUMBER 0 9 0 9 VARIABLE IDENTIFIER 360 7 Acronym CGM Constrained Goal Model DAN Domain Assumption Node ERC European Research Council GUI Graphical User Interface OS Operating System RCP Rich Client Platform Application SMT Satisfiability Modulo Theories 37 References 11 Mai Chi Nguyen Roberto Sebastiani Paolo Giorgini and John Mvlopoulos Multi objective reasoning with constrained goal models 2 Roberto Sebastiani and Patrick Trentin Optimathsat A tool for optimization modulo theories 38
11. arnings such as invalid goal node it will report the warnings for the modeler and will give an option to automatically correct these problem by itself Figure 36 If everything goes fine and if no problem detected by the analysis a dialog box with a text field for the name of the scenario 29 will appear on the screen Figure 37 give it a valid name and press Finish to complete the scenario generation process There are some invalid refinernents in this model Please see the analysis report and fix them first Figure 35 Scenario generation error notification GF Warning This model have some invalid root and or leaf nodes Do you want the tool to fix them automatically ye ne Figure 36 Scenario generation warning notification es EGS Make ready to reason wizard Mame scenarioOnel Figure 37 Scenario generation dialog box The generated scenario model will be stored inside Scenarios folder of the current project Specifically it will be found inside a folder named by the original model name which reside inside Scenarios folder Figure 38 30 a 2 CGMProject a 2 Models ExampleOne cgm 0 il Orginal Model Optimathsat a 2 Scenarios 4 ExampleOne a 2 Model 2 scenarioOne cgm i Generated Scenario Reports Model Figure 38 Generated scenario location 5 3 Reasoning on the Model CGM Tool provides automated mulit
12. atisfied and it will be denied when its negative constraint is satisfied To define local constraint for a node follow the following steps Figure 25 I Right click on the desired node and choose Define element constraint command from the context menu A pop up window with two text fields will appear II Write the positive and negative constraints formulas in the text field respectively and then press OK CO Define Constraint emo gt ri Positive Constraint RI and not CallHotelsAndConventionCenters not and CallPartnerinstitution G X Delete Negative Constraint and CollectTimetable lt x 7 y 3 y gt z 73 q l 3 y Force True Force False 4 Convert to Goal Wall Define element constraints Cancel Figure 25 Defining Element Constraint Note e Constraint formulas must be written based on the SMT BNF listed on Appendix one 6 Tip e The text field has integrated content assist pressing Ctrl space while writing the formula will reveal the list of available options e The syntax check feature of the constraint text field will assist you to write a syntactically correct SMT formula It automatically checks the user input and underline red below the incorrect ones 4 6 2 Defining Global Constraints Global constraints are SMT formulas which need to be satisfied for the whole model to be satisfied These formulas can be defined on CGM models by using
13. ct using this option a Right click anywhere on the Project Navigator then select New CGM Project command from New context menu b Give a name for the new project and click Finish button New tE New CGM Project LA Mew CGM Diagram Go Into Figure 20 Creating CGM project using Project Navigator context menu 4 2 Creating New CGM Model Models of constrained goals must always be created inside Models folder of a CGM project And it can be created either from the File menu of the tool or using the context menu of Project navigator 14 I From file menu a Click on the File menu and select New CGM Model b A new model creation wizard will be opened Figure 21 ensure that the selected parent folder is Models c Give a name for the model and click Finish button II Using project navigator a Right click anywhere on the Project navigator then select New CGM Model command from New context menu b After that follow step b and c of the above method 4 3 Adding Nodes Follow the following steps to add CGM nodes in the editor area Figure III Select the node that you want to add from the tool palette by clicking on it II Move the mouse cursor over the editor canvas the cursor of the mouse will change its icon this time Then left click on the area of the editor that you want to add the node III You
14. cture of the model The outline view has two parts a The lower part is a miniature of the entire model b Where as the upper part is a hierarchical representation of the model Selection of an element on this part will automatically reveal the selected element in the editor area 3 CGM Nodes and Relations This section presents some of the major constructs nodes and relations of constrained goal models Moreover it introduces how to use these elements to build a valid goal model and provides basic modeling guidelines 3 1 CGM Nodes In constrained goal models Requirements are used to represent the desired state of affairs that modelers want the system to achieve these elements can be progressively refined into intermediate goals Goal until the refinement process produces actionable leaf goals which require no further decomposition Task Whereas propositions about the domain which need to be held for a goal refinement relation to work can be represented as Domain As sumption nodes in the model Refinements are used to represent the alternative ways to achieve a particular goal in the model The refinement of an element is a conjunction of the sub elements that are necessary to achieve that element 1 I Requirement Requirements Figure are root goals in the model which can be refined into other nodes in the model However no other node in the model cannot be refined into it
15. e target of a refinement is a goal node then its source should contain at least one goal node e If the target of a refinement is a domain assumption node then its source should only contain domain assumptions e Refinements should not form cycle Table 1 lists available properties for CGM nodes Name Text field which contains name of the selected CGM Node Description Text field which contains the general description of the selected CGM Node Positive constraint Text field which contains the positive constraint of the node Negative Constraint Text field which contains the negative constraint of the node Table 1 CGM nodes properties 3 2 CGM Relations CGM Relations links are graphical ways of specifying constraints in the goal model CGM Tool supports expression of the following relation between nodes III Contribution If a contribution relation defined between two CGM nodes it means that satisfying the source node will force the target node to be satisfied Graphically it is denoted as a directed arrow with label on the middle and can be created by Contribution tool located in the CGM Tool palette 01 Conflict If a conflict relation defined between two CGM nodes it means that these two nodes cannot be satisfied simultaneously Graphically it is denoted as a directed arrow with label on the middle and can be created by Conflict tool located in the CGM Tool palet
16. equipped with other func tionalities that helps to perform well formedness check and automated reasoning on the underlying model furthermore it enables generation of reasoning report in pdf format 5 1 Well formedness Check The well formedness check of CGM Tool helps to examine and verify the well formedness and validity of constrained goal models A CGM is considered to be well formed if its constitute elements nodes and relations are modeled and interconnected according to the syntax and semantics of the modeling language Thus the provided functionality for well formedness check performs the following post modeling analysis to verify the compliance of the underlying model with the semantics of the modeling language I Empty diagram check verify the emptiness of the given model If it is empty none of the succeeding well formedness checks will be performed However if it has contents i e nodes and relations the check will return No error found and will perform the next check II Invalid goal node check This check examines the validity of goal nodes in the model According to CGM every root goals should be Requirement and leaf goals should be Task This check helps to identify goal nodes that violates this demand of the modeling language III Invalid refinement check Based on the modeling language of CGM jif the target of a refinement relation is goal node then at least one of the sources of that refi
17. iMathSAT output file will be stored in the Optimathsat folder of the current project And the reasoning report will be found on the Report folder of the active Scenario folder 33 6 Acknowledgment The research leading to these results has received funding from European Research Councel ERC under grant number 267856 Lucretius 34 Appendices A BNE of SMT Formulas FORMULA ATOM ATOM and FORMULA FORMULA or FORMULA FORMULA not FORMULA xor FORMULA FORMULA Note in SMT language iff is written as FORMULA FORMULA implies FORMULA FORMULA Syntactic sugaring formulas if then else Ite FORMULA FORMULA FORMULA Equivalent to xor Alternative FORMULA FORMULA Equivalent to implies Causes FORMULA FORMULA Requires FORMULA FORMULA Cardnality boolean constraints OneOf FORMULA FORMULA AtMostOneOf FORMULA FORMULA AtLeastOneOf FORMULA FORMULA ExactlyNOf INTEGER NUMBER FORMULA FORMULA 6 9 AtMostNOf INTEGER NUMBER FORMULA FORMULA AtLeastNOf INTEGER NUMBER FORMULA FORMULA NOTE for boolean formulas only no SMT the preceding op tion is sufficient BOOLEAN ATOM MATH ATOM BOOLEAN ATOM IDENTIFIER 39 IDENTIFIER a zA Z a zA Z0 9 MATH ATOM OP MATH TERM MATH TERM OP GS gt gt lt MATH TER
18. iable name text field and choose Define Button 19 KI KI Upper bound Model level The upper bound of the value of the eet ae ee Lower bound Model level The lower bound of the value of the Priority Model level The priority order of the variables Lowest number i e 0 has highest pri ority Objective MINIMIZE Model level Stakeholder s objectives towards the value of the variable in terms of min imizing or Maximizing Calculation method Default Model level The choice of stakeholders for compu tation of the variable outcome Stake holders can either follow the default calculation method of the tool or define a calculation method by themselves Table 2 List of SMT variables attributes III It is possible to define more than one variable to the model for this follow the above step repeatedly until you finish defining any number of variables In case if you want to remove a previously defined variable from the list you can do so by right click on the required variable from the list and select Remove variable context menu Note e weight is a default variable for all constrained goal models therefore it is not possible to remove change it from SMT variable list SMT variables are composed of several model level and node level fields attributes Node level fields are available for all element nodes except intermediate goals i e goals in the model Table 2 presents the summa
19. ive Value Negative Value weight 20 7 cost 4 O Figure 28 Node SMT Variables Table 21 4 8 Frequent Modeling Operations 4 8 1 Converting Nodes to Each Other CGM Tool enables modelers to automatically convert nodes in the model to one another Perform the following steps to access these functionality Figure 29 III Right click on the node that you want to convert II From the list of context menus i e Convert to Requirement Convert to Task Convert to Goal and Convert to DAN choose the target node type into which you want to covert fenton y gt GoalOne Delete Fa Force True Force False Convert to Requirement Convert to Task Convert to DAN Figure 29 Converting Node Note e In order to maintain the validity and correctness of the model the availability of these node conversion commands will be customized based on the refinement relations of the selected node Table 3 presents the availability requirements of each function on a particular node e All node conversion commands are available on Isolated CGM Nodes Isolated nodes are neither source nor target node of any refinement relation in the model 22 4 8 2 Converting Relations to Each Other In addition to the support for converting nodes CGM Tool allows modelers to convert relations to each other Perform the following steps to access these functionality I Righ
20. nement should be a goal node This check helps to verify whether the underlying model satisfies this requirement or not If the model contain nodes that breach this need the check will automatically return their lists and possible causes IV Undeclared variables check Modelers must declare every numeric variables that they are using in both global and local constraints The purpose of this check is to examine every user defined constraints in the model and identify the use of any unde clared SMT variables inside it And in case of discovery it will notify the name of the 21 undeclared variable and its location i e name of specific node or global constraint where it is being used 5 1 1 Launch Well formedness Analysis Well formedness analysis can be launched through Check well formedness command of Analysis menu Alternatively you can also launch it through Well formedness check icon of the tool bar Once you choose the well formedness check command a dialog box with an empty white area will appear Figure 33 To start the analysis you must press Run Analysis button This will automatically start the analysis engine subsequently tasks being performed and their completion status will fill the white area one by one while the progress of the analysis also shown on the progress bar of the dialog ES Well formedness ES Well formedness es Well formedness Well formedness B Well formed
21. ness Analysis Completed 4 Empty Diagram Completed amp Invalid Goal Node Completed 4 Refinement Validity Check Completed B Undeclared Variable Completed en Figure 33 Well formedness analysis dialog Completion status of each checks of the analysis can be categorized into one of the following results e Started The task has started and is performing the required check e Completed Green The task completed without finding any errors e Completed Orange The task completed and found some non serious errors warn ings e Completed Red The task completed and found some serious errors 28 e Exception The task has encountered an internal error while executing This should never occur in case you revive this error please contact the CGM Tool support Upon completion lists of errors and warnings discovered in the model by the analysis will be displayed in the Analysis Report table Figure 34 of the tool E Properties Analysis Report TI Node Variable 7 Model Variable 7 Reasoning Result Problem Description a Well formedness Analysis ii Goal Element DAN should be a Requirement node Invalid Goal Node Undeclared SMT Variable time in Global constraint Undeclared Variable Goal Element fsdaf should be a Requirement node Invalid Goal Node Invalid Refinement RL Refinement Validity Check ii Goal Element G1 should be a Requirement node Invalid Goal Node
22. nt and then click on it This will create the required relation between the elements 2 Relations if Refinement Conflict FA Contr Conflict Create Conflict Link Figure 23 Creating CGM relation 4 5 Force True and Force False Operations In constrained goal modeling nodes can be forced either to be true satisfied to achieve the desired result or to be false denied to reduce the effort of achieving them To force a node to True or to False Figure 24 Right click on the desired node and then select either Force True or False Force command from the context menu Performing this operation will change the color of the node into Red or Green when forced to true or false respectively eN I Delete Force True Force False Figure 24 Force node to true false 4 6 Global and Local Constraints In addition to constraints which can be expressed graphically in terms of contribution con flict refinement binding and bi contribution modelers can further enrich their models by defining arbitrary prerequisite logic formulas constraints These formulas can be expressed either globally to the model or as a local positive and negative constraints for a particular element in the model 17 4 6 1 Defining Local Constraints Local constraints are positive and negative pair of prerequisite formulas expressed on the top of CGM nodes Where an element will be satisfied when its positive constraint is s
23. ool menu bar Figure 4 is a collection of the following menus a File Menu File menu Figure 5 of the tool contains commands such as Create New CGM Project Create New CGM Model and Save options which are mainly used for handling of CGM models and projects Furthermore it offers commands for closing the active editor and for exiting from the application Edit Model Analysis Window New CGM Project LA Mew CGM Diagram Save Ctrl 5 Save As Save All Ctrl Shift Close Ctrl W Close All Ctrl Shift W Exit Figure 5 CGM Tool File menu b Edit Menu The modeler can perform Undo Redo and Select All actions on the active model by accessing commands from this menu Figure 6 Model Analysis Wi Undo Ctrl Zz Redo Ctri Select All Ctrl A Figure 6 CGM Tool Edit menu c Model Menu The model menu Figure of CGM Tool provides basic commands to define SMT Variables see section 4 7 for more and Global Constraints see section 4 6 for more into the active goal model Analysis Window Var SMT Variable Ge Global Constraint Figure 7 CGM Tool Model menu d Analysis Menu This menu Figure provide access to the following main functions of the tool 1 Check Well formedness Performs well formedness check see section over a CGM model to verify that it comply with the semantics of the modeling language li Generate Scenario This command allows the user to generate a scenario model of the current acti
24. ry of these attributes their default values and availability in terms of location where you can define their values 20 4 7 2 Variable Naming I SMT variable name can be any legal identifier which begin with a letter and followed by any combination of letters and digits II SMT variable names are case sensitive therefore please make sure that you wrote the exact variable name while utilizing them inside prerequisite constraints 4 7 3 Setting Model Level SMT Variable Values You can set modify model level global values of SMT variables such as Upper bound Lower bound Priority Objective and Calculation Method by going into Model variable table Figure 27 located below the editor area of the tool FI Properties 2 Analysis Report CI Node Variable T Model Variable Reasoning Result Name Upper Bound Lower Bound Priority Objective Calculation Method weight Infinity Infinity 1 MINIMIZE Default cost Infinity Infinity O MINIMIZE Default Figure 27 Model SMT Variables Table 4 7 4 Setting Node Level SMT Variable Values Node level SMT variable values such as positive and negative values can be expressed in Node Variable table which is located right next to Model variable table This table is filled with list of variables and their values for the actively selected node on the editor E Properties a Analysis Report C Node Variable DI Model Variable Rei Mame Posit
25. s of recent changes made on the tool The log window can be closed by the little X button right next to the Change Log tab ICGM Tool is Eclipse RCP based application because of this no prior set up installation is required amp Constrained Goal Model Tool e ES a File Edit Window GF Welcome El Change Log Version 1 0 0 30 01 2015 First release of the tool Figure 2 CGM Tool change log Minimum requirement e To run CGM Tool you need to install Java 7 or more Important for Linux based OS Users CGM Tool and OptiMathSAT solver require execute privilege to function correctly Please follow the following steps to fulfill this need I For CGM Tool a Right click on the launcher i e CGM Tool and select Property b Then on permission tab check Allow executing file as a program check box ILI For OptiMathSAT a First go to bin folder of the extracted OptiMathSAT folder which re sides inside CGMTool Linux 64bit OptiMathSAT optimathsat 1 3 1 linux 164 bin b Inside bin directory you will find optimathsat file right click on it and choose property Then on permission tab check Allow executing file as a program check box 2 GUI and Working Environment This section describes the basic GUI parts of CGM Tool and also provides a general overview of the tool working environment Figure 3 outlines the general appearance of the tool aS Constrained
26. t Total Reasoning Time 0 094 Seconds weight 65 costRoom 80 cost 80 Figure 40 Reasoning Result Table However if the solver identifies that the model is unrealizable unsatisfied the tool will give you an option to reveal parts of the model which made the whole model unrealizable Figure 41 Proceeding with this option will run unsat core extraction on the model and produce the results for the unachievability of the model in the following format e Highlight parts of the model in yellow which are unrealizable unsatisfied Figure 42 e Generate a pdf report for unsat core extraction result which contains the diagram matic result encoded smt2 file and the OptiMathSAT output file e And tabular result Figure filled lists of encountered problems that made the model unsatifiable UNSAT Model a Cox Figure 41 UnSAT core extraction dialog box result 32 Figure 42 Highlighted UnSAT Core result E Properties UNSAT Core Extraction a Analysis Report El Node Variable O Model Variable O Reasoning Rest Elernent Encountered Problern Budget gt Budget weight 40 Hotel implies Hotel Hotel weight 0 Lapland gt Lapland weight 200 weight weight Comfortable weight Budget weight Relaxed weight Fun weight B Couchsurting gt Couchsurfing welght 0 Description Figure 43 UnSAT Core extraction tabular result During the reasoning process the encoded formula and the Opt
27. t click on the relation that you want to convert ILI From the list of context menus i e Convert to Contribution Convert to Con flict and Convert to Bi Contribution choose the target relation type into which you want to covert 4 8 3 Elements Deletion Use on of the following ways to delete CGM elements from the model I From keyboard Select the Node Relation you want to delete and press Delete key from your keyboard I By Mouse Right click on the Node Relation you want to delete and then select Delete from the pop up menu Figure 30 kl Goal 3 Delete Force True Force False Figure 30 Deleting CGM Element 4 8 4 Renaming Nodes CGM nodes can be renamed by the following way e Select the node that you want to change its name and type the new name of the node press enter to confirm Note e Node names in the model should be unique 23 4 8 5 Moving Elements and Relations I Moving Nodes Nodes can be moved by selecting them and dragging them around to a new position While dragging a node on the model editor area a phantom figure will show the new location to be of the node Figure 31 Figure 31 Moving CGM Node ILI LL Moving Relations To move relations you first need to select them When selected a relation will display a little handle on the middle of the link figure Figure 32 this handle can be dragged with a mouse to the new loca
28. te 12 II Bi Contribution Bi contribution relations are used to represent a two side contribution link between two CGM nodes Graphically it is denoted as a two headed arrow with label on the middle and can be created by Bi Contribution tool located in the CGM Tool palette TV Refinement Binding These are relations between two refinement nodes Graphically it is represented as a two headed dashed arrow and can be created by Refinement binding tool located in the CGM Tool palette Goal Figure 18 CGM Relations Note e All these relations are allowed to form loop in the model 13 4 Basic Operations This section will cover basic operations and techniques that modelers need to follow to build constrained goal models using CGM Tool 4 1 Creating New CGM Project To start modeling and reasoning using CGM Tool you first need to have at least one active project thus the tool allows creation of CGM projects in two different ways I From file menu Follow the following steps to a create CGM project from the file menu of the tool a Click on the File menu and choose New CGM Project b Give a name for the new project and click Finish button Edit Model Analysis Window 12 New CGM Project LA New CGM Diagram Figure 19 Creating CGM project using File menu II Using project navigator Follow the following steps to create a CGM proje
29. the following steps Figure 26 18 I From the tool bar or from Model menu in the menu bar select Global Constraint command it will open a pop up window II In the pop up window Add global constraint text field type the formula of the con straint you want to define and press Add TL Lumma Global formulas can be many therefore follow the above step until you finish defining the constraints In case if you want to remove the previously defined constraint form the list you can do so by right click on the formula and select Remove constraint in addition double clicking on the top of a formula will let you to modify update the formula F Add Global Constraint Add global variable Analysis Window time scheduleTime collect Var SMT Variable Gc Global Constraint Global Constraint f cost costCall costRoom time scheduleTime collectTime ri Figure 26 Add Global Constraint 4 7 SMT Variables SMT variables in CGM are global numeric variables used to express different numerical attributes of elements such as cost work time space fuel etc 4 7 1 Variable Declaration Follow the following steps to define SMT variables to the underlying model I From the tool bar or from the Model menu of the menu bar select SMT Variable command as a result a new pop up window will be opened II Write the name of the variable in the var
30. tion you want to move RI a Figure 32 Moving CGM Relation 4 8 6 Undo Redo Operations All operations performed on CGM Tool editor can be undone or redone using support of the tool You can perform undo redo operation using one of the following ways I Keyboard shortcut e Ctrl Command for Mac Z for Undo e Ctrl Command for Mac Y for Redo 24 TI Menu bar e The the Edit menu of the tool contain Undo and Redo commands for the respective operations III Tool bar e From the tool bar of the tool choose the undo redo icons for the undoing or redoing operations 29 Node conversion command Availability requirement Available only if the selected node is Root node Convert to Requirement i e A node in the model into which no other node is refined Available only if the selected node is Leaf node Convert to Goal i e A node which is not refined into any other node in the model Available only if the selected node is Leaf node Convert to Task i e A node which is not refined into any other node in the model Available only if the selected node is Leaf node Convert to DAN i e A node which is not refined into any other node in the model Table 3 Node conversion commands and their availability requirement 26 5 Well formedness Analysis Scenario Generation and Reasoning Beside the support for modeling constrained goals CGM Tool is
31. ve model details about scenario models can be found on section 5 2 111 Launch Reasoner This command runs OptiMathSAT solver over the current active scenario model and presents the reasoning result by coloring the satisfied nodes of the active scenario model For more information about the reasoning process please see section 5 3 Window Check well formedness Generate Scenario Launch reasoner Figure 8 CGM Tool Analysis Menu ILI Toolbar Functions that are commonly performed within the application can be quickly ac cessed from the tool bar The tool bar of CGM Tool accommodates Check Well formedness Generate Scenario Launch Reasoner and few other commands 2 1 2 Editor Area and Palette I Editor Area The editor area is the main place where main editing operations such as creation deletion modification of the graphical model will be performed CGM Tool support opening of multiple editors at the same time More details about CGM Tool editing area and supported operations will be discussed on section II Palette CGM Tool palette Figure 9 supplies a simple drag and drop facility for creation of nodes and relations graphically on the editor area se Palette gt X gt Nodes as DI Requirement O Goal O Task O Domain Assumption L7 Relations a 7 Refinement Conflict c Contribution 4 Bl Contribution e Refinement Binding Figure 9 CGM Tool Palette Details about the nodes and relations
Download Pdf Manuals
Related Search