aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-24 19:54:57 -0400
committerLibravatar ArenBabikian <aren.babikian@mail.mcgill.ca>2019-04-24 19:54:57 -0400
commit8af821e133a51179c1692cd48fb03cad80124e54 (patch)
tree18b0c29469d3bb9843baf61bb372bdaeb9f88f21
parentVAMPIRE: add to #40. I am tired (diff)
downloadVIATRA-Generator-8af821e133a51179c1692cd48fb03cad80124e54.tar.gz
VIATRA-Generator-8af821e133a51179c1692cd48fb03cad80124e54.tar.zst
VIATRA-Generator-8af821e133a51179c1692cd48fb03cad80124e54.zip
VAMPIRE : initial model handling almost done. only typeScope remains #40
Diffstat
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend8
-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.xtend63
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend70
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend30
-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.xtendbinbin18159 -> 18151 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbinbin4481 -> 4581 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.xtendbinbin11150 -> 11478 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbinbin6457 -> 6455 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbinbin9839 -> 10180 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 -> 13048 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbinbin11070 -> 11135 bytes
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java2
-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.java31
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java32
-rw-r--r--Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java102
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.xtend5
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/src/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.xtend6
-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.xtendbinbin6302 -> 6360 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.FileSystemTest.xtendbinbin6618 -> 6654 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.YakinduTest.xtendbinbin6040 -> 6171 bytes
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FAMTest.java3
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/FileSystemTest.java5
-rw-r--r--Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/YakinduTest.java8
28 files changed, 238 insertions, 141 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
index 2be6c093..13db3c99 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend
@@ -78,10 +78,7 @@ class Logic2VampireLanguageMapper {
78 if (!problem.types.isEmpty) { 78 if (!problem.types.isEmpty) {
79 typeMapper.transformTypes(problem.types, problem.elements, this, trace) 79 typeMapper.transformTypes(problem.types, problem.elements, this, trace)
80 } 80 }
81 81
82 // SCOPE MAPPER
83 scopeMapper.transformScope(config, trace)
84
85 // RELATION MAPPER 82 // RELATION MAPPER
86 trace.relationDefinitions = problem.collectRelationDefinitions 83 trace.relationDefinitions = problem.collectRelationDefinitions
87 problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] 84 problem.relations.forEach[this.relationMapper.transformRelation(it, trace)]
@@ -89,6 +86,9 @@ class Logic2VampireLanguageMapper {
89 // CONTAINMENT MAPPER 86 // CONTAINMENT MAPPER
90 containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) 87 containmentMapper.transformContainment(config,problem.containmentHierarchies, trace)
91 88
89 // SCOPE MAPPER
90 scopeMapper.transformScope(problem.types, config, trace)
91
92 // CONSTANT MAPPER 92 // CONSTANT MAPPER
93 // only transforms definitions 93 // only transforms definitions
94 trace.constantDefinitions = problem.collectConstantDefinitions 94 trace.constantDefinitions = problem.collectConstantDefinitions
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 b9928383..e0089c41 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
@@ -31,6 +31,7 @@ class Logic2VampireLanguageMapperTrace {
31 public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace 31 public var Logic2VampireLanguageMapper_TypeMapperTrace typeMapperTrace
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 35
35 public val Map<Type, VLSFunction> type2Predicate = new HashMap; 36 public val Map<Type, VLSFunction> type2Predicate = new HashMap;
36 public val Map<DefinedElement, VLSFunction> element2Predicate = new HashMap 37 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 c56b54be..9f29ea49 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
@@ -15,6 +15,7 @@ import java.util.Map
15 15
16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 16import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition 17import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
18import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl
18 19
19class Logic2VampireLanguageMapper_ContainmentMapper { 20class Logic2VampireLanguageMapper_ContainmentMapper {
20 val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE 21 val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE
@@ -36,7 +37,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
36 val containmentListCopy = hierarchy.typesOrderedInHierarchy 37 val containmentListCopy = hierarchy.typesOrderedInHierarchy
37 val relationsList = hierarchy.containmentRelations 38 val relationsList = hierarchy.containmentRelations
38 val toRemove = newArrayList 39 val toRemove = newArrayList
39 40
40 // STEP 1 41 // STEP 1
41 // Find root element 42 // Find root element
42 for (l : relationsList) { 43 for (l : relationsList) {
@@ -48,7 +49,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
48 containmentListCopy.remove(c) 49 containmentListCopy.remove(c)
49 } 50 }
50 } 51 }
51 52
52// OLD 53// OLD
53// for (c : containmentListCopy) { 54// for (c : containmentListCopy) {
54// if(c.isIsAbstract) { 55// if(c.isIsAbstract) {
@@ -58,42 +59,43 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
58 // State that there must exist 1 and only 1 root element 59 // State that there must exist 1 and only 1 root element
59// val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString 60// val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString
60// val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) 61// val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate))
61
62 var topTermVar = containmentListCopy.get(0) 62 var topTermVar = containmentListCopy.get(0)
63 for (l : relationsList) { 63 for (l : relationsList) {
64 var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type 64 var pointingFrom = (l.parameters.get(0) as ComplexTypeReference).referred as Type
65 if(containmentListCopy.contains(pointingFrom)) { 65 if (containmentListCopy.contains(pointingFrom)) {
66 //The correct topTerm will be identified 66 // The correct topTerm will be identified
67 topTermVar = pointingFrom 67 topTermVar = pointingFrom
68 } 68 }
69 } 69 }
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 73
74
75
76 var topLvlIsInInitModel = false 74 var topLvlIsInInitModel = false
77 var topLvlString = "" 75 var topLvlString = ""
78 for ( c : topTermVar.subtypes) { 76 var listToCheck = newArrayList(topTermVar)
79 if (c.class.simpleName.equals("TypeDefinitionImpl") ) { 77 listToCheck.addAll(topTermVar.subtypes)
78 for (c : listToCheck) {
79 if (c.class == typeof(TypeDefinitionImpl)) {
80 80
81 for (d : (c as TypeDefinition).elements) { 81 if((c as TypeDefinition).elements.length >1) {
82 if (trace.definedElement2String.containsKey(d)) { 82 throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model")
83 topLvlIsInInitModel = true 83 }
84 topLvlString = d.lookup(trace.definedElement2String) 84
85 for (d : (c as TypeDefinition).elements) {
86 if (trace.definedElement2String.containsKey(d)) {
87 topLvlIsInInitModel = true
88 topLvlString = d.lookup(trace.definedElement2String)
89 }
85 } 90 }
86 } 91 }
87 92
88 }
89
90
91 } 93 }
94
95 trace.topLvlElementIsInInitialModel = topLvlIsInInitModel
92 val topInIM = topLvlIsInInitModel 96 val topInIM = topLvlIsInInitModel
93 val topStr = topLvlString 97 val topStr = topLvlString
94 print(topInIM) 98
95 print(topStr)
96
97 val contTop = createVLSFofFormula => [ 99 val contTop = createVLSFofFormula => [
98 it.name = support.toIDMultiple("containment_topLevel", topName) 100 it.name = support.toIDMultiple("containment_topLevel", topName)
99 it.fofRole = "axiom" 101 it.fofRole = "axiom"
@@ -105,7 +107,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
105 it.right = createVLSEquality => [ 107 it.right = createVLSEquality => [
106 it.left = support.duplicate(variable) 108 it.left = support.duplicate(variable)
107 it.right = createVLSConstant => [ 109 it.right = createVLSConstant => [
108 it.name = if (topInIM) topStr else "o1" 110 it.name = if(topInIM) topStr else "o1"
109 ] 111 ]
110 ] 112 ]
111 ] 113 ]
@@ -119,8 +121,8 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
119 ] 121 ]
120 trace.specification.formulas += contTop 122 trace.specification.formulas += contTop
121 123
122 // STEP 2 124// STEP 2
123 // for each edge, if the pointedTo element exists,the edge must exist also 125// for each edge, if the pointedTo element exists,the edge must exist also
124 val varA = createVLSVariable => [it.name = "A"] 126 val varA = createVLSVariable => [it.name = "A"]
125 val varB = createVLSVariable => [it.name = "B"] 127 val varB = createVLSVariable => [it.name = "B"]
126 val varC = createVLSVariable => [it.name = "C"] 128 val varC = createVLSVariable => [it.name = "C"]
@@ -207,23 +209,22 @@ class Logic2VampireLanguageMapper_ContainmentMapper {
207 // STEP 4 209 // STEP 4
208 // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) 210 // Ensure that there are no cycles in the hierarchy (maybe same as for step3?)
209 // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed 211 // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed
210
211
212 val variables = newArrayList 212 val variables = newArrayList
213 val disjunctionList = newArrayList 213 val disjunctionList = newArrayList
214 val conjunctionList = newArrayList 214 val conjunctionList = newArrayList
215 for (var i = 1; i <= config.contCycleLevel; i++) { 215 for (var i = 1; i <= config.contCycleLevel; i++) {
216 val ind = i 216 val ind = i
217 variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) 217 variables.add(createVLSVariable => [it.name = ("V" + Integer.toString(ind))])
218 for ( var j = 0; j < i;j++){ 218 for (var j = 0; j < i; j++) {
219 for (l : relationsList) { 219 for (l : relationsList) {
220 val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) 220 val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate),
221 newArrayList(variables.get(j), variables.get((j + 1) % i)))
221 disjunctionList.add(rel) 222 disjunctionList.add(rel)
222 } 223 }
223 conjunctionList.add(support.unfoldOr(disjunctionList)) 224 conjunctionList.add(support.unfoldOr(disjunctionList))
224 disjunctionList.clear 225 disjunctionList.clear
225 } 226 }
226 227
227 val contCycleForm = createVLSFofFormula => [ 228 val contCycleForm = createVLSFofFormula => [
228 it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) 229 it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind))
229 it.fofRole = "axiom" 230 it.fofRole = "axiom"
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 c50aa770..ec841546 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
@@ -5,8 +5,10 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm
5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable 5import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable
6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory 6import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory
7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type 7import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
8import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition
8import java.util.ArrayList 9import java.util.ArrayList
9import java.util.HashMap 10import java.util.HashMap
11import java.util.List
10import java.util.Map 12import java.util.Map
11 13
12import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* 14import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.*
@@ -21,7 +23,7 @@ class Logic2VampireLanguageMapper_ScopeMapper {
21 this.base = base 23 this.base = base
22 } 24 }
23 25
24 def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { 26 def dispatch public void transformScope(List<Type> types, VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) {
25 val ABSOLUTE_MIN = 0 27 val ABSOLUTE_MIN = 0
26 val ABSOLUTE_MAX = Integer.MAX_VALUE 28 val ABSOLUTE_MAX = Integer.MAX_VALUE
27 29
@@ -31,8 +33,22 @@ class Logic2VampireLanguageMapper_ScopeMapper {
31 // 1. make a list of constants equaling the min number of specified objects 33 // 1. make a list of constants equaling the min number of specified objects
32 //These numbers do not include enums or initial model elements 34 //These numbers do not include enums or initial model elements
33 35
34 val GLOBAL_MIN = config.typeScopes.minNewElements 36 //Number of defined non-abstract elements that are not enum elements
35 val GLOBAL_MAX = config.typeScopes.maxNewElements 37 //Equals the number of elements in te initial model
38 var elemsInIM = trace.definedElement2String.size
39// var elemsInIM = 0
40//
41// for(t : types.filter(TypeDefinition).filter[!isIsAbstract]) {
42// val len = t.name.length
43// val isNotEnum = !t.name.substring(len-4, len).equals("enum")
44// if (isNotEnum) {
45// elemsInIM += 1
46// }
47// }
48
49 //TODO handle errors related to GLOBAL_MIN/MAX < 0
50 val GLOBAL_MIN = config.typeScopes.minNewElements-elemsInIM
51 val GLOBAL_MAX = config.typeScopes.maxNewElements-elemsInIM
36 52
37 val localInstances = newArrayList 53 val localInstances = newArrayList
38 54
@@ -63,31 +79,61 @@ class Logic2VampireLanguageMapper_ScopeMapper {
63 79
64 // Handling Minimum_Specific 80 // Handling Minimum_Specific
65 var i = 1 81 var i = 1
82 if (trace.topLvlElementIsInInitialModel as Boolean){
83 i = 0
84 }
66 var minNum = -1 85 var minNum = -1
67 var Map<Type, Integer> startPoints = new HashMap 86 var Map<Type, Integer> startPoints = new HashMap
68 for (t : config.typeScopes.minNewElementsByType.keySet) { 87// var inIM = false
69 minNum = t.lookup(config.typeScopes.minNewElementsByType) 88 for (tConfig : config.typeScopes.minNewElementsByType.keySet) {
89// var numIniIntModel = 0
90// for (elem : trace.definedElement2String.keySet) {
91// println(elem.definedInType)
92// for (tDefined : elem.definedInType) {
93// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
94// }
95// if (inIM) {
96// numIniIntModel += 1
97// }
98// inIM = false
99// }
100
101 minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
70 if (minNum != 0) { 102 if (minNum != 0) {
71 getInstanceConstants(i + minNum, i, localInstances, trace, true, false) 103 getInstanceConstants(i + minNum, i, localInstances, trace, true, false)
72 startPoints.put(t, i) 104 startPoints.put(tConfig, i)
73 i += minNum 105 i += minNum
74 makeFofFormula(localInstances, trace, true, t) 106 makeFofFormula(localInstances, trace, true, tConfig)
75 } 107 }
76 } 108 }
77 109
78 // TODO: calc sum of mins, compare to current value of i 110 // TODO: calc sum of mins, compare to current value of i
79 // Handling Maximum_Specific 111 // Handling Maximum_Specific
80 for (t : config.typeScopes.maxNewElementsByType.keySet) { 112 for (tConfig : config.typeScopes.maxNewElementsByType.keySet) {
81 var maxNum = t.lookup(config.typeScopes.maxNewElementsByType) 113
82 minNum = t.lookup(config.typeScopes.minNewElementsByType) 114// var numIniIntModel = 0
83 var startpoint = t.lookup(startPoints) 115// for (elem : trace.definedElement2String.keySet) {
116// println(elem.definedInType)
117// for (tDefined : elem.definedInType) {
118// inIM = support.dfsSubtypeCheck(tConfig, tDefined) || tConfig.equals(tDefined)
119// }
120// if (inIM) {
121// numIniIntModel += 1
122// }
123// inIM = false
124// }
125
126 var maxNum = tConfig.lookup(config.typeScopes.maxNewElementsByType)//-numIniIntModel
127 minNum = tConfig.lookup(config.typeScopes.minNewElementsByType)//-numIniIntModel
128 var startpoint = tConfig.lookup(startPoints)
84 if (minNum != 0) { 129 if (minNum != 0) {
85 getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false) 130 getInstanceConstants(startpoint + minNum, startpoint, localInstances, trace, true, false)
86 } 131 }
132 //I do not understand the line below
87 if (maxNum != minNum) { 133 if (maxNum != minNum) {
88 var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum) 134 var instEndInd = Math.min(GLOBAL_MAX, i + maxNum - minNum)
89 getInstanceConstants(instEndInd, i, localInstances, trace, false, false) 135 getInstanceConstants(instEndInd, i, localInstances, trace, false, false)
90 makeFofFormula(localInstances, trace, false, t) 136 makeFofFormula(localInstances, trace, false, tConfig)
91 } 137 }
92 } 138 }
93 139
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
index 2a121446..1b30393f 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend
@@ -44,13 +44,31 @@ class Logic2VampireLanguageMapper_TypeMapper {
44 trace.type2Predicate.put(type, typePred) 44 trace.type2Predicate.put(type, typePred)
45 } 45 }
46 46
47 // 2. Map each ENUM type definition to fof formula 47 // 2. Map each ENUM/InitialModelElement type definition to fof formula
48 // This also Handles initial Model stuff 48 // In the case where , for example, a supertype that is abstract has a subtype of which an instance is in the initial model,
49 for (type : types.filter(TypeDefinition)) { 49 // The logic problem will contain a TypeDefinition for the subtype as well as for the supertype
50 // This defined elemtn for the supertype will be abstract, and we do not wish to associate a constant to it, or associate it with a type
51 // Within our vampireproblem.tptp
52 for (type : types.filter(TypeDefinition).filter[!isIsAbstract]) {
53
54 //Detect if it is a defined element (from initial model)
55 //Otherwise it is an Enum
56
57 //val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract
58 //^does not work in cases where a defined type already has a supertype from within the MM
59
60// var isNotEnumVar = !type.supertypes.isEmpty
61// if(isNotEnumVar) {
62// for (sup : type.supertypes){
63// type.name.contains(sup.name)
64// }
65// }
66//
67// val isNotEnum = isNotEnumVar
50 68
51 //Detect if is an Enum 69 //Another possibility is..
52 //Otherwise, it is a defined element (from initial model) 70 val len = type.name.length
53 val isNotEnum = type.supertypes.length == 1 && type.supertypes.get(0).isIsAbstract 71 val isNotEnum = !type.name.substring(len-4, len).equals("enum")
54 72
55 // Create a VLSFunction for each Enum Element 73 // Create a VLSFunction for each Enum Element
56 val List<VLSFunction> orElems = newArrayList 74 val List<VLSFunction> orElems = newArrayList
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 80a74b4c..f312e3a8 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 2dc1ce19..88960abc 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 3c14aa6c..580eb165 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 b51b8ceb..adc1b1cf 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 02b4f393..57f21798 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 1feb9930..355315f8 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 fbc106a5..77a5ce95 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 77ffdd4b..5eef76af 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 070afd3c..b042022e 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/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
index f04bd7dc..65f58281 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java
@@ -117,13 +117,13 @@ public class Logic2VampireLanguageMapper {
117 if (_not) { 117 if (_not) {
118 this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace); 118 this.typeMapper.transformTypes(problem.getTypes(), problem.getElements(), this, trace);
119 } 119 }
120 this.scopeMapper.transformScope(config, trace);
121 trace.relationDefinitions = this.collectRelationDefinitions(problem); 120 trace.relationDefinitions = this.collectRelationDefinitions(problem);
122 final Consumer<Relation> _function_3 = (Relation it) -> { 121 final Consumer<Relation> _function_3 = (Relation it) -> {
123 this.relationMapper.transformRelation(it, trace); 122 this.relationMapper.transformRelation(it, trace);
124 }; 123 };
125 problem.getRelations().forEach(_function_3); 124 problem.getRelations().forEach(_function_3);
126 this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); 125 this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace);
126 this.scopeMapper.transformScope(problem.getTypes(), config, trace);
127 trace.constantDefinitions = this.collectConstantDefinitions(problem); 127 trace.constantDefinitions = this.collectConstantDefinitions(problem);
128 final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { 128 final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> {
129 this.constantMapper.transformConstantDefinitionSpecification(it, trace); 129 this.constantMapper.transformConstantDefinitionSpecification(it, trace);
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 621a6e58..f1600087 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
@@ -31,6 +31,8 @@ public class Logic2VampireLanguageMapperTrace {
31 31
32 public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>(); 32 public Map<DefinedElement, String> definedElement2String = new HashMap<DefinedElement, String>();
33 33
34 public Object topLvlElementIsInInitialModel = null;
35
34 public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>(); 36 public final Map<Type, VLSFunction> type2Predicate = new HashMap<Type, VLSFunction>();
35 37
36 public final Map<DefinedElement, VLSFunction> element2Predicate = new HashMap<DefinedElement, VLSFunction>(); 38 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 855d7637..07677b7a 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
@@ -25,6 +25,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration;
25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; 25import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type;
26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; 26import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition;
27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; 27import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference;
28import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl;
28import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; 29import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy;
29import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; 30import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil;
30import java.util.ArrayList; 31import java.util.ArrayList;
@@ -36,7 +37,6 @@ import org.eclipse.emf.common.util.EList;
36import org.eclipse.xtext.xbase.lib.CollectionLiterals; 37import org.eclipse.xtext.xbase.lib.CollectionLiterals;
37import org.eclipse.xtext.xbase.lib.Conversions; 38import org.eclipse.xtext.xbase.lib.Conversions;
38import org.eclipse.xtext.xbase.lib.Extension; 39import org.eclipse.xtext.xbase.lib.Extension;
39import org.eclipse.xtext.xbase.lib.InputOutput;
40import org.eclipse.xtext.xbase.lib.ObjectExtensions; 40import org.eclipse.xtext.xbase.lib.ObjectExtensions;
41import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; 41import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
42 42
@@ -91,10 +91,17 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
91 final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate)); 91 final VLSFunction topTerm = this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(topTermVar, trace.type2Predicate));
92 boolean topLvlIsInInitModel = false; 92 boolean topLvlIsInInitModel = false;
93 String topLvlString = ""; 93 String topLvlString = "";
94 EList<Type> _subtypes = topTermVar.getSubtypes(); 94 ArrayList<Type> listToCheck = CollectionLiterals.<Type>newArrayList(topTermVar);
95 for (final Type c : _subtypes) { 95 listToCheck.addAll(topTermVar.getSubtypes());
96 boolean _equals = c.getClass().getSimpleName().equals("TypeDefinitionImpl"); 96 for (final Type c : listToCheck) {
97 Class<? extends Type> _class = c.getClass();
98 boolean _equals = Objects.equal(_class, TypeDefinitionImpl.class);
97 if (_equals) { 99 if (_equals) {
100 int _length = ((Object[])Conversions.unwrapArray(((TypeDefinition) c).getElements(), Object.class)).length;
101 boolean _greaterThan = (_length > 1);
102 if (_greaterThan) {
103 throw new IllegalArgumentException("You cannot have multiple top-level elements in your initial model");
104 }
98 EList<DefinedElement> _elements = ((TypeDefinition) c).getElements(); 105 EList<DefinedElement> _elements = ((TypeDefinition) c).getElements();
99 for (final DefinedElement d : _elements) { 106 for (final DefinedElement d : _elements) {
100 boolean _containsKey = trace.definedElement2String.containsKey(d); 107 boolean _containsKey = trace.definedElement2String.containsKey(d);
@@ -105,10 +112,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
105 } 112 }
106 } 113 }
107 } 114 }
115 trace.topLvlElementIsInInitialModel = Boolean.valueOf(topLvlIsInInitModel);
108 final boolean topInIM = topLvlIsInInitModel; 116 final boolean topInIM = topLvlIsInInitModel;
109 final String topStr = topLvlString; 117 final String topStr = topLvlString;
110 InputOutput.<Boolean>print(Boolean.valueOf(topInIM));
111 InputOutput.<String>print(topStr);
112 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); 118 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
113 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { 119 final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> {
114 it.setName(this.support.toIDMultiple("containment_topLevel", topName)); 120 it.setName(this.support.toIDMultiple("containment_topLevel", topName));
@@ -174,8 +180,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
174 final Type toType = ((Type) _referred); 180 final Type toType = ((Type) _referred);
175 final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate); 181 final VLSFunction toFunc = CollectionsUtil.<Type, VLSFunction>lookup(toType, trace.type2Predicate);
176 this.addToMap(type2cont, toFunc, rel); 182 this.addToMap(type2cont, toFunc, rel);
177 EList<Type> _subtypes_1 = toType.getSubtypes(); 183 EList<Type> _subtypes = toType.getSubtypes();
178 for (final Type c_1 : _subtypes_1) { 184 for (final Type c_1 : _subtypes) {
179 this.addToMap(type2cont, toFunc, rel); 185 this.addToMap(type2cont, toFunc, rel);
180 } 186 }
181 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); 187 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
@@ -242,9 +248,9 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
242 EList<VLSVariable> _variables_1 = it_3.getVariables(); 248 EList<VLSVariable> _variables_1 = it_3.getVariables();
243 VLSVariable _duplicate_1 = this.support.duplicate(varB); 249 VLSVariable _duplicate_1 = this.support.duplicate(varB);
244 _variables_1.add(_duplicate_1); 250 _variables_1.add(_duplicate_1);
245 int _length = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length; 251 int _length_1 = ((Object[])Conversions.unwrapArray(e.getValue(), Object.class)).length;
246 boolean _greaterThan = (_length > 1); 252 boolean _greaterThan_1 = (_length_1 > 1);
247 if (_greaterThan) { 253 if (_greaterThan_1) {
248 it_3.setOperand(this.makeUnique(e.getValue())); 254 it_3.setOperand(this.makeUnique(e.getValue()));
249 } else { 255 } else {
250 it_3.setOperand(e.getValue().get(0)); 256 it_3.setOperand(e.getValue().get(0));
@@ -282,7 +288,8 @@ public class Logic2VampireLanguageMapper_ContainmentMapper {
282 { 288 {
283 for (final Relation l_3 : relationsList) { 289 for (final Relation l_3 : relationsList) {
284 { 290 {
285 final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); 291 final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_3), trace.rel2Predicate),
292 CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i))));
286 disjunctionList.add(rel); 293 disjunctionList.add(rel);
287 } 294 }
288 } 295 }
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 f5d35b28..bf7b70d0 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
@@ -47,11 +47,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
47 this.base = base; 47 this.base = base;
48 } 48 }
49 49
50 public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { 50 public void _transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
51 final int ABSOLUTE_MIN = 0; 51 final int ABSOLUTE_MIN = 0;
52 final int ABSOLUTE_MAX = Integer.MAX_VALUE; 52 final int ABSOLUTE_MAX = Integer.MAX_VALUE;
53 final int GLOBAL_MIN = config.typeScopes.minNewElements; 53 int elemsInIM = trace.definedElement2String.size();
54 final int GLOBAL_MAX = config.typeScopes.maxNewElements; 54 final int GLOBAL_MIN = (config.typeScopes.minNewElements - elemsInIM);
55 final int GLOBAL_MAX = (config.typeScopes.maxNewElements - elemsInIM);
55 final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); 56 final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList();
56 final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); 57 final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN);
57 if ((GLOBAL_MIN != ABSOLUTE_MIN)) { 58 if ((GLOBAL_MIN != ABSOLUTE_MIN)) {
@@ -74,34 +75,37 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
74 } 75 }
75 } 76 }
76 int i_1 = 1; 77 int i_1 = 1;
78 if ((((Boolean) trace.topLvlElementIsInInitialModel)).booleanValue()) {
79 i_1 = 0;
80 }
77 int minNum = (-1); 81 int minNum = (-1);
78 Map<Type, Integer> startPoints = new HashMap<Type, Integer>(); 82 Map<Type, Integer> startPoints = new HashMap<Type, Integer>();
79 Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet(); 83 Set<Type> _keySet = config.typeScopes.minNewElementsByType.keySet();
80 for (final Type t : _keySet) { 84 for (final Type tConfig : _keySet) {
81 { 85 {
82 minNum = (CollectionsUtil.<Type, Integer>lookup(t, config.typeScopes.minNewElementsByType)).intValue(); 86 minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig, config.typeScopes.minNewElementsByType)).intValue();
83 if ((minNum != 0)) { 87 if ((minNum != 0)) {
84 this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false); 88 this.getInstanceConstants((i_1 + minNum), i_1, localInstances, trace, true, false);
85 startPoints.put(t, Integer.valueOf(i_1)); 89 startPoints.put(tConfig, Integer.valueOf(i_1));
86 int _i = i_1; 90 int _i = i_1;
87 i_1 = (_i + minNum); 91 i_1 = (_i + minNum);
88 this.makeFofFormula(localInstances, trace, true, t); 92 this.makeFofFormula(localInstances, trace, true, tConfig);
89 } 93 }
90 } 94 }
91 } 95 }
92 Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet(); 96 Set<Type> _keySet_1 = config.typeScopes.maxNewElementsByType.keySet();
93 for (final Type t_1 : _keySet_1) { 97 for (final Type tConfig_1 : _keySet_1) {
94 { 98 {
95 Integer maxNum = CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.maxNewElementsByType); 99 Integer maxNum = CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.maxNewElementsByType);
96 minNum = (CollectionsUtil.<Type, Integer>lookup(t_1, config.typeScopes.minNewElementsByType)).intValue(); 100 minNum = (CollectionsUtil.<Type, Integer>lookup(tConfig_1, config.typeScopes.minNewElementsByType)).intValue();
97 Integer startpoint = CollectionsUtil.<Type, Integer>lookup(t_1, startPoints); 101 Integer startpoint = CollectionsUtil.<Type, Integer>lookup(tConfig_1, startPoints);
98 if ((minNum != 0)) { 102 if ((minNum != 0)) {
99 this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false); 103 this.getInstanceConstants(((startpoint).intValue() + minNum), (startpoint).intValue(), localInstances, trace, true, false);
100 } 104 }
101 if (((maxNum).intValue() != minNum)) { 105 if (((maxNum).intValue() != minNum)) {
102 int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum)); 106 int instEndInd = Math.min(GLOBAL_MAX, ((i_1 + (maxNum).intValue()) - minNum));
103 this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false); 107 this.getInstanceConstants(instEndInd, i_1, localInstances, trace, false, false);
104 this.makeFofFormula(localInstances, trace, false, t_1); 108 this.makeFofFormula(localInstances, trace, false, tConfig_1);
105 } 109 }
106 } 110 }
107 } 111 }
@@ -246,8 +250,8 @@ public class Logic2VampireLanguageMapper_ScopeMapper {
246 _formulas.add(cstDec); 250 _formulas.add(cstDec);
247 } 251 }
248 252
249 public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { 253 public void transformScope(final List<Type> types, final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) {
250 _transformScope(config, trace); 254 _transformScope(types, config, trace);
251 return; 255 return;
252 } 256 }
253} 257}
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
index 2d9d566d..73e59774 100644
--- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
+++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.java
@@ -77,10 +77,16 @@ public class Logic2VampireLanguageMapper_TypeMapper {
77 trace.type2Predicate.put(type, typePred); 77 trace.type2Predicate.put(type, typePred);
78 } 78 }
79 } 79 }
80 Iterable<TypeDefinition> _filter = Iterables.<TypeDefinition>filter(types, TypeDefinition.class); 80 final Function1<TypeDefinition, Boolean> _function_1 = (TypeDefinition it) -> {
81 boolean _isIsAbstract = it.isIsAbstract();
82 return Boolean.valueOf((!_isIsAbstract));
83 };
84 Iterable<TypeDefinition> _filter = IterableExtensions.<TypeDefinition>filter(Iterables.<TypeDefinition>filter(types, TypeDefinition.class), _function_1);
81 for (final TypeDefinition type_1 : _filter) { 85 for (final TypeDefinition type_1 : _filter) {
82 { 86 {
83 final boolean isNotEnum = ((((Object[])Conversions.unwrapArray(type_1.getSupertypes(), Object.class)).length == 1) && type_1.getSupertypes().get(0).isIsAbstract()); 87 final int len = type_1.getName().length();
88 boolean _equals = type_1.getName().substring((len - 4), len).equals("enum");
89 final boolean isNotEnum = (!_equals);
84 final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList(); 90 final List<VLSFunction> orElems = CollectionLiterals.<VLSFunction>newArrayList();
85 EList<DefinedElement> _elements = type_1.getElements(); 91 EList<DefinedElement> _elements = type_1.getElements();
86 for (final DefinedElement e : _elements) { 92 for (final DefinedElement e : _elements) {
@@ -88,21 +94,21 @@ public class Logic2VampireLanguageMapper_TypeMapper {
88 final String[] nameArray = e.getName().split(" "); 94 final String[] nameArray = e.getName().split(" ");
89 String relNameVar = ""; 95 String relNameVar = "";
90 int _length = nameArray.length; 96 int _length = nameArray.length;
91 boolean _equals = (_length == 3); 97 boolean _equals_1 = (_length == 3);
92 if (_equals) { 98 if (_equals_1) {
93 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]); 99 relNameVar = this.support.toIDMultiple(nameArray[0], nameArray[2]);
94 } else { 100 } else {
95 relNameVar = e.getName(); 101 relNameVar = e.getName();
96 } 102 }
97 final String relName = relNameVar; 103 final String relName = relNameVar;
98 VLSFunction _createVLSFunction = this.factory.createVLSFunction(); 104 VLSFunction _createVLSFunction = this.factory.createVLSFunction();
99 final Procedure1<VLSFunction> _function_1 = (VLSFunction it) -> { 105 final Procedure1<VLSFunction> _function_2 = (VLSFunction it) -> {
100 it.setConstant(this.support.toIDMultiple("e", relName)); 106 it.setConstant(this.support.toIDMultiple("e", relName));
101 EList<VLSTerm> _terms = it.getTerms(); 107 EList<VLSTerm> _terms = it.getTerms();
102 VLSVariable _duplicate = this.support.duplicate(variable); 108 VLSVariable _duplicate = this.support.duplicate(variable);
103 _terms.add(_duplicate); 109 _terms.add(_duplicate);
104 }; 110 };
105 final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_1); 111 final VLSFunction enumElemPred = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_2);
106 trace.element2Predicate.put(e, enumElemPred); 112 trace.element2Predicate.put(e, enumElemPred);
107 } 113 }
108 } 114 }
@@ -113,17 +119,17 @@ public class Logic2VampireLanguageMapper_TypeMapper {
113 { 119 {
114 EList<DefinedElement> _elements_2 = type_1.getElements(); 120 EList<DefinedElement> _elements_2 = type_1.getElements();
115 for (final DefinedElement t2 : _elements_2) { 121 for (final DefinedElement t2 : _elements_2) {
116 boolean _equals = Objects.equal(t1, t2); 122 boolean _equals_1 = Objects.equal(t1, t2);
117 if (_equals) { 123 if (_equals_1) {
118 final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); 124 final VLSFunction fct = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
119 possibleNots.add(fct); 125 possibleNots.add(fct);
120 } else { 126 } else {
121 final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable); 127 final VLSFunction op = this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(t2, trace.element2Predicate), variable);
122 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); 128 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
123 final Procedure1<VLSUnaryNegation> _function_1 = (VLSUnaryNegation it) -> { 129 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> {
124 it.setOperand(op); 130 it.setOperand(op);
125 }; 131 };
126 final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_1); 132 final VLSUnaryNegation negFct = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2);
127 possibleNots.add(negFct); 133 possibleNots.add(negFct);
128 } 134 }
129 } 135 }
@@ -132,32 +138,32 @@ public class Logic2VampireLanguageMapper_TypeMapper {
132 } 138 }
133 } 139 }
134 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); 140 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
135 final Procedure1<VLSFofFormula> _function_1 = (VLSFofFormula it) -> { 141 final Procedure1<VLSFofFormula> _function_2 = (VLSFofFormula it) -> {
136 it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString())); 142 it.setName(this.support.toIDMultiple("typeDef", CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate).getConstant().toString()));
137 it.setFofRole("axiom"); 143 it.setFofRole("axiom");
138 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); 144 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
139 final Procedure1<VLSUniversalQuantifier> _function_2 = (VLSUniversalQuantifier it_1) -> { 145 final Procedure1<VLSUniversalQuantifier> _function_3 = (VLSUniversalQuantifier it_1) -> {
140 EList<VLSVariable> _variables = it_1.getVariables(); 146 EList<VLSVariable> _variables = it_1.getVariables();
141 VLSVariable _duplicate = this.support.duplicate(variable); 147 VLSVariable _duplicate = this.support.duplicate(variable);
142 _variables.add(_duplicate); 148 _variables.add(_duplicate);
143 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); 149 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
144 final Procedure1<VLSEquivalent> _function_3 = (VLSEquivalent it_2) -> { 150 final Procedure1<VLSEquivalent> _function_4 = (VLSEquivalent it_2) -> {
145 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate)); 151 it_2.setLeft(CollectionsUtil.<TypeDefinition, VLSFunction>lookup(type_1, trace.type2Predicate));
146 VLSAnd _createVLSAnd = this.factory.createVLSAnd(); 152 VLSAnd _createVLSAnd = this.factory.createVLSAnd();
147 final Procedure1<VLSAnd> _function_4 = (VLSAnd it_3) -> { 153 final Procedure1<VLSAnd> _function_5 = (VLSAnd it_3) -> {
148 it_3.setLeft(this.support.topLevelTypeFunc(variable)); 154 it_3.setLeft(this.support.topLevelTypeFunc(variable));
149 it_3.setRight(this.support.unfoldOr(typeDefs)); 155 it_3.setRight(this.support.unfoldOr(typeDefs));
150 }; 156 };
151 VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_4); 157 VLSAnd _doubleArrow = ObjectExtensions.<VLSAnd>operator_doubleArrow(_createVLSAnd, _function_5);
152 it_2.setRight(_doubleArrow); 158 it_2.setRight(_doubleArrow);
153 }; 159 };
154 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_3); 160 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_4);
155 it_1.setOperand(_doubleArrow); 161 it_1.setOperand(_doubleArrow);
156 }; 162 };
157 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_2); 163 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_3);
158 it.setFofFormula(_doubleArrow); 164 it.setFofFormula(_doubleArrow);
159 }; 165 };
160 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_1); 166 final VLSFofFormula res = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_2);
161 EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); 167 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
162 _formulas.add(res); 168 _formulas.add(res);
163 for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) { 169 for (int i = globalCounter; (i < (globalCounter + ((Object[])Conversions.unwrapArray(type_1.getElements(), Object.class)).length)); i++) {
@@ -165,17 +171,17 @@ public class Logic2VampireLanguageMapper_TypeMapper {
165 final int num = (i + 1); 171 final int num = (i + 1);
166 final int index = (i - globalCounter); 172 final int index = (i - globalCounter);
167 VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); 173 VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm();
168 final Procedure1<VLSFunctionAsTerm> _function_2 = (VLSFunctionAsTerm it) -> { 174 final Procedure1<VLSFunctionAsTerm> _function_3 = (VLSFunctionAsTerm it) -> {
169 it.setFunctor(("eo" + Integer.valueOf(num))); 175 it.setFunctor(("eo" + Integer.valueOf(num)));
170 }; 176 };
171 final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_2); 177 final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3);
172 if (isNotEnum) { 178 if (isNotEnum) {
173 trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); 179 trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor());
174 } 180 }
175 final VLSConstant cst = this.support.toConstant(cstTerm); 181 final VLSConstant cst = this.support.toConstant(cstTerm);
176 trace.uniqueInstances.add(cst); 182 trace.uniqueInstances.add(cst);
177 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); 183 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
178 final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { 184 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
179 String _xifexpression = null; 185 String _xifexpression = null;
180 if (isNotEnum) { 186 if (isNotEnum) {
181 _xifexpression = "definedType"; 187 _xifexpression = "definedType";
@@ -186,28 +192,28 @@ public class Logic2VampireLanguageMapper_TypeMapper {
186 type_1.getElements().get(index).getName().split(" ")[0])); 192 type_1.getElements().get(index).getName().split(" ")[0]));
187 it.setFofRole("axiom"); 193 it.setFofRole("axiom");
188 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); 194 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
189 final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { 195 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
190 EList<VLSVariable> _variables = it_1.getVariables(); 196 EList<VLSVariable> _variables = it_1.getVariables();
191 VLSVariable _duplicate = this.support.duplicate(variable); 197 VLSVariable _duplicate = this.support.duplicate(variable);
192 _variables.add(_duplicate); 198 _variables.add(_duplicate);
193 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); 199 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
194 final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { 200 final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
195 VLSEquality _createVLSEquality = this.factory.createVLSEquality(); 201 VLSEquality _createVLSEquality = this.factory.createVLSEquality();
196 final Procedure1<VLSEquality> _function_6 = (VLSEquality it_3) -> { 202 final Procedure1<VLSEquality> _function_7 = (VLSEquality it_3) -> {
197 it_3.setLeft(this.support.duplicate(variable)); 203 it_3.setLeft(this.support.duplicate(variable));
198 it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm))); 204 it_3.setRight(this.support.duplicate(this.support.toConstant(cstTerm)));
199 }; 205 };
200 VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_6); 206 VLSEquality _doubleArrow = ObjectExtensions.<VLSEquality>operator_doubleArrow(_createVLSEquality, _function_7);
201 it_2.setLeft(_doubleArrow); 207 it_2.setLeft(_doubleArrow);
202 it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable)); 208 it_2.setRight(this.support.duplicate(CollectionsUtil.<DefinedElement, VLSFunction>lookup(type_1.getElements().get(index), trace.element2Predicate), variable));
203 }; 209 };
204 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); 210 VLSEquivalent _doubleArrow = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);
205 it_1.setOperand(_doubleArrow); 211 it_1.setOperand(_doubleArrow);
206 }; 212 };
207 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); 213 VLSUniversalQuantifier _doubleArrow = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
208 it.setFofFormula(_doubleArrow); 214 it.setFofFormula(_doubleArrow);
209 }; 215 };
210 final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_3); 216 final VLSFofFormula enumScope = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4);
211 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); 217 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
212 _formulas_1.add(enumScope); 218 _formulas_1.add(enumScope);
213 } 219 }
@@ -217,11 +223,11 @@ public class Logic2VampireLanguageMapper_TypeMapper {
217 globalCounter = (_globalCounter + _size); 223 globalCounter = (_globalCounter + _size);
218 } 224 }
219 } 225 }
220 final Function1<Type, Boolean> _function_1 = (Type it) -> { 226 final Function1<Type, Boolean> _function_2 = (Type it) -> {
221 boolean _isIsAbstract = it.isIsAbstract(); 227 boolean _isIsAbstract = it.isIsAbstract();
222 return Boolean.valueOf((!_isIsAbstract)); 228 return Boolean.valueOf((!_isIsAbstract));
223 }; 229 };
224 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_1); 230 Iterable<Type> _filter_1 = IterableExtensions.<Type>filter(types, _function_2);
225 for (final Type t1 : _filter_1) { 231 for (final Type t1 : _filter_1) {
226 { 232 {
227 for (final Type t2 : types) { 233 for (final Type t2 : types) {
@@ -229,10 +235,10 @@ public class Logic2VampireLanguageMapper_TypeMapper {
229 trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); 235 trace.type2PossibleNot.put(t2, this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
230 } else { 236 } else {
231 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); 237 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
232 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { 238 final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
233 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate))); 239 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t2, trace.type2Predicate)));
234 }; 240 };
235 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); 241 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
236 trace.type2PossibleNot.put(t2, _doubleArrow); 242 trace.type2PossibleNot.put(t2, _doubleArrow);
237 } 243 }
238 } 244 }
@@ -245,63 +251,63 @@ public class Logic2VampireLanguageMapper_TypeMapper {
245 final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList(); 251 final List<VLSTerm> type2Not = CollectionLiterals.<VLSTerm>newArrayList();
246 for (final Type t : types) { 252 for (final Type t : types) {
247 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); 253 VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation();
248 final Procedure1<VLSUnaryNegation> _function_2 = (VLSUnaryNegation it) -> { 254 final Procedure1<VLSUnaryNegation> _function_3 = (VLSUnaryNegation it) -> {
249 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate))); 255 it.setOperand(this.support.duplicate(CollectionsUtil.<Type, VLSFunction>lookup(t, trace.type2Predicate)));
250 }; 256 };
251 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_2); 257 VLSUnaryNegation _doubleArrow = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_3);
252 type2Not.add(_doubleArrow); 258 type2Not.add(_doubleArrow);
253 } 259 }
254 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); 260 VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula();
255 final Procedure1<VLSFofFormula> _function_3 = (VLSFofFormula it) -> { 261 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> {
256 it.setName("notObjectHandler"); 262 it.setName("notObjectHandler");
257 it.setFofRole("axiom"); 263 it.setFofRole("axiom");
258 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); 264 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
259 final Procedure1<VLSUniversalQuantifier> _function_4 = (VLSUniversalQuantifier it_1) -> { 265 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> {
260 EList<VLSVariable> _variables = it_1.getVariables(); 266 EList<VLSVariable> _variables = it_1.getVariables();
261 VLSVariable _duplicate = this.support.duplicate(variable); 267 VLSVariable _duplicate = this.support.duplicate(variable);
262 _variables.add(_duplicate); 268 _variables.add(_duplicate);
263 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); 269 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
264 final Procedure1<VLSEquivalent> _function_5 = (VLSEquivalent it_2) -> { 270 final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> {
265 VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation(); 271 VLSUnaryNegation _createVLSUnaryNegation_1 = this.factory.createVLSUnaryNegation();
266 final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_3) -> { 272 final Procedure1<VLSUnaryNegation> _function_7 = (VLSUnaryNegation it_3) -> {
267 it_3.setOperand(this.support.topLevelTypeFunc()); 273 it_3.setOperand(this.support.topLevelTypeFunc());
268 }; 274 };
269 VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_6); 275 VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation_1, _function_7);
270 it_2.setLeft(_doubleArrow_1); 276 it_2.setLeft(_doubleArrow_1);
271 it_2.setRight(this.support.unfoldAnd(type2Not)); 277 it_2.setRight(this.support.unfoldAnd(type2Not));
272 }; 278 };
273 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_5); 279 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6);
274 it_1.setOperand(_doubleArrow_1); 280 it_1.setOperand(_doubleArrow_1);
275 }; 281 };
276 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_4); 282 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5);
277 it.setFofFormula(_doubleArrow_1); 283 it.setFofFormula(_doubleArrow_1);
278 }; 284 };
279 final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_3); 285 final VLSFofFormula notObj = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function_4);
280 EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); 286 EList<VLSFofFormula> _formulas = trace.specification.getFormulas();
281 _formulas.add(notObj); 287 _formulas.add(notObj);
282 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); 288 VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula();
283 final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { 289 final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> {
284 it.setName("inheritanceHierarchyHandler"); 290 it.setName("inheritanceHierarchyHandler");
285 it.setFofRole("axiom"); 291 it.setFofRole("axiom");
286 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier(); 292 VLSUniversalQuantifier _createVLSUniversalQuantifier = this.factory.createVLSUniversalQuantifier();
287 final Procedure1<VLSUniversalQuantifier> _function_5 = (VLSUniversalQuantifier it_1) -> { 293 final Procedure1<VLSUniversalQuantifier> _function_6 = (VLSUniversalQuantifier it_1) -> {
288 EList<VLSVariable> _variables = it_1.getVariables(); 294 EList<VLSVariable> _variables = it_1.getVariables();
289 VLSVariable _duplicate = this.support.duplicate(variable); 295 VLSVariable _duplicate = this.support.duplicate(variable);
290 _variables.add(_duplicate); 296 _variables.add(_duplicate);
291 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent(); 297 VLSEquivalent _createVLSEquivalent = this.factory.createVLSEquivalent();
292 final Procedure1<VLSEquivalent> _function_6 = (VLSEquivalent it_2) -> { 298 final Procedure1<VLSEquivalent> _function_7 = (VLSEquivalent it_2) -> {
293 it_2.setLeft(this.support.topLevelTypeFunc()); 299 it_2.setLeft(this.support.topLevelTypeFunc());
294 Collection<VLSTerm> _values = trace.type2And.values(); 300 Collection<VLSTerm> _values = trace.type2And.values();
295 final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values); 301 final ArrayList<VLSTerm> reversedList = new ArrayList<VLSTerm>(_values);
296 it_2.setRight(this.support.unfoldOr(reversedList)); 302 it_2.setRight(this.support.unfoldOr(reversedList));
297 }; 303 };
298 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_6); 304 VLSEquivalent _doubleArrow_1 = ObjectExtensions.<VLSEquivalent>operator_doubleArrow(_createVLSEquivalent, _function_7);
299 it_1.setOperand(_doubleArrow_1); 305 it_1.setOperand(_doubleArrow_1);
300 }; 306 };
301 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_5); 307 VLSUniversalQuantifier _doubleArrow_1 = ObjectExtensions.<VLSUniversalQuantifier>operator_doubleArrow(_createVLSUniversalQuantifier, _function_6);
302 it.setFofFormula(_doubleArrow_1); 308 it.setFofFormula(_doubleArrow_1);
303 }; 309 };
304 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_4); 310 final VLSFofFormula hierarch = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5);
305 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); 311 EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas();
306 _xblockexpression = _formulas_1.add(hierarch); 312 _xblockexpression = _formulas_1.add(hierarch);
307 } 313 }
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 bbea9822..ccf36550 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
@@ -17,6 +17,7 @@ import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace
17import java.util.HashMap 17import java.util.HashMap
18import org.eclipse.emf.ecore.resource.Resource 18import org.eclipse.emf.ecore.resource.Resource
19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl 19import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl
20import functionalarchitecture.FunctionalArchitectureModel
20 21
21class FAMTest { 22class FAMTest {
22 def static void main(String[] args) { 23 def static void main(String[] args) {
@@ -46,7 +47,7 @@ class FAMTest {
46 47
47 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 48 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
48 var problem = modelGenerationProblem.output 49 var problem = modelGenerationProblem.output
49 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 50// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
50// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 51// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
51 workspace.writeModel(problem, "Fam.logicproblem") 52 workspace.writeModel(problem, "Fam.logicproblem")
52 53
@@ -62,6 +63,7 @@ class FAMTest {
62 // ///////////////////////////////////////////////////// 63 // /////////////////////////////////////////////////////
63 // Minimum Scope 64 // Minimum Scope
64 val classMapMin = new HashMap<Class, Integer> 65 val classMapMin = new HashMap<Class, Integer>
66 classMapMin.put(FunctionalArchitectureModel, 1)
65 classMapMin.put(Function, 1) 67 classMapMin.put(Function, 1)
66 classMapMin.put(FunctionalInterface, 2) 68 classMapMin.put(FunctionalInterface, 2)
67 classMapMin.put(FunctionalOutput, 3) 69 classMapMin.put(FunctionalOutput, 3)
@@ -70,6 +72,7 @@ class FAMTest {
70 72
71 // Maximum Scope 73 // Maximum Scope
72 val classMapMax = new HashMap<Class, Integer> 74 val classMapMax = new HashMap<Class, Integer>
75 classMapMax.put(FunctionalArchitectureModel, 3)
73 classMapMax.put(Function, 5) 76 classMapMax.put(Function, 5)
74 classMapMax.put(FunctionalInterface, 2) 77 classMapMax.put(FunctionalInterface, 2)
75 classMapMax.put(FunctionalOutput, 4) 78 classMapMax.put(FunctionalOutput, 4)
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 d4cbb299..61a20a34 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
@@ -43,7 +43,7 @@ class FileSystemTest {
43 43
44 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 44 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
45 var problem = modelGenerationProblem.output 45 var problem = modelGenerationProblem.output
46// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 46 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
47// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 47// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
48 workspace.writeModel(problem, "FileSystem.logicproblem") 48 workspace.writeModel(problem, "FileSystem.logicproblem")
49 49
@@ -76,8 +76,8 @@ class FileSystemTest {
76 // add configuration things, in config file first 76 // add configuration things, in config file first
77 it.documentationLevel = DocumentationLevel::FULL 77 it.documentationLevel = DocumentationLevel::FULL
78 78
79 it.typeScopes.minNewElements = 40 79 it.typeScopes.minNewElements = 10
80 it.typeScopes.maxNewElements = 59 80 it.typeScopes.maxNewElements = 25
81 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin 81 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
82 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax 82 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
83 it.contCycleLevel = 5 83 it.contCycleLevel = 5
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 f0d88b49..3342c18a 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,6 +14,7 @@ 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 18
18class YakinduTest { 19class YakinduTest {
19 def static void main(String[] args) { 20 def static void main(String[] args) {
@@ -42,7 +43,7 @@ class YakinduTest {
42 43
43 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration()) 44 val modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, new Ecore2LogicConfiguration())
44 var problem = modelGenerationProblem.output 45 var problem = modelGenerationProblem.output
45// problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output 46 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).output
46// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output 47// problem = viatra2Logic.transformQueries(queries, modelGenerationProblem, new Viatra2LogicConfiguration).output
47 workspace.writeModel(problem, "Yakindu.logicproblem") 48 workspace.writeModel(problem, "Yakindu.logicproblem")
48 49
@@ -58,14 +59,14 @@ class YakinduTest {
58 // ///////////////////////////////////////////////////// 59 // /////////////////////////////////////////////////////
59 // Minimum Scope 60 // Minimum Scope
60 val classMapMin = new HashMap<Class, Integer> 61 val classMapMin = new HashMap<Class, Integer>
61// classMapMin.put(Function, 1) 62 classMapMin.put(Region, 1)
62// classMapMin.put(FunctionalInterface, 2) 63// classMapMin.put(FunctionalInterface, 2)
63// classMapMin.put(FunctionalOutput, 3) 64// classMapMin.put(FunctionalOutput, 3)
64 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) 65 val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace)
65 66
66 // Maximum Scope 67 // Maximum Scope
67 val classMapMax = new HashMap<Class, Integer> 68 val classMapMax = new HashMap<Class, Integer>
68// classMapMax.put(Function, 5) 69 classMapMax.put(Region, 5)
69// classMapMax.put(FunctionalInterface, 2) 70// classMapMax.put(FunctionalInterface, 2)
70// classMapMax.put(FunctionalOutput, 4) 71// classMapMax.put(FunctionalOutput, 4)
71 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) 72 val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace)
@@ -75,8 +76,8 @@ class YakinduTest {
75 // add configuration things, in config file first 76 // add configuration things, in config file first
76 it.documentationLevel = DocumentationLevel::FULL 77 it.documentationLevel = DocumentationLevel::FULL
77 78
78 it.typeScopes.minNewElements = 53 79 it.typeScopes.minNewElements = 20
79 it.typeScopes.maxNewElements = 53 80 it.typeScopes.maxNewElements = 30
80 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin 81 if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin
81 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax 82 if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax
82 it.contCycleLevel = 5 83 it.contCycleLevel = 5
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 9ac7c906..796bed43 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 60e770c6..830ec7f9 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 5b017f34..395fc452 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 1fcaf9bd..855909aa 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
@@ -4,6 +4,7 @@ import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 4import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; 5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration;
6import functionalarchitecture.Function; 6import functionalarchitecture.Function;
7import functionalarchitecture.FunctionalArchitectureModel;
7import functionalarchitecture.FunctionalOutput; 8import functionalarchitecture.FunctionalOutput;
8import functionalarchitecture.FunctionalarchitecturePackage; 9import functionalarchitecture.FunctionalarchitecturePackage;
9import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; 10import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic;
@@ -65,11 +66,13 @@ public class FAMTest {
65 VampireSolver _vampireSolver = new VampireSolver(); 66 VampireSolver _vampireSolver = new VampireSolver();
66 reasoner = _vampireSolver; 67 reasoner = _vampireSolver;
67 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));
68 classMapMin.put(Function.class, Integer.valueOf(1)); 70 classMapMin.put(Function.class, Integer.valueOf(1));
69 classMapMin.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2)); 71 classMapMin.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2));
70 classMapMin.put(FunctionalOutput.class, Integer.valueOf(3)); 72 classMapMin.put(FunctionalOutput.class, Integer.valueOf(3));
71 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());
72 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 74 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
75 classMapMax.put(FunctionalArchitectureModel.class, Integer.valueOf(3));
73 classMapMax.put(Function.class, Integer.valueOf(5)); 76 classMapMax.put(Function.class, Integer.valueOf(5));
74 classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2)); 77 classMapMax.put(functionalarchitecture.FunctionalInterface.class, Integer.valueOf(2));
75 classMapMax.put(FunctionalOutput.class, Integer.valueOf(4)); 78 classMapMax.put(FunctionalOutput.class, Integer.valueOf(4));
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 f7f8a5ee..21d2a307 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
@@ -57,6 +57,7 @@ public class FileSystemTest {
57 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); 57 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
58 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); 58 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
59 LogicProblem problem = modelGenerationProblem.getOutput(); 59 LogicProblem problem = modelGenerationProblem.getOutput();
60 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
60 workspace.writeModel(problem, "FileSystem.logicproblem"); 61 workspace.writeModel(problem, "FileSystem.logicproblem");
61 InputOutput.<String>println("Problem created"); 62 InputOutput.<String>println("Problem created");
62 long startTime = System.currentTimeMillis(); 63 long startTime = System.currentTimeMillis();
@@ -70,8 +71,8 @@ public class FileSystemTest {
70 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 71 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
71 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 72 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
72 it.documentationLevel = DocumentationLevel.FULL; 73 it.documentationLevel = DocumentationLevel.FULL;
73 it.typeScopes.minNewElements = 40; 74 it.typeScopes.minNewElements = 10;
74 it.typeScopes.maxNewElements = 59; 75 it.typeScopes.maxNewElements = 25;
75 int _size = typeMapMin.size(); 76 int _size = typeMapMin.size();
76 boolean _notEquals = (_size != 0); 77 boolean _notEquals = (_size != 0);
77 if (_notEquals) { 78 if (_notEquals) {
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 3a322ee0..ceae8ed2 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,5 +1,6 @@
1package ca.mcgill.ecse.dslreasoner.vampire.icse; 1package ca.mcgill.ecse.dslreasoner.vampire.icse;
2 2
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region;
3import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage; 4import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage;
4import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; 5import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest;
5import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; 6import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver;
@@ -55,6 +56,7 @@ public class YakinduTest {
55 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration(); 56 Ecore2LogicConfiguration _ecore2LogicConfiguration = new Ecore2LogicConfiguration();
56 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration); 57 final TracedOutput<LogicProblem, Ecore2Logic_Trace> modelGenerationProblem = ecore2Logic.transformMetamodel(metamodel, _ecore2LogicConfiguration);
57 LogicProblem problem = modelGenerationProblem.getOutput(); 58 LogicProblem problem = modelGenerationProblem.getOutput();
59 problem = instanceModel2Logic.transform(modelGenerationProblem, partialModel).getOutput();
58 workspace.writeModel(problem, "Yakindu.logicproblem"); 60 workspace.writeModel(problem, "Yakindu.logicproblem");
59 InputOutput.<String>println("Problem created"); 61 InputOutput.<String>println("Problem created");
60 long startTime = System.currentTimeMillis(); 62 long startTime = System.currentTimeMillis();
@@ -62,14 +64,16 @@ public class YakinduTest {
62 VampireSolver _vampireSolver = new VampireSolver(); 64 VampireSolver _vampireSolver = new VampireSolver();
63 reasoner = _vampireSolver; 65 reasoner = _vampireSolver;
64 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>(); 66 final HashMap<Class, Integer> classMapMin = new HashMap<Class, Integer>();
67 classMapMin.put(Region.class, Integer.valueOf(1));
65 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 68 final Map<Type, Integer> typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
66 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>(); 69 final HashMap<Class, Integer> classMapMax = new HashMap<Class, Integer>();
70 classMapMax.put(Region.class, Integer.valueOf(5));
67 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace()); 71 final Map<Type, Integer> typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.getTrace());
68 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); 72 VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration();
69 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { 73 final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> {
70 it.documentationLevel = DocumentationLevel.FULL; 74 it.documentationLevel = DocumentationLevel.FULL;
71 it.typeScopes.minNewElements = 53; 75 it.typeScopes.minNewElements = 20;
72 it.typeScopes.maxNewElements = 53; 76 it.typeScopes.maxNewElements = 30;
73 int _size = typeMapMin.size(); 77 int _size = typeMapMin.size();
74 boolean _notEquals = (_size != 0); 78 boolean _notEquals = (_size != 0);
75 if (_notEquals) { 79 if (_notEquals) {
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 13:26:05 +0000