From f63a94c06268b5233264436cc538062f1f7b01bc Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 8 Oct 2019 03:00:08 -0400 Subject: VAMPIRE: fix bug in transformation, further implement measurement code --- .../reasoner/VampireAnalyzerConfiguration.xtend | 1 + .../vampire/reasoner/VampireSolver.xtend | 8 +- .../builder/Logic2VampireLanguageMapper.xtend | 56 ++++++++--- ...ogic2VampireLanguageMapper_RelationMapper.xtend | 49 ++++----- .../reasoner/builder/Vampire2LogicMapper.xtend | 5 +- .../vampire/reasoner/builder/VampireHandler.xtend | 2 +- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2691 -> 2845 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 7020 -> 6973 bytes .../vampire/reasoner/VampireSolver.java | 13 +-- .../reasoner/VampireSolverConfiguration.java | 2 + .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18099 -> 19565 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3165 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 11807 -> 11807 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 7934 -> 7880 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 10676 -> 10676 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 13060 -> 13059 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 11037 -> 11038 bytes .../reasoner/builder/.Vampire2LogicMapper.xtendbin | Bin 3950 -> 3997 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 6882 -> 6937 bytes .../builder/Logic2VampireLanguageMapper.java | 60 ++++++++++- ...Logic2VampireLanguageMapper_RelationMapper.java | 2 - .../reasoner/builder/Vampire2LogicMapper.java | 3 +- .../vampire/reasoner/builder/VampireHandler.java | 2 +- .../META-INF/MANIFEST.MF | 8 +- .../plugin.xml | 10 +- .../dslreasoner/vampire/icse/YakinduTest.xtend | 111 ++++++++------------- .../dslreasoner/vampire/queries/FamPatterns.vql | 8 ++ .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6624 -> 6624 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6204 -> 6204 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6456 -> 6456 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 7597 -> 7838 bytes .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 91 ++++++++++------- .../vampire/test/.MedicalSystem.xtendbin | Bin 4997 -> 4997 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6500 -> 6500 bytes 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 relations, Logic2VampireLanguageMapperTrace trace) { + val List 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 variables) { // createVLSReal => [it.value = literal.value.toString()] // } - def dispatch protected VLSTerm transformTerm(Not not, Logic2VampireLanguageMapperTrace trace, Map variables) { createVLSUnaryNegation => [operand = not.operand.transformTerm(trace, variables)] @@ -265,10 +298,10 @@ class Logic2VampireLanguageMapper { def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, List parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, Map 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 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ 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 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin differ 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 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ 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 _function_3 = (Relation it) -> { + final Function1 _function_3 = (Relation it) -> { + Class _class = it.getClass(); + return Boolean.valueOf(Objects.equal(_class, RelationDefinitionImpl.class)); + }; + this.toTrace(IterableExtensions.filter(problem.getRelations(), _function_3), trace); + final Consumer _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 _function_4 = (ConstantDefinition it) -> { + final Consumer _function_5 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); }; - Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_4); + Iterables.filter(problem.getConstants(), ConstantDefinition.class).forEach(_function_5); EList _assertions = problem.getAssertions(); for (final Assertion assertion : _assertions) { this.transformAssertion(assertion, trace); @@ -137,6 +146,49 @@ public class Logic2VampireLanguageMapper { return new TracedOutput(specification, trace); } + public void toTrace(final Iterable relations, final Logic2VampireLanguageMapperTrace trace) { + final List vars = CollectionLiterals.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 _function = (VLSVariable it) -> { + it.setName(this.support.toIDMultiple("V", i.toString())); + }; + final VLSVariable v = ObjectExtensions.operator_doubleArrow(_createVLSVariable, _function); + vars.add(v); + } + } + VLSFunction _createVLSFunction = this.factory.createVLSFunction(); + final Procedure1 _function = (VLSFunction it) -> { + it.setConstant(this.support.toIDMultiple("r", relName)); + for (final VLSVariable v : vars) { + EList _terms = it.getTerms(); + VLSVariable _duplicate = this.support.duplicate(v); + _terms.add(_duplicate); + } + }; + final VLSFunction relFunc = ObjectExtensions.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.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 _function = (Statistics it) -> { long _solverTime = solution.getSolverTime(); - it.setTransformationTime(((int) _solverTime)); + it.setSolverTime(((int) _solverTime)); + it.setTransformationTime(((int) transformationTime)); }; return ObjectExtensions.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 @@ - - - - - - + + + + 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin differ 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 map = reg.getExtensionToFactoryMap(); XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); map.put("logicproblem", _xMIResourceFactoryImpl); InputOutput.println("Input and output workspaces are created"); - final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); - final EList partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); - final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); + final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE); + final EList partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); + final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); InputOutput.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 solverTimes = CollectionLiterals.newArrayList(); + ArrayList transformationTimes = CollectionLiterals.newArrayList(); boolean modelFound = true; LogicResult solution = null; { @@ -87,18 +102,20 @@ public class YakinduTest { { final int num = ((i - START) / INC); InputOutput.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.print(Integer.valueOf(j)); Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - LogicProblem problem = modelGenerationProblem.getOutput(); - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); + TracedOutput modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); + Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); + TracedOutput 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 _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.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.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.sort(solverTimes).get((REPS / 2)); + Double transformationMed = IterableExtensions.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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin differ 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 Binary files a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin differ -- cgit v1.2.3-54-g00ecf