From 4d27f2788d2f728d4ee2be8861df09da62bf135f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 3 Feb 2020 15:20:02 -0500 Subject: VAMPIRE: last commit --- .../output/FAMTest/Fam.logicproblem | 62 +++++++++++++++++++-- .../ecse/dslreasoner/vampire/icse/FAMTest.xtend | 45 ++++++++------- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4545 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6626 -> 6381 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6201 -> 6201 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 6625 -> 6625 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 9352 -> 9352 bytes .../ecse/dslreasoner/vampire/icse/FAMTest.java | 14 +---- .../vampire/test/.MedicalSystem.xtendbin | Bin 5003 -> 5003 bytes .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 687 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 6581 -> 6581 bytes 11 files changed, 81 insertions(+), 40 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test') diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index f86a2f3c..48991faa 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem @@ -1,7 +1,7 @@ - + @@ -10,8 +10,6 @@ - - @@ -496,6 +494,55 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -556,11 +603,14 @@ + + + + - - + @@ -580,4 +630,6 @@ + + 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 a7da818c..17f9ae5e 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 @@ -1,5 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration import functionalarchitecture.FAMTerminator @@ -8,7 +9,6 @@ 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.ecore2logic.Ecore2Logic import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel @@ -16,7 +16,6 @@ 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.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace @@ -46,7 +45,7 @@ class FAMTest { // Load DSL val metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE) - val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") +// val partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi") // val queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance) val queries = null @@ -54,7 +53,7 @@ class FAMTest { val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) var problem = modelGenerationProblem.output - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output +// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output // problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output workspace.writeModel(problem, "Fam.logicproblem") @@ -96,6 +95,7 @@ class FAMTest { it.typeScopes.maxNewElements = 10//25 // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax + it.solver = BackendSolver::LOCVAMP it.contCycleLevel = 5 it.uniquenessDuplicates = false ] @@ -110,25 +110,25 @@ class FAMTest { // 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) +// print(interpretations.class) +// for (interpretation : interpretations) { +// val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) +// workspace.writeModel(model, "model.xmi") // -// 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 - } +//// 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 +// } // transform interpretation to ecore, and it is easy from there /*/ @@ -147,7 +147,6 @@ class FAMTest { var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 - println("Problem solved") println("Time was: " + totalTimeMin + ":" + totalTimeSec) } 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 197ef5c9..7ccbe59f 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 52c819c4..b03f527f 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 b3b15fba..6bc303df 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 03bcbad7..a34d7d3b 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 0f06a39a..a8c5f173 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/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java index 8cd08fd8..cd9ba3c1 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java @@ -1,6 +1,7 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse; import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.BackendSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import functionalarchitecture.FAMTerminator; @@ -27,8 +28,6 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; import java.util.HashMap; import java.util.List; import java.util.Map; -import org.eclipse.emf.common.util.EList; -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; @@ -59,13 +58,11 @@ public class FAMTest { 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 Object queries = null; InputOutput.println("DSL loaded"); Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); LogicProblem problem = modelGenerationProblem.getOutput(); - problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); workspace.writeModel(problem, "Fam.logicproblem"); InputOutput.println("Problem created"); long startTime = System.currentTimeMillis(); @@ -86,6 +83,7 @@ public class FAMTest { it.documentationLevel = DocumentationLevel.FULL; it.typeScopes.minNewElements = 8; it.typeScopes.maxNewElements = 10; + it.solver = BackendSolver.LOCVAMP; it.contCycleLevel = 5; it.uniquenessDuplicates = false; }; @@ -93,13 +91,6 @@ public class FAMTest { LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); InputOutput.println("Problem solved"); List interpretations = reasoner.getInterpretations(((ModelResult) solution)); - InputOutput.>print(interpretations.getClass()); - for (final LogicModelInterpretation interpretation : interpretations) { - { - final EObject model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.getTrace()); - workspace.writeModel(model, "model.xmi"); - } - } long _currentTimeMillis = System.currentTimeMillis(); long _minus = (_currentTimeMillis - startTime); long totalTimeMin = (_minus / 60000); @@ -107,7 +98,6 @@ public class FAMTest { long _minus_1 = (_currentTimeMillis_1 - startTime); long _divide = (_minus_1 / 1000); long totalTimeSec = (_divide % 60); - InputOutput.println("Problem solved"); InputOutput.println(((("Time was: " + Long.valueOf(totalTimeMin)) + ":") + Long.valueOf(totalTimeSec))); } catch (Throwable _e) { throw Exceptions.sneakyThrow(_e); 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 5dcd3133..9a2c84d7 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 68ade593..f39505b0 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 80e7ebe0..51d32da7 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