VAMPIRE: fix bug in transformation, further implement measurement code

9 files changed, 56 insertions, 35 deletions

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
--- 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
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
--- 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
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
--- 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
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
--- 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
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
--- 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
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<String, Object> map = reg.getExtensionToFactoryMap();

       XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl();

       map.put("logicproblem", _xMIResourceFactoryImpl);

       InputOutput.<String>println("Input and output workspaces are created");

-      final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE);

-      final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi");

-      final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance());

+      final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE);

+      final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

+      final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance());

       InputOutput.<String>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<Double> solverTimes = CollectionLiterals.<Double>newArrayList();

+      ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList();

       boolean modelFound = true;

       LogicResult solution = null;

       {

@@ -87,18 +102,20 @@ public class YakinduTest {
           {

             final int num = ((i - START) / INC);

             InputOutput.<String>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.<Integer>print(Integer.valueOf(j));

                 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

                 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);

-                LogicProblem problem = modelGenerationProblem.getOutput();

-                problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();

+                TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel);

+                Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

+                TracedOutput<LogicProblem, Viatra2LogicTrace> 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<VampireSolverConfiguration> _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.<String>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.<String>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.<Double>sort(solverTimes).get((REPS / 2));

+            Double transformationMed = IterableExtensions.<Double>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
--- 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
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
--- 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
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
--- 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