diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src')
7 files changed, 151 insertions, 11 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend new file mode 100644 index 00000000..f7603cf9 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation.xtend | |||
@@ -0,0 +1,21 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
6 | import java.util.Map | ||
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.List | ||
11 | |||
12 | interface AlloyModelInterpretation_TypeInterpretation { | ||
13 | def void resolveUnknownAtoms( | ||
14 | Iterable<ExprVar> objectAtoms, | ||
15 | A4Solution solution, | ||
16 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
17 | Map<String, Sig> name2AlloySig, | ||
18 | Map<String, Field> name2AlloyField, | ||
19 | Map<String,DefinedElement> expression2DefinedElement, | ||
20 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
21 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend new file mode 100644 index 00000000..934a863a --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_FilteredTypes.xtend | |||
@@ -0,0 +1,72 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
5 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
6 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.ArrayList | ||
11 | import java.util.List | ||
12 | import java.util.Map | ||
13 | |||
14 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
15 | |||
16 | class AlloyModelInterpretation_TypeInterpretation_FilteredTypes implements AlloyModelInterpretation_TypeInterpretation{ | ||
17 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
18 | |||
19 | override resolveUnknownAtoms( | ||
20 | Iterable<ExprVar> objectAtoms, | ||
21 | A4Solution solution, | ||
22 | Logic2AlloyLanguageMapperTrace forwardTrace, | ||
23 | Map<String, Sig> name2AlloySig, | ||
24 | Map<String, Field> name2AlloyField, | ||
25 | Map<String,DefinedElement> expression2DefinedElement, | ||
26 | Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) | ||
27 | { | ||
28 | /*val Map<String,DefinedElement> expression2DefinedElement = new HashMap() | ||
29 | val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap;*/ | ||
30 | |||
31 | val typeTrace = forwardTrace.typeMapperTrace as Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
32 | |||
33 | // 1. Evaluate the defined elements | ||
34 | for(definedElementMappingEntry : typeTrace.definedElement2Declaration.entrySet) { | ||
35 | val name = definedElementMappingEntry.value.name | ||
36 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
37 | val elementsOfSingletonSignature = solution.eval(matchingSig) | ||
38 | if(elementsOfSingletonSignature.size != 1) { | ||
39 | throw new IllegalArgumentException('''Defined element is unambigous: "«name»", possible values: «elementsOfSingletonSignature»!''') | ||
40 | } else { | ||
41 | val expressionOfDefinedElement = elementsOfSingletonSignature.head.atom(0)// as ExprVar | ||
42 | expression2DefinedElement.put(expressionOfDefinedElement, definedElementMappingEntry.key) | ||
43 | } | ||
44 | } | ||
45 | |||
46 | // 2. evaluate the signatures and create new elements if necessary | ||
47 | for(type2SingatureEntry : typeTrace.type2ALSType.entrySet) { | ||
48 | val type = type2SingatureEntry.key | ||
49 | if(type instanceof TypeDeclaration) { | ||
50 | val name = type2SingatureEntry.value.name | ||
51 | val matchingSig = '''this/«name»'''.toString.lookup(name2AlloySig) | ||
52 | val elementsOfSignature = solution.eval(matchingSig) | ||
53 | val elementList = new ArrayList(elementsOfSignature.size) | ||
54 | var newVariableIndex = 1; | ||
55 | for(elementOfSignature : elementsOfSignature) { | ||
56 | val expressionOfDefinedElement = elementOfSignature.atom(0) | ||
57 | if(expression2DefinedElement.containsKey(expressionOfDefinedElement)) { | ||
58 | elementList += expressionOfDefinedElement.lookup(expression2DefinedElement) | ||
59 | } else { | ||
60 | val newElementName = '''newObject «newVariableIndex.toString»''' | ||
61 | val newRepresentation = createDefinedElement => [ | ||
62 | it.name = newElementName | ||
63 | ] | ||
64 | elementList += newRepresentation | ||
65 | expression2DefinedElement.put(expressionOfDefinedElement,newRepresentation) | ||
66 | } | ||
67 | } | ||
68 | interpretationOfUndefinedType.put(type,elementList) | ||
69 | } | ||
70 | } | ||
71 | } | ||
72 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..8019c6b5 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,20 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar | ||
4 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
5 | import java.util.Map | ||
6 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig | ||
7 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.Field | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
10 | import java.util.List | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
12 | |||
13 | class AlloyModelInterpretation_TypeInterpretation_InheritanceAndHorizontal implements AlloyModelInterpretation_TypeInterpretation{ | ||
14 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
15 | |||
16 | override resolveUnknownAtoms(Iterable<ExprVar> objectAtoms, A4Solution solution, Logic2AlloyLanguageMapperTrace forwardTrace, Map<String, Sig> name2AlloySig, Map<String, Field> name2AlloyField, Map<String, DefinedElement> expression2DefinedElement, Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType) { | ||
17 | throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
18 | } | ||
19 | |||
20 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend index d6c62f54..ee7c092a 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper.xtend | |||
@@ -1,6 +1,7 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | 1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder |
2 | 2 | ||
3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration | 3 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.AlloySolverConfiguration |
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | ||
4 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument | 5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDocument |
5 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral | 6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSEnumLiteral |
6 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity | 7 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSMultiplicity |
@@ -8,6 +9,9 @@ import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSNumericOperator | |||
8 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm | 9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSTerm |
9 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration | 10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSVariableDeclaration |
10 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory | 11 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.AlloyLanguageFactory |
12 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
13 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
14 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | 15 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration |
12 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | 16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput |
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And |
@@ -46,8 +50,12 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | |||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
47 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | 51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue |
48 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | 52 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term |
53 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | ||
49 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | 54 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable |
55 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation | ||
56 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | 57 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem |
58 | import java.util.Collection | ||
51 | import java.util.Collections | 59 | import java.util.Collections |
52 | import java.util.HashMap | 60 | import java.util.HashMap |
53 | import java.util.List | 61 | import java.util.List |
@@ -57,15 +65,6 @@ import org.eclipse.viatra.query.runtime.emf.EMFScope | |||
57 | import org.eclipse.xtend.lib.annotations.Accessors | 65 | import org.eclipse.xtend.lib.annotations.Accessors |
58 | 66 | ||
59 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 67 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
60 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.Annotation | ||
61 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.InverseRelationAssertion | ||
62 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.AssertionAnnotation | ||
63 | import java.util.Collection | ||
64 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.LowerMultiplicityAssertion | ||
65 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.UpperMultiplicityAssertion | ||
66 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSDirectProduct | ||
67 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TransitiveClosure | ||
68 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
69 | 68 | ||
70 | class Logic2AlloyLanguageMapper { | 69 | class Logic2AlloyLanguageMapper { |
71 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE | 70 | private val extension AlloyLanguageFactory factory = AlloyLanguageFactory.eINSTANCE |
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend new file mode 100644 index 00000000..8cdb7769 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.HashMap | ||
7 | import java.util.Map | ||
8 | |||
9 | class Logic2AlloyLanguageMapper_TypeMapperTrace_FilteredTypes | ||
10 | implements Logic2AlloyLanguageMapper_TypeMapperTrace | ||
11 | { | ||
12 | public var ALSSignatureDeclaration objectSupperClass; | ||
13 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
14 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
15 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend new file mode 100644 index 00000000..8377aca4 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal.xtend | |||
@@ -0,0 +1,15 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.alloyLanguage.ALSSignatureDeclaration | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import java.util.HashMap | ||
7 | import java.util.List | ||
8 | import java.util.Map | ||
9 | |||
10 | class Logic2AlloyLanguageMapper_TypeMapperTrace_InheritanceAndHorizontal implements Logic2AlloyLanguageMapper_TypeMapperTrace { | ||
11 | public var ALSSignatureDeclaration objectSupperClass; | ||
12 | public val Map<Type, ALSSignatureDeclaration> type2ALSType = new HashMap; | ||
13 | public val Map<DefinedElement, ALSSignatureDeclaration> definedElement2Declaration = new HashMap | ||
14 | public val Map<Type, List<ALSSignatureDeclaration>> typeSelection = new HashMap | ||
15 | } | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend index 3b2e3390..397fb84b 100644 --- a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/src/hu/bme/mit/inf/dlsreasoner/alloy/reasoner/builder/Logic2AlloyLanguageMapper_TypeMapper_FilteredTypes.xtend | |||
@@ -14,11 +14,9 @@ import java.util.ArrayList | |||
14 | import java.util.Collection | 14 | import java.util.Collection |
15 | import java.util.HashMap | 15 | import java.util.HashMap |
16 | import java.util.List | 16 | import java.util.List |
17 | import java.util.Map | ||
18 | 17 | ||
19 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
20 | 19 | ||
21 | |||
22 | /** | 20 | /** |
23 | * Each object is an element of an Object set, and types are subsets of the objects. | 21 | * Each object is an element of an Object set, and types are subsets of the objects. |
24 | */ | 22 | */ |