Skip to content
  Projet Triskell  
 

Generation of Models

Document Actions
In this section we describe how an experiment available as an Alloy model is solved leading to model generation. We specify parameters such as number of models per criteria and SAT solver used.

Steps

1. We copy the generated Alloy file (for example, from platform:/resource/Pramana/demo/MDD4DRES/SimpleUMLCD/output/alloyModel/simpleUML_MM_gts.als) to the directory

"platform:/resource/Pramana/Temp/currentMetaModel"

2. We copy the input domain meta-model (for example, from platform:/resource/Pramana/demo/MDD4DRES/SimpleUMLCD/input/metamodel/simpleUML_MM.ecore) to the directory

" platform:/resource/Pramana/Temp/currentMetaModel"

3. We rename the ecore and als files (for example, simpleUML_MM.als, simpleUML_MM.ecore) to current.als and current.ecore respectively.

4. Go to project "platform:/resource/solveAlloy" and open file "platform:/resource/solveAlloy/src/runAlloy.java"

5. You can set some options:

     5.1 Setting the output directory:

        //Change the root on a different machine
        String root = new String("/Users/sagarsen/Desktop/PramanaDemo/demoSpace/Pramana/");


     5.2 Setting the number of solutions per predicate:

         //Choose number of solutions desired per predicate
           Integer numberOfSolutions=new Integer(5);

    5.3 Choosing a SAT solver (at present it is set to MINISAT which allows incremental solving and several solutions). Other options include BerkMin, ZChaff, SAT4J etc..

          options.solver = A4Options.SatSolver.MiniSatJNI;

6.  Run the program runAlloy.java after correctly setting these options to generate (or not if no solutions exist) models in the directory:

"platform:/resource/Pramana/Temp/alloySolutions"


7. Alloy Instances are generated are in XML format.