diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-03 00:03:48 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-09-03 00:03:48 -0400 |
commit | 9fc9e413e61ca00beaf7d8217be173f25cf52b5d (patch) | |
tree | e105e400cceb0a2a3c0c43dd6ab47eda5b4292b3 | |
parent | VAMPIRE: implement Vampire Model Interpreter, 2/3 done (diff) | |
download | VIATRA-Generator-9fc9e413e61ca00beaf7d8217be173f25cf52b5d.tar.gz VIATRA-Generator-9fc9e413e61ca00beaf7d8217be173f25cf52b5d.tar.zst VIATRA-Generator-9fc9e413e61ca00beaf7d8217be173f25cf52b5d.zip |
VAMPIRE: complete first version of VampireModelInterpretation
43 files changed, 181 insertions, 44 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index 79296fd6..a0d8ad91 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index 7781bf9d..7f0974a6 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index 4d13e9b6..e814f9af 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index 32c4c595..acbea6c4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index 12c73d57..2b006891 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index 656552a6..4c2a01e7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index cdb80449..f712428d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index b8138e88..db6e5d42 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index 23feccda..bc9ce4bc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index 7fb53220..322bb058 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index 64554698..2bd5f5f8 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index 7a8125bb..c332270d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 2f49f152..60bd0c88 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index f762dd38..fe1d6bf2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin | |||
Binary files differ | |||
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 7ab15fba..6b383b12 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 | |||
@@ -46,6 +46,7 @@ class Logic2VampireLanguageMapperTrace { | |||
46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions | 46 | public var Map<ConstantDeclaration, ConstantDefinition> constantDefinitions |
47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions | 47 | public var Map<RelationDeclaration, RelationDefinition> relationDefinitions |
48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap | 48 | public var Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap |
49 | public var Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap | ||
49 | 50 | ||
50 | 51 | ||
51 | //NOT NEEDED //public var VLSFunction constantDec | 52 | //NOT NEEDED //public var VLSFunction constantDec |
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 2dec281d..18e97020 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 | |||
@@ -71,6 +71,7 @@ class Logic2VampireLanguageMapper_RelationMapper { | |||
71 | } | 71 | } |
72 | ] | 72 | ] |
73 | trace.rel2Predicate.put(r, rel) | 73 | trace.rel2Predicate.put(r, rel) |
74 | trace.predicate2Relation.put(rel, r) | ||
74 | it.left = support.duplicate(rel) | 75 | it.left = support.duplicate(rel) |
75 | it.right = support.unfoldAnd(relVar2TypeDecComply) | 76 | it.right = support.unfoldAnd(relVar2TypeDecComply) |
76 | ] | 77 | ] |
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 0c93e3fe..5df47bbc 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 | |||
@@ -22,22 +22,27 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | |||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration |
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | 24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition |
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.RelationDeclarationImpl | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl | 26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDeclarationImpl |
27 | import java.util.Arrays | ||
26 | import java.util.HashMap | 28 | import java.util.HashMap |
27 | import java.util.List | 29 | import java.util.List |
28 | import java.util.Map | 30 | import java.util.Map |
31 | import java.util.Set | ||
29 | 32 | ||
30 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 33 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
34 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.impl.TypeDefinitionImpl | ||
31 | 35 | ||
32 | class VampireModelInterpretation implements LogicModelInterpretation { | 36 | class VampireModelInterpretation implements LogicModelInterpretation { |
33 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | 37 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE |
34 | 38 | ||
35 | protected val Logic2VampireLanguageMapperTrace forwardTrace; | 39 | protected val Logic2VampireLanguageMapperTrace forwardTrace; |
36 | 40 | ||
41 | //These three maps capture all the information found in the Vampire output | ||
37 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap | 42 | private val Map<String, DefinedElement> name2DefinedElement = new HashMap |
38 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap | 43 | private val Map<TypeDeclaration, List<DefinedElement>> type2DefinedElement = new HashMap |
39 | 44 | private val Map<RelationDeclaration, List<String[]>> rel2Inst = new HashMap | |
40 | var num = -1 | 45 | //end |
41 | 46 | ||
42 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { | 47 | public new(VampireModel model, Logic2VampireLanguageMapperTrace trace) { |
43 | this.forwardTrace = trace | 48 | this.forwardTrace = trace |
@@ -74,6 +79,7 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
74 | // Fill keys of map | 79 | // Fill keys of map |
75 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] | 80 | val allTypeDecls = trace.type2Predicate.keySet.filter[class == TypeDeclarationImpl] |
76 | val allTypeFunctions = trace.predicate2Type | 81 | val allTypeFunctions = trace.predicate2Type |
82 | println(trace.type2Predicate.keySet.filter[class == TypeDefinitionImpl]) | ||
77 | 83 | ||
78 | for (type : allTypeDecls) { | 84 | for (type : allTypeDecls) { |
79 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) | 85 | type2DefinedElement.put(type as TypeDeclaration, newArrayList) |
@@ -116,12 +122,56 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
116 | } | 122 | } |
117 | } | 123 | } |
118 | } | 124 | } |
119 | 125 | ||
120 | printMap() | 126 | printMap() |
127 | |||
128 | // 3. get relations | ||
129 | // Fill keys of map | ||
130 | val allRelDecls = trace.rel2Predicate.keySet.filter[class == RelationDeclarationImpl] | ||
131 | val allRelFunctions = trace.predicate2Relation | ||
132 | |||
133 | for (rel : allRelDecls) { | ||
134 | rel2Inst.put(rel as RelationDeclaration, newArrayList) | ||
135 | } | ||
136 | |||
137 | // USE THE DECLARE_<RELATION_NAME> FORMULAS TO SEE WHAT THE RELATIONS ARE | ||
138 | val relFormulas = model.tfformulas.filter[name.length > 12 && name.substring(0, 12) == "predicate_r_"] | ||
139 | |||
140 | for (formula : relFormulas) { | ||
141 | // get associated type | ||
142 | val associatedRelName = (formula as VLSTffFormula).name.substring(10) | ||
143 | val associatedRelFunction = allRelFunctions.keySet.filter[constant == associatedRelName]. | ||
144 | get(0) as VLSFunction | ||
145 | val associatedRel = associatedRelFunction.lookup(allRelFunctions) as RelationDeclaration | ||
146 | |||
147 | // get definedElements | ||
148 | var andFormulaTerm = formula.fofFormula | ||
149 | end = false | ||
150 | val List<String[]> instances = newArrayList | ||
151 | while (!end) { | ||
152 | if (andFormulaTerm.class == VLSAndImpl) { | ||
153 | val andFormula = andFormulaTerm as VLSAnd | ||
154 | val andRight = andFormula.right | ||
155 | addRelIfNotNeg(andRight, instances) | ||
156 | andFormulaTerm = andFormula.left | ||
157 | } else { | ||
158 | addRelIfNotNeg(andFormulaTerm as VLSTerm, instances) | ||
159 | end = true | ||
160 | } | ||
161 | |||
162 | } | ||
163 | for (elem : instances) { | ||
164 | associatedRel.lookup(rel2Inst).add(elem) | ||
165 | } | ||
166 | |||
167 | } | ||
168 | |||
169 | // printMap2() | ||
121 | 170 | ||
122 | } | 171 | } |
123 | 172 | ||
124 | def printMap() { | 173 | def printMap() { |
174 | println("------------------") | ||
125 | for (key : type2DefinedElement.keySet) { | 175 | for (key : type2DefinedElement.keySet) { |
126 | println(key.name + "==>") | 176 | println(key.name + "==>") |
127 | for (elem : key.lookup(type2DefinedElement)) { | 177 | for (elem : key.lookup(type2DefinedElement)) { |
@@ -132,6 +182,19 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
132 | } | 182 | } |
133 | println() | 183 | println() |
134 | } | 184 | } |
185 | |||
186 | def printMap2() { | ||
187 | println("------------------") | ||
188 | for (key : rel2Inst.keySet) { | ||
189 | println(key.name + "==>") | ||
190 | for (elem : key.lookup(rel2Inst)) { | ||
191 | print("[" + elem.get(0) + "-" + elem.get(1) + "], ") | ||
192 | } | ||
193 | println() | ||
194 | |||
195 | } | ||
196 | println() | ||
197 | } | ||
135 | 198 | ||
136 | def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) { | 199 | def private addIfNotNeg(VLSTerm term, List<DefinedElement> list) { |
137 | if (term.class != VLSUnaryNegationImpl) { | 200 | if (term.class != VLSUnaryNegationImpl) { |
@@ -140,6 +203,15 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
140 | list.add(defnElem) | 203 | list.add(defnElem) |
141 | } | 204 | } |
142 | } | 205 | } |
206 | |||
207 | def private addRelIfNotNeg(VLSTerm term, List<String[]> list) { | ||
208 | if (term.class != VLSUnaryNegationImpl) { | ||
209 | val nodeName1 = ((term as VLSFunction).terms.get(0) as VLSFunctionAsTerm).functor | ||
210 | val nodeName2 = ((term as VLSFunction).terms.get(1) as VLSFunctionAsTerm).functor | ||
211 | val strArr = newArrayList(nodeName1, nodeName2) | ||
212 | list.add(strArr) | ||
213 | } | ||
214 | } | ||
143 | 215 | ||
144 | def private add2ConstDefMap(VLSEquality eq) { | 216 | def private add2ConstDefMap(VLSEquality eq) { |
145 | val defElemConst = (eq.right as VLSConstant) | 217 | val defElemConst = (eq.right as VLSConstant) |
@@ -160,7 +232,15 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
160 | } | 232 | } |
161 | 233 | ||
162 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | 234 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { |
163 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | 235 | val node1 = (parameterSubstitution.get(0) as DefinedElement).name |
236 | val node2 = (parameterSubstitution.get(1) as DefinedElement).name | ||
237 | val realRelations = relation.lookup(rel2Inst) | ||
238 | for (real : realRelations){ | ||
239 | if(real.contains(node1) && real.contains(node2)){ | ||
240 | return true | ||
241 | } | ||
242 | } | ||
243 | return false | ||
164 | } | 244 | } |
165 | 245 | ||
166 | override getInterpretation(ConstantDeclaration constant) { | 246 | override getInterpretation(ConstantDeclaration constant) { |
@@ -180,3 +260,26 @@ class VampireModelInterpretation implements LogicModelInterpretation { | |||
180 | } | 260 | } |
181 | 261 | ||
182 | } | 262 | } |
263 | |||
264 | /** | ||
265 | * Helper class for efficiently matching parameter substitutions for functions and relations. | ||
266 | */ | ||
267 | class ParameterSubstitution { | ||
268 | val Object[] data; | ||
269 | |||
270 | new(Object[] data) { | ||
271 | this.data = data | ||
272 | } | ||
273 | |||
274 | override equals(Object obj) { | ||
275 | if(obj === this) return true else if(obj == null) return false | ||
276 | if (obj instanceof ParameterSubstitution) { | ||
277 | return Arrays.equals(this.data, obj.data) | ||
278 | } | ||
279 | return false | ||
280 | } | ||
281 | |||
282 | override hashCode() { | ||
283 | Arrays.hashCode(data) | ||
284 | } | ||
285 | } | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index 499504af..a1d6f783 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin | |||
Binary files differ | |||
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 0fafa9e9..6ac0457b 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 7174bfba..f5991439 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 af66dabc..0d6c8b61 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 b9301875..659d4637 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 88c3e932..927327e1 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 e3437e53..d8fc0296 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 1a884261..bc3caa3b 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 7e2aba1c..299c4e0c 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 187a0447..da8c1d26 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/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index ee115b16..adc3fff4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 319f863c..2ab5b32f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.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/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index 3b6009bb..41af19ec 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index d8329084..2b46d5c2 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapperTrace.java index 4537240e..4e77d45d 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 | |||
@@ -53,6 +53,8 @@ public class Logic2VampireLanguageMapperTrace { | |||
53 | 53 | ||
54 | public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>(); | 54 | public Map<RelationDeclaration, VLSFunction> rel2Predicate = new HashMap<RelationDeclaration, VLSFunction>(); |
55 | 55 | ||
56 | public Map<VLSFunction, RelationDeclaration> predicate2Relation = new HashMap<VLSFunction, RelationDeclaration>(); | ||
57 | |||
56 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); | 58 | public final Map<Variable, VLSVariable> relationVar2VLS = new HashMap<Variable, VLSVariable>(); |
57 | 59 | ||
58 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); | 60 | public final Map<Variable, VLSFunction> relationVar2TypeDec = new HashMap<Variable, VLSFunction>(); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java index 8d36952b..143d3db5 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_RelationMapper.java | |||
@@ -94,6 +94,7 @@ public class Logic2VampireLanguageMapper_RelationMapper { | |||
94 | }; | 94 | }; |
95 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); | 95 | final VLSFunction rel = ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function_3); |
96 | trace.rel2Predicate.put(r, rel); | 96 | trace.rel2Predicate.put(r, rel); |
97 | trace.predicate2Relation.put(rel, r); | ||
97 | it_2.setLeft(this.support.duplicate(rel)); | 98 | it_2.setLeft(this.support.duplicate(rel)); |
98 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); | 99 | it_2.setRight(this.support.unfoldAnd(relVar2TypeDecComply)); |
99 | }; | 100 | }; |
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 4efbc821..1045189c 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 | |||
@@ -2,7 +2,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.icse | |||
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.VampireModelInterpretation | ||
6 | import functionalarchitecture.Function | 5 | import functionalarchitecture.Function |
7 | import functionalarchitecture.FunctionalArchitectureModel | 6 | import functionalarchitecture.FunctionalArchitectureModel |
8 | import functionalarchitecture.FunctionalInterface | 7 | import functionalarchitecture.FunctionalInterface |
@@ -16,18 +15,22 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | |||
16 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore | 15 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore |
17 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic | 16 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic | 17 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic |
18 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation | ||
19 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation | ||
20 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml | ||
21 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser | ||
19 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace | 22 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace |
20 | import java.util.HashMap | 23 | import java.util.HashMap |
21 | import java.util.List | ||
22 | import org.eclipse.emf.ecore.resource.Resource | 24 | import org.eclipse.emf.ecore.resource.Resource |
23 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl | 25 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl |
24 | 26 | ||
25 | class FAMTest { | 27 | class FAMTest { |
26 | def static void main(String[] args) { | 28 | def static void main(String[] args) { |
27 | val Ecore2Logic ecore2Logic = new Ecore2Logic | 29 | val Ecore2Logic ecore2Logic = new Ecore2Logic |
28 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) | 30 | val Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic) |
29 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) | 31 | val Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic) |
30 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic | 32 | val InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic |
33 | val InstanceModel2PartialInterpretation im2pi = new InstanceModel2PartialInterpretation | ||
31 | 34 | ||
32 | // Workspace setup | 35 | // Workspace setup |
33 | val inputs = new FileSystemWorkspace('''initialModels/''', "") | 36 | val inputs = new FileSystemWorkspace('''initialModels/''', "") |
@@ -56,8 +59,8 @@ class FAMTest { | |||
56 | workspace.writeModel(problem, "Fam.logicproblem") | 59 | workspace.writeModel(problem, "Fam.logicproblem") |
57 | 60 | ||
58 | println("Problem created") | 61 | println("Problem created") |
59 | 62 | ||
60 | //Start Time | 63 | // Start Time |
61 | var startTime = System.currentTimeMillis | 64 | var startTime = System.currentTimeMillis |
62 | 65 | ||
63 | var VampireSolver reasoner | 66 | var VampireSolver reasoner |
@@ -71,16 +74,16 @@ class FAMTest { | |||
71 | // classMapMin.put(Function, 1) | 74 | // classMapMin.put(Function, 1) |
72 | // classMapMin.put(FunctionalInterface, 2) | 75 | // classMapMin.put(FunctionalInterface, 2) |
73 | classMapMin.put(FunctionalOutput, 3) | 76 | classMapMin.put(FunctionalOutput, 3) |
74 | 77 | ||
75 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) | 78 | val typeMapMin = GeneralTest.getTypeMap(classMapMin, metamodel, ecore2Logic, modelGenerationProblem.trace) |
76 | 79 | ||
77 | // Maximum Scope | 80 | // Maximum Scope |
78 | val classMapMax = new HashMap<Class, Integer> | 81 | val classMapMax = new HashMap<Class, Integer> |
79 | classMapMax.put(FunctionalArchitectureModel, 3) | 82 | classMapMax.put(FunctionalArchitectureModel, 3) |
80 | classMapMax.put(Function, 5) | 83 | classMapMax.put(Function, 5) |
81 | classMapMax.put(FunctionalInterface, 3) | 84 | classMapMax.put(FunctionalInterface, 3) |
82 | classMapMax.put(FunctionalOutput, 4) | 85 | classMapMax.put(FunctionalOutput, 4) |
83 | 86 | ||
84 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) | 87 | val typeMapMax = GeneralTest.getTypeMap(classMapMax, metamodel, ecore2Logic, modelGenerationProblem.trace) |
85 | 88 | ||
86 | // Define Config File | 89 | // Define Config File |
@@ -88,27 +91,43 @@ class FAMTest { | |||
88 | // add configuration things, in config file first | 91 | // add configuration things, in config file first |
89 | it.documentationLevel = DocumentationLevel::FULL | 92 | it.documentationLevel = DocumentationLevel::FULL |
90 | 93 | ||
91 | it.typeScopes.minNewElements = 24 | 94 | it.typeScopes.minNewElements = 4//24 |
92 | it.typeScopes.maxNewElements = 25 | 95 | it.typeScopes.maxNewElements = 5//25 |
93 | if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin | 96 | // if(typeMapMin.size != 0) it.typeScopes.minNewElementsByType = typeMapMin |
94 | if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax | 97 | // if(typeMapMin.size != 0) it.typeScopes.maxNewElementsByType = typeMapMax |
95 | it.contCycleLevel = 5 | 98 | it.contCycleLevel = 5 |
96 | it.uniquenessDuplicates = false | 99 | it.uniquenessDuplicates = false |
97 | ] | 100 | ] |
98 | 101 | ||
99 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) | 102 | var LogicResult solution = reasoner.solve(problem, vampireConfig, workspace) |
100 | |||
101 | //visualisation, see | ||
102 | var interpretations = reasoner.getInterpretations(solution as ModelResult) | ||
103 | interpretations.get(0) as VampireModelInterpretation | ||
104 | println(ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)) | ||
105 | |||
106 | // for(interpretation : interpretations) { | ||
107 | // val model = logic2Ecore.transformInterpretation(interpretation,modelGenerationProblem.trace) | ||
108 | // //look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor | ||
109 | // } | ||
110 | //transform interpretation to ecore, and it is easy from there | ||
111 | 103 | ||
104 | // visualisation, see | ||
105 | var interpretations = reasoner.getInterpretations(solution as ModelResult) | ||
106 | // interpretations.get(0) as VampireModelInterpretation | ||
107 | // println(ecore2Logic.IsAttributeValue(modelGenerationProblem.trace, ) | ||
108 | // Literal(modelGenerationProblem.trace, ecore2Logic.allLiteralsInScope(modelGenerationProblem.trace).get(0) ) | ||
109 | // ) | ||
110 | // println((ecore2Logic.allAttributesInScope(modelGenerationProblem.trace)).get(0).EAttributeType) | ||
111 | for (interpretation : interpretations) { | ||
112 | val model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.trace) | ||
113 | workspace.writeModel(model, "model.xmi") | ||
114 | |||
115 | val representation = im2pi.transform(modelGenerationProblem, model.eAllContents.toList, false)//solution.representation.get(0) // TODO: fix for multiple represenations | ||
116 | if (representation instanceof PartialInterpretation) { | ||
117 | val vis1 = new PartialInterpretation2Gml | ||
118 | val gml = vis1.transform(representation) | ||
119 | workspace.writeText("model.gml", gml) | ||
120 | |||
121 | val vis2 = new GraphvizVisualiser | ||
122 | val dot = vis2.visualiseConcretization(representation) | ||
123 | dot.writeToFile(workspace, "model.png") | ||
124 | } else { | ||
125 | println("ERROR") | ||
126 | } | ||
127 | // look here: hu.bme.mit.inf.dslreasoner.application.execution.GenerationTaskExecutor | ||
128 | } | ||
129 | |||
130 | // transform interpretation to ecore, and it is easy from there | ||
112 | /*/ | 131 | /*/ |
113 | * | 132 | * |
114 | * reasoner = new AlloySolver | 133 | * reasoner = new AlloySolver |
@@ -121,8 +140,7 @@ class FAMTest { | |||
121 | * ] | 140 | * ] |
122 | * solution = reasoner.solve(problem, alloyConfig, workspace) | 141 | * solution = reasoner.solve(problem, alloyConfig, workspace) |
123 | //*/ | 142 | //*/ |
124 | // ///////////////////////////////////////////////////// | 143 | // ///////////////////////////////////////////////////// |
125 | |||
126 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 | 144 | var totalTimeMin = (System.currentTimeMillis - startTime) / 60000 |
127 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 | 145 | var totalTimeSec = ((System.currentTimeMillis - startTime) / 1000) % 60 |
128 | 146 | ||
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 9033512f..771e1d1a 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 18295021..ad844992 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 eb8d5506..7dcb4392 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 1023ad44..dc040005 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 c996fa4f..2bb8be0d 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 71f522de..8ef096d9 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 | |||
@@ -21,18 +21,23 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult; | |||
21 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; | 21 | import hu.bme.mit.inf.dslreasoner.logic2ecore.Logic2Ecore; |
22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; | 22 | import hu.bme.mit.inf.dslreasoner.viatra2logic.Viatra2Logic; |
23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; | 23 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2Logic; |
24 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretation2logic.InstanceModel2PartialInterpretation; | ||
25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PartialInterpretation; | ||
26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretation2Gml; | ||
27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.visualisation.PartialInterpretationVisualisation; | ||
28 | import hu.bme.mit.inf.dslreasoner.visualisation.pi2graphviz.GraphvizVisualiser; | ||
24 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | 29 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; |
25 | import java.util.HashMap; | 30 | import java.util.HashMap; |
26 | import java.util.List; | 31 | import java.util.List; |
27 | import java.util.Map; | 32 | import java.util.Map; |
28 | import org.eclipse.emf.common.util.EList; | 33 | import org.eclipse.emf.common.util.EList; |
29 | import org.eclipse.emf.ecore.EAttribute; | ||
30 | import org.eclipse.emf.ecore.EObject; | 34 | import org.eclipse.emf.ecore.EObject; |
31 | import org.eclipse.emf.ecore.resource.Resource; | 35 | import org.eclipse.emf.ecore.resource.Resource; |
32 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | 36 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; |
33 | import org.eclipse.xtend2.lib.StringConcatenation; | 37 | import org.eclipse.xtend2.lib.StringConcatenation; |
34 | import org.eclipse.xtext.xbase.lib.Exceptions; | 38 | import org.eclipse.xtext.xbase.lib.Exceptions; |
35 | import org.eclipse.xtext.xbase.lib.InputOutput; | 39 | import org.eclipse.xtext.xbase.lib.InputOutput; |
40 | import org.eclipse.xtext.xbase.lib.IteratorExtensions; | ||
36 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | 41 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; |
37 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | 42 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; |
38 | 43 | ||
@@ -44,6 +49,7 @@ public class FAMTest { | |||
44 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); | 49 | final Logic2Ecore logic2Ecore = new Logic2Ecore(ecore2Logic); |
45 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); | 50 | final Viatra2Logic viatra2Logic = new Viatra2Logic(ecore2Logic); |
46 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); | 51 | final InstanceModel2Logic instanceModel2Logic = new InstanceModel2Logic(); |
52 | final InstanceModel2PartialInterpretation im2pi = new InstanceModel2PartialInterpretation(); | ||
47 | StringConcatenation _builder = new StringConcatenation(); | 53 | StringConcatenation _builder = new StringConcatenation(); |
48 | _builder.append("initialModels/"); | 54 | _builder.append("initialModels/"); |
49 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); | 55 | final FileSystemWorkspace inputs = new FileSystemWorkspace(_builder.toString(), ""); |
@@ -82,26 +88,31 @@ public class FAMTest { | |||
82 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | 88 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); |
83 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | 89 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { |
84 | it.documentationLevel = DocumentationLevel.FULL; | 90 | it.documentationLevel = DocumentationLevel.FULL; |
85 | it.typeScopes.minNewElements = 24; | 91 | it.typeScopes.minNewElements = 4; |
86 | it.typeScopes.maxNewElements = 25; | 92 | it.typeScopes.maxNewElements = 5; |
87 | int _size = typeMapMin.size(); | ||
88 | boolean _notEquals = (_size != 0); | ||
89 | if (_notEquals) { | ||
90 | it.typeScopes.minNewElementsByType = typeMapMin; | ||
91 | } | ||
92 | int _size_1 = typeMapMin.size(); | ||
93 | boolean _notEquals_1 = (_size_1 != 0); | ||
94 | if (_notEquals_1) { | ||
95 | it.typeScopes.maxNewElementsByType = typeMapMax; | ||
96 | } | ||
97 | it.contCycleLevel = 5; | 93 | it.contCycleLevel = 5; |
98 | it.uniquenessDuplicates = false; | 94 | it.uniquenessDuplicates = false; |
99 | }; | 95 | }; |
100 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | 96 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); |
101 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); | 97 | LogicResult solution = reasoner.solve(problem, vampireConfig, workspace); |
102 | List<? extends LogicModelInterpretation> interpretations = reasoner.getInterpretations(((ModelResult) solution)); | 98 | List<? extends LogicModelInterpretation> interpretations = reasoner.getInterpretations(((ModelResult) solution)); |
103 | interpretations.get(0); | 99 | for (final LogicModelInterpretation interpretation : interpretations) { |
104 | InputOutput.<Iterable<EAttribute>>println(ecore2Logic.allAttributesInScope(modelGenerationProblem.getTrace())); | 100 | { |
101 | final EObject model = logic2Ecore.transformInterpretation(interpretation, modelGenerationProblem.getTrace()); | ||
102 | workspace.writeModel(model, "model.xmi"); | ||
103 | final PartialInterpretation representation = im2pi.transform(modelGenerationProblem, IteratorExtensions.<EObject>toList(model.eAllContents()), false); | ||
104 | if ((representation instanceof PartialInterpretation)) { | ||
105 | final PartialInterpretation2Gml vis1 = new PartialInterpretation2Gml(); | ||
106 | final String gml = vis1.transform(representation); | ||
107 | workspace.writeText("model.gml", gml); | ||
108 | final GraphvizVisualiser vis2 = new GraphvizVisualiser(); | ||
109 | final PartialInterpretationVisualisation dot = vis2.visualiseConcretization(representation); | ||
110 | dot.writeToFile(workspace, "model.png"); | ||
111 | } else { | ||
112 | InputOutput.<String>println("ERROR"); | ||
113 | } | ||
114 | } | ||
115 | } | ||
105 | long _currentTimeMillis = System.currentTimeMillis(); | 116 | long _currentTimeMillis = System.currentTimeMillis(); |
106 | long _minus = (_currentTimeMillis - startTime); | 117 | long _minus = (_currentTimeMillis - startTime); |
107 | long totalTimeMin = (_minus / 60000); | 118 | long totalTimeMin = (_minus / 60000); |
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 796f7103..7ab6b54b 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 a2cecacf..f7c267ec 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 c1a25e40..e91e816f 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 | |||