VAMPIRE: fix bug in transformation, further implement measurement code

36 files changed, 260 insertions, 171 deletions

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
index 98967181..fc8d3e99 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend
@@ -6,6 +6,7 @@ class VampireSolverConfiguration extends LogicSolverConfiguration {
         
         public var int contCycleLevel = 0
         public var boolean uniquenessDuplicates = false
+        public var int iteration = -1
         //choose needed backend solver
 //      public var VampireBackendSolver solver = VampireBackendSolver.SAT4J
 }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
index 3b5cec0a..3281a196 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.xtend
@@ -46,6 +46,8 @@ class VampireSolver extends LogicReasoner {
                 val transformationStart = System.currentTimeMillis
                 // TODO
                 val result = forwardMapper.transformProblem(problem, vampireConfig)
+                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 val vampireProblem = result.output
                 val forwardTrace = result.trace
 
@@ -71,19 +73,17 @@ class VampireSolver extends LogicReasoner {
                 
 
                 // Result as String
-                val transformationTime = System.currentTimeMillis - transformationStart
+                
                 // Finish: Logic -> Vampire mapping
                 
                 // Start: Solving .tptp problem
-                val solverStart = System.currentTimeMillis
                 val MonitoredVampireSolution vampSol = handler.callSolver(vampireProblem, workspace, vampireConfig)
-                val solvingTime = System.currentTimeMillis - solverStart
                 // Finish: Solving .tptp problem
                 
                 // Start: Vampire -> Logic mapping
                 val backTransformationStart = System.currentTimeMillis
                 // Backwards Mapper
-                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,solvingTime)
+                val logicResult = backwardMapper.transformOutput(problem,vampireConfig.solutionScope.numberOfRequiredSolution,vampSol,forwardTrace,transformationTime)
 
                 val backTransformationTime = System.currentTimeMillis - backTransformationStart
                 // Finish: Vampire -> Logic Mapping
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index b617912d..60309f2d 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -79,14 +79,15 @@ class Logic2VampireLanguageMapper {
                 if (!problem.types.isEmpty) {
                         typeMapper.transformTypes(problem.types, problem.elements, this, trace)
                 }
-                
+
                 // RELATION MAPPER
                 trace.relationDefinitions = problem.collectRelationDefinitions
 //              println(problem.relations.filter[class == RelationDefinitionImpl])
+                toTrace(problem.relations.filter[class == RelationDefinitionImpl], trace)
                 problem.relations.forEach[this.relationMapper.transformRelation(it, trace, new Logic2VampireLanguageMapper)]
-                
+
                 // CONTAINMENT MAPPER
-                containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
+                containmentMapper.transformContainment(config, problem.containmentHierarchies, trace)
 
                 // SCOPE MAPPER
                 scopeMapper.transformScope(problem.types, config, trace)
@@ -107,6 +108,39 @@ class Logic2VampireLanguageMapper {
                 return new TracedOutput(specification, trace)
         }
 
+        def toTrace(Iterable<Relation> relations, Logic2VampireLanguageMapperTrace trace) {
+                val List<VLSVariable> vars = newArrayList
+                for (rel : relations) {
+                        //decide name
+                        val nameArray = rel.name.split(" ")
+                        var relNameVar = ""
+                        if (nameArray.length == 3) {
+                                relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
+                        } else {
+                                relNameVar = rel.name
+                        }
+                        val relName = relNameVar
+                        
+                        val relDef = rel as RelationDefinition
+                        for (i : 0 ..< rel.parameters.length) {
+
+                                val v = createVLSVariable => [
+                                        it.name = support.toIDMultiple("V", i.toString)
+                                ]
+                                vars.add(v)
+                        }
+
+                        val relFunc = createVLSFunction => [
+                                it.constant = support.toIDMultiple("r", relName)
+                                for (v : vars) {
+                                        it.terms += support.duplicate(v)
+                                }
+                        ]
+                        trace.relDef2Predicate.put(relDef, relFunc)
+                        trace.predicate2RelDef.put(relFunc, relDef)
+                }
+        }
+
         // End of transformProblem
         // ////////////
         // Type References
@@ -169,7 +203,6 @@ class Logic2VampireLanguageMapper {
 //              Map<Variable, VLSVariable> variables) {
 //              createVLSReal => [it.value = literal.value.toString()]
 //      }
-
         def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
                 createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)]
@@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper {
         def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred,
                 List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace,
                 Map<Variable, VLSVariable> variables) {
-                        val name = referred.lookup(trace.definedElement2String)
-                        return createVLSConstant => [
-                                it.name = name
-                        ]
+                val name = referred.lookup(trace.definedElement2String)
+                return createVLSConstant => [
+                        it.name = name
+                ]
 //              typeMapper.transformReference(referred, trace)
         }
 
@@ -390,12 +423,11 @@ class Logic2VampireLanguageMapper {
 //              }
                 return createVLSFunction => [
                         if (relation.class == RelationDeclarationImpl) {
-                                                        it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
-                        }
-                        else {
+                                it.constant = (relation as RelationDeclaration).lookup(trace.rel2Predicate).constant
+                        } else {
                                 it.constant = (relation as RelationDefinition).lookup(trace.relDef2Predicate).constant
                         }
-                        
+
                         it.terms += parameterSubstitutions.map[p|p.transformTerm(trace, variables)]
                 ]
         }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
index 181c59ca..efedf6dc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend
@@ -23,7 +23,8 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 this.base = base
         }
 
-        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
+        def dispatch public void transformRelation(RelationDeclaration r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
                 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
@@ -42,19 +43,18 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                val comply = createVLSFofFormula=> [
-                        
+
+                val comply = createVLSFofFormula => [
+
                         it.name = support.toIDMultiple("compliance", relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -79,10 +79,10 @@ class Logic2VampireLanguageMapper_RelationMapper {
                 trace.specification.formulas += comply
         }
 
-        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace, Logic2VampireLanguageMapper mapper) {
-                
-//              println("XXXXXXXXXXXXXXXXX")
+        def dispatch public void transformRelation(RelationDefinition r, Logic2VampireLanguageMapperTrace trace,
+                Logic2VampireLanguageMapper mapper) {
 
+//              println("XXXXXXXXXXXXXXXXX")
 // 1. store all variables in support wrt their name
                 // 1.1 if variable has type, creating list of type declarations
                 val Map<Variable, VLSVariable> relVar2VLS = new HashMap
@@ -102,34 +102,30 @@ class Logic2VampireLanguageMapper_RelationMapper {
 
                 }
 
-                //deciding name of relation
+                // deciding name of relation
                 val nameArray = r.name.split(" ")
                 var relNameVar = ""
                 if (nameArray.length == 3) {
                         relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2))
-                }
-                else {
+                } else {
                         relNameVar = r.name
                 }
                 val relName = relNameVar
-                
-                //define logic for pattern
+
+                // define logic for pattern
 //              val map = new HashMap
 //              map.put(r.variables.get(0), createVLSVariable)
                 val definition = mapper.transformTerm(r.value, trace, relVar2VLS)
-                
-                
-                
-                
-                //get entire contents of and
+
+                // get entire contents of and
                 val compliance = support.unfoldAnd(relVar2TypeDecComply)
-                val compDefn = createVLSAnd=> [
+                val compDefn = createVLSAnd => [
                         it.left = compliance
                         it.right = definition
                 ]
-                
-                val relDef = createVLSFofFormula=> [
-                        
+
+                val relDef = createVLSFofFormula => [
+
                         it.name = support.toID(relName)
                         it.fofRole = "axiom"
                         it.fofFormula = createVLSUniversalQuantifier => [
@@ -143,14 +139,13 @@ class Logic2VampireLanguageMapper_RelationMapper {
                                                         it.terms += support.duplicate(v)
                                                 }
                                         ]
-                                        trace.relDef2Predicate.put(r, rel)
-                                        trace.predicate2RelDef.put(rel, r)
+//                                      trace.relDef2Predicate.put(r, rel)
+//                                      trace.predicate2RelDef.put(rel, r)
                                         it.left = support.duplicate(rel)
                                         it.right = compDefn
                                 ]
                         ]
                 ]
-
                 trace.specification.formulas += relDef
 
         }
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
index 489bf423..e136d1c6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.xtend
@@ -8,7 +8,7 @@ class Vampire2LogicMapper {
 

 //      

         public def transformOutput(LogicProblem problem, int requiredNumberOfSolution,

-                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace,

+                MonitoredVampireSolution monitoredVampireSolution, Logic2VampireLanguageMapperTrace trace, 

                 long transformationTime) {

 

                 // ModelRsult implements LogicResult

@@ -22,7 +22,8 @@ class Vampire2LogicMapper {
 

         def transformStatistics(MonitoredVampireSolution solution, long transformationTime) {

                 return createStatistics => [

-                        it.transformationTime = solution.solverTime as int

+                        it.solverTime = solution.solverTime as int

+                        it.transformationTime = transformationTime as int

                 ]

 //              createStatistics => [

 //                      it.transformationTime = transformationTime as int

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
index 74532ee5..c5cfb1c7 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.xtend
@@ -44,7 +44,7 @@ class VampireHandler {
                 val VAMPNAME = "vampire.exe"

                 val TEMPNAME = "TEMP.tptp"

                 val OPTION = " --mode casc_sat -t 300 "

-                val SOLNNAME = "_solution" + configuration.typeScopes.maxNewElements + ".tptp"

+                val SOLNNAME = "solution" + configuration.typeScopes.maxNewElements +"_" + configuration.iteration + ".tptp"

                 val PATH = "C:/cygwin64/bin"

 

                 val wsURI = workspace.workspaceURI

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
index 600187ca..2c203d6e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index 9517185f..f2461efc 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
index 1241dcb2..c3e185f5 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolver.java
@@ -62,6 +62,8 @@ public class VampireSolver extends LogicReasoner {
     final VampireSolverConfiguration vampireConfig = this.asConfig(config);

     final long transformationStart = System.currentTimeMillis();

     final TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace> result = this.forwardMapper.transformProblem(problem, vampireConfig);

+    long _currentTimeMillis = System.currentTimeMillis();

+    final long transformationTime = (_currentTimeMillis - transformationStart);

     final VampireModel vampireProblem = result.getOutput();

     final Logic2VampireLanguageMapperTrace forwardTrace = result.getTrace();

     String fileURI = null;

@@ -72,16 +74,11 @@ public class VampireSolver extends LogicReasoner {
     if (writeFile) {

       fileURI = workspace.writeModel(vampireProblem, this.fileName).toFileString();

     }

-    long _currentTimeMillis = System.currentTimeMillis();

-    final long transformationTime = (_currentTimeMillis - transformationStart);

-    final long solverStart = System.currentTimeMillis();

     final MonitoredVampireSolution vampSol = this.handler.callSolver(vampireProblem, workspace, vampireConfig);

-    long _currentTimeMillis_1 = System.currentTimeMillis();

-    final long solvingTime = (_currentTimeMillis_1 - solverStart);

     final long backTransformationStart = System.currentTimeMillis();

-    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, solvingTime);

-    long _currentTimeMillis_2 = System.currentTimeMillis();

-    final long backTransformationTime = (_currentTimeMillis_2 - backTransformationStart);

+    final ModelResult logicResult = this.backwardMapper.transformOutput(problem, vampireConfig.solutionScope.numberOfRequiredSolution, vampSol, forwardTrace, transformationTime);

+    long _currentTimeMillis_1 = System.currentTimeMillis();

+    final long backTransformationTime = (_currentTimeMillis_1 - backTransformationStart);

     return logicResult;

   }

   

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
index ac55ebd7..5086d15a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java
@@ -7,4 +7,6 @@ public class VampireSolverConfiguration extends LogicSolverConfiguration {
   public int contCycleLevel = 0;

   

   public boolean uniquenessDuplicates = false;

+  

+  public int iteration = (-1);

 }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 3ebc907b..f537b830 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index c9ae6c62..14a639ad 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index ec8fae35..ba5dbd89 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 5e770b94..f5e4ca8c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 1d3cd01c..6c06a366 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 72067608..1ee73cd6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index a9228720..edda9f05 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
index 3697ed87..8edf2fe9 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
index c489bf07..18c788c6 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index c8961c6e..dc5ec788 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -54,6 +54,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable;

 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl;

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDefinitionImpl;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

 import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;

 import java.util.Arrays;

@@ -65,6 +66,9 @@ import java.util.function.Consumer;
 import org.eclipse.emf.common.util.EList;

 import org.eclipse.xtend.lib.annotations.AccessorType;

 import org.eclipse.xtend.lib.annotations.Accessors;

+import org.eclipse.xtext.xbase.lib.CollectionLiterals;

+import org.eclipse.xtext.xbase.lib.Conversions;

+import org.eclipse.xtext.xbase.lib.ExclusiveRange;

 import org.eclipse.xtext.xbase.lib.Extension;

 import org.eclipse.xtext.xbase.lib.Functions.Function1;

 import org.eclipse.xtext.xbase.lib.IterableExtensions;

@@ -118,18 +122,23 @@ public class Logic2VampireLanguageMapper {
       this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);

     }

     trace.relationDefinitions = this.collectRelationDefinitions(problem);

-    final Consumer<Relation> _function_3 = (Relation it) -> {

+    final Function1<Relation, Boolean> _function_3 = (Relation it) -> {

+      Class<? extends Relation> _class = it.getClass();

+      return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class));

+    };

+    this.toTrace(IterableExtensions.<Relation>filter(problem.getRelations(), _function_3), trace);

+    final Consumer<Relation> _function_4 = (Relation it) -> {

       Logic2VampireLanguageMapper _logic2VampireLanguageMapper = new Logic2VampireLanguageMapper();

       this.relationMapper.transformRelation(it, trace, _logic2VampireLanguageMapper);

     };

-    problem.getRelations().forEach(_function_3);

+    problem.getRelations().forEach(_function_4);

     this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);

     this.scopeMapper.transformScope(problem.getTypes(), config, trace);

     trace.constantDefinitions = this.collectConstantDefinitions(problem);

-    final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {

+    final Consumer<ConstantDefinition> _function_5 = (ConstantDefinition it) -> {

       this.constantMapper.transformConstantDefinitionSpecification(it, trace);

     };

-    Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4);

+    Iterables.<ConstantDefinition>filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5);

     EList<Assertion> _assertions = problem.getAssertions();

     for (final Assertion assertion : _assertions) {

       this.transformAssertion(assertion, trace);

@@ -137,6 +146,49 @@ public class Logic2VampireLanguageMapper {
     return new TracedOutput<VampireModel, Logic2VampireLanguageMapperTrace>(specification, trace);

   }

   

+  public void toTrace(final Iterable<Relation> relations, final Logic2VampireLanguageMapperTrace trace) {

+    final List<VLSVariable> vars = CollectionLiterals.<VLSVariable>newArrayList();

+    for (final Relation rel : relations) {

+      {

+        final String[] nameArray = rel.getName().split(" ");

+        String relNameVar = "";

+        int _length = nameArray.length;

+        boolean _equals = (_length == 3);

+        if (_equals) {

+          relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);

+        } else {

+          relNameVar = rel.getName();

+        }

+        final String relName = relNameVar;

+        final RelationDefinition relDef = ((RelationDefinition) rel);

+        int _length_1 = ((Object[])Conversions.unwrapArray(rel.getParameters(), Object.class)).length;

+        ExclusiveRange _doubleDotLessThan = new ExclusiveRange(0, _length_1, true);

+        for (final Integer i : _doubleDotLessThan) {

+          {

+            VLSVariable _createVLSVariable = this.factory.createVLSVariable();

+            final Procedure1<VLSVariable> _function = (VLSVariable it) -> {

+              it.setName(this.support.toIDMultiple("V", i.toString()));

+            };

+            final VLSVariable v = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function);

+            vars.add(v);

+          }

+        }

+        VLSFunction _createVLSFunction = this.factory.createVLSFunction();

+        final Procedure1<VLSFunction> _function = (VLSFunction it) -> {

+          it.setConstant(this.support.toIDMultiple("r", relName));

+          for (final VLSVariable v : vars) {

+            EList<VLSTerm> _terms = it.getTerms();

+            VLSVariable _duplicate = this.support.duplicate(v);

+            _terms.add(_duplicate);

+          }

+        };

+        final VLSFunction relFunc = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function);

+        trace.relDef2Predicate.put(relDef, relFunc);

+        trace.predicate2RelDef.put(relFunc, relDef);

+      }

+    }

+  }

+  

   protected VLSTerm _transformTypeReference(final BoolTypeReference boolTypeReference, final Logic2VampireLanguageMapperTrace trace) {

     return null;

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
index c175c72a..4c14e93e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java
@@ -176,8 +176,6 @@ public class Logic2VampireLanguageMapper_RelationMapper {
             }

           };

           final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_4);

-          trace.relDef2Predicate.put(r, rel);

-          trace.predicate2RelDef.put(rel, r);

           it_2.setLeft(this.support.duplicate(rel));

           it_2.setRight(compDefn);

         };

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
index 4fbf7291..9fb23c71 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Vampire2LogicMapper.java
@@ -34,7 +34,8 @@ public class Vampire2LogicMapper {
     Statistics _createStatistics = this.resultFactory.createStatistics();

     final Procedure1<Statistics> _function = (Statistics it) -> {

       long _solverTime = solution.getSolverTime();

-      it.setTransformationTime(((int) _solverTime));

+      it.setSolverTime(((int) _solverTime));

+      it.setTransformationTime(((int) transformationTime));

     };

     return ObjectExtensions.<Statistics>operator_doubleArrow(_createStatistics, _function);

   }

diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
index 0c8b0013..a1f19410 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireHandler.java
@@ -25,7 +25,7 @@ public class VampireHandler {
       final String VAMPNAME = "vampire.exe";

       final String TEMPNAME = "TEMP.tptp";

       final String OPTION = " --mode casc_sat -t 300 ";

-      final String SOLNNAME = (("_solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + ".tptp");

+      final String SOLNNAME = (((("solution" + Integer.valueOf(configuration.typeScopes.maxNewElements)) + "_") + Integer.valueOf(configuration.iteration)) + ".tptp");

       final String PATH = "C:/cygwin64/bin";

       final URI wsURI = workspace.getWorkspaceURI();

       final String tempLoc = (wsURI + TEMPNAME);

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
index 9e50006e..b786abfb 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/META-INF/MANIFEST.MF
@@ -6,7 +6,13 @@ Bundle-Version: 1.0.0.qualifier
 Bundle-ClassPath: .
 Bundle-Vendor: %providerName
 Bundle-Localization: plugin
-Export-Package: ca.mcgill.ecse.dslreasoner.vampire.queries,
+Export-Package: ca.mcgill.ecse.dslreasoner.vamipre.yakindumm,
+  ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.impl,
+  ca.mcgill.ecse.dslreasoner.vamipre.yakindumm.util,
+  ca.mcgill.ecse.dslreasoner.vampire.queries,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.impl,
+  ca.mcgill.ecse.dslreasoner.vampire.yakindumm.util,
   yakindumm,
   yakindumm.impl,
   yakindumm.util,
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
index 6a9aee5e..fa271bd3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/plugin.xml
@@ -1,15 +1,13 @@
 <?xml version="1.0" encoding="UTF-8"?><plugin>

   <extension point="org.eclipse.emf.ecore.generated_package">

-    <!-- @generated yakindu_simplified -->

-    <package class="yakindumm.YakindummPackage" genModel="initialModels/yakindu/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/>

-  </extension>

-  <extension point="org.eclipse.emf.ecore.generated_package">

-    <!-- @generated yakindu_simplified -->

-    <package class="yakindumm.yakindumm.YakindummPackage" genModel="initialModels/yakindu/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/>

+    <!-- @generated xGen -->

+    <package class="ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage" genModel="initialModels/yakindu/yakindu_simplified.genmodel" uri="hu.bme.mit.inf.yakindumm"/>

   </extension>

   <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification">

     <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns" id="ca.mcgill.ecse.dslreasoner.vampire.queries.FamPatterns">

       <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.terminatorAndInformation"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.rootElements"/>

+      <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.parent"/>

     </group>

   </extension>

 </plugin>

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
index 057bcf12..cc7f4809 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend
@@ -1,10 +1,10 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse

 

-import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns

+import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel

-import functionalarchitecture.FunctionalarchitecturePackage

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration

 import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel

@@ -12,9 +12,13 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic

+import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace

 import java.io.PrintWriter

+import java.text.SimpleDateFormat

+import java.time.LocalDate

+import java.util.Date

 import org.eclipse.emf.ecore.resource.Resource

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl

 

@@ -26,8 +30,12 @@ class YakinduTest {
                 val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic

 

                 // Workspace setup

+                val Date date = new Date(System.currentTimeMillis)

+                val SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");

+                val formattedDate = format.format(date)

+

                 val inputs = new FileSystemWorkspace('''initialModels/''', "")

-                val workspace = new FileSystemWorkspace('''output/YakinduTest/''', "")

+                val workspace = new FileSystemWorkspace('''output/YakinduTest/''' + formattedDate + '''/''', "")

                 workspace.initAndClear

 

                 // Logicproblem writing setup

@@ -37,12 +45,12 @@ class YakinduTest {
 

                 println("Input and output workspaces are created")

 

-//              val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)

-                val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)

-//              val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")

-                val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")

-//              val queries = GeneralTest.loadQueries(metamodel, YakinduPatterns.instance)

-                val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)

+                val metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE)

+                val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi")

+                val queries = GeneralTest.loadQueries(metamodel, Patterns.instance)

+//              val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE)

+//              val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi")

+//              val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance)

 //              val queries = null

                 println("DSL loaded")

 

@@ -50,40 +58,42 @@ class YakinduTest {
                 var START = 10

                 var INC = 20

                 var REPS = 1

-                

-                val EXACT = -1

-                if (EXACT!= -1) {

+

+                val EXACT = 50

+                if (EXACT != -1) {

                         MAX = EXACT

                         START = EXACT

                         INC = 1

-                        REPS = 5

+                        REPS = 3

                 }

 

-                var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv")

+                var writer = new PrintWriter(workspace.workspaceURI + "//_yakinduStats.csv")

                 writer.append("size,")

                 for (var x = 0; x < REPS; x++) {

-                        writer.append("t" + x + ",")

+                        writer.append("tTransf" + x + "," + "tSolv" + x + ",")

                 }

-                writer.append("avg\n")

-                var totalTime = 0.0

-                var totFound = 0.0

+                writer.append("medSolv,medTransf\n")

+                var solverTimes = newArrayList

+                var transformationTimes = newArrayList

                 var modelFound = true

                 var LogicResult solution = null

                 for (var i = START; i <= MAX; i += INC) {

                         val num = (i - START) / INC

                         print("Generation " + num + ": SIZE=" + i + " Attempt: ")

                         writer.append(i + ",")

-                        totalTime = 0.0

-                        totFound = 0.0

+                        solverTimes.clear

+                        transformationTimes.clear

                         modelFound = true

                         for (var j = 0; j < REPS; j++) {

 

                                 print(j)

 

                                 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())

-                                var problem = modelGenerationProblem.output

-                                problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output

-//              problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output

+                                var modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel)

+                                var validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem,

+                                        new Viatra2LogicConfiguration)

+

+                                var problem = validModelExtensionProblem.output

                                 workspace.writeModel(problem, "Yakindu.logicproblem")

 

 //                               println("Problem created")

@@ -110,9 +120,11 @@ class YakinduTest {
                                 // Define Config File           

                                 val size = i

                                 val inc = INC

+                                val iter = j

                                 val vampireConfig = new VampireSolverConfiguration => [

                                         // add configuration things, in config file first

                                         it.documentationLevel = DocumentationLevel::FULL

+                                        it.iteration = iter

 

                                         it.typeScopes.minNewElements = size - inc

                                         it.typeScopes.maxNewElements = size

@@ -132,11 +144,12 @@ class YakinduTest {
 //                              ].isEmpty

 //

 //                              if (modelFound) {

-                                val time = solution.statistics.transformationTime / 1000.0

-                                writer.append(time + ",")

-                                print("(" + time + ")..")

-                                totalTime += time

-                                totFound += 1

+                                val tTime = solution.statistics.transformationTime / 1000.0

+                                val sTime = solution.statistics.solverTime / 1000.0

+                                writer.append(tTime + "," + sTime + ",")

+                                print("(" + tTime + "/" + sTime + "s)..")

+                                solverTimes.add(sTime)

+                                transformationTimes.add(tTime)

 //                              } else {

 //                                      writer.append("MNF" + ",")

 ////                                    print("MNF")

@@ -144,55 +157,19 @@ class YakinduTest {
                         // println("Problem solved")

                         // visualisation, see 

 //                              var interpretations = reasoner.getInterpretations(solution as ModelResult)

-                        /*      interpretations.get(0) as VampireModelInterpretation

-                         *      println(ecore2Logic.IsAttributeValue(modelGenerationProblem.trace, )

-                         *              Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) )

-                         *      )

-                         *      println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType)

-                         print(interpretations.class)*/

 //                       for (interpretation : interpretations) {

 //                       val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace)

 //                       workspace.writeModel(model, "model.xmi")

-                        /*              val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations

-                         *              if (representation instanceof PartialInterpretation) {

-                         *                      val vis1 = new PartialInterpretation2Gml

-                         *                      val gml = vis1.transform(representation)

-                         *                      workspace.writeText("model.gml", gml)

-

-                         *                      val vis2 = new GraphvizVisualiser

-                         *                      val dot = vis2.visualiseConcretization(representation)

-                         *                      dot.writeToFile(workspace, "model.png")

-                         *              } else {

-                         *                      println("ERROR")

-                         *              }

-                         look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor*/

 //                      }

-                        /*/

-                         * 

-                         * reasoner = new AlloySolver

-                         * val alloyConfig = new AlloySolverConfiguration => [

-                         *      it.typeScopes.maxNewElements = 7

-                         *      it.typeScopes.minNewElements = 3

-                         *      it.solutionScope.numberOfRequiredSolution = 1

-                         *      it.typeScopes.maxNewIntegers = 0

-                         *      it.documentationLevel = DocumentationLevel::NORMAL

-                         * ]

-                         * solution = reasoner.solve(problem, alloyConfig, workspace)

-                         //*/

-                        // /////////////////////////////////////////////////////

 //                       var totalTimeMin = (System.currentTimeMillis - startTime) / 60000

 //                       var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60

 //                       println("Problem solved")

 //                       println("Time was: " + totalTimeMin + ":" + totalTimeSec)

                         }

                         println()

-                        var avg = 0.0

-                        if (totFound == 0) {

-                                avg = -1

-                        } else {

-                                avg = totalTime / totFound

-                        }

-                        writer.append(avg.toString)

+                        var solverMed = solverTimes.sort.get(REPS/2)

+                        var transformationMed = transformationTimes.sort.get(REPS/2)

+                        writer.append(solverMed.toString + "," + transformationMed.toString)

                         writer.append("\n")

                 }

                 writer.close

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
index 60679874..d9d6b881 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/queries/FamPatterns.vql
@@ -9,4 +9,12 @@ pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = {
 } or {

         InformationLink.to(I,In);

         FunctionalInput.terminator(In,T);

+}

+

+pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = {

+        FunctionalArchitectureModel.rootElements(Model, Root);

+}

+

+pattern parent(Func : Function, Par : Function) = {

+        Function.parent(Func, Par);

 }
\ No newline at end of file
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
index 4880c751..1d9db781 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
index 8ad6dfed..15159cb7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
index 164e6c2f..69cbcc0a 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
index 46cad7ee..16a24539 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index eeb7c77a..57a6fa02 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
index 616868a6..35c48de2 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java
@@ -1,11 +1,11 @@
 package ca.mcgill.ecse.dslreasoner.vampire.icse;

 

-import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns;

 import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;

+import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;

 import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;

+import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage;

 import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel;

-import functionalarchitecture.FunctionalarchitecturePackage;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration;

 import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace;

@@ -17,10 +17,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;
 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult;

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;

+import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;

+import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicTrace;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor;

 import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic;

 import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace;

 import java.io.PrintWriter;

+import java.text.SimpleDateFormat;

+import java.util.ArrayList;

+import java.util.Date;

 import java.util.Map;

 import org.eclipse.emf.common.util.EList;

 import org.eclipse.emf.common.util.URI;

@@ -28,8 +33,10 @@ import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.resource.Resource;

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;

 import org.eclipse.xtend2.lib.StringConcatenation;

+import org.eclipse.xtext.xbase.lib.CollectionLiterals;

 import org.eclipse.xtext.xbase.lib.Exceptions;

 import org.eclipse.xtext.xbase.lib.InputOutput;

+import org.eclipse.xtext.xbase.lib.IterableExtensions;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

 import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;

 

@@ -41,43 +48,51 @@ public class YakinduTest {
       final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic);

       final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic);

       final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

+      long _currentTimeMillis = System.currentTimeMillis();

+      final Date date = new Date(_currentTimeMillis);

+      final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");

+      final String formattedDate = format.format(date);

       StringConcatenation _builder = new StringConcatenation();

       _builder.append("initialModels/");

       final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), "");

       StringConcatenation _builder_1 = new StringConcatenation();

       _builder_1.append("output/YakinduTest/");

-      final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), "");

+      String _plus = (_builder_1.toString() + formattedDate);

+      StringConcatenation _builder_2 = new StringConcatenation();

+      _builder_2.append("/");

+      String _plus_1 = (_plus + _builder_2);

+      final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, "");

       workspace.initAndClear();

       final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;

       final Map<String, Object> map = reg.getExtensionToFactoryMap();

       XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();

       map.put("logicproblem", _xMIResourceFactoryImpl);

       InputOutput.<String>println("Input and output workspaces are created");

-      final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);

-      final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi");

-      final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());

+      final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE);

+      final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

+      final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());

       InputOutput.<String>println("DSL loaded");

       int MAX = 150;

       int START = 10;

       int INC = 20;

       int REPS = 1;

-      final int EXACT = (-1);

+      final int EXACT = 50;

       if ((EXACT != (-1))) {

         MAX = EXACT;

         START = EXACT;

         INC = 1;

-        REPS = 5;

+        REPS = 3;

       }

       URI _workspaceURI = workspace.getWorkspaceURI();

-      String _plus = (_workspaceURI + "//yakinduStats.csv");

-      PrintWriter writer = new PrintWriter(_plus);

+      String _plus_2 = (_workspaceURI + "//_yakinduStats.csv");

+      PrintWriter writer = new PrintWriter(_plus_2);

       writer.append("size,");

       for (int x = 0; (x < REPS); x++) {

-        writer.append((("t" + Integer.valueOf(x)) + ","));

+        writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ","));

       }

-      writer.append("avg\n");

-      double totalTime = 0.0;

-      double totFound = 0.0;

+      writer.append("medSolv,medTransf\n");

+      ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList();

+      ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList();

       boolean modelFound = true;

       LogicResult solution = null;

       {

@@ -87,18 +102,20 @@ public class YakinduTest {
           {

             final int num = ((i - START) / INC);

             InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: "));

-            String _plus_1 = (Integer.valueOf(i) + ",");

-            writer.append(_plus_1);

-            totalTime = 0.0;

-            totFound = 0.0;

+            String _plus_3 = (Integer.valueOf(i) + ",");

+            writer.append(_plus_3);

+            solverTimes.clear();

+            transformationTimes.clear();

             modelFound = true;

             for (int j = 0; (j < REPS); j++) {

               {

                 InputOutput.<Integer>print(Integer.valueOf(j));

                 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

                 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);

-                LogicProblem problem = modelGenerationProblem.getOutput();

-                problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();

+                TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);

+                Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

+                TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

+                LogicProblem problem = validModelExtensionProblem.getOutput();

                 workspace.writeModel(problem, "Yakindu.logicproblem");

                 long startTime = System.currentTimeMillis();

                 VampireSolver reasoner = null;

@@ -106,9 +123,11 @@ public class YakinduTest {
                 reasoner = _vampireSolver;

                 final int size = i;

                 final int inc = INC;

+                final int iter = j;

                 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();

                 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {

                   it.documentationLevel = DocumentationLevel.FULL;

+                  it.iteration = iter;

                   it.typeScopes.minNewElements = (size - inc);

                   it.typeScopes.maxNewElements = size;

                   it.contCycleLevel = 5;

@@ -119,24 +138,26 @@ public class YakinduTest {
                 Object _get = ((ModelResult) solution).getRepresentation().get(0);

                 final VampireModel soln = ((VampireModel) _get);

                 int _transformationTime = solution.getStatistics().getTransformationTime();

-                final double time = (_transformationTime / 1000.0);

-                String _plus_2 = (Double.valueOf(time) + ",");

-                writer.append(_plus_2);

-                InputOutput.<String>print((("(" + Double.valueOf(time)) + ").."));

-                double _talTime = totalTime;

-                totalTime = (_talTime + time);

-                double _tFound = totFound;

-                totFound = (_tFound + 1);

+                final double tTime = (_transformationTime / 1000.0);

+                int _solverTime = solution.getStatistics().getSolverTime();

+                final double sTime = (_solverTime / 1000.0);

+                String _plus_4 = (Double.valueOf(tTime) + ",");

+                String _plus_5 = (_plus_4 + Double.valueOf(sTime));

+                String _plus_6 = (_plus_5 + ",");

+                writer.append(_plus_6);

+                InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s).."));

+                solverTimes.add(Double.valueOf(sTime));

+                transformationTimes.add(Double.valueOf(tTime));

               }

             }

             InputOutput.println();

-            double avg = 0.0;

-            if ((totFound == 0)) {

-              avg = (-1);

-            } else {

-              avg = (totalTime / totFound);

-            }

-            writer.append(Double.valueOf(avg).toString());

+            Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2));

+            Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2));

+            String _string = solverMed.toString();

+            String _plus_4 = (_string + ",");

+            String _string_1 = transformationMed.toString();

+            String _plus_5 = (_plus_4 + _string_1);

+            writer.append(_plus_5);

             writer.append("\n");

           }

           int _i = i;

diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
index e9a1a8db..74f8e73f 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
index 39d9c161..68b3fd77 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
index effd204e..fc4464b3 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin