From d0e4ffcc9dfc85367ccc73bf070404416081a477 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 --- .../dslreasoner/vampire/icse/YakinduTest.xtend | 111 ++++++++------------- .../dslreasoner/vampire/queries/FamPatterns.vql | 8 ++ 2 files changed, 52 insertions(+), 67 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse') 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 -- cgit v1.2.3-54-g00ecf