diff options
author | 2019-10-08 03:00:08 -0400 | |
---|---|---|
committer | 2020-06-07 19:43:10 -0400 | |
commit | d0e4ffcc9dfc85367ccc73bf070404416081a477 (patch) | |
tree | 0db0134207f473f6a12d7c362512b008bd6449eb /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse | |
parent | VAMPIRE: Implement Vampire measurement code (diff) | |
download | VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.gz VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.tar.zst VIATRA-Generator-d0e4ffcc9dfc85367ccc73bf070404416081a477.zip |
VAMPIRE: fix bug in transformation, further implement measurement code
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse')
6 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.fam.queries.FamPatterns; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | 3 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage; | ||
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel; |
8 | import functionalarchitecture.FunctionalarchitecturePackage; | ||
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; |
10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration; |
11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic_Trace; |
@@ -17,10 +17,15 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | |||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; |
18 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 18 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 19 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration; | ||
21 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicTrace; | ||
20 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; | 22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.ViatraQuerySetDescriptor; |
21 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; |
22 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | 24 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; |
23 | import java.io.PrintWriter; | 25 | import java.io.PrintWriter; |
26 | import java.text.SimpleDateFormat; | ||
27 | import java.util.ArrayList; | ||
28 | import java.util.Date; | ||
24 | import java.util.Map; | 29 | import java.util.Map; |
25 | import org.eclipse.emf.common.util.EList; | 30 | import org.eclipse.emf.common.util.EList; |
26 | import org.eclipse.emf.common.util.URI; | 31 | import org.eclipse.emf.common.util.URI; |
@@ -28,8 +33,10 @@ import org.eclipse.emf.ecore.EObject; | |||
28 | import org.eclipse.emf.ecore.resource.Resource; | 33 | import org.eclipse.emf.ecore.resource.Resource; |
29 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 34 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
30 | import org.eclipse.xtend2.lib.StringConcatenation; | 35 | import org.eclipse.xtend2.lib.StringConcatenation; |
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
31 | import org.eclipse.xtext.xbase.lib.Exceptions; | 37 | import org.eclipse.xtext.xbase.lib.Exceptions; |
32 | import org.eclipse.xtext.xbase.lib.InputOutput; | 38 | import org.eclipse.xtext.xbase.lib.InputOutput; |
39 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
33 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
34 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
35 | 42 | ||
@@ -41,43 +48,51 @@ public class YakinduTest { | |||
41 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); | 48 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); |
42 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); | 49 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); |
43 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 50 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
51 | long _currentTimeMillis = System.currentTimeMillis(); | ||
52 | final Date date = new Date(_currentTimeMillis); | ||
53 | final SimpleDateFormat format = new SimpleDateFormat("MMdd-HHmmss"); | ||
54 | final String formattedDate = format.format(date); | ||
44 | StringConcatenation _builder = new StringConcatenation(); | 55 | StringConcatenation _builder = new StringConcatenation(); |
45 | _builder.append("initialModels/"); | 56 | _builder.append("initialModels/"); |
46 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | 57 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); |
47 | StringConcatenation _builder_1 = new StringConcatenation(); | 58 | StringConcatenation _builder_1 = new StringConcatenation(); |
48 | _builder_1.append("output/YakinduTest/"); | 59 | _builder_1.append("output/YakinduTest/"); |
49 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder_1.toString(), ""); | 60 | String _plus = (_builder_1.toString() + formattedDate); |
61 | StringConcatenation _builder_2 = new StringConcatenation(); | ||
62 | _builder_2.append("/"); | ||
63 | String _plus_1 = (_plus + _builder_2); | ||
64 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_plus_1, ""); | ||
50 | workspace.initAndClear(); | 65 | workspace.initAndClear(); |
51 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | 66 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; |
52 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); | 67 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); |
53 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); | 68 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); |
54 | map.put("logicproblem", _xMIResourceFactoryImpl); | 69 | map.put("logicproblem", _xMIResourceFactoryImpl); |
55 | InputOutput.<String>println("Input and output workspaces are created"); | 70 | InputOutput.<String>println("Input and output workspaces are created"); |
56 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(FunctionalarchitecturePackage.eINSTANCE); | 71 | final EcoreMetamodelDescriptor metamodel = GeneralTest.loadMetamodel(YakindummPackage.eINSTANCE); |
57 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "FAM/FaModel.xmi"); | 72 | final EList<EObject> partialModel = GeneralTest.loadPartialModel(inputs, "yakindu/Yakindu.xmi"); |
58 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, FamPatterns.instance()); | 73 | final ViatraQuerySetDescriptor queries = GeneralTest.loadQueries(metamodel, Patterns.instance()); |
59 | InputOutput.<String>println("DSL loaded"); | 74 | InputOutput.<String>println("DSL loaded"); |
60 | int MAX = 150; | 75 | int MAX = 150; |
61 | int START = 10; | 76 | int START = 10; |
62 | int INC = 20; | 77 | int INC = 20; |
63 | int REPS = 1; | 78 | int REPS = 1; |
64 | final int EXACT = (-1); | 79 | final int EXACT = 50; |
65 | if ((EXACT != (-1))) { | 80 | if ((EXACT != (-1))) { |
66 | MAX = EXACT; | 81 | MAX = EXACT; |
67 | START = EXACT; | 82 | START = EXACT; |
68 | INC = 1; | 83 | INC = 1; |
69 | REPS = 5; | 84 | REPS = 3; |
70 | } | 85 | } |
71 | URI _workspaceURI = workspace.getWorkspaceURI(); | 86 | URI _workspaceURI = workspace.getWorkspaceURI(); |
72 | String _plus = (_workspaceURI + "//yakinduStats.csv"); | 87 | String _plus_2 = (_workspaceURI + "//_yakinduStats.csv"); |
73 | PrintWriter writer = new PrintWriter(_plus); | 88 | PrintWriter writer = new PrintWriter(_plus_2); |
74 | writer.append("size,"); | 89 | writer.append("size,"); |
75 | for (int x = 0; (x < REPS); x++) { | 90 | for (int x = 0; (x < REPS); x++) { |
76 | writer.append((("t" + Integer.valueOf(x)) + ",")); | 91 | writer.append(((((("tTransf" + Integer.valueOf(x)) + ",") + "tSolv") + Integer.valueOf(x)) + ",")); |
77 | } | 92 | } |
78 | writer.append("avg\n"); | 93 | writer.append("medSolv,medTransf\n"); |
79 | double totalTime = 0.0; | 94 | ArrayList<Double> solverTimes = CollectionLiterals.<Double>newArrayList(); |
80 | double totFound = 0.0; | 95 | ArrayList<Double> transformationTimes = CollectionLiterals.<Double>newArrayList(); |
81 | boolean modelFound = true; | 96 | boolean modelFound = true; |
82 | LogicResult solution = null; | 97 | LogicResult solution = null; |
83 | { | 98 | { |
@@ -87,18 +102,20 @@ public class YakinduTest { | |||
87 | { | 102 | { |
88 | final int num = ((i - START) / INC); | 103 | final int num = ((i - START) / INC); |
89 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); | 104 | InputOutput.<String>print((((("Generation " + Integer.valueOf(num)) + ": SIZE=") + Integer.valueOf(i)) + " Attempt: ")); |
90 | String _plus_1 = (Integer.valueOf(i) + ","); | 105 | String _plus_3 = (Integer.valueOf(i) + ","); |
91 | writer.append(_plus_1); | 106 | writer.append(_plus_3); |
92 | totalTime = 0.0; | 107 | solverTimes.clear(); |
93 | totFound = 0.0; | 108 | transformationTimes.clear(); |
94 | modelFound = true; | 109 | modelFound = true; |
95 | for (int j = 0; (j < REPS); j++) { | 110 | for (int j = 0; (j < REPS); j++) { |
96 | { | 111 | { |
97 | InputOutput.<Integer>print(Integer.valueOf(j)); | 112 | InputOutput.<Integer>print(Integer.valueOf(j)); |
98 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); | 113 | Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); |
99 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); | 114 | final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); |
100 | LogicProblem problem = modelGenerationProblem.getOutput(); | 115 | TracedOutput<LogicProblem, Ecore2Logic_Trace> modelExtensionProblem = instanceModel2Logic.transform(modelGenerationProblem, partialModel); |
101 | problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput(); | 116 | Viatra2LogicConfiguration _viatra2LogicConfiguration = new Viatra2LogicConfiguration(); |
117 | TracedOutput<LogicProblem, Viatra2LogicTrace> validModelExtensionProblem = viatra2Logic.transformQueries(queries, modelExtensionProblem, _viatra2LogicConfiguration); | ||
118 | LogicProblem problem = validModelExtensionProblem.getOutput(); | ||
102 | workspace.writeModel(problem, "Yakindu.logicproblem"); | 119 | workspace.writeModel(problem, "Yakindu.logicproblem"); |
103 | long startTime = System.currentTimeMillis(); | 120 | long startTime = System.currentTimeMillis(); |
104 | VampireSolver reasoner = null; | 121 | VampireSolver reasoner = null; |
@@ -106,9 +123,11 @@ public class YakinduTest { | |||
106 | reasoner = _vampireSolver; | 123 | reasoner = _vampireSolver; |
107 | final int size = i; | 124 | final int size = i; |
108 | final int inc = INC; | 125 | final int inc = INC; |
126 | final int iter = j; | ||
109 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 127 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
110 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 128 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
111 | it.documentationLevel = DocumentationLevel.FULL; | 129 | it.documentationLevel = DocumentationLevel.FULL; |
130 | it.iteration = iter; | ||
112 | it.typeScopes.minNewElements = (size - inc); | 131 | it.typeScopes.minNewElements = (size - inc); |
113 | it.typeScopes.maxNewElements = size; | 132 | it.typeScopes.maxNewElements = size; |
114 | it.contCycleLevel = 5; | 133 | it.contCycleLevel = 5; |
@@ -119,24 +138,26 @@ public class YakinduTest { | |||
119 | Object _get = ((ModelResult) solution).getRepresentation().get(0); | 138 | Object _get = ((ModelResult) solution).getRepresentation().get(0); |
120 | final VampireModel soln = ((VampireModel) _get); | 139 | final VampireModel soln = ((VampireModel) _get); |
121 | int _transformationTime = solution.getStatistics().getTransformationTime(); | 140 | int _transformationTime = solution.getStatistics().getTransformationTime(); |
122 | final double time = (_transformationTime / 1000.0); | 141 | final double tTime = (_transformationTime / 1000.0); |
123 | String _plus_2 = (Double.valueOf(time) + ","); | 142 | int _solverTime = solution.getStatistics().getSolverTime(); |
124 | writer.append(_plus_2); | 143 | final double sTime = (_solverTime / 1000.0); |
125 | InputOutput.<String>print((("(" + Double.valueOf(time)) + ")..")); | 144 | String _plus_4 = (Double.valueOf(tTime) + ","); |
126 | double _talTime = totalTime; | 145 | String _plus_5 = (_plus_4 + Double.valueOf(sTime)); |
127 | totalTime = (_talTime + time); | 146 | String _plus_6 = (_plus_5 + ","); |
128 | double _tFound = totFound; | 147 | writer.append(_plus_6); |
129 | totFound = (_tFound + 1); | 148 | InputOutput.<String>print((((("(" + Double.valueOf(tTime)) + "/") + Double.valueOf(sTime)) + "s)..")); |
149 | solverTimes.add(Double.valueOf(sTime)); | ||
150 | transformationTimes.add(Double.valueOf(tTime)); | ||
130 | } | 151 | } |
131 | } | 152 | } |
132 | InputOutput.println(); | 153 | InputOutput.println(); |
133 | double avg = 0.0; | 154 | Double solverMed = IterableExtensions.<Double>sort(solverTimes).get((REPS / 2)); |
134 | if ((totFound == 0)) { | 155 | Double transformationMed = IterableExtensions.<Double>sort(transformationTimes).get((REPS / 2)); |
135 | avg = (-1); | 156 | String _string = solverMed.toString(); |
136 | } else { | 157 | String _plus_4 = (_string + ","); |
137 | avg = (totalTime / totFound); | 158 | String _string_1 = transformationMed.toString(); |
138 | } | 159 | String _plus_5 = (_plus_4 + _string_1); |
139 | writer.append(Double.valueOf(avg).toString()); | 160 | writer.append(_plus_5); |
140 | writer.append("\n"); | 161 | writer.append("\n"); |
141 | } | 162 | } |
142 | int _i = i; | 163 | int _i = i; |