From 606f6965f3ccec837aa216cbb3f56fdcf943a59b Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 11 Oct 2019 15:51:49 -0400 Subject: VAMPIRE: complete testing setup --- .../dslreasoner/vampire/icse/.EcoreTest.xtendbin | Bin 4552 -> 4545 bytes .../dslreasoner/vampire/icse/.FAMTest.xtendbin | Bin 6632 -> 6626 bytes .../vampire/icse/.FileSystemTest.xtendbin | Bin 6207 -> 6201 bytes .../dslreasoner/vampire/icse/.GeneralTest.xtendbin | Bin 10182 -> 6625 bytes .../dslreasoner/vampire/icse/.YakinduTest.xtendbin | Bin 8484 -> 8992 bytes .../ecse/dslreasoner/vampire/icse/GeneralTest.java | 68 ------ .../ecse/dslreasoner/vampire/icse/YakinduTest.java | 250 ++++++++++++--------- .../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 10 files changed, 146 insertions(+), 172 deletions(-) (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire') 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 93d27b4d..5dc01040 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 bc2bae6f..e96cf904 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 5687258f..688908b9 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 de68a908..0d18615c 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 16a3cd03..cf52d6a6 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/GeneralTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java index ce057092..bdea5746 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/GeneralTest.java @@ -13,11 +13,6 @@ import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.Set; -import okhttp3.MediaType; -import okhttp3.OkHttpClient; -import okhttp3.Request; -import okhttp3.RequestBody; -import okhttp3.Response; import org.eclipse.emf.common.util.EList; import org.eclipse.emf.ecore.EAttribute; import org.eclipse.emf.ecore.EClass; @@ -33,75 +28,12 @@ import org.eclipse.viatra.query.runtime.api.IQueryGroup; import org.eclipse.viatra.query.runtime.api.IQuerySpecification; import org.eclipse.viatra.query.runtime.matchers.psystem.annotations.PAnnotation; import org.eclipse.xtext.xbase.lib.CollectionLiterals; -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.ListExtensions; @SuppressWarnings("all") public class GeneralTest { - private final static String USER_AGENT = "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36"; - - public static void main(final String[] args) { - try { - final String form = GeneralTest.makeForm("fof (a, axiom, ! [A] : a(A) ) .", "Z3---4.4.1", "run_z3_tptp -proof -model -t:20 -file:%s", 300); - final String x = GeneralTest.sendPost(form); - InputOutput.print(x.toString()); - } catch (Throwable _e) { - throw Exceptions.sneakyThrow(_e); - } - } - - public static String makeForm(final String formula, final String solver, final String cmd, final int time) { - String _header = GeneralTest.getHeader(); - String _addSpec = GeneralTest.addSpec(formula); - String _plus = (_header + _addSpec); - String _addOptions = GeneralTest.addOptions(); - String _plus_1 = (_plus + _addOptions); - String _addSolver = GeneralTest.addSolver(solver, cmd.replace("%d", Integer.valueOf(time).toString())); - String _plus_2 = (_plus_1 + _addSolver); - String _addEnd = GeneralTest.addEnd(); - return (_plus_2 + _addEnd); - } - - public static String sendPost(final String formData) throws Exception { - final OkHttpClient client = new OkHttpClient(); - final MediaType mediaType = MediaType.parse( - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA"); - final RequestBody body = RequestBody.create(mediaType, formData); - final Request request = new Request.Builder().url("http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply").post(body).addHeader("Connection", "keep-alive").addHeader("Cache-Control", "max-age=0").addHeader("Origin", - "http://tptp.cs.miami.edu").addHeader("Upgrade-Insecure-Requests", "1").addHeader("Content-Type", - "multipart/form-data boundary=----WebKitFormBoundaryBdFiQ5zEvTbBl4DA").addHeader("User-Agent", - "Mozilla/5.0 (Windows NT 10.0 Win64 x64) AppleWebKit/537.36 (KHTML, like Gecko) Chrome/77.0.3865.90 Safari/537.36").addHeader("Accept", - "text/html,application/xhtml+xml,application/xmlq=0.9,image/webp,image/apng,*/*q=0.8,application/signed-exchangev=b3").addHeader("Referer", "http://tptp.cs.miami.edu/cgi-bin/SystemOnTPTP").addHeader("Accept-Encoding", - "gzip, deflate").addHeader("Accept-Language", "en-US,enq=0.9").addHeader("Postman-Token", - "639ff59f-ab5c-4d9f-9da5-ac8bb64be466,ecb71882-f4d8-4126-8a97-4edb07d4055c").addHeader("Host", - "www.tptp.org").addHeader("Content-Length", "44667").addHeader("cache-control", "no-cache").build(); - final Response response = client.newCall(request).execute(); - return response.body().string(); - } - - public static String getHeader() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"ProblemSource\"\r\n\r\nFORMULAE\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"FORMULAEProblem\"\r\n\r\n\r\n"; - } - - public static String addSpec(final String spec) { - return spec.replace("\n", "\r\n"); - } - - public static String addOptions() { - return "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"QuietFlag\"\r\n\r\n-q3\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"SubmitButton\"\r\n\r\nRunSelectedSystems\r\n"; - } - - public static String addSolver(final String ID, final String cmd) { - return (((((((("------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"System___" + ID) + "\"\r\n\r\n") + ID) + "\r\n------WebKitFormBoundaryBdFiQ5zEvTbBl4DA\r\nContent-Disposition: form-data; name=\"Command___") + ID) + "\"\r\n\r\n") + cmd) + "\r\n"); - } - - public static String addEnd() { - return "------WebKitFormBoundaryBdFiQ5zEvTbBl4DA--"; - } - public static Map getTypeMap(final Map classMap, final EcoreMetamodelDescriptor metamodel, final Ecore2Logic e2l, final Ecore2Logic_Trace trace) { final HashMap typeMap = new HashMap(); final Function1 _function = (EClass s) -> { 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 partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); InputOutput.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 BACKENDSOLVERS = CollectionLiterals.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 solverTimes = CollectionLiterals.newArrayList(); - ArrayList transformationTimes = CollectionLiterals.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 solverTimes = CollectionLiterals.newArrayList(); + ArrayList transformationTimes = CollectionLiterals.newArrayList(); LogicResult solution = null; - { - int i = SZ_BOT; - boolean _while = (i <= SZ_TOP); - while (_while) { - { - final int num = ((i - SZ_BOT) / INC); - InputOutput.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.print(Integer.valueOf(j)); - Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); - final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); - TracedOutput modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); - Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); - TracedOutput 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 classMapMin = new HashMap(); - classMapMin.put(Region.class, Integer.valueOf(1)); - classMapMin.put(Transition.class, Integer.valueOf(2)); - classMapMin.put(CompositeElement.class, Integer.valueOf(3)); - final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); - final HashMap classMapMax = new HashMap(); - classMapMax.put(Region.class, Integer.valueOf(5)); - classMapMax.put(Transition.class, Integer.valueOf(2)); - final Map 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 _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.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.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.println(_plus_16); + InputOutput.println(); + solverTimes.clear(); + transformationTimes.clear(); + for (int j = 0; (j < REPS); j++) { + { + InputOutput.print((("<> :")); + Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); + final TracedOutput modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); + TracedOutput modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); + Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); + TracedOutput 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 classMapMin = new HashMap(); + classMapMin.put(Region.class, Integer.valueOf(1)); + classMapMin.put(Transition.class, Integer.valueOf(2)); + classMapMin.put(CompositeElement.class, Integer.valueOf(3)); + final Map typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, + modelGenerationProblem.getTrace()); + final HashMap classMapMax = new HashMap(); + classMapMax.put(Region.class, Integer.valueOf(5)); + classMapMax.put(Transition.class, Integer.valueOf(2)); + final Map 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 _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.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 _function_1 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "satOut")); + }; + StatisticEntry _get = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_1), StatisticEntry.class))[0]; + final String satOut = ((StringStatisticEntry) _get).getValue(); + final Function1 _function_2 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "satTime")); + }; + StatisticEntry _get_1 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_2), StatisticEntry.class))[0]; + final double satTime = ((RealStatisticEntry) _get_1).getValue(); + final Function1 _function_3 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "modOut")); + }; + StatisticEntry _get_2 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.filter(solution.getStatistics().getEntries(), _function_3), StatisticEntry.class))[0]; + final String modOut = ((StringStatisticEntry) _get_2).getValue(); + final Function1 _function_4 = (StatisticEntry it) -> { + String _name_2 = it.getName(); + return Boolean.valueOf(Objects.equal(_name_2, "modTime")); + }; + StatisticEntry _get_3 = ((StatisticEntry[])Conversions.unwrapArray(IterableExtensions.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.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; + i = (_i + INC); + _while = (i <= SZ_TOP); } - int _i = i; - i = (_i + INC); - _while = (i <= SZ_TOP); } } writer.close(); 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 96f343fa..b596dc1f 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 1ca8223d..e1434d74 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 5d6a9ee2..50068d97 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