diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-04-16 10:32:11 +0200 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-04-16 10:32:11 +0200 |
commit | 416e0352d2b4a97c978b166c076d540fe9af40bc (patch) | |
tree | ece50271862fd3260e9c29c098cc8858729fc78a /Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu | |
parent | Satellite constellation case study WIP (diff) | |
parent | Fixed misformalization of (may/must)(X!=Y) for abstract objects (diff) | |
download | VIATRA-Generator-416e0352d2b4a97c978b166c076d540fe9af40bc.tar.gz VIATRA-Generator-416e0352d2b4a97c978b166c076d540fe9af40bc.tar.zst VIATRA-Generator-416e0352d2b4a97c978b166c076d540fe9af40bc.zip |
Merge remote-tracking branch 'origin/master' into kris
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu')
2 files changed, 9 insertions, 4 deletions
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend index c9e64a9d..24b3e870 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/PatternGenerator.xtend | |||
@@ -203,6 +203,11 @@ class PatternGenerator { | |||
203 | find mayExist(problem,interpretation,b); | 203 | find mayExist(problem,interpretation,b); |
204 | a == b; | 204 | a == b; |
205 | } | 205 | } |
206 | pattern mustEquivalent(problem:LogicProblem, interpretation:PartialInterpretation, a: DefinedElement, b: DefinedElement) { | ||
207 | find mustExist(problem,interpretation,a); | ||
208 | find mustExist(problem,interpretation,b); | ||
209 | a == b; | ||
210 | } | ||
206 | 211 | ||
207 | //////////////////////// | 212 | //////////////////////// |
208 | // 0.3 Required Patterns by TypeIndexer | 213 | // 0.3 Required Patterns by TypeIndexer |
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend index a67a24c4..cedcec5a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/patterns/RelationDefinitionIndexer.xtend | |||
@@ -179,7 +179,7 @@ class RelationDefinitionIndexer { | |||
179 | } | 179 | } |
180 | 180 | ||
181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { | 181 | private def CharSequence transformEquality(Modality modality, PVariable a, PVariable b) { |
182 | if(modality.isMustOrCurrent) '''«a.canonizeName» == «b.canonizeName»;''' | 182 | if(modality.isMustOrCurrent) '''find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | 183 | else '''find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
184 | } | 184 | } |
185 | 185 | ||
@@ -187,11 +187,11 @@ class RelationDefinitionIndexer { | |||
187 | val a = inequality.who | 187 | val a = inequality.who |
188 | val b = inequality.withWhom | 188 | val b = inequality.withWhom |
189 | if(modality.isCurrent) { | 189 | if(modality.isCurrent) { |
190 | return '''«a.canonizeName» != «b.canonizeName»;''' | 190 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
191 | } else if(modality.isMust) { | 191 | } else if(modality.isMust) { |
192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' | 192 | return '''neg find mayEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
193 | } else { | 193 | } else { // modality.isMay |
194 | return '''«a.canonizeName» != «b.canonizeName»;''' | 194 | return '''neg find mustEquivalent(problem, interpretation, «a.canonizeName», «b.canonizeName»);''' |
195 | } | 195 | } |
196 | } | 196 | } |
197 | 197 | ||