diff options
author | 2019-10-10 22:25:07 -0400 | |
---|---|---|
committer | 2020-06-07 19:43:14 -0400 | |
commit | b97501f5f1cdce51ead750e806dc16013f59ec38 (patch) | |
tree | 4e8f60623112320eaece09b7854063d02ff93259 /Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |
parent | VAMPIRE: Further develop testing fo r Vampire solver (diff) | |
download | VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.gz VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.tar.zst VIATRA-Generator-b97501f5f1cdce51ead750e806dc16013f59ec38.zip |
implement http requests for the TPTP server
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend')
-rw-r--r-- | Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | 58 |
1 files changed, 30 insertions, 28 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend index 28e3e685..c35b200e 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend | |||
@@ -3,13 +3,14 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns | 3 | import ca.mcgill.ecse.dslreasoner.vampire.queries.Patterns |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.CompositeElement | ||
7 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Region | ||
8 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.Transition | ||
6 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage | 9 | import ca.mcgill.ecse.dslreasoner.vampire.yakindumm.YakindummPackage |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireModel | ||
8 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic | 10 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration | 11 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2LogicConfiguration |
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | 12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel |
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | 13 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | ||
13 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 14 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
14 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
15 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration | 16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2LogicConfiguration |
@@ -17,8 +18,8 @@ import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.Insta | |||
17 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 18 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
18 | import java.io.PrintWriter | 19 | import java.io.PrintWriter |
19 | import java.text.SimpleDateFormat | 20 | import java.text.SimpleDateFormat |
20 | import java.time.LocalDate | ||
21 | import java.util.Date | 21 | import java.util.Date |
22 | import java.util.HashMap | ||
22 | import org.eclipse.emf.ecore.resource.Resource | 23 | import org.eclipse.emf.ecore.resource.Resource |
23 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 24 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
24 | 25 | ||
@@ -54,16 +55,18 @@ class YakinduTest { | |||
54 | // val queries = null | 55 | // val queries = null |
55 | println("DSL loaded") | 56 | println("DSL loaded") |
56 | 57 | ||
57 | var MAX = 80 | 58 | var SZ_TOP = 10 |
58 | var START = 79 | 59 | var SZ_BOT = 126 |
59 | var INC = 1 | 60 | var INC = 1 |
60 | var REPS = 3 | 61 | var REPS = 1 |
62 | |||
63 | val RANGE = 3 | ||
61 | 64 | ||
62 | val EXACT = 130 | 65 | val EXACT = 10 |
63 | if (EXACT != -1) { | 66 | if (EXACT != -1) { |
64 | MAX = EXACT | 67 | SZ_TOP = EXACT |
65 | START = EXACT | 68 | SZ_BOT = EXACT |
66 | INC = 5 | 69 | INC = 1 |
67 | REPS = 1 | 70 | REPS = 1 |
68 | } | 71 | } |
69 | 72 | ||
@@ -77,8 +80,8 @@ class YakinduTest { | |||
77 | var transformationTimes = newArrayList | 80 | var transformationTimes = newArrayList |
78 | var modelFound = true | 81 | var modelFound = true |
79 | var LogicResult solution = null | 82 | var LogicResult solution = null |
80 | for (var i = START; i <= MAX; i += INC) { | 83 | for (var i = SZ_BOT; i <= SZ_TOP; i += INC) { |
81 | val num = (i - START) / INC | 84 | val num = (i - SZ_BOT) / INC |
82 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") | 85 | print("Generation " + num + ": SIZE=" + i + " Attempt: ") |
83 | writer.append(i + ",") | 86 | writer.append(i + ",") |
84 | solverTimes.clear | 87 | solverTimes.clear |
@@ -106,17 +109,16 @@ class YakinduTest { | |||
106 | 109 | ||
107 | // ///////////////////////////////////////////////////// | 110 | // ///////////////////////////////////////////////////// |
108 | // Minimum Scope | 111 | // Minimum Scope |
109 | // val classMapMin = new HashMap<Class, Integer> | 112 | val classMapMin = new HashMap<Class, Integer> |
110 | // classMapMin.put(Region, 1) | 113 | classMapMin.put(Region, 1) |
111 | // classMapMin.put(Transition, 2) | 114 | classMapMin.put(Transition, 2) |
112 | // classMapMin.put(CompositeElement, 3) | 115 | classMapMin.put(CompositeElement, 3) |
113 | // val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 116 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
114 | // Maximum Scope | 117 | // Maximum Scope |
115 | // val classMapMax = new HashMap<Class, Integer> | 118 | val classMapMax = new HashMap<Class, Integer> |
116 | // classMapMax.put(Region, 5) | 119 | classMapMax.put(Region, 5) |
117 | // classMapMax.put(Transition, 2) | 120 | classMapMax.put(Transition, 2) |
118 | // classMapMax.put(Synchronization, 4) | 121 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
119 | // val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | ||
120 | // Define Config File | 122 | // Define Config File |
121 | val size = i | 123 | val size = i |
122 | val inc = INC | 124 | val inc = INC |
@@ -126,18 +128,18 @@ class YakinduTest { | |||
126 | it.documentationLevel = DocumentationLevel::FULL | 128 | it.documentationLevel = DocumentationLevel::FULL |
127 | it.iteration = iter | 129 | it.iteration = iter |
128 | it.runtimeLimit = 60 | 130 | it.runtimeLimit = 60 |
129 | it.typeScopes.maxNewElements = size | 131 | it.typeScopes.maxNewElements = -1 |
130 | it.typeScopes.minNewElements = size - 5 | 132 | it.typeScopes.minNewElements = size |
131 | 133 | it.genModel = false | |
132 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 134 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
133 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 135 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
134 | it.contCycleLevel = 5 | 136 | it.contCycleLevel = 5 |
135 | it.uniquenessDuplicates = false | 137 | it.uniquenessDuplicates = false |
136 | ] | 138 | ] |
137 | 139 | ||
138 | solution = reasoner.solve(problem, vampireConfig, workspace) | 140 | solution = reasoner.solve(problem, vampireConfig, workspace) |
139 | // print((solution as ModelResult).representation.get(0)) | 141 | // print((solution as ModelResult).representation.get(0)) |
140 | val soln = ((solution as ModelResult).representation.get(0) as VampireModel) | 142 | // val soln = ((solution as ModelResult).representation.get(0) as VampireModel) |
141 | // println(soln.confirmations) | 143 | // println(soln.confirmations) |
142 | // println((solution as ModelResult).representation) | 144 | // println((solution as ModelResult).representation) |
143 | // modelFound = !soln.confirmations.filter [ | 145 | // modelFound = !soln.confirmations.filter [ |