aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-25 02:50:40 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-25 02:50:40 -0400
commit9f743fd84ab112b4736eaa7923595e9c5fa1a788 (patch)
tree06e80deccac2ac8ac1235ade6cff4f93954cf0ae
parentVAMPIRE : initial model handling almost done. only typeScope remains #40 (diff)
downloadVIATRA-Generator-9f743fd84ab112b4736eaa7923595e9c5fa1a788.tar.gz
VIATRA-Generator-9f743fd84ab112b4736eaa7923595e9c5fa1a788.tar.zst
VIATRA-Generator-9f743fd84ab112b4736eaa7923595e9c5fa1a788.zip
VAMPIRE: fixed MANY bugs in containment and scope. #40 is good for now
Diffstat
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend1
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend38
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend101
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbinbin5892 -> 5892 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbinbin18151 -> 18150 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbinbin4581 -> 4656 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbinbin3164 -> 3164 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbinbin11478 -> 11904 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbinbin6455 -> 6454 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbinbin10180 -> 10667 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbinbin13048 -> 13046 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbinbin11135 -> 11136 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java2
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java56
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java82
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend10
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend15
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.xtend11
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FAMTest.xtendbinbin6360 -> 6314 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin6654 -> 7116 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin6171 -> 6678 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java5
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java6
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java7
24 files changed, 219 insertions, 115 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
index e0089c41..e94584ae 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.xtend
@@ -32,6 +32,7 @@ class Logic2VampireLanguageMapperTrace {
32 32
33 public var Map<DefinedElement, String> definedElement2String = new HashMap 33 public var Map<DefinedElement, String> definedElement2String = new HashMap
34 public var topLvlElementIsInInitialModel = null 34 public var topLvlElementIsInInitialModel = null
35 public var topLevelType = null
35 36
36 public val Map<Type, VLSFunction> type2Predicate = new HashMap; 37 public val Map<Type, VLSFunction> type2Predicate = new HashMap;
37 public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap 38 public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
index 9f29ea49..93c28e7c 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend
@@ -70,6 +70,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
70 70
71 val topName = topTermVar.lookup(trace.type2Predicate).constant.toString 71 val topName = topTermVar.lookup(trace.type2Predicate).constant.toString
72 val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate)) 72 val topTerm = support.duplicate(topTermVar.lookup(trace.type2Predicate))
73 trace.topLevelType = topTermVar
73 74
74 var topLvlIsInInitModel = false 75 var topLvlIsInInitModel = false
75 var topLvlString = "" 76 var topLvlString = ""
@@ -129,16 +130,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
129 val varList = newArrayList(varB, varA) 130 val varList = newArrayList(varB, varA)
130 val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap 131 val Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap
131 for (l : relationsList) { 132 for (l : relationsList) {
132 val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList) 133 val rel = (l as RelationDeclaration).lookup(trace.rel2Predicate)
133// val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type 134// val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type
134 val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type) 135 val toType = ((l.parameters.get(1) as ComplexTypeReference).referred as Type)
135 val toFunc = toType.lookup(trace.type2Predicate) 136 val toFunc = toType.lookup(trace.type2Predicate)
136 137
137 addToMap(type2cont, toFunc, rel) 138 addToMap(type2cont, support.duplicate(toFunc), support.duplicate(rel, varList))
138 139
139 for (c : toType.subtypes) { 140 var subTypes = newArrayList
140 addToMap(type2cont, toFunc, rel) 141 support.listSubtypes(toType, subTypes)
142 for (c : subTypes) {
143 addToMap(type2cont, support.duplicate(c.lookup(trace.type2Predicate)), support.duplicate(rel, varList))
141 } 144 }
145
146
147
148
142// for (c : support.listSubtypes(toType)) { 149// for (c : support.listSubtypes(toType)) {
143// addToMap(type2cont, toFunc, rel) 150// addToMap(type2cont, toFunc, rel)
144// } 151// }
@@ -182,6 +189,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
182 189
183// STEP 2 CONT'D 190// STEP 2 CONT'D
184 for (e : type2cont.entrySet) { 191 for (e : type2cont.entrySet) {
192 println(e.key + " " + e.value)
185 val relFormula = createVLSFofFormula => [ 193 val relFormula = createVLSFofFormula => [
186 it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) 194 it.name = support.toIDMultiple("containment_contained", e.key.constant.toString)
187 it.fofRole = "axiom" 195 it.fofRole = "axiom"
@@ -192,6 +200,11 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
192 it.left = support.duplicate(e.key, varA) 200 it.left = support.duplicate(e.key, varA)
193 it.right = createVLSExistentialQuantifier => [ 201 it.right = createVLSExistentialQuantifier => [
194 it.variables += support.duplicate(varB) 202 it.variables += support.duplicate(varB)
203// for ( x : type2cont.entrySet) {
204// if (support.dfsSupertypeCheck(e.key, x.key)) {
205// e.value.addAll(x.value)
206// }
207// }
195 if (e.value.length > 1) { 208 if (e.value.length > 1) {
196 it.operand = makeUnique(e.value) 209 it.operand = makeUnique(e.value)
197 } else { 210 } else {
@@ -264,11 +277,20 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
264 } 277 }
265 278
266 protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) { 279 protected def Object addToMap(Map<VLSFunction, List<VLSFunction>> type2cont, VLSFunction toFunc, VLSFunction rel) {
267 if (!type2cont.containsKey(toFunc)) { 280 var keyInMap = false
281 var existingKey = createVLSFunction
282 for (k : type2cont.keySet) {
283 if (k.constant.equals(toFunc.constant)) {
284 keyInMap = true
285 existingKey = k
286 }
287 }
288
289 if (!keyInMap) {
268 type2cont.put(toFunc, newArrayList(rel)) 290 type2cont.put(toFunc, newArrayList(rel))
269 } else { 291 } else {
270 if (!type2cont.get(toFunc).contains(rel)) { 292 if (!type2cont.get(existingKey).contains(rel)) {
271 type2cont.get(toFunc).add(rel) 293 type2cont.get(existingKey).add(rel)
272 // type2cont.replace(toFunc, newArrayList(firstRel)) 294 // type2cont.replace(toFunc, newArrayList(firstRel))
273 } 295 }
274 296
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
index ec841546..df3cfd82 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend
@@ -23,18 +23,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
23 this.base = base 23 this.base = base
24 } 24 }
25 25
26 def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { 26 def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config,
27 Logic2VampireLanguageMapperTrace trace) {
27 val ABSOLUTE_MIN = 0 28 val ABSOLUTE_MIN = 0
28 val ABSOLUTE_MAX = Integer.MAX_VALUE 29 val ABSOLUTE_MAX = Integer.MAX_VALUE
29 30
30// TODO HANDLE ERRORS RELATED TO MAX > MIN 31// TODO HANDLE ERRORS RELATED TO MAX > MIN
31// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS 32// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS
32// TODO HANDLE 33// TODO HANDLE case where init model does not satisfy for example ine and only one criterion of toplvl elem
33 // 1. make a list of constants equaling the min number of specified objects 34// We are currently ignoring all typescope spec related to the topLevel type
34 //These numbers do not include enums or initial model elements 35// TODO Case where typeScope spec continas numbers for a type and its subtype
36// We shouldnt waste constants for each one
35 37
36 //Number of defined non-abstract elements that are not enum elements 38 // 1. make a list of constants equaling the min number of specified objects
37 //Equals the number of elements in te initial model 39 // These numbers do not include enums or initial model elements
40 // Number of defined non-abstract elements that are not enum elements
41 // Equals the number of elements in te initial model
38 var elemsInIM = trace.definedElement2String.size 42 var elemsInIM = trace.definedElement2String.size
39// var elemsInIM = 0 43// var elemsInIM = 0
40// 44//
@@ -45,10 +49,9 @@ class Logic2VampireLanguageMapper_ScopeMapper {
45// elemsInIM += 1 49// elemsInIM += 1
46// } 50// }
47// } 51// }
48 52 // TODO handle errors related to GLOBAL_MIN/MAX < 0
49 //TODO handle errors related to GLOBAL_MIN/MAX < 0 53 val GLOBAL_MIN = config.typeScopes.minNewElements - elemsInIM
50 val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM 54 val GLOBAL_MAX = config.typeScopes.maxNewElements - elemsInIM
51 val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM
52 55
53 val localInstances = newArrayList 56 val localInstances = newArrayList
54 57
@@ -79,62 +82,60 @@ class Logic2VampireLanguageMapper_ScopeMapper {
79 82
80 // Handling Minimum_Specific 83 // Handling Minimum_Specific
81 var i = 1 84 var i = 1
82 if (trace.topLvlElementIsInInitialModel as Boolean){ 85 if (trace.topLvlElementIsInInitialModel as Boolean) {
83 i = 0 86 i = 0
84 } 87 }
85 var minNum = -1 88 var minNum = -1
86 var Map<Type, Integer> startPoints = new HashMap 89 var Map<Type, Integer> startPoints = new HashMap
87// var inIM = false 90 for (t : config.typeScopes.minNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
88 for (tConfig : config.typeScopes.minNewElementsByType.keySet) { 91 var numIniIntModel = 0
89// var numIniIntModel = 0 92 for (elem : trace.definedElement2String.keySet) {
90// for (elem : trace.definedElement2String.keySet) { 93 for (tDefined : elem.definedInType) {
91// println(elem.definedInType) 94 if (support.dfsSubtypeCheck(t, tDefined)) {
92// for (tDefined : elem.definedInType) { 95 numIniIntModel += 1
93// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) 96 }
94// } 97 }
95// if (inIM) { 98 }
96// numIniIntModel += 1 99 minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
97// }
98// inIM = false
99// }
100
101 minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
102 if (minNum != 0) { 100 if (minNum != 0) {
103 getInstanceConstants(i + minNum, i, localInstances, trace, true, false) 101 getInstanceConstants(i + minNum, i, localInstances, trace, true, false)
104 startPoints.put(tConfig, i) 102 startPoints.put(t, i)
105 i += minNum 103 i += minNum
106 makeFofFormula(localInstances, trace, true, tConfig) 104 makeFofFormula(localInstances, trace, true, t)
107 } 105 }
108 } 106 }
109 107
110 // TODO: calc sum of mins, compare to current value of i 108 // TODO: calc sum of mins, compare to current value of i
111 // Handling Maximum_Specific 109 // Handling Maximum_Specific
112 for (tConfig : config.typeScopes.maxNewElementsByType.keySet) { 110 for (t : config.typeScopes.maxNewElementsByType.keySet.filter[!equals(trace.topLevelType)]) {
113 111
114// var numIniIntModel = 0 112 var numIniIntModel = 0
115// for (elem : trace.definedElement2String.keySet) { 113 for (elem : trace.definedElement2String.keySet) {
116// println(elem.definedInType) 114 if (elem.definedInType == t) {
117// for (tDefined : elem.definedInType) { 115 numIniIntModel += 1
118// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined) 116 }
119// } 117 }
120// if (inIM) { 118
121// numIniIntModel += 1 119 var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) - numIniIntModel
122// } 120 if (config.typeScopes.minNewElementsByType.keySet.contains(t)) {
123// inIM = false 121 minNum = t.lookup(config.typeScopes.minNewElementsByType) - numIniIntModel
124// } 122 } else {
125 123 minNum = 0
126 var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel 124 }
127 minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel 125
128 var startpoint = tConfig.lookup(startPoints)
129 if (minNum != 0) { 126 if (minNum != 0) {
127 var startpoint = t.lookup(startPoints)
130 getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) 128 getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)
131 } 129 }
132 //I do not understand the line below 130 else {
133 if (maxNum != minNum) { 131 localInstances.clear
134 var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
135 getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
136 makeFofFormula(localInstances, trace, false, tConfig)
137 } 132 }
133 // I do not understand the line below
134// if (maxNum != minNum) {
135 var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
136 getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
137 makeFofFormula(localInstances, trace, false, t)
138// }
138 } 139 }
139 140
140// 3. Specify uniqueness of elements 141// 3. Specify uniqueness of elements
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
index f312e3a8..677cb718 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
index 88960abc..d071aa8a 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
index 580eb165..48090814 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
index adc1b1cf..154e42a2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
index 57f21798..61774e26 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
index 355315f8..2798d324 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
index 77a5ce95..5f3f349b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
index 5eef76af..787c44a2 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
index b042022e..b6e94088 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin
Binary files differ
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
index f1600087..c2ae099e 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java
@@ -33,6 +33,8 @@ public class Logic2VampireLanguageMapperTrace {
33 33
34 public Object topLvlElementIsInInitialModel = null; 34 public Object topLvlElementIsInInitialModel = null;
35 35
36 public Object topLevelType = null;
37
36 public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); 38 public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
37 39
38 public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); 40 public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>();
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
index 07677b7a..dd549c29 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java
@@ -37,6 +37,7 @@ import org.eclipse.emf.common.util.EList;
37import org.eclipse.xtext.xbase.lib.CollectionLiterals; 37import org.eclipse.xtext.xbase.lib.CollectionLiterals;
38import org.eclipse.xtext.xbase.lib.Conversions; 38import org.eclipse.xtext.xbase.lib.Conversions;
39import org.eclipse.xtext.xbase.lib.Extension; 39import org.eclipse.xtext.xbase.lib.Extension;
40import org.eclipse.xtext.xbase.lib.InputOutput;
40import org.eclipse.xtext.xbase.lib.ObjectExtensions; 41import org.eclipse.xtext.xbase.lib.ObjectExtensions;
41import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; 42import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
42 43
@@ -89,6 +90,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
89 } 90 }
90 final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString(); 91 final String topName = CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate).getConstant().toString();
91 final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); 92 final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));
93 trace.topLevelType = topTermVar;
92 boolean topLvlIsInInitModel = false; 94 boolean topLvlIsInInitModel = false;
93 String topLvlString = ""; 95 String topLvlString = "";
94 ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar); 96 ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar);
@@ -174,15 +176,16 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
174 final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>(); 176 final Map<VLSFunction, List<VLSFunction>> type2cont = new HashMap<VLSFunction, List<VLSFunction>>();
175 for (final Relation l_2 : relationsList) { 177 for (final Relation l_2 : relationsList) {
176 { 178 {
177 final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), varList); 179 final VLSFunction rel = CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate);
178 TypeReference _get = l_2.getParameters().get(1); 180 TypeReference _get = l_2.getParameters().get(1);
179 Type _referred = ((ComplexTypeReference) _get).getReferred(); 181 Type _referred = ((ComplexTypeReference) _get).getReferred();
180 final Type toType = ((Type) _referred); 182 final Type toType = ((Type) _referred);
181 final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); 183 final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);
182 this.addToMap(type2cont, toFunc, rel); 184 this.addToMap(type2cont, this.support.duplicate(toFunc), this.support.duplicate(rel, varList));
183 EList<Type> _subtypes = toType.getSubtypes(); 185 ArrayList<Type> subTypes = CollectionLiterals.<Type>newArrayList();
184 for (final Type c_1 : _subtypes) { 186 this.support.listSubtypes(toType, subTypes);
185 this.addToMap(type2cont, toFunc, rel); 187 for (final Type c_1 : subTypes) {
188 this.addToMap(type2cont, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(c_1, trace.type2Predicate)), this.support.duplicate(rel, varList));
186 } 189 }
187 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); 190 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
188 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { 191 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
@@ -231,6 +234,11 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
231 Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet(); 234 Set<Map.Entry<VLSFunction, List<VLSFunction>>> _entrySet = type2cont.entrySet();
232 for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) { 235 for (final Map.Entry<VLSFunction, List<VLSFunction>> e : _entrySet) {
233 { 236 {
237 VLSFunction _key = e.getKey();
238 String _plus = (_key + " ");
239 List<VLSFunction> _value = e.getValue();
240 String _plus_1 = (_plus + _value);
241 InputOutput.<String>println(_plus_1);
234 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); 242 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
235 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { 243 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
236 it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString())); 244 it.setName(this.support.toIDMultiple("containment_contained", e.getKey().getConstant().toString()));
@@ -352,20 +360,32 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
352 } 360 }
353 361
354 protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) { 362 protected Object addToMap(final Map<VLSFunction, List<VLSFunction>> type2cont, final VLSFunction toFunc, final VLSFunction rel) {
355 Object _xifexpression = null; 363 Object _xblockexpression = null;
356 boolean _containsKey = type2cont.containsKey(toFunc); 364 {
357 boolean _not = (!_containsKey); 365 boolean keyInMap = false;
358 if (_not) { 366 VLSFunction existingKey = this.factory.createVLSFunction();
359 _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel)); 367 Set<VLSFunction> _keySet = type2cont.keySet();
360 } else { 368 for (final VLSFunction k : _keySet) {
361 boolean _xifexpression_1 = false; 369 boolean _equals = k.getConstant().equals(toFunc.getConstant());
362 boolean _contains = type2cont.get(toFunc).contains(rel); 370 if (_equals) {
363 boolean _not_1 = (!_contains); 371 keyInMap = true;
364 if (_not_1) { 372 existingKey = k;
365 _xifexpression_1 = type2cont.get(toFunc).add(rel); 373 }
374 }
375 Object _xifexpression = null;
376 if ((!keyInMap)) {
377 _xifexpression = type2cont.put(toFunc, CollectionLiterals.<VLSFunction>newArrayList(rel));
378 } else {
379 boolean _xifexpression_1 = false;
380 boolean _contains = type2cont.get(existingKey).contains(rel);
381 boolean _not = (!_contains);
382 if (_not) {
383 _xifexpression_1 = type2cont.get(existingKey).add(rel);
384 }
385 _xifexpression = Boolean.valueOf(_xifexpression_1);
366 } 386 }
367 _xifexpression = Boolean.valueOf(_xifexpression_1); 387 _xblockexpression = _xifexpression;
368 } 388 }
369 return _xifexpression; 389 return _xblockexpression;
370 } 390 }
371} 391}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
index bf7b70d0..c2e4033b 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java
@@ -14,7 +14,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm;
14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; 14import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier;
15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; 15import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable;
16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; 16import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory;
17import com.google.common.base.Objects;
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement;
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; 19import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
20import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
18import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; 21import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
19import java.util.ArrayList; 22import java.util.ArrayList;
20import java.util.HashMap; 23import java.util.HashMap;
@@ -26,6 +29,7 @@ import org.eclipse.xtext.xbase.lib.CollectionLiterals;
26import org.eclipse.xtext.xbase.lib.Conversions; 29import org.eclipse.xtext.xbase.lib.Conversions;
27import org.eclipse.xtext.xbase.lib.Extension; 30import org.eclipse.xtext.xbase.lib.Extension;
28import org.eclipse.xtext.xbase.lib.Functions.Function1; 31import org.eclipse.xtext.xbase.lib.Functions.Function1;
32import org.eclipse.xtext.xbase.lib.IterableExtensions;
29import org.eclipse.xtext.xbase.lib.ListExtensions; 33import org.eclipse.xtext.xbase.lib.ListExtensions;
30import org.eclipse.xtext.xbase.lib.ObjectExtensions; 34import org.eclipse.xtext.xbase.lib.ObjectExtensions;
31import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; 35import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
@@ -80,33 +84,73 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
80 } 84 }
81 int minNum = (-1); 85 int minNum = (-1);
82 Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); 86 Map<Type, Integer> startPoints = new HashMap<Type, Integer>();
83 Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); 87 final Function1<Type, Boolean> _function = (Type it) -> {
84 for (final Type tConfig : _keySet) { 88 boolean _equals = it.equals(trace.topLevelType);
89 return Boolean.valueOf((!_equals));
90 };
91 Iterable<Type> _filter = IterableExtensions.<Type>filter(config.typeScopes.minNewElementsByType.keySet(), _function);
92 for (final Type t : _filter) {
85 { 93 {
86 minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue(); 94 int numIniIntModel = 0;
95 Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
96 for (final DefinedElement elem : _keySet) {
97 EList<TypeDefinition> _definedInType = elem.getDefinedInType();
98 for (final TypeDefinition tDefined : _definedInType) {
99 boolean _dfsSubtypeCheck = this.support.dfsSubtypeCheck(t, tDefined);
100 if (_dfsSubtypeCheck) {
101 int _numIniIntModel = numIniIntModel;
102 numIniIntModel = (_numIniIntModel + 1);
103 }
104 }
105 }
106 Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType);
107 int _minus = ((_lookup).intValue() - numIniIntModel);
108 minNum = _minus;
87 if ((minNum != 0)) { 109 if ((minNum != 0)) {
88 this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); 110 this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);
89 startPoints.put(tConfig, Integer.valueOf(i_1)); 111 startPoints.put(t, Integer.valueOf(i_1));
90 int _i = i_1; 112 int _i = i_1;
91 i_1 = (_i + minNum); 113 i_1 = (_i + minNum);
92 this.makeFofFormula(localInstances, trace, true, tConfig); 114 this.makeFofFormula(localInstances, trace, true, t);
93 } 115 }
94 } 116 }
95 } 117 }
96 Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); 118 final Function1<Type, Boolean> _function_1 = (Type it) -> {
97 for (final Type tConfig_1 : _keySet_1) { 119 boolean _equals = it.equals(trace.topLevelType);
120 return Boolean.valueOf((!_equals));
121 };
122 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(config.typeScopes.maxNewElementsByType.keySet(), _function_1);
123 for (final Type t_1 : _filter_1) {
98 { 124 {
99 Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType); 125 int numIniIntModel = 0;
100 minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue(); 126 Set<DefinedElement> _keySet = trace.definedElement2String.keySet();
101 Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints); 127 for (final DefinedElement elem : _keySet) {
128 EList<TypeDefinition> _definedInType = elem.getDefinedInType();
129 boolean _equals = Objects.equal(_definedInType, t_1);
130 if (_equals) {
131 int _numIniIntModel = numIniIntModel;
132 numIniIntModel = (_numIniIntModel + 1);
133 }
134 }
135 Integer _lookup = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType);
136 int maxNum = ((_lookup).intValue() - numIniIntModel);
137 boolean _contains = config.typeScopes.minNewElementsByType.keySet().contains(t_1);
138 if (_contains) {
139 Integer _lookup_1 = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType);
140 int _minus = ((_lookup_1).intValue() - numIniIntModel);
141 minNum = _minus;
142 } else {
143 minNum = 0;
144 }
102 if ((minNum != 0)) { 145 if ((minNum != 0)) {
146 Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints);
103 this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); 147 this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);
148 } else {
149 localInstances.clear();
104 } 150 }
105 if (((maxNum).intValue() != minNum)) { 151 int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + maxNum) - minNum));
106 int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); 152 this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);
107 this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); 153 this.makeFofFormula(localInstances, trace, false, t_1);
108 this.makeFofFormula(localInstances, trace, false, tConfig_1);
109 }
110 } 154 }
111 } 155 }
112 final boolean DUPLICATES = config.uniquenessDuplicates; 156 final boolean DUPLICATES = config.uniquenessDuplicates;
@@ -118,12 +162,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
118 { 162 {
119 final int x = ind; 163 final int x = ind;
120 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); 164 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
121 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { 165 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
122 it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); 166 it.setName(this.support.toIDMultiple("t_uniqueness", e.getName()));
123 it.setFofRole("axiom"); 167 it.setFofRole("axiom");
124 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e)); 168 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances, e));
125 }; 169 };
126 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); 170 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
127 EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); 171 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
128 _formulas.add(uniqueness); 172 _formulas.add(uniqueness);
129 ind++; 173 ind++;
@@ -135,12 +179,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
135 { 179 {
136 final int x = ind; 180 final int x = ind;
137 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); 181 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
138 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { 182 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
139 it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName())); 183 it.setName(this.support.toIDMultiple("t_uniqueness", e_1.getName()));
140 it.setFofRole("axiom"); 184 it.setFofRole("axiom");
141 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1)); 185 it.setFofFormula(this.support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e_1));
142 }; 186 };
143 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); 187 final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
144 EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); 188 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
145 _formulas.add(uniqueness); 189 _formulas.add(uniqueness);
146 ind++; 190 ind++;
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
index ccf36550..3c24abf9 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend
@@ -47,7 +47,7 @@ class FAMTest {
47 47
48 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 48 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
49 var problem = modelGenerationProblem.output 49 var problem = modelGenerationProblem.output
50// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 50 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
51// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 51// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
52 workspace.writeModel(problem, "Fam.logicproblem") 52 workspace.writeModel(problem, "Fam.logicproblem")
53 53
@@ -63,9 +63,9 @@ class FAMTest {
63 // ///////////////////////////////////////////////////// 63 // /////////////////////////////////////////////////////
64 // Minimum Scope 64 // Minimum Scope
65 val classMapMin = new HashMap<Class, Integer> 65 val classMapMin = new HashMap<Class, Integer>
66 classMapMin.put(FunctionalArchitectureModel, 1) 66// classMapMin.put(FunctionalArchitectureModel, 1)
67 classMapMin.put(Function, 1) 67// classMapMin.put(Function, 1)
68 classMapMin.put(FunctionalInterface, 2) 68// classMapMin.put(FunctionalInterface, 2)
69 classMapMin.put(FunctionalOutput, 3) 69 classMapMin.put(FunctionalOutput, 3)
70 70
71 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 71 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
@@ -74,7 +74,7 @@ class FAMTest {
74 val classMapMax = new HashMap<Class, Integer> 74 val classMapMax = new HashMap<Class, Integer>
75 classMapMax.put(FunctionalArchitectureModel, 3) 75 classMapMax.put(FunctionalArchitectureModel, 3)
76 classMapMax.put(Function, 5) 76 classMapMax.put(Function, 5)
77 classMapMax.put(FunctionalInterface, 2) 77 classMapMax.put(FunctionalInterface, 3)
78 classMapMax.put(FunctionalOutput, 4) 78 classMapMax.put(FunctionalOutput, 4)
79 79
80 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 80 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
index 61a20a34..ba7ff028 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend
@@ -15,6 +15,7 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
15import java.util.HashMap 15import java.util.HashMap
16import org.eclipse.emf.ecore.resource.Resource 16import org.eclipse.emf.ecore.resource.Resource
17import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 17import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
18import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.*
18 19
19class FileSystemTest { 20class FileSystemTest {
20 def static void main(String[] args) { 21 def static void main(String[] args) {
@@ -59,16 +60,18 @@ class FileSystemTest {
59 // ///////////////////////////////////////////////////// 60 // /////////////////////////////////////////////////////
60 // Minimum Scope 61 // Minimum Scope
61 val classMapMin = new HashMap<Class, Integer> 62 val classMapMin = new HashMap<Class, Integer>
62// classMapMin.put(Function, 1) 63// Currently does not work
63// classMapMin.put(FunctionalInterface, 2) 64// classMapMin.put(FSObject, 20)
64// classMapMin.put(FunctionalOutput, 3) 65 classMapMin.put(Dir, 10)
66 classMapMin.put(File, 5)
65 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 67 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
66 68
67 // Maximum Scope 69 // Maximum Scope
68 val classMapMax = new HashMap<Class, Integer> 70 val classMapMax = new HashMap<Class, Integer>
69// classMapMax.put(Function, 5) 71 classMapMax.put(File, 15)
70// classMapMax.put(FunctionalInterface, 2) 72 classMapMax.put(Dir, 15)
71// classMapMax.put(FunctionalOutput, 4) 73// Currently does not work
74// classMapMax.put(FSObject, 20)
72 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 75 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
73 76
74 // Define Config File 77 // Define Config File
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 3342c18a..76ac727a 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
@@ -14,7 +14,8 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
14import java.util.HashMap 14import java.util.HashMap
15import org.eclipse.emf.ecore.resource.Resource 15import org.eclipse.emf.ecore.resource.Resource
16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 16import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
17import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region 17
18import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.*
18 19
19class YakinduTest { 20class YakinduTest {
20 def static void main(String[] args) { 21 def static void main(String[] args) {
@@ -60,15 +61,15 @@ class YakinduTest {
60 // Minimum Scope 61 // Minimum Scope
61 val classMapMin = new HashMap<Class, Integer> 62 val classMapMin = new HashMap<Class, Integer>
62 classMapMin.put(Region, 1) 63 classMapMin.put(Region, 1)
63// classMapMin.put(FunctionalInterface, 2) 64 classMapMin.put(Transition, 2)
64// classMapMin.put(FunctionalOutput, 3) 65 classMapMin.put(CompositeElement, 3)
65 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 66 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
66 67
67 // Maximum Scope 68 // Maximum Scope
68 val classMapMax = new HashMap<Class, Integer> 69 val classMapMax = new HashMap<Class, Integer>
69 classMapMax.put(Region, 5) 70 classMapMax.put(Region, 5)
70// classMapMax.put(FunctionalInterface, 2) 71 classMapMax.put(Transition, 2)
71// classMapMax.put(FunctionalOutput, 4) 72 classMapMax.put(Synchronization, 4)
72 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 73 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
73 74
74 // Define Config File 75 // Define Config File
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 796bed43..9ef2b1a0 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 830ec7f9..468a5b6f 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/.YakinduTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbin
index 395fc452..bed2786b 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/FAMTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
index 855909aa..ddbe05d7 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java
@@ -66,15 +66,12 @@ public class FAMTest {
66 VampireSolver _vampireSolver = new VampireSolver(); 66 VampireSolver _vampireSolver = new VampireSolver();
67 reasoner = _vampireSolver; 67 reasoner = _vampireSolver;
68 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 68 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
69 classMapMin.put(FunctionalArchitectureModel.class, Integer.valueOf(1));
70 classMapMin.put(Function.class, Integer.valueOf(1));
71 classMapMin.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2));
72 classMapMin.put(FunctionalOutput.class, Integer.valueOf(3)); 69 classMapMin.put(FunctionalOutput.class, Integer.valueOf(3));
73 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 70 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
74 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 71 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
75 classMapMax.put(FunctionalArchitectureModel.class, Integer.valueOf(3)); 72 classMapMax.put(FunctionalArchitectureModel.class, Integer.valueOf(3));
76 classMapMax.put(Function.class, Integer.valueOf(5)); 73 classMapMax.put(Function.class, Integer.valueOf(5));
77 classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2)); 74 classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(3));
78 classMapMax.put(FunctionalOutput.class, Integer.valueOf(4)); 75 classMapMax.put(FunctionalOutput.class, Integer.valueOf(4));
79 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 76 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
80 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 77 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
index 21d2a307..4a971fd6 100644
--- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
+++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java
@@ -1,5 +1,7 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.Dir;
4import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.File;
3import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage; 5import ca.mcgill.ecse.dslreasoner.standalone.test.filesystem.filesystemPackage;
4import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 6import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
5import ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns; 7import ca.mcgill.ecse.dslreasoner.vampire.queries.FileSystemPatterns;
@@ -65,8 +67,12 @@ public class FileSystemTest {
65 VampireSolver _vampireSolver = new VampireSolver(); 67 VampireSolver _vampireSolver = new VampireSolver();
66 reasoner = _vampireSolver; 68 reasoner = _vampireSolver;
67 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 69 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
70 classMapMin.put(Dir.class, Integer.valueOf(10));
71 classMapMin.put(File.class, Integer.valueOf(5));
68 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 72 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
69 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 73 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
74 classMapMax.put(File.class, Integer.valueOf(15));
75 classMapMax.put(Dir.class, Integer.valueOf(15));
70 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 76 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
71 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 77 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
72 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 78 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
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 ceae8ed2..f0d7d924 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,6 +1,9 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.CompositeElement;
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region; 4import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region;
5import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Synchronization;
6import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Transition;
4import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage; 7import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage;
5import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 8import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 9import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
@@ -65,9 +68,13 @@ public class YakinduTest {
65 reasoner = _vampireSolver; 68 reasoner = _vampireSolver;
66 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 69 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
67 classMapMin.put(Region.class, Integer.valueOf(1)); 70 classMapMin.put(Region.class, Integer.valueOf(1));
71 classMapMin.put(Transition.class, Integer.valueOf(2));
72 classMapMin.put(CompositeElement.class, Integer.valueOf(3));
68 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 73 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
69 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 74 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
70 classMapMax.put(Region.class, Integer.valueOf(5)); 75 classMapMax.put(Region.class, Integer.valueOf(5));
76 classMapMax.put(Transition.class, Integer.valueOf(2));
77 classMapMax.put(Synchronization.class, Integer.valueOf(4));
71 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 78 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
72 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 79 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
73 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 80 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 18:35:40 +0000