diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-24 19:54:57 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2020-06-07 19:37:06 -0400 |
commit | 06b2801cd5893ced25745d79959592f99b4ef83b (patch) | |
tree | c1b5ae4feb156332847bf0cc7c30a30f5f893d64 | |
parent | VAMPIRE: add to #40. I am tired (diff) | |
download | VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.tar.gz VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.tar.zst VIATRA-Generator-06b2801cd5893ced25745d79959592f99b4ef83b.zip |
VAMPIRE : initial model handling almost done. only typeScope remains #40
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 | ||
16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 16 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | ||
18 | 19 | ||
19 | class Logic2VampireLanguageMapper_ContainmentMapper { | 20 | class 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 | |||
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
8 | import java.util.ArrayList | 9 | import java.util.ArrayList |
9 | import java.util.HashMap | 10 | import java.util.HashMap |
11 | import java.util.List | ||
10 | import java.util.Map | 12 | import java.util.Map |
11 | 13 | ||
12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 14 | import 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; | |||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition; |
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; | 27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference; |
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl; | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; | 29 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy; |
29 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 30 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
30 | import java.util.ArrayList; | 31 | import java.util.ArrayList; |
@@ -36,7 +37,6 @@ import org.eclipse.emf.common.util.EList; | |||
36 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | 37 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; |
37 | import org.eclipse.xtext.xbase.lib.Conversions; | 38 | import org.eclipse.xtext.xbase.lib.Conversions; |
38 | import org.eclipse.xtext.xbase.lib.Extension; | 39 | import org.eclipse.xtext.xbase.lib.Extension; |
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 41 | import 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 | |||
17 | import java.util.HashMap | 17 | import java.util.HashMap |
18 | import org.eclipse.emf.ecore.resource.Resource | 18 | import org.eclipse.emf.ecore.resource.Resource |
19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 19 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
20 | import functionalarchitecture.FunctionalArchitectureModel | ||
20 | 21 | ||
21 | class FAMTest { | 22 | class 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 | |||
14 | import java.util.HashMap | 14 | import java.util.HashMap |
15 | import org.eclipse.emf.ecore.resource.Resource | 15 | import org.eclipse.emf.ecore.resource.Resource |
16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 16 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
17 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region | ||
17 | 18 | ||
18 | class YakinduTest { | 19 | class 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; | |||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; |
6 | import functionalarchitecture.Function; | 6 | import functionalarchitecture.Function; |
7 | import functionalarchitecture.FunctionalArchitectureModel; | ||
7 | import functionalarchitecture.FunctionalOutput; | 8 | import functionalarchitecture.FunctionalOutput; |
8 | import functionalarchitecture.FunctionalarchitecturePackage; | 9 | import functionalarchitecture.FunctionalarchitecturePackage; |
9 | import hu.bme.mit.inf.dslreasoner.ecore2logic.Ecore2Logic; | 10 | import 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.icse; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.Region; | ||
3 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage; | 4 | import ca.mcgill.ecse.dslreasoner.standalone.test.yakindu.yakinduPackage; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.icse.GeneralTest; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | 6 | import 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) { |