1 files changed, 146 insertions, 104 deletions

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 3a8f3fb4..1837b768 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
@@ -2,12 +2,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse;
 

 import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;

 import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns;

+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 ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement;

 import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region;

 import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition;

 import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage;

+import com.google.common.base.Objects;

 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,6 +19,9 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput;
 import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem;

 import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.RealStatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StatisticEntry;

+import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.StringStatisticEntry;

 import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic;

 import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration;

@@ -37,7 +42,9 @@ 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.Conversions;

 import org.eclipse.xtext.xbase.lib.Exceptions;

+import org.eclipse.xtext.xbase.lib.Functions.Function1;

 import org.eclipse.xtext.xbase.lib.InputOutput;

 import org.eclipse.xtext.xbase.lib.IterableExtensions;

 import org.eclipse.xtext.xbase.lib.ObjectExtensions;

@@ -53,17 +60,20 @@ public class YakinduTest {
       final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic();

       long _currentTimeMillis = System.currentTimeMillis();

       final Date date = new Date(_currentTimeMillis);

-      final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss");

+      final SimpleDateFormat format = new SimpleDateFormat("dd-HHmm");

       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/");

-      String _plus = (_builder_1.toString() + formattedDate);

+      final FileSystemWorkspace dataWorkspace = new FileSystemWorkspace(_builder_1.toString(), "");

       StringConcatenation _builder_2 = new StringConcatenation();

-      _builder_2.append("/");

-      String _plus_1 = (_plus + _builder_2);

+      _builder_2.append("output/YakinduTest/");

+      String _plus = (_builder_2.toString() + formattedDate);

+      StringConcatenation _builder_3 = new StringConcatenation();

+      _builder_3.append("/");

+      String _plus_1 = (_plus + _builder_3);

       final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, "");

       workspace.initAndClear();

       final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE;

@@ -75,117 +85,149 @@ public class YakinduTest {
       final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi");

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

       InputOutput.<String>println("DSL loaded");

-      int SZ_TOP = 10;

-      int SZ_BOT = 126;

-      int INC = 1;

+      int SZ_TOP = 30;

+      int SZ_BOT = 5;

+      int INC = 5;

       int REPS = 1;

-      final int RANGE = 3;

-      final int EXACT = 10;

+      final int RUNTIME = 20;

+      final int EXACT = (-1);

       if ((EXACT != (-1))) {

         SZ_TOP = EXACT;

         SZ_BOT = EXACT;

         INC = 1;

-        REPS = 1;

+        REPS = 10;

       }

-      URI _workspaceURI = workspace.getWorkspaceURI();

-      String _plus_2 = (_workspaceURI + "//_yakinduStats.csv");

-      PrintWriter writer = new PrintWriter(_plus_2);

-      writer.append("size,");

-      for (int x = 0; (x < REPS); x++) {

-        writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ","));

+      final ArrayList<BackendSolver> BACKENDSOLVERS = CollectionLiterals.<BackendSolver>newArrayList(

+        BackendSolver.IPROVER);

+      String str = "";

+      for (final BackendSolver solver : BACKENDSOLVERS) {

+        String _str = str;

+        String _substring = solver.name().substring(0, 1);

+        str = (_str + _substring);

       }

-      writer.append("medSolv,medTransf\n");

-      ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList();

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

-      boolean modelFound = true;

+      URI _workspaceURI = dataWorkspace.getWorkspaceURI();

+      String _plus_2 = (_workspaceURI + "//_stats");

+      String _plus_3 = (_plus_2 + formattedDate);

+      String _plus_4 = (_plus_3 + "-");

+      String _plus_5 = (_plus_4 + str);

+      String _plus_6 = (_plus_5 + Integer.valueOf(SZ_BOT));

+      String _plus_7 = (_plus_6 + "to");

+      String _plus_8 = (_plus_7 + Integer.valueOf(SZ_TOP));

+      String _plus_9 = (_plus_8 + "by");

+      String _plus_10 = (_plus_9 + Integer.valueOf(INC));

+      String _plus_11 = (_plus_10 + 

+        "x");

+      String _plus_12 = (_plus_11 + Integer.valueOf(REPS));

+      String _plus_13 = (_plus_12 + ".csv");

+      PrintWriter writer = new PrintWriter(_plus_13);

+      writer.append("solver,size,transTime,sat?,satTime,model?,modelTime\n");

+      ArrayList<Object> solverTimes = CollectionLiterals.<Object>newArrayList();

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

       LogicResult solution = null;

-      {

-        int i = SZ_BOT;

-        boolean _while = (i <= SZ_TOP);

-        while (_while) {

-          {

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

-            InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: "));

-            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);

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

-                Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

-                TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

-                LogicProblem problem = modelGenerationProblem.getOutput();

-                workspace.writeModel(problem, "Yakindu.logicproblem");

-                long startTime = System.currentTimeMillis();

-                VampireSolver reasoner = null;

-                VampireSolver _vampireSolver = new VampireSolver();

-                reasoner = _vampireSolver;

-                final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();

-                classMapMin.put(Region.class, Integer.valueOf(1));

-                classMapMin.put(Transition.class, Integer.valueOf(2));

-                classMapMin.put(CompositeElement.class, Integer.valueOf(3));

-                final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

-                final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();

-                classMapMax.put(Region.class, Integer.valueOf(5));

-                classMapMax.put(Transition.class, Integer.valueOf(2));

-                final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());

-                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.runtimeLimit = 60;

-                  it.typeScopes.maxNewElements = (-1);

-                  it.typeScopes.minNewElements = size;

-                  it.genModel = false;

-                  int _size = typeMapMin.size();

-                  boolean _notEquals = (_size != 0);

-                  if (_notEquals) {

-                    it.typeScopes.minNewElementsByType = typeMapMin;

-                  }

-                  int _size_1 = typeMapMin.size();

-                  boolean _notEquals_1 = (_size_1 != 0);

-                  if (_notEquals_1) {

-                    it.typeScopes.maxNewElementsByType = typeMapMax;

-                  }

-                  it.contCycleLevel = 5;

-                  it.uniquenessDuplicates = false;

-                };

-                final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

-                solution = reasoner.solve(problem, vampireConfig, workspace);

-                int _transformationTime = solution.getStatistics().getTransformationTime();

-                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));

+      for (final BackendSolver BESOLVER : BACKENDSOLVERS) {

+        {

+          int i = SZ_BOT;

+          boolean _while = (i <= SZ_TOP);

+          while (_while) {

+            {

+              final int num = ((i - SZ_BOT) / INC);

+              InputOutput.println();

+              String _name = BESOLVER.name();

+              String _plus_14 = ("SOLVER: " + _name);

+              String _plus_15 = (_plus_14 + ", SIZE=");

+              String _plus_16 = (_plus_15 + Integer.valueOf(i));

+              InputOutput.<String>println(_plus_16);

+              InputOutput.println();

+              solverTimes.clear();

+              transformationTimes.clear();

+              for (int j = 0; (j < REPS); j++) {

+                {

+                  InputOutput.<String>print((("<<Run number " + Integer.valueOf(j)) + ">> :"));

+                  Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();

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

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

+                  Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration();

+                  TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration);

+                  LogicProblem problem = modelGenerationProblem.getOutput();

+                  long startTime = System.currentTimeMillis();

+                  VampireSolver reasoner = null;

+                  VampireSolver _vampireSolver = new VampireSolver();

+                  reasoner = _vampireSolver;

+                  final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();

+                  classMapMin.put(Region.class, Integer.valueOf(1));

+                  classMapMin.put(Transition.class, Integer.valueOf(2));

+                  classMapMin.put(CompositeElement.class, Integer.valueOf(3));

+                  final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, 

+                    modelGenerationProblem.getTrace());

+                  final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();

+                  classMapMax.put(Region.class, Integer.valueOf(5));

+                  classMapMax.put(Transition.class, Integer.valueOf(2));

+                  final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, 

+                    modelGenerationProblem.getTrace());

+                  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.runtimeLimit = RUNTIME;

+                    it.typeScopes.minNewElements = size;

+                    it.genModel = true;

+                    it.server = true;

+                    it.solver = BESOLVER;

+                    it.contCycleLevel = 5;

+                    it.uniquenessDuplicates = false;

+                  };

+                  final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function);

+                  solution = reasoner.solve(problem, vampireConfig, workspace);

+                  String _name_1 = vampireConfig.solver.name();

+                  String _plus_17 = (_name_1 + ",");

+                  writer.append(_plus_17);

+                  String _plus_18 = (Integer.valueOf(size) + ",");

+                  writer.append(_plus_18);

+                  int _transformationTime = solution.getStatistics().getTransformationTime();

+                  double _divide = (_transformationTime / 1000.0);

+                  String _plus_19 = (Double.valueOf(_divide) + ",");

+                  writer.append(_plus_19);

+                  final Function1<StatisticEntry, Boolean> _function_1 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "satOut"));

+                  };

+                  StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0];

+                  final String satOut = ((StringStatisticEntry) _get).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_2 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "satTime"));

+                  };

+                  StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0];

+                  final double satTime = ((RealStatisticEntry) _get_1).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_3 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "modOut"));

+                  };

+                  StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0];

+                  final String modOut = ((StringStatisticEntry) _get_2).getValue();

+                  final Function1<StatisticEntry, Boolean> _function_4 = (StatisticEntry it) -> {

+                    String _name_2 = it.getName();

+                    return Boolean.valueOf(Objects.equal(_name_2, "modTime"));

+                  };

+                  StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.<StatisticEntry>filter(solution.getStatistics().getEntries(), _function_4), StatisticEntry.class))[0];

+                  final double modTime = ((RealStatisticEntry) _get_3).getValue();

+                  writer.append((satOut + ","));

+                  String _plus_20 = (Double.valueOf(satTime) + ",");

+                  writer.append(_plus_20);

+                  writer.append((modOut + ","));

+                  String _plus_21 = (Double.valueOf(modTime) + ",");

+                  writer.append(_plus_21);

+                  writer.append("\n");

+                }

               }

             }

-            InputOutput.println();

-            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;

+            i = (_i + INC);

+            _while = (i <= SZ_TOP);

           }

-          int _i = i;

-          i = (_i + INC);

-          _while = (i <= SZ_TOP);

         }

       }

       writer.close();