Use

  • open the Gr-Tool
  • design your goal model. The name of the goal should be constructed based on the following grammar: IDENTIFIER: GOAL NAME, where IDENTIFIER identifies the goal, and GOAL NAME specifies the name of the goal. For example, G2: Quote Given specifies that the goal Quote Given is associated with the identifier G2.
  • save your goal model, e.g., in the file model.goal
  • create a .lts file using MTSA
  • specify the FLTL description of goals through assertions, i.e., assert G2=(), where G2 is the identifier of the goal. Note that, the identifier of the assertion must mach the identifier used for the goal.
  • design your MTS using MTSA
  • save your design into an appropriate .lts file
  • run COVER by typing the command java -jar COVER.jar goalModelInitial.goal design.lts PROCESS finalGoalModel.goal where
    • goalModelInitial.goal contains the original goal model;
    • design.lts contains the current design (the MTS);
    • PROCESS contains the identifier of the process to be considered in the file design.lts
    • finalGoalModel.goal contains the goal model updated with the values obtained by COVER open the generated file (i.e., finalGoalModel.goal) with the Gr-Tool