diff options
author | 2019-04-16 10:32:11 +0200 | |
---|---|---|
committer | 2019-04-16 10:32:11 +0200 | |
commit | 416e0352d2b4a97c978b166c076d540fe9af40bc (patch) | |
tree | ece50271862fd3260e9c29c098cc8858729fc78a | |
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
3 files changed, 11 insertions, 5 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF index 1fda4212..8fa4517d 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF | |||
@@ -17,7 +17,8 @@ Require-Bundle: com.google.guava, | |||
17 | org.eclipse.emf.ecore;visibility:=reexport, | 17 | org.eclipse.emf.ecore;visibility:=reexport, |
18 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, | 18 | hu.bme.mit.inf.dslreasoner.logic.model;bundle-version="1.0.0";visibility:=reexport, |
19 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", | 19 | org.eclipse.viatra.query.runtime.base.itc;bundle-version="1.5.0", |
20 | org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0" | 20 | org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0", |
21 | org.eclipse.xtext | ||
21 | Bundle-ActivationPolicy: lazy | 22 | Bundle-ActivationPolicy: lazy |
22 | Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic, | 23 | Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic, |
23 | hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations, | 24 | hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations, |
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 | ||