diff options
22 files changed, 329 insertions, 72 deletions
diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore index a8a3bf64..3b138659 100644 --- a/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore +++ b/Domains/Examples/ModelGenExampleFAM_plugin/model/FamMetamodel.ecore | |||
@@ -1,4 +1,5 @@ | |||
1 | <<<<<<< HEAD | 1 | <<<<<<< HEAD |
2 | <<<<<<< HEAD | ||
2 | <?xml version="1.0" encoding="UTF-8"?> | 3 | <?xml version="1.0" encoding="UTF-8"?> |
3 | <ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | 4 | <ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" |
4 | xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="functionalarchitecture" nsURI="http://www.inf.mit.bme.hu/viatrasolver/example/fam" | 5 | xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="functionalarchitecture" nsURI="http://www.inf.mit.bme.hu/viatrasolver/example/fam" |
@@ -131,3 +132,74 @@ | |||
131 | </eClassifiers> | 132 | </eClassifiers> |
132 | </ecore:EPackage> | 133 | </ecore:EPackage> |
133 | >>>>>>> 71108d46... VAMPIRE: Implement wf constraint handling | 134 | >>>>>>> 71108d46... VAMPIRE: Implement wf constraint handling |
135 | ======= | ||
136 | <?xml version="1.0" encoding="UTF-8"?> | ||
137 | <ecore:EPackage xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" | ||
138 | xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore" name="functionalarchitecture" nsURI="http://www.inf.mit.bme.hu/viatrasolver/example/fam" | ||
139 | nsPrefix="functionalarchitecture"> | ||
140 | <eAnnotations source="http://www.eclipse.org/emf/2002/Ecore"> | ||
141 | <details key="settingDelegates" value="org.eclipse.viatra.query.querybasedfeature"/> | ||
142 | </eAnnotations> | ||
143 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalElement" abstract="true"> | ||
144 | <eStructuralFeatures xsi:type="ecore:EReference" name="interface" eType="#//FunctionalInterface" | ||
145 | containment="true" eOpposite="#//FunctionalInterface/element"/> | ||
146 | <eStructuralFeatures xsi:type="ecore:EReference" name="model" lowerBound="1" eType="#//FunctionalArchitectureModel" | ||
147 | volatile="true" transient="true" derived="true"> | ||
148 | <eAnnotations source="org.eclipse.viatra.query.querybasedfeature"> | ||
149 | <details key="patternFQN" value="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> | ||
150 | </eAnnotations> | ||
151 | </eStructuralFeatures> | ||
152 | <eStructuralFeatures xsi:type="ecore:EReference" name="parent" eType="#//Function" | ||
153 | eOpposite="#//Function/subElements"/> | ||
154 | </eClassifiers> | ||
155 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalArchitectureModel"> | ||
156 | <eStructuralFeatures xsi:type="ecore:EReference" name="rootElements" upperBound="-1" | ||
157 | eType="#//FunctionalElement" containment="true"/> | ||
158 | </eClassifiers> | ||
159 | <eClassifiers xsi:type="ecore:EClass" name="Function" eSuperTypes="#//FunctionalElement"> | ||
160 | <eStructuralFeatures xsi:type="ecore:EReference" name="subElements" upperBound="-1" | ||
161 | eType="#//FunctionalElement" containment="true" eOpposite="#//FunctionalElement/parent"/> | ||
162 | <eStructuralFeatures xsi:type="ecore:EAttribute" name="type" lowerBound="1" eType="#//FunctionType" | ||
163 | changeable="false" volatile="true" transient="true" derived="true"> | ||
164 | <eAnnotations source="org.eclipse.viatra.query.querybasedfeature"> | ||
165 | <details key="patternFQN" value="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
166 | </eAnnotations> | ||
167 | </eStructuralFeatures> | ||
168 | </eClassifiers> | ||
169 | <eClassifiers xsi:type="ecore:EClass" name="FAMTerminator"> | ||
170 | <eStructuralFeatures xsi:type="ecore:EReference" name="data" eType="#//FunctionalData" | ||
171 | eOpposite="#//FunctionalData/terminator"/> | ||
172 | </eClassifiers> | ||
173 | <eClassifiers xsi:type="ecore:EClass" name="InformationLink"> | ||
174 | <eStructuralFeatures xsi:type="ecore:EReference" name="from" eType="#//FunctionalOutput" | ||
175 | eOpposite="#//FunctionalOutput/outgoingLinks"/> | ||
176 | <eStructuralFeatures xsi:type="ecore:EReference" name="to" lowerBound="1" eType="#//FunctionalInput" | ||
177 | eOpposite="#//FunctionalInput/IncomingLinks"/> | ||
178 | </eClassifiers> | ||
179 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalInterface"> | ||
180 | <eStructuralFeatures xsi:type="ecore:EReference" name="data" upperBound="-1" eType="#//FunctionalData" | ||
181 | containment="true" eOpposite="#//FunctionalData/interface"/> | ||
182 | <eStructuralFeatures xsi:type="ecore:EReference" name="element" eType="#//FunctionalElement" | ||
183 | eOpposite="#//FunctionalElement/interface"/> | ||
184 | </eClassifiers> | ||
185 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalInput" eSuperTypes="#//FunctionalData"> | ||
186 | <eStructuralFeatures xsi:type="ecore:EReference" name="IncomingLinks" upperBound="-1" | ||
187 | eType="#//InformationLink" eOpposite="#//InformationLink/to"/> | ||
188 | </eClassifiers> | ||
189 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalOutput" eSuperTypes="#//FunctionalData"> | ||
190 | <eStructuralFeatures xsi:type="ecore:EReference" name="outgoingLinks" upperBound="-1" | ||
191 | eType="#//InformationLink" containment="true" eOpposite="#//InformationLink/from"/> | ||
192 | </eClassifiers> | ||
193 | <eClassifiers xsi:type="ecore:EClass" name="FunctionalData" abstract="true"> | ||
194 | <eStructuralFeatures xsi:type="ecore:EReference" name="terminator" eType="#//FAMTerminator" | ||
195 | containment="true" eOpposite="#//FAMTerminator/data"/> | ||
196 | <eStructuralFeatures xsi:type="ecore:EReference" name="interface" eType="#//FunctionalInterface" | ||
197 | eOpposite="#//FunctionalInterface/data"/> | ||
198 | </eClassifiers> | ||
199 | <eClassifiers xsi:type="ecore:EEnum" name="FunctionType"> | ||
200 | <eLiterals name="Root"/> | ||
201 | <eLiterals name="Intermediate" value="1"/> | ||
202 | <eLiterals name="Leaf" value="2"/> | ||
203 | </eClassifiers> | ||
204 | </ecore:EPackage> | ||
205 | >>>>>>> ce5aafc0... VAMPIRE: fix model generation | ||
diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml index c7fcc081..19fa9181 100644 --- a/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml +++ b/Domains/Examples/ModelGenExampleFAM_plugin/plugin.xml | |||
@@ -1,4 +1,5 @@ | |||
1 | <<<<<<< HEAD | 1 | <<<<<<< HEAD |
2 | <<<<<<< HEAD | ||
2 | <?xml version="1.0" encoding="UTF-8"?><plugin> | 3 | <?xml version="1.0" encoding="UTF-8"?><plugin> |
3 | <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.model" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features"> | 4 | <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.model" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features"> |
4 | <wellbehaving-derived-feature classifier-name="FunctionalElement" feature-name="model" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/> | 5 | <wellbehaving-derived-feature classifier-name="FunctionalElement" feature-name="model" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/> |
@@ -36,3 +37,26 @@ | |||
36 | </extension> | 37 | </extension> |
37 | </plugin> | 38 | </plugin> |
38 | >>>>>>> 71108d46... VAMPIRE: Implement wf constraint handling | 39 | >>>>>>> 71108d46... VAMPIRE: Implement wf constraint handling |
40 | ======= | ||
41 | <?xml version="1.0" encoding="UTF-8"?><plugin> | ||
42 | <extension point="org.eclipse.emf.ecore.generated_package"> | ||
43 | <!-- @generated FamMetamodel --> | ||
44 | <package class="functionalarchitecture.FunctionalarchitecturePackage" genModel="model/FamMetamodel.genmodel" uri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/> | ||
45 | </extension> | ||
46 | <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.model" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features"> | ||
47 | <wellbehaving-derived-feature classifier-name="FunctionalElement" feature-name="model" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/> | ||
48 | </extension> | ||
49 | <extension id="extension.derived.hu.bme.mit.inf.dslreasoner.domains.transima.fam.type" point="org.eclipse.viatra.query.runtime.base.wellbehaving.derived.features"> | ||
50 | <wellbehaving-derived-feature classifier-name="Function" feature-name="type" package-nsUri="http://www.inf.mit.bme.hu/viatrasolver/example/fam"/> | ||
51 | </extension> | ||
52 | <extension id="hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns" point="org.eclipse.viatra.query.runtime.queryspecification"> | ||
53 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns" id="hu.bme.mit.inf.dslreasoner.domains.transima.fam.FamPatterns"> | ||
54 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | ||
55 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
56 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/> | ||
57 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/> | ||
58 | <query-specification fqn="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> | ||
59 | </group> | ||
60 | </extension> | ||
61 | </plugin> | ||
62 | >>>>>>> ce5aafc0... VAMPIRE: fix model generation | ||
diff --git a/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql b/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql index 15f70963..24348eb0 100644 --- a/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql +++ b/Domains/Examples/ModelGenExampleFAM_plugin/src/hu/bme/mit/inf/dslreasoner/domains/transima/fam/FamPatterns.vql | |||
@@ -11,35 +11,34 @@ pattern terminatorAndInformation(T : FAMTerminator, I : InformationLink) = { | |||
11 | FunctionalInput.terminator(In,T); | 11 | FunctionalInput.terminator(In,T); |
12 | } | 12 | } |
13 | 13 | ||
14 | //@QueryBasedFeature | 14 | @QueryBasedFeature |
15 | //pattern type(This : Function, Target : FunctionType) = { | 15 | pattern type(This : Function, Target : FunctionType) = { |
16 | // find rootElements(_Model, This); | 16 | find rootElements(_Model, This); |
17 | // Target == FunctionType::Root; | 17 | Target == FunctionType::Root; |
18 | //} or { | 18 | } or { |
19 | // neg find parent(_Child, This); | 19 | neg find parent(_Child, This); |
20 | // neg find rootElements(_Model, This); | 20 | neg find rootElements(_Model, This); |
21 | // Target == FunctionType::Leaf; | 21 | Target == FunctionType::Leaf; |
22 | //} or { | 22 | } or { |
23 | // find parent(This, _Par); | 23 | find parent(This, _Par); |
24 | // find parent(_Child, This); | 24 | find parent(_Child, This); |
25 | // Target == FunctionType::Intermediate; | 25 | Target == FunctionType::Intermediate; |
26 | //} | 26 | } |
27 | // | 27 | |
28 | ////@Constraint | 28 | pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = { |
29 | //pattern rootElements(Model: FunctionalArchitectureModel, Root : Function) = { | 29 | FunctionalArchitectureModel.rootElements(Model, Root); |
30 | // FunctionalArchitectureModel.rootElements(Model, Root); | 30 | } |
31 | //} | 31 | |
32 | // | 32 | pattern parent(Func : Function, Par : Function) = { |
33 | //pattern parent(Func : Function, Par : Function) = { | 33 | Function.parent(Func, Par); |
34 | // Function.parent(Func, Par); | 34 | } |
35 | //} | 35 | |
36 | // | 36 | @QueryBasedFeature |
37 | //@QueryBasedFeature | 37 | pattern model(This:FunctionalElement, Target: FunctionalArchitectureModel) { |
38 | //pattern model(This:FunctionalElement, Target: FunctionalArchitectureModel) { | 38 | FunctionalElement(This); |
39 | // FunctionalElement(This); | 39 | FunctionalArchitectureModel(Target); |
40 | // FunctionalArchitectureModel(Target); | 40 | } |
41 | //} | 41 | |
42 | // | ||
43 | //pattern hasRoot(F : Function) { | 42 | //pattern hasRoot(F : Function) { |
44 | // find rootElements(_Model, F); | 43 | // find rootElements(_Model, F); |
45 | //} | 44 | //} |
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 14926280..b617912d 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 | |||
@@ -265,7 +265,11 @@ class Logic2VampireLanguageMapper { | |||
265 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, | 265 | def dispatch protected VLSTerm transformSymbolicReference(DefinedElement referred, |
266 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, | 266 | List<Term> parameterSubstitutions, Logic2VampireLanguageMapperTrace trace, |
267 | Map<Variable, VLSVariable> variables) { | 267 | Map<Variable, VLSVariable> variables) { |
268 | typeMapper.transformReference(referred, trace) | 268 | val name = referred.lookup(trace.definedElement2String) |
269 | return createVLSConstant => [ | ||
270 | it.name = name | ||
271 | ] | ||
272 | // typeMapper.transformReference(referred, trace) | ||
269 | } | 273 | } |
270 | 274 | ||
271 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, | 275 | def dispatch protected VLSTerm transformSymbolicReference(ConstantDeclaration constant, |
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 d2a01e0e..38c99a89 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 | |||
@@ -138,9 +138,9 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
138 | val cstTerm = createVLSFunctionAsTerm => [ | 138 | val cstTerm = createVLSFunctionAsTerm => [ |
139 | it.functor = "eo" + num | 139 | it.functor = "eo" + num |
140 | ] | 140 | ] |
141 | if (isNotEnum) { | 141 | // if (isNotEnum) { |
142 | trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) | 142 | trace.definedElement2String.put(type.elements.get(index),cstTerm.functor) |
143 | } | 143 | // } |
144 | 144 | ||
145 | val cst = support.toConstant(cstTerm) | 145 | val cst = support.toConstant(cstTerm) |
146 | trace.uniqueInstances.add(cst) | 146 | trace.uniqueInstances.add(cst) |
@@ -249,8 +249,13 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
249 | } | 249 | } |
250 | 250 | ||
251 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { | 251 | def protected transformReference(DefinedElement referred, Logic2VampireLanguageMapperTrace trace) { |
252 | createVLSDoubleQuote => [ | 252 | |
253 | it.value = "\"a" + referred.name + "\"" | 253 | // createVLSDoubleQuote => [ |
254 | // it.value = "\"a" + referred.name + "\"" | ||
255 | // ] | ||
256 | |||
257 | createVLSConstant => [ | ||
258 | it.name = referred.name | ||
254 | ] | 259 | ] |
255 | } | 260 | } |
256 | 261 | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend index ef77b6ca..9eb47f41 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/VampireModelInterpretation.xtend | |||
@@ -246,7 +246,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
246 | return declaration.lookup(this.type2DefinedElement) | 246 | return declaration.lookup(this.type2DefinedElement) |
247 | } | 247 | } |
248 | 248 | ||
249 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | 249 | def private dispatch getElementsDispatch(TypeDefinition declaration) { |
250 | println("~~" + declaration) | ||
251 | println(declaration.elements) | ||
252 | println() | ||
253 | return declaration.elements | ||
254 | } | ||
250 | 255 | ||
251 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 256 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
252 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 257 | throw new UnsupportedOperationException("TODO: auto-generated method stub") |
@@ -260,12 +265,12 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
260 | for (real : realRelations) { | 265 | for (real : realRelations) { |
261 | if (real.contains(node1) && real.contains(node2)) { | 266 | if (real.contains(node1) && real.contains(node2)) { |
262 | println(" true") | 267 | println(" true") |
263 | TimeUnit.SECONDS.sleep(1) | 268 | TimeUnit.MILLISECONDS.sleep(10) |
264 | return true | 269 | return true |
265 | } | 270 | } |
266 | } | 271 | } |
267 | println(" false") | 272 | println(" false") |
268 | TimeUnit.SECONDS.sleep(1) | 273 | TimeUnit.MILLISECONDS.sleep(10) |
269 | return false | 274 | return false |
270 | } | 275 | } |
271 | 276 | ||
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 b1e3b95d..8ce1beed 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/.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 803b5fed..f7259e75 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_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 7e8b1703..116b2d15 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 f8a65187..c8961c6e 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 | |||
@@ -283,7 +283,12 @@ public class Logic2VampireLanguageMapper { | |||
283 | } | 283 | } |
284 | 284 | ||
285 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 285 | protected VLSTerm _transformSymbolicReference(final DefinedElement referred, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
286 | return this.typeMapper.transformReference(referred, trace); | 286 | final String name = CollectionsUtil.<DefinedElement, String>lookup(referred, trace.definedElement2String); |
287 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
288 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
289 | it.setName(name); | ||
290 | }; | ||
291 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
287 | } | 292 | } |
288 | 293 | ||
289 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { | 294 | protected VLSTerm _transformSymbolicReference(final ConstantDeclaration constant, final List<Term> parameterSubstitutions, final Logic2VampireLanguageMapperTrace trace, final Map<Variable, VLSVariable> variables) { |
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 c8888eb0..72fea6d3 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 | |||
@@ -5,7 +5,6 @@ import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguage | |||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSDoubleQuote; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquality; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; | 9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSEquivalent; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFofFormula; |
@@ -177,9 +176,7 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
177 | it.setFunctor(("eo" + Integer.valueOf(num))); | 176 | it.setFunctor(("eo" + Integer.valueOf(num))); |
178 | }; | 177 | }; |
179 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); | 178 | final VLSFunctionAsTerm cstTerm = ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function_3); |
180 | if (isNotEnum) { | 179 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); |
181 | trace.definedElement2String.put(type_1.getElements().get(index), cstTerm.getFunctor()); | ||
182 | } | ||
183 | final VLSConstant cst = this.support.toConstant(cstTerm); | 180 | final VLSConstant cst = this.support.toConstant(cstTerm); |
184 | trace.uniqueInstances.add(cst); | 181 | trace.uniqueInstances.add(cst); |
185 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 182 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
@@ -328,15 +325,12 @@ public class Logic2VampireLanguageMapper_TypeMapper { | |||
328 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); | 325 | throw new UnsupportedOperationException("TODO: auto-generated method stub"); |
329 | } | 326 | } |
330 | 327 | ||
331 | protected VLSDoubleQuote transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { | 328 | protected VLSConstant transformReference(final DefinedElement referred, final Logic2VampireLanguageMapperTrace trace) { |
332 | VLSDoubleQuote _createVLSDoubleQuote = this.factory.createVLSDoubleQuote(); | 329 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
333 | final Procedure1<VLSDoubleQuote> _function = (VLSDoubleQuote it) -> { | 330 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { |
334 | String _name = referred.getName(); | 331 | it.setName(referred.getName()); |
335 | String _plus = ("\"a" + _name); | ||
336 | String _plus_1 = (_plus + "\""); | ||
337 | it.setValue(_plus_1); | ||
338 | }; | 332 | }; |
339 | return ObjectExtensions.<VLSDoubleQuote>operator_doubleArrow(_createVLSDoubleQuote, _function); | 333 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); |
340 | } | 334 | } |
341 | 335 | ||
342 | protected void getTypeInterpreter() { | 336 | protected void getTypeInterpreter() { |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem index fe14bb31..226150e8 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/output/FAMTest/Fam.logicproblem | |||
@@ -496,7 +496,7 @@ | |||
496 | </expression> | 496 | </expression> |
497 | </value> | 497 | </value> |
498 | </assertions> | 498 | </assertions> |
499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.20"> | 499 | <assertions name="errorpattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.24"> |
500 | <value xsi:type="language_1:Forall"> | 500 | <value xsi:type="language_1:Forall"> |
501 | <quantifiedVariables name="p0"> | 501 | <quantifiedVariables name="p0"> |
502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 502 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
@@ -505,7 +505,7 @@ | |||
505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 505 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
506 | </quantifiedVariables> | 506 | </quantifiedVariables> |
507 | <expression xsi:type="language_1:Not"> | 507 | <expression xsi:type="language_1:Not"> |
508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | 508 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17"> |
509 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> | 509 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.0"/> |
510 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> | 510 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@assertions.19/@value/@quantifiedVariables.1"/> |
511 | </operand> | 511 | </operand> |
@@ -572,7 +572,51 @@ | |||
572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | 572 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | 573 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> |
574 | </relations> | 574 | </relations> |
575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.19"> | 575 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam rootElements" annotations="//@annotations.19"> |
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
578 | <variables name="parameter Model"> | ||
579 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
580 | </variables> | ||
581 | <variables name="parameter Root"> | ||
582 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
583 | </variables> | ||
584 | <value xsi:type="language_1:Or"> | ||
585 | <operands xsi:type="language_1:And"> | ||
586 | <operands xsi:type="language_1:InstanceOf"> | ||
587 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
588 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
589 | </operands> | ||
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.3"> | ||
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | ||
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | ||
593 | </operands> | ||
594 | </operands> | ||
595 | </value> | ||
596 | </relations> | ||
597 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam model" annotations="//@annotations.20"> | ||
598 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
599 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
600 | <variables name="parameter This"> | ||
601 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
602 | </variables> | ||
603 | <variables name="parameter Target"> | ||
604 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
605 | </variables> | ||
606 | <value xsi:type="language_1:Or"> | ||
607 | <operands xsi:type="language_1:And"> | ||
608 | <operands xsi:type="language_1:InstanceOf"> | ||
609 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.0"/> | ||
610 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.0"/> | ||
611 | </operands> | ||
612 | <operands xsi:type="language_1:InstanceOf"> | ||
613 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.16/@variables.1"/> | ||
614 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
615 | </operands> | ||
616 | </operands> | ||
617 | </value> | ||
618 | </relations> | ||
619 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam terminatorAndInformation" annotations="//@annotations.21"> | ||
576 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> | 620 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.3"/> |
577 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> | 621 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.4"/> |
578 | <variables name="parameter T"> | 622 | <variables name="parameter T"> |
@@ -588,12 +632,12 @@ | |||
588 | </quantifiedVariables> | 632 | </quantifiedVariables> |
589 | <expression xsi:type="language_1:And"> | 633 | <expression xsi:type="language_1:And"> |
590 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> | 634 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.11"> |
591 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | 635 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> |
592 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | 636 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> |
593 | </operands> | 637 | </operands> |
594 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 638 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> |
595 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.0/@quantifiedVariables.0"/> | 639 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.0/@quantifiedVariables.0"/> |
596 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | 640 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> |
597 | </operands> | 641 | </operands> |
598 | </expression> | 642 | </expression> |
599 | </operands> | 643 | </operands> |
@@ -603,16 +647,117 @@ | |||
603 | </quantifiedVariables> | 647 | </quantifiedVariables> |
604 | <expression xsi:type="language_1:And"> | 648 | <expression xsi:type="language_1:And"> |
605 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> | 649 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.7"> |
606 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.1"/> | 650 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.1"/> |
607 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 651 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> |
652 | </operands> | ||
653 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | ||
654 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@value/@operands.1/@quantifiedVariables.0"/> | ||
655 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.17/@variables.0"/> | ||
656 | </operands> | ||
657 | </expression> | ||
658 | </operands> | ||
659 | </value> | ||
660 | </relations> | ||
661 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam parent" annotations="//@annotations.22"> | ||
662 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
663 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
664 | <variables name="parameter Func"> | ||
665 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
666 | </variables> | ||
667 | <variables name="parameter Par"> | ||
668 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
669 | </variables> | ||
670 | <value xsi:type="language_1:Or"> | ||
671 | <operands xsi:type="language_1:And"> | ||
672 | <operands xsi:type="language_1:InstanceOf"> | ||
673 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
674 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
675 | </operands> | ||
676 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.2"> | ||
677 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.0"/> | ||
678 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
679 | </operands> | ||
680 | <operands xsi:type="language_1:InstanceOf"> | ||
681 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18/@variables.1"/> | ||
682 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
683 | </operands> | ||
684 | </operands> | ||
685 | </value> | ||
686 | </relations> | ||
687 | <relations xsi:type="language_1:RelationDefinition" name="pattern hu bme mit inf dslreasoner domains transima fam type" annotations="//@annotations.23"> | ||
688 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
689 | <parameters xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
690 | <variables name="parameter This"> | ||
691 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
692 | </variables> | ||
693 | <variables name="parameter Target"> | ||
694 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.9"/> | ||
695 | </variables> | ||
696 | <value xsi:type="language_1:Or"> | ||
697 | <operands xsi:type="language_1:Exists"> | ||
698 | <quantifiedVariables name="variable Model"> | ||
699 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
700 | </quantifiedVariables> | ||
701 | <expression xsi:type="language_1:And"> | ||
702 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
703 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.0/@quantifiedVariables.0"/> | ||
704 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
705 | </operands> | ||
706 | <operands xsi:type="language_1:Equals"> | ||
707 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
708 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.0"/> | ||
608 | </operands> | 709 | </operands> |
710 | </expression> | ||
711 | </operands> | ||
712 | <operands xsi:type="language_1:Forall"> | ||
713 | <quantifiedVariables name="variable Child"> | ||
714 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
715 | </quantifiedVariables> | ||
716 | <quantifiedVariables name="variable Model"> | ||
717 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.1"/> | ||
718 | </quantifiedVariables> | ||
719 | <expression xsi:type="language_1:And"> | ||
609 | <operands xsi:type="language_1:InstanceOf"> | 720 | <operands xsi:type="language_1:InstanceOf"> |
610 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 721 | <value xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> |
611 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.6"/> | 722 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> |
612 | </operands> | 723 | </operands> |
613 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.12"> | 724 | <operands xsi:type="language_1:Not"> |
614 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@value/@operands.1/@quantifiedVariables.0"/> | 725 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> |
615 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15/@variables.0"/> | 726 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.0"/> |
727 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
728 | </operand> | ||
729 | </operands> | ||
730 | <operands xsi:type="language_1:Not"> | ||
731 | <operand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.15"> | ||
732 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.1/@quantifiedVariables.1"/> | ||
733 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
734 | </operand> | ||
735 | </operands> | ||
736 | <operands xsi:type="language_1:Equals"> | ||
737 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
738 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.2"/> | ||
739 | </operands> | ||
740 | </expression> | ||
741 | </operands> | ||
742 | <operands xsi:type="language_1:Exists"> | ||
743 | <quantifiedVariables name="variable Par"> | ||
744 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
745 | </quantifiedVariables> | ||
746 | <quantifiedVariables name="variable Child"> | ||
747 | <range xsi:type="language_1:ComplexTypeReference" referred="//@types.2"/> | ||
748 | </quantifiedVariables> | ||
749 | <expression xsi:type="language_1:And"> | ||
750 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
751 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
752 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.0"/> | ||
753 | </operands> | ||
754 | <operands xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.18"> | ||
755 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@value/@operands.2/@quantifiedVariables.1"/> | ||
756 | <parameterSubstitutions xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.0"/> | ||
757 | </operands> | ||
758 | <operands xsi:type="language_1:Equals"> | ||
759 | <leftOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@relations.19/@variables.1"/> | ||
760 | <rightOperand xsi:type="language_1:SymbolicValue" symbolicReference="//@elements.1"/> | ||
616 | </operands> | 761 | </operands> |
617 | </expression> | 762 | </expression> |
618 | </operands> | 763 | </operands> |
@@ -642,6 +787,10 @@ | |||
642 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> | 787 | <annotations xsi:type="ecore2logicannotations:InverseRelationAssertion" target="//@assertions.16" inverseA="//@relations.8" inverseB="//@relations.13"/> |
643 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> | 788 | <annotations xsi:type="ecore2logicannotations:LowerMultiplicityAssertion" target="//@assertions.17" relation="//@relations.14" lower="1"/> |
644 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> | 789 | <annotations xsi:type="ecore2logicannotations:UpperMultiplicityAssertion" target="//@assertions.18" relation="//@relations.14" upper="1"/> |
645 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | 790 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.15" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.rootElements"/> |
646 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.19"/> | 791 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.16" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.model"/> |
792 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.17" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.terminatorAndInformation"/> | ||
793 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.18" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.parent"/> | ||
794 | <annotations xsi:type="viatra2logicannotations:TransfomedViatraQuery" target="//@relations.19" patternFullyQualifiedName="hu.bme.mit.inf.dslreasoner.domains.transima.fam.type"/> | ||
795 | <annotations xsi:type="viatra2logicannotations:TransformedViatraWellformednessConstraint" target="//@assertions.19" query="//@annotations.21"/> | ||
647 | </language:LogicProblem> | 796 | </language:LogicProblem> |
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 3c6a65ca..5143641b 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 | |||
@@ -86,16 +86,16 @@ class FAMTest { | |||
86 | classMapMax.put(FunctionalOutput, 4) | 86 | classMapMax.put(FunctionalOutput, 4) |
87 | 87 | ||
88 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | 88 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
89 | 89 | ||
90 | // Define Config File | 90 | // Define Config File |
91 | val vampireConfig = new VampireSolverConfiguration => [ | 91 | val vampireConfig = new VampireSolverConfiguration => [ |
92 | // add configuration things, in config file first | 92 | // add configuration things, in config file first |
93 | it.documentationLevel = DocumentationLevel::FULL | 93 | it.documentationLevel = DocumentationLevel::FULL |
94 | 94 | ||
95 | it.typeScopes.minNewElements = 4//24 | 95 | it.typeScopes.minNewElements = 8//24 |
96 | it.typeScopes.maxNewElements = 5//25 | 96 | it.typeScopes.maxNewElements = 10//25 |
97 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 97 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
98 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 98 | // if(typeMapMax.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
99 | it.contCycleLevel = 5 | 99 | it.contCycleLevel = 5 |
100 | it.uniquenessDuplicates = false | 100 | it.uniquenessDuplicates = false |
101 | ] | 101 | ] |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin index 775c1663..a30b7cfc 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.EcoreTest.xtendbin | |||
Binary files differ | |||
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 4e802213..a818eb7e 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 f7e42672..b913bd4b 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/.GeneralTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin index ae8b52eb..4a9e17e1 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/icse/.GeneralTest.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 73b1182c..3dcefc79 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 7f6dfcd5..26252d6c 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 | |||
@@ -89,8 +89,8 @@ public class FAMTest { | |||
89 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 89 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
90 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 90 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
91 | it.documentationLevel = DocumentationLevel.FULL; | 91 | it.documentationLevel = DocumentationLevel.FULL; |
92 | it.typeScopes.minNewElements = 4; | 92 | it.typeScopes.minNewElements = 8; |
93 | it.typeScopes.maxNewElements = 5; | 93 | it.typeScopes.maxNewElements = 10; |
94 | int _size = typeMapMin.size(); | 94 | int _size = typeMapMin.size(); |
95 | boolean _notEquals = (_size != 0); | 95 | boolean _notEquals = (_size != 0); |
96 | if (_notEquals) { | 96 | if (_notEquals) { |
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin index 91c99504..4fb4dbc3 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.MedicalSystem.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin index dec17082..0eacff72 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin index 3c55afad..2c32163b 100644 --- a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||