From 5d1165ceef23e20c4bbe46fe6f88e95f317234b5 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 7 Oct 2019 00:35:42 -0400 Subject: VAMPIRE: Implement Vampire measurement code --- .../ecse/dslreasoner/vampire/icse/EcoreTest.xtend | 2 +- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 15 +- .../dslreasoner/vampire/icse/YakinduTest.xtend | 236 ++++++++++++++------- 3 files changed, 173 insertions(+), 80 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend index 70ded02d..35b76350 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/EcoreTest.xtend @@ -50,7 +50,7 @@ class EcoreTest { it.documentationLevel = DocumentationLevel::FULL ] - solution = reasoner.solve(logicProblem, vampireConfig, workspace, "ECO") + solution = reasoner.solve(logicProblem, vampireConfig, workspace) println("Problem solved") diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend index 5143641b..a7da818c 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend @@ -2,12 +2,13 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +import functionalarchitecture.FAMTerminator import functionalarchitecture.Function import functionalarchitecture.FunctionalArchitectureModel import functionalarchitecture.FunctionalInterface import functionalarchitecture.FunctionalOutput import functionalarchitecture.FunctionalarchitecturePackage -import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns +//import hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns 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 @@ -22,7 +23,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace import java.util.HashMap import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import functionalarchitecture.FAMTerminator class FAMTest { def static void main(String[] args) { @@ -47,15 +47,15 @@ class FAMTest { // Load DSL val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") - val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) -// val queries = null +// val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) + val queries = null println("DSL loaded") 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 +// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output workspace.writeModel(problem, "Fam.logicproblem") println("Problem created") @@ -94,14 +94,15 @@ class FAMTest { it.typeScopes.minNewElements = 8//24 it.typeScopes.maxNewElements = 10//25 - if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin +// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax it.contCycleLevel = 5 it.uniquenessDuplicates = false ] var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) - + + println("Problem solved") // visualisation, see var interpretations = reasoner.getInterpretations(solution as ModelResult) // interpretations.get(0) as VampireModelInterpretation 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 fb1bdb59..057bcf12 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,25 +1,27 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse -import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage +import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration +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 -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner 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.viatrasolver.partialinterpretation2logic.InstanceModel2Logic import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace -import java.util.HashMap +import java.io.PrintWriter import org.eclipse.emf.ecore.resource.Resource import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl -import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.* - class YakinduTest { def static void main(String[] args) { val Ecore2Logic ecore2Logic = new Ecore2Logic + val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic @@ -35,76 +37,166 @@ class YakinduTest { println("Input and output workspaces are created") - val metamodel = GeneralTest.loadMetamodel(yakinduPackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/yakinduinstance.xmi") -// val queries = GeneralTest.loadQueries(metamodel, yakinduPatterns.instance) - val queries = null - +// 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 queries = null println("DSL loaded") - val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) - var problem = modelGenerationProblem.output - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output + var MAX = 150 + var START = 10 + var INC = 20 + var REPS = 1 + + val EXACT = -1 + if (EXACT!= -1) { + MAX = EXACT + START = EXACT + INC = 1 + REPS = 5 + } + + var writer = new PrintWriter(workspace.workspaceURI + "//yakinduStats.csv") + writer.append("size,") + for (var x = 0; x < REPS; x++) { + writer.append("t" + x + ",") + } + writer.append("avg\n") + var totalTime = 0.0 + var totFound = 0.0 + 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 + 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 - workspace.writeModel(problem, "Yakindu.logicproblem") - - println("Problem created") - - // Start Time - var startTime = System.currentTimeMillis - - var VampireSolver reasoner - // * - reasoner = new VampireSolver - - // ///////////////////////////////////////////////////// - // Minimum Scope - val classMapMin = new HashMap - classMapMin.put(Region, 1) - classMapMin.put(Transition, 2) - classMapMin.put(CompositeElement, 3) - val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) - - // Maximum Scope - val classMapMax = new HashMap - classMapMax.put(Region, 5) - classMapMax.put(Transition, 2) - classMapMax.put(Synchronization, 4) - val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) - - // Define Config File - val vampireConfig = new VampireSolverConfiguration => [ - // add configuration things, in config file first - it.documentationLevel = DocumentationLevel::FULL - - it.typeScopes.minNewElements = 20 - it.typeScopes.maxNewElements = 30 - if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin - if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax - it.contCycleLevel = 5 - it.uniquenessDuplicates = false - ] - - var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace, "YAK") - - /*/ - * - * 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) + workspace.writeModel(problem, "Yakindu.logicproblem") + +// println("Problem created") +// Start Time + var startTime = System.currentTimeMillis + + var VampireSolver reasoner + // * + reasoner = new VampireSolver + + // ///////////////////////////////////////////////////// + // Minimum Scope +// val classMapMin = new HashMap +// classMapMin.put(Region, 1) +// classMapMin.put(Transition, 2) +// classMapMin.put(CompositeElement, 3) +// val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) + // Maximum Scope +// val classMapMax = new HashMap +// classMapMax.put(Region, 5) +// classMapMax.put(Transition, 2) +// classMapMax.put(Synchronization, 4) +// val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) + // Define Config File + val size = i + val inc = INC + val vampireConfig = new VampireSolverConfiguration => [ + // add configuration things, in config file first + it.documentationLevel = DocumentationLevel::FULL + + it.typeScopes.minNewElements = size - inc + it.typeScopes.maxNewElements = size +// if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin +// if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.contCycleLevel = 5 + it.uniquenessDuplicates = false + ] + + solution = reasoner.solve(problem, vampireConfig, workspace) +// print((solution as ModelResult).representation.get(0)) + val soln = ((solution as ModelResult).representation.get(0) as VampireModel) +// println(soln.confirmations) +// println((solution as ModelResult).representation) +// modelFound = !soln.confirmations.filter [ +// class == VLSFiniteModelImpl +// ].isEmpty +// +// if (modelFound) { + val time = solution.statistics.transformationTime / 1000.0 + writer.append(time + ",") + print("(" + time + ")..") + totalTime += time + totFound += 1 +// } else { +// writer.append("MNF" + ",") +//// print("MNF") +// } + // 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) + writer.append("\n") + } + writer.close + } } -- cgit v1.2.3-54-g00ecf