diff options
author | 2019-04-15 00:06:29 -0400 | |
---|---|---|
committer | 2019-04-15 00:06:29 -0400 | |
commit | 2f8149678539a94f2f4ca2e7ff5640ff5d7087cc (patch) | |
tree | 87355cdeb19a987a6ffc2dd215460e2bc34f1683 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner | |
parent | VAMPIRE: #39 Reorganise tests, working yakindu test, need debugging (diff) | |
download | VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.tar.gz VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.tar.zst VIATRA-Generator-2f8149678539a94f2f4ca2e7ff5640ff5d7087cc.zip |
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner')
5 files changed, 126 insertions, 105 deletions
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 395b4305..8e0e0b11 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 | |||
@@ -39,7 +39,15 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
39 | for (l : relationsList) { | 39 | for (l : relationsList) { |
40 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type | 40 | var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type |
41 | containmentListCopy.remove(pointingTo) | 41 | containmentListCopy.remove(pointingTo) |
42 | for (c : pointingTo.subtypes) { | 42 | var List<Type> allSubtypes = newArrayList |
43 | support.listSubtypes(pointingTo, allSubtypes) | ||
44 | for (c : allSubtypes) { | ||
45 | containmentListCopy.remove(c) | ||
46 | } | ||
47 | } | ||
48 | |||
49 | for (c : containmentListCopy) { | ||
50 | if(c.isIsAbstract) { | ||
43 | containmentListCopy.remove(c) | 51 | containmentListCopy.remove(c) |
44 | } | 52 | } |
45 | } | 53 | } |
@@ -135,7 +143,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
135 | // STEP 2 CONT'D | 143 | // STEP 2 CONT'D |
136 | for (e : type2cont.entrySet) { | 144 | for (e : type2cont.entrySet) { |
137 | val relFormula = createVLSFofFormula => [ | 145 | val relFormula = createVLSFofFormula => [ |
138 | it.name = support.toIDMultiple("containment", e.key.constant.toString) | 146 | it.name = support.toIDMultiple("containment_contained", e.key.constant.toString) |
139 | it.fofRole = "axiom" | 147 | it.fofRole = "axiom" |
140 | 148 | ||
141 | it.fofFormula = createVLSUniversalQuantifier => [ | 149 | it.fofFormula = createVLSUniversalQuantifier => [ |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend index 0ae06bc3..2dec281d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.xtend | |||
@@ -44,9 +44,20 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
44 | 44 | ||
45 | } | 45 | } |
46 | 46 | ||
47 | //deciding name of relation | ||
48 | val nameArray = r.name.split(" ") | ||
49 | var relNameVar = "" | ||
50 | if (nameArray.length == 3) { | ||
51 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | ||
52 | } | ||
53 | else { | ||
54 | relNameVar = r.name | ||
55 | } | ||
56 | val relName = relNameVar | ||
57 | |||
47 | val comply = createVLSFofFormula=> [ | 58 | val comply = createVLSFofFormula=> [ |
48 | val nameArray = r.name.split(" ") | 59 | |
49 | it.name = support.toIDMultiple("compliance", nameArray.get(0), nameArray.get(2)) | 60 | it.name = support.toIDMultiple("compliance", relName) |
50 | it.fofRole = "axiom" | 61 | it.fofRole = "axiom" |
51 | it.fofFormula = createVLSUniversalQuantifier => [ | 62 | it.fofFormula = createVLSUniversalQuantifier => [ |
52 | for (v : relVar2VLS) { | 63 | for (v : relVar2VLS) { |
@@ -54,7 +65,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
54 | } | 65 | } |
55 | it.operand = createVLSImplies => [ | 66 | it.operand = createVLSImplies => [ |
56 | val rel = createVLSFunction => [ | 67 | val rel = createVLSFunction => [ |
57 | it.constant = support.toIDMultiple("r", nameArray.get(0), nameArray.get(2)) | 68 | it.constant = support.toIDMultiple("r", relName) |
58 | for (v : relVar2VLS) { | 69 | for (v : relVar2VLS) { |
59 | it.terms += support.duplicate(v) | 70 | it.terms += support.duplicate(v) |
60 | } | 71 | } |
@@ -71,89 +82,89 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
71 | 82 | ||
72 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { | 83 | def dispatch public void transformRelation(RelationDefinition reldef, Logic2VampireLanguageMapperTrace trace) { |
73 | 84 | ||
74 | // 1. store all variables in support wrt their name | 85 | // // 1. store all variables in support wrt their name |
75 | // 1.1 if variable has type, creating list of type declarations | 86 | // // 1.1 if variable has type, creating list of type declarations |
76 | // val VLSVariable variable = createVLSVariable => [it.name = "A"] | 87 | //// val VLSVariable variable = createVLSVariable => [it.name = "A"] |
77 | val Map<Variable, VLSVariable> relationVar2VLS = new HashMap | 88 | // val Map<Variable, VLSVariable> relationVar2VLS = new HashMap |
78 | val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap | 89 | // val Map<Variable, VLSFunction> relationVar2TypeDecComply = new HashMap |
79 | val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap | 90 | // val Map<Variable, VLSFunction> relationVar2TypeDecRes = new HashMap |
80 | val typedefs = new ArrayList<VLSTerm> | 91 | // val typedefs = new ArrayList<VLSTerm> |
81 | 92 | // | |
82 | for (variable : reldef.variables) { | 93 | // for (variable : reldef.variables) { |
83 | val v = createVLSVariable => [ | 94 | // val v = createVLSVariable => [ |
84 | it.name = support.toIDMultiple("V", variable.name) | 95 | // it.name = support.toIDMultiple("V", variable.name) |
85 | ] | 96 | // ] |
86 | relationVar2VLS.put(variable, v) | 97 | // relationVar2VLS.put(variable, v) |
87 | 98 | // | |
88 | val varTypeComply = createVLSFunction => [ | 99 | // val varTypeComply = createVLSFunction => [ |
89 | it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) | 100 | // it.constant = support.toIDMultiple("t", (variable.range as ComplexTypeReference).referred.name) |
90 | it.terms += support.duplicate(v) | 101 | // it.terms += support.duplicate(v) |
91 | ] | 102 | // ] |
92 | relationVar2TypeDecComply.put(variable, varTypeComply) | 103 | // relationVar2TypeDecComply.put(variable, varTypeComply) |
93 | relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) | 104 | // relationVar2TypeDecRes.put(variable, support.duplicate(varTypeComply)) |
94 | } | 105 | // } |
95 | val nameArray = reldef.name.split(" ") | 106 | // val nameArray = reldef.name.split(" ") |
96 | val comply = createVLSFofFormula => [ | 107 | // val comply = createVLSFofFormula => [ |
97 | it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), | 108 | // it.name = support.toIDMultiple("compliance", nameArray.get(nameArray.length - 2), |
98 | nameArray.get(nameArray.length - 1)) | 109 | // nameArray.get(nameArray.length - 1)) |
99 | it.fofRole = "axiom" | 110 | // it.fofRole = "axiom" |
100 | it.fofFormula = createVLSUniversalQuantifier => [ | 111 | // it.fofFormula = createVLSUniversalQuantifier => [ |
101 | for (variable : reldef.variables) { | 112 | // for (variable : reldef.variables) { |
102 | it.variables += support.duplicate(variable.lookup(relationVar2VLS)) | 113 | // it.variables += support.duplicate(variable.lookup(relationVar2VLS)) |
103 | 114 | // | |
104 | } | 115 | // } |
105 | it.operand = createVLSImplies => [ | 116 | // it.operand = createVLSImplies => [ |
106 | it.left = createVLSFunction => [ | 117 | // it.left = createVLSFunction => [ |
107 | it.constant = support.toIDMultiple("rel", reldef.name) | 118 | // it.constant = support.toIDMultiple("rel", reldef.name) |
108 | for (variable : reldef.variables) { | 119 | // for (variable : reldef.variables) { |
109 | val v = createVLSVariable => [ | 120 | // val v = createVLSVariable => [ |
110 | it.name = variable.lookup(relationVar2VLS).name | 121 | // it.name = variable.lookup(relationVar2VLS).name |
111 | ] | 122 | // ] |
112 | it.terms += v | 123 | // it.terms += v |
113 | } | 124 | // } |
114 | ] | 125 | // ] |
115 | it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) | 126 | // it.right = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecComply.values)) |
116 | ] | 127 | // ] |
117 | ] | 128 | // ] |
118 | ] | 129 | // ] |
119 | 130 | // | |
120 | val res = createVLSFofFormula => [ | 131 | // val res = createVLSFofFormula => [ |
121 | it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), | 132 | // it.name = support.toIDMultiple("relation", nameArray.get(nameArray.length - 2), |
122 | nameArray.get(nameArray.length - 1)) | 133 | // nameArray.get(nameArray.length - 1)) |
123 | it.fofRole = "axiom" | 134 | // it.fofRole = "axiom" |
124 | it.fofFormula = createVLSUniversalQuantifier => [ | 135 | // it.fofFormula = createVLSUniversalQuantifier => [ |
125 | for (variable : reldef.variables) { | 136 | // for (variable : reldef.variables) { |
126 | val v = createVLSVariable => [ | 137 | // val v = createVLSVariable => [ |
127 | it.name = variable.lookup(relationVar2VLS).name | 138 | // it.name = variable.lookup(relationVar2VLS).name |
128 | ] | 139 | // ] |
129 | it.variables += v | 140 | // it.variables += v |
130 | 141 | // | |
131 | } | 142 | // } |
132 | it.operand = createVLSImplies => [ | 143 | // it.operand = createVLSImplies => [ |
133 | it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) | 144 | // it.left = support.unfoldAnd(new ArrayList<VLSTerm>(relationVar2TypeDecRes.values)) |
134 | it.right = createVLSEquivalent => [ | 145 | // it.right = createVLSEquivalent => [ |
135 | it.left = createVLSFunction => [ | 146 | // it.left = createVLSFunction => [ |
136 | it.constant = support.toIDMultiple("rel", reldef.name) | 147 | // it.constant = support.toIDMultiple("rel", reldef.name) |
137 | for (variable : reldef.variables) { | 148 | // for (variable : reldef.variables) { |
138 | val v = createVLSVariable => [ | 149 | // val v = createVLSVariable => [ |
139 | it.name = variable.lookup(relationVar2VLS).name | 150 | // it.name = variable.lookup(relationVar2VLS).name |
140 | ] | 151 | // ] |
141 | it.terms += v | 152 | // it.terms += v |
142 | 153 | // | |
143 | } | 154 | // } |
144 | ] | 155 | // ] |
145 | it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) | 156 | // it.right = base.transformTerm(reldef.value, trace, relationVar2VLS) |
146 | ] | 157 | // ] |
147 | 158 | // | |
148 | ] | 159 | // ] |
149 | 160 | // | |
150 | ] | 161 | // ] |
151 | 162 | // | |
152 | ] | 163 | // ] |
153 | 164 | // | |
154 | // trace.relationDefinition2Predicate.put(r,res) | 165 | // // trace.relationDefinition2Predicate.put(r,res) |
155 | trace.specification.formulas += comply; | 166 | // trace.specification.formulas += comply; |
156 | trace.specification.formulas += res; | 167 | // trace.specification.formulas += res; |
157 | 168 | ||
158 | } | 169 | } |
159 | 170 | ||
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 0a8812e4..4a8d2827 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 | |||
@@ -29,6 +29,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
30 | // TODO HANDLE | 30 | // TODO HANDLE |
31 | // 1. make a list of constants equaling the min number of specified objects | 31 | // 1. make a list of constants equaling the min number of specified objects |
32 | //These numbers do not include enums or initial model elements | ||
32 | val GLOBAL_MIN = config.typeScopes.minNewElements | 33 | val GLOBAL_MIN = config.typeScopes.minNewElements |
33 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 34 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
34 | 35 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 195b89bb..680213ab 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend | |||
@@ -273,15 +273,11 @@ class Logic2VampireLanguageMapper_Support { | |||
273 | } | 273 | } |
274 | } | 274 | } |
275 | 275 | ||
276 | def protected List<Type> listSubtypes(Type t) { | 276 | def protected void listSubtypes(Type t, List<Type> allSubtypes) { |
277 | var List<Type> allSubtypes = newArrayList | 277 | for (subt : t.subtypes) { |
278 | if (!t.subtypes.isEmpty) { | 278 | allSubtypes.add(subt) |
279 | for (subt : t.subtypes) { | 279 | listSubtypes(subt, allSubtypes) |
280 | allSubtypes.add(subt) | ||
281 | allSubtypes = listSubtypes(subt) | ||
282 | } | ||
283 | } | 280 | } |
284 | return allSubtypes | ||
285 | } | 281 | } |
286 | 282 | ||
287 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 283 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
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 3bc945df..2f3af593 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,14 +44,19 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
44 | 44 | ||
45 | // Create a VLSFunction for each Enum Element | 45 | // Create a VLSFunction for each Enum Element |
46 | val List<VLSFunction> orElems = newArrayList | 46 | val List<VLSFunction> orElems = newArrayList |
47 | |||
47 | for (e : type.elements) { | 48 | for (e : type.elements) { |
49 | val nameArray = e.name.split(" ") | ||
50 | var relNameVar = "" | ||
51 | if (nameArray.length == 3) { | ||
52 | relNameVar = support.toIDMultiple(nameArray.get(0), nameArray.get(2)) | ||
53 | } else { | ||
54 | relNameVar = e.name | ||
55 | } | ||
56 | val relName = relNameVar | ||
57 | |||
48 | val enumElemPred = createVLSFunction => [ | 58 | val enumElemPred = createVLSFunction => [ |
49 | val splitName = e.name.split(" ") | 59 | it.constant = support.toIDMultiple("e", relName) |
50 | if (splitName.length > 2) { | ||
51 | it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) | ||
52 | } else { | ||
53 | it.constant = support.toIDMultiple("e", splitName.get(0)) | ||
54 | } | ||
55 | it.terms += support.duplicate(variable) | 60 | it.terms += support.duplicate(variable) |
56 | ] | 61 | ] |
57 | trace.element2Predicate.put(e, enumElemPred) | 62 | trace.element2Predicate.put(e, enumElemPred) |
@@ -80,7 +85,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
80 | 85 | ||
81 | // Implement Enum Inheritence Hierarchy | 86 | // Implement Enum Inheritence Hierarchy |
82 | val res = createVLSFofFormula => [ | 87 | val res = createVLSFofFormula => [ |
83 | it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) | 88 | it.name = support.toIDMultiple("typeDef", type.lookup(trace.type2Predicate).constant.toString) |
84 | it.fofRole = "axiom" | 89 | it.fofRole = "axiom" |
85 | it.fofFormula = createVLSUniversalQuantifier => [ | 90 | it.fofFormula = createVLSUniversalQuantifier => [ |
86 | it.variables += support.duplicate(variable) | 91 | it.variables += support.duplicate(variable) |
@@ -105,9 +110,9 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
105 | val cst = support.toConstant(cstTerm) | 110 | val cst = support.toConstant(cstTerm) |
106 | trace.uniqueInstances.add(cst) | 111 | trace.uniqueInstances.add(cst) |
107 | 112 | ||
108 | val index = i | 113 | val index = i-globalCounter |
109 | val enumScope = createVLSFofFormula => [ | 114 | val enumScope = createVLSFofFormula => [ |
110 | it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), | 115 | it.name = support.toIDMultiple("enumScope", type.lookup(trace.type2Predicate).constant.toString, |
111 | type.elements.get(index).name.split(" ").get(0)) | 116 | type.elements.get(index).name.split(" ").get(0)) |
112 | it.fofRole = "axiom" | 117 | it.fofRole = "axiom" |
113 | it.fofFormula = createVLSUniversalQuantifier => [ | 118 | it.fofFormula = createVLSUniversalQuantifier => [ |