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 --- .../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 9 files changed, 56 insertions(+), 35 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill') 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