diff options
Diffstat (limited to 'Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused')
4 files changed, 671 insertions, 0 deletions
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ new file mode 100644 index 00000000..05b97b0c --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/AlloyModelInterpretation.xtend_ | |||
@@ -0,0 +1,212 @@ | |||
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.Field | ||
5 | import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicModelInterpretation | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDeclaration | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LogiclanguageFactory | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
15 | import java.util.Arrays | ||
16 | import java.util.HashMap | ||
17 | import java.util.LinkedList | ||
18 | import java.util.List | ||
19 | import java.util.Map | ||
20 | import java.util.Set | ||
21 | |||
22 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | ||
23 | |||
24 | class AlloyModelInterpretation implements LogicModelInterpretation{ | ||
25 | |||
26 | protected val extension LogiclanguageFactory factory = LogiclanguageFactory.eINSTANCE | ||
27 | //protected val extension LogicProblemBuilder builder = new LogicProblemBuilder | ||
28 | |||
29 | protected val Logic2AlloyLanguageMapper forwardMapper | ||
30 | protected val Logic2AlloyLanguageMapperTrace forwardTrace; | ||
31 | |||
32 | private var ExprVar logicLanguage; | ||
33 | private var String logicBooleanTrue; | ||
34 | private var String logicBooleanFalse; | ||
35 | |||
36 | val Map<String,DefinedElement> alloyAtom2LogicElement = new HashMap | ||
37 | private val Map<TypeDeclaration, List<DefinedElement>> interpretationOfUndefinedType = new HashMap | ||
38 | |||
39 | private val Map<ConstantDeclaration, Object> constant2Value | ||
40 | private val Map<FunctionDeclaration, ? extends Map<ParameterSubstitution, Object>> function2Value | ||
41 | private val Map<RelationDeclaration, ? extends Set<ParameterSubstitution>> relation2Value | ||
42 | |||
43 | private val int minInt | ||
44 | private val int maxInt | ||
45 | |||
46 | public new (A4Solution solution, Logic2AlloyLanguageMapper forwardMapper, Logic2AlloyLanguageMapperTrace trace) { | ||
47 | |||
48 | this.forwardMapper = forwardMapper | ||
49 | this.forwardTrace = trace | ||
50 | |||
51 | //TMP sig maps to identify alloy signatures by their names | ||
52 | val Map<String,Type> sigName2LogicType = | ||
53 | forwardTrace.type2ALSType.keySet.toMap[x|forwardTrace.type2ALSType.get(x).name] | ||
54 | val Map<String,DefinedElement> elementNameNamel2DefinedElement = | ||
55 | forwardTrace.definedElement2Declaration.keySet.toMap[x|forwardTrace.definedElement2Declaration.get(x).name] | ||
56 | |||
57 | // Fill the interpretation map with empty lists | ||
58 | forwardTrace.type2ALSType.keySet.filter(TypeDeclaration).forEach[x|interpretationOfUndefinedType.put(x,new LinkedList)] | ||
59 | |||
60 | // exporing individuals | ||
61 | for(atom: solution.allAtoms) { | ||
62 | val typeName = getName(atom.type) | ||
63 | val atomName = atom.name | ||
64 | //println(atom.toString + " < - " + typeName) | ||
65 | if(typeName == forwardTrace.logicLanguage.name) { | ||
66 | this.logicLanguage = atom | ||
67 | } else if(typeName == "Int" || typeName == "seq/Int") { | ||
68 | // do nothing | ||
69 | } else if(sigName2LogicType.containsKey(typeName) && typeName.lookup(sigName2LogicType) instanceof TypeDefinition) { | ||
70 | val element = elementNameNamel2DefinedElement.get(atomName.head) | ||
71 | alloyAtom2LogicElement.put(atom.label,element) | ||
72 | } else if(sigName2LogicType.containsKey(typeName)) { | ||
73 | val type = sigName2LogicType.get(typeName) | ||
74 | val elementsOfType = interpretationOfUndefinedType.get(type) | ||
75 | val element = createDefinedElement => [ | ||
76 | it.name += type.name | ||
77 | it.name += (elementsOfType.size+1).toString | ||
78 | ] | ||
79 | alloyAtom2LogicElement.put(atom.label,element) | ||
80 | elementsOfType+=element | ||
81 | } else if(forwardTrace.boolType != null && typeName == forwardTrace.boolType.name) { | ||
82 | if(atomName.head == forwardTrace.boolTrue.name) { this.logicBooleanTrue = atom.label } | ||
83 | else if(atomName.head == forwardTrace.boolFalse.name) { this.logicBooleanFalse = atom.label} | ||
84 | else throw new UnsupportedOperationException('''Unknown boolean value: «atom»''') | ||
85 | } | ||
86 | else throw new UnsupportedOperationException('''Unknown atom: «atom»''') | ||
87 | } | ||
88 | |||
89 | //TMP field maps | ||
90 | val Map<String, Field> name2AlloyField = new HashMap | ||
91 | // exploring signatures | ||
92 | for(sig:solution.allReachableSigs) { | ||
93 | for(field : sig.fields) { | ||
94 | name2AlloyField.put(field.label,field) | ||
95 | } | ||
96 | } | ||
97 | |||
98 | // eval consants | ||
99 | constant2Value = forwardTrace.constantDeclaration2LanguageField.mapValues[ | ||
100 | solution.eval(it.name.lookup(name2AlloyField)).head.atom(1).atomLabel2Term | ||
101 | ] | ||
102 | // eval functions | ||
103 | val hostedfunction2Value = forwardTrace.functionDeclaration2HostedField.mapValues[ function | | ||
104 | newHashMap( | ||
105 | solution.eval(function.name.lookup(name2AlloyField)) | ||
106 | .map[t | new ParameterSubstitution(#[t.atom(0).atomLabel2Term]) -> t.atom(1).atomLabel2Term])] | ||
107 | |||
108 | val globalfunction2Value = forwardTrace.functionDeclaration2LanguageField.keySet.toInvertedMap[ function | | ||
109 | val alsFunction = function.lookup(forwardTrace.functionDeclaration2LanguageField) | ||
110 | val paramIndexes = 1..(function.parameters.size) | ||
111 | return newHashMap( | ||
112 | solution.eval(alsFunction.name.lookup(name2AlloyField)).map[t | | ||
113 | new ParameterSubstitution(paramIndexes.map[t.atom(it).atomLabel2Term]) | ||
114 | -> | ||
115 | t.atom(function.parameters.size + 1).atomLabel2Term | ||
116 | ])] | ||
117 | this.function2Value = Union(hostedfunction2Value,globalfunction2Value) | ||
118 | // eval relations | ||
119 | val hostedRelation2Value = forwardTrace.relationDeclaration2Field.mapValues[ relation | | ||
120 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
121 | new ParameterSubstitution(#[t.atom(0).atomLabel2Term,t.atom(1).atomLabel2Term])].toSet] | ||
122 | val globalRelation2Value = forwardTrace.relationDeclaration2Global.mapValues[ relation | | ||
123 | solution.eval(relation.name.lookup(name2AlloyField)).map[ t | | ||
124 | new ParameterSubstitution((1..<t.arity).map[int a|t.atom(a).atomLabel2Term])].toSet] | ||
125 | this.relation2Value = Union(hostedRelation2Value,globalRelation2Value) | ||
126 | |||
127 | //Int limits | ||
128 | this.minInt = solution.min | ||
129 | this.maxInt = solution.max | ||
130 | |||
131 | |||
132 | } | ||
133 | |||
134 | def print() { | ||
135 | println('''Elements-----''') | ||
136 | interpretationOfUndefinedType.forEach[k,v|println('''«k.name» -> «v»''')] | ||
137 | |||
138 | println('''Constants-----''') | ||
139 | constant2Value.forEach[k, v|println('''«k.name» : «v»''')] | ||
140 | println('''Functions-----''') | ||
141 | function2Value.forEach[f,m|m.forEach[k,v| println('''«f.name» : «k» |-> «v»''')]] | ||
142 | println('''Relations-----''') | ||
143 | relation2Value.forEach[r,s|s.forEach[t | println('''«r.name»: («t»)''')]] | ||
144 | } | ||
145 | |||
146 | def private getName(edu.mit.csail.sdg.alloy4compiler.ast.Type type) { | ||
147 | val name = type.toString | ||
148 | if(name.startsWith("{this/") && name.endsWith("}")) { | ||
149 | return type.toString.replaceFirst("\\{this\\/","").replace("}","") | ||
150 | } | ||
151 | else throw new IllegalArgumentException('''Unknown type format: "«name»"!''') | ||
152 | } | ||
153 | def private getName(ExprVar atom) { atom.toString.split("\\$") } | ||
154 | |||
155 | override getElements(Type type) { getElementsDispatch(type) } | ||
156 | def private dispatch getElementsDispatch(TypeDeclaration declaration) { return declaration.lookup(this.interpretationOfUndefinedType) } | ||
157 | def private dispatch getElementsDispatch(TypeDefinition declaration) { return declaration.elements } | ||
158 | |||
159 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | ||
160 | val transformedParams = new ParameterSubstitution(parameterSubstitution) | ||
161 | return transformedParams.lookup( | ||
162 | function.lookup(this.function2Value) | ||
163 | ) | ||
164 | } | ||
165 | |||
166 | override getInterpretation(RelationDeclaration relation, Object[] parameterSubstitution) { | ||
167 | relation.lookup(this.relation2Value).contains(new ParameterSubstitution(parameterSubstitution)) | ||
168 | } | ||
169 | |||
170 | override getInterpretation(ConstantDeclaration constant) { | ||
171 | constant.lookup(this.constant2Value) | ||
172 | } | ||
173 | |||
174 | override getMinimalInteger() { this.minInt } | ||
175 | override getMaximalInteger() { this.maxInt } | ||
176 | |||
177 | // Alloy term -> logic term | ||
178 | def private atomLabel2Term(String label) { | ||
179 | if(label.number) return Integer.parseInt(label) | ||
180 | else if(label == this.logicBooleanTrue) return true | ||
181 | else if(label == this.logicBooleanFalse) return false | ||
182 | else if(this.alloyAtom2LogicElement.containsKey(label)) return label.lookup(alloyAtom2LogicElement) | ||
183 | else throw new IllegalArgumentException('''Unknown atom label: "«label»"!''') | ||
184 | } | ||
185 | def isNumber(String s) { | ||
186 | try{ | ||
187 | Integer.parseInt(s) | ||
188 | return true | ||
189 | }catch(NumberFormatException e) { | ||
190 | return false | ||
191 | } | ||
192 | } | ||
193 | } | ||
194 | |||
195 | class ParameterSubstitution{ | ||
196 | val Object[] data; | ||
197 | |||
198 | new(Object[] data) { this.data = data } | ||
199 | |||
200 | override equals(Object obj) { | ||
201 | if(obj === this) return true | ||
202 | else if(obj == null) return false | ||
203 | if(obj instanceof ParameterSubstitution) { | ||
204 | return Arrays.equals(this.data,obj.data) | ||
205 | } | ||
206 | return false | ||
207 | } | ||
208 | |||
209 | override hashCode() { | ||
210 | Arrays.hashCode(data) | ||
211 | } | ||
212 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ new file mode 100644 index 00000000..8c03af6e --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/FunctionWithTimeout.xtend_ | |||
@@ -0,0 +1,40 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import org.eclipse.xtext.xbase.lib.Functions.Function0 | ||
4 | import java.util.concurrent.Executors | ||
5 | import java.util.concurrent.Callable | ||
6 | import java.util.concurrent.TimeUnit | ||
7 | import java.util.concurrent.TimeoutException | ||
8 | import java.util.concurrent.ExecutionException | ||
9 | |||
10 | class FunctionWithTimeout<Type> { | ||
11 | val Function0<Type> function; | ||
12 | |||
13 | new(Function0<Type> function) { | ||
14 | this.function = function | ||
15 | } | ||
16 | |||
17 | def execute(long millisecs) { | ||
18 | if(millisecs>0) { | ||
19 | val executor = Executors.newCachedThreadPool(); | ||
20 | val task = new Callable<Type>() { | ||
21 | override Type call() { function.apply } | ||
22 | }; | ||
23 | val future = executor.submit(task); | ||
24 | try { | ||
25 | val result = future.get(millisecs, TimeUnit.MILLISECONDS); | ||
26 | return result | ||
27 | } catch (TimeoutException ex) { | ||
28 | // handle the timeout | ||
29 | } catch (InterruptedException e) { | ||
30 | // handle the interrupts | ||
31 | } catch (ExecutionException e) { | ||
32 | // handle other exceptions | ||
33 | } finally { | ||
34 | future.cancel(true); // may or may not desire this | ||
35 | } | ||
36 | return null | ||
37 | } | ||
38 | else return function.apply | ||
39 | } | ||
40 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ new file mode 100644 index 00000000..29acd681 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/Logic2AlloyApiMapper.xtend_ | |||
@@ -0,0 +1,345 @@ | |||
1 | package hu.bme.mit.inf.dlsreasoner.alloy.reasoner.builder | ||
2 | |||
3 | import java.util.Map | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TracedOutput | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
6 | import java.util.List | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolTypeReference | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntTypeReference | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealTypeReference | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference | ||
11 | import edu.mit.csail.sdg.alloy4compiler.ast.ExprConstant | ||
12 | import edu.mit.csail.sdg.alloy4compiler.ast.Expr | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.BoolLiteral | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.IntLiteral | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Impl | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreThan | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessThan | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.MoreOrEqualThan | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.LessOrEqualThan | ||
26 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Equals | ||
27 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Plus | ||
28 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Minus | ||
29 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Multiply | ||
30 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Divison | ||
31 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Mod | ||
32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Forall | ||
33 | import java.util.HashMap | ||
34 | import edu.mit.csail.sdg.alloy4compiler.ast.Decl | ||
35 | import java.util.ArrayList | ||
36 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists | ||
37 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RealLiteral | ||
38 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration | ||
39 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
40 | import edu.mit.csail.sdg.alloy4compiler.ast.Attr | ||
41 | import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig | ||
42 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation | ||
43 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
44 | import javax.naming.OperationNotSupportedException | ||
45 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
46 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Constant | ||
47 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.AlloySpecification | ||
48 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.Multiplicity | ||
49 | import hu.bme.mit.inf.dlsreasoner.alloy.reasoner.alloylanguage.InverseReference | ||
50 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition | ||
51 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
52 | |||
53 | class AlloyInput{ | ||
54 | public val List<PrimSig> typeDeclarations=new ArrayList | ||
55 | public val List<Expr> functionDeclarations=new ArrayList | ||
56 | public val List<Expr> assertions=new ArrayList | ||
57 | public val List<Expr> multiplicityConstraints=new ArrayList | ||
58 | public val List<Expr> inverseConstraints=new ArrayList | ||
59 | } | ||
60 | |||
61 | class Logic2AlloyApiMapperTrace { | ||
62 | val Map<Type, PrimSig> typeMap | ||
63 | val Map<DefinedElement, PrimSig> elementMap | ||
64 | //val Map<Function, SMTFunctionDeclaration> functionMap | ||
65 | val Map<Relation,Expr> relationMap | ||
66 | //val Map<Constant,SMTFunctionDeclaration> constantMap | ||
67 | |||
68 | new () { | ||
69 | this.typeMap = new HashMap | ||
70 | this.elementMap = new HashMap | ||
71 | //this.functionMap = new HashMap | ||
72 | this.relationMap = new HashMap | ||
73 | //this.constantMap = new HashMap | ||
74 | } | ||
75 | new (Map<Type, PrimSig> typeMap, | ||
76 | Map<DefinedElement, PrimSig> elementMap, | ||
77 | //Map<Function, SMTFunctionDeclaration> functionMap, | ||
78 | Map<Relation,Expr> relationMap/*, | ||
79 | Map<Constant,SMTFunctionDeclaration> constantMap*/) | ||
80 | { | ||
81 | this.typeMap = typeMap | ||
82 | this.elementMap = elementMap | ||
83 | //this.functionMap = functionMap | ||
84 | this.relationMap = relationMap | ||
85 | //this.constantMap = constantMap | ||
86 | } | ||
87 | |||
88 | def types() { typeMap } | ||
89 | def elements() { elementMap } | ||
90 | //def functions() { functionMap } | ||
91 | def relations() { relationMap } | ||
92 | //def constants() { constantMap } | ||
93 | } | ||
94 | |||
95 | class Logic2AlloyApiMapper{ | ||
96 | //TODO output | ||
97 | public def TracedOutput<List<PrimSig>, Logic2AlloyApiMapperTrace> transformProblem(LogicProblem problem) { | ||
98 | val documentInput = new AlloyInput() | ||
99 | //createSMTInput => [satCommand = createSMTSimpleSatCommand getModelCommand = createSMTGetModelCommand] | ||
100 | //val document = createSMTDocument => [input = documentInput] | ||
101 | val List<PrimSig> document=new ArrayList | ||
102 | val trace = new Logic2AlloyApiMapperTrace | ||
103 | |||
104 | // Trafo | ||
105 | documentInput.typeDeclarations += problem.types.map[transformType(trace)] | ||
106 | //documentInput.functionDeclarations += problem.functions.map[transformFunction(trace)] | ||
107 | documentInput.functionDeclarations += problem.relations.map[transformRelation(trace)] | ||
108 | //documentInput.functionDeclarations += problem.constants.map[transformConstant(trace)] | ||
109 | documentInput.assertions += problem.assertions.map[transformAssertion(trace)] | ||
110 | |||
111 | |||
112 | val alloySpecification = problem.specifications.filter(AlloySpecification).head | ||
113 | |||
114 | for(mult: alloySpecification.multiplicities){ | ||
115 | if(mult.min>0){ | ||
116 | documentInput.multiplicityConstraints+=mult.transformMultiplicityLowerBound(trace) | ||
117 | } | ||
118 | if(mult.max!=-1){ | ||
119 | documentInput.multiplicityConstraints+=mult.transformMultiplicityUpperBound(trace) | ||
120 | } | ||
121 | } | ||
122 | |||
123 | for(inv: alloySpecification.inverses){ | ||
124 | documentInput.inverseConstraints += inv.transformInverse(trace) | ||
125 | } | ||
126 | // End trafo | ||
127 | |||
128 | return new TracedOutput(document,trace) | ||
129 | } | ||
130 | |||
131 | def Expr transformMultiplicityLowerBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ | ||
132 | |||
133 | val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl | ||
134 | return (forallVariable.get.cardinality.gte(ExprConstant.makeNUMBER(multiplicity.min))).forAll(forallVariable) | ||
135 | |||
136 | } | ||
137 | |||
138 | def Expr transformMultiplicityUpperBound(Multiplicity multiplicity, Logic2AlloyApiMapperTrace trace){ | ||
139 | |||
140 | val Decl forallVariable=(trace.relations.get(multiplicity.multiplicityOf)).oneOf("o") as Decl | ||
141 | return (forallVariable.get.cardinality.lte(ExprConstant.makeNUMBER(multiplicity.max))).forAll(forallVariable) | ||
142 | |||
143 | } | ||
144 | |||
145 | def Expr transformInverse(InverseReference inverse, Logic2AlloyApiMapperTrace trace){ | ||
146 | return trace.relations.get(inverse.inverseOf.get(0)).equal(trace.relations.get(inverse.inverseOf.get(1)).transpose) | ||
147 | } | ||
148 | |||
149 | private def toID(List<String> names) {names.join("!") } | ||
150 | |||
151 | def dispatch protected transformType(TypeDefinition declaration, Logic2AlloyApiMapperTrace trace) { | ||
152 | val result = new PrimSig(declaration.name.toID, Attr.ABSTRACT) | ||
153 | trace.types.put(declaration,result) | ||
154 | return result | ||
155 | } | ||
156 | |||
157 | def protected transformDefinedElement(TypeDefinition enumType, DefinedElement element, Logic2AlloyApiMapperTrace trace) { | ||
158 | val result=new PrimSig(element.name.toID, trace.types.get(enumType), Attr.ONE) | ||
159 | trace.elements.put(element,result) | ||
160 | return result | ||
161 | } | ||
162 | |||
163 | def dispatch protected transformType(TypeDeclaration declaration, Logic2AlloyApiMapperTrace trace) { | ||
164 | //TODO �r�kles, absztrakt | ||
165 | val result = new PrimSig(declaration.name.toID) | ||
166 | trace.types.put(declaration,result) | ||
167 | return result | ||
168 | } | ||
169 | |||
170 | def dispatch protected transformTypeReference(BoolTypeReference boolTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
171 | throw new UnsupportedOperationException("BoolTypeReference is not supported.") | ||
172 | } | ||
173 | def dispatch protected transformTypeReference(IntTypeReference intTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
174 | return PrimSig.SIGINT | ||
175 | } | ||
176 | def dispatch protected transformTypeReference(RealTypeReference realTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
177 | throw new UnsupportedOperationException("RealTypeReference is not supported.") | ||
178 | } | ||
179 | def dispatch protected PrimSig transformTypeReference(ComplexTypeReference complexTypeReference, Logic2AlloyApiMapperTrace trace) { | ||
180 | return trace.types.get(complexTypeReference.referred) | ||
181 | } | ||
182 | |||
183 | /*def protected transformFunction(Function declaration, Logic2AlloyApiMapperTrace trace) { | ||
184 | val functionDeclaration = createSMTFunctionDeclaration => [ | ||
185 | name = declaration.name.toID | ||
186 | range = declaration.range.transformTypeReference(trace) | ||
187 | parameters+= declaration.parameters.map[transformTypeReference(trace)] | ||
188 | ] | ||
189 | trace.functions.put(declaration,functionDeclaration) | ||
190 | return functionDeclaration | ||
191 | }*/ | ||
192 | |||
193 | def transformRelation(Relation relation, Logic2AlloyApiMapperTrace trace) { | ||
194 | if(relation.parameters.size==2){ | ||
195 | trace.relations.put(relation,(relation.parameters.get(0).transformTypeReference(trace) as PrimSig).addField(relation.name.toID, (relation.parameters.get(1).transformTypeReference(trace) as PrimSig).setOf)) | ||
196 | } else{ | ||
197 | throw new OperationNotSupportedException("More parameters are not supported.") | ||
198 | } | ||
199 | } | ||
200 | |||
201 | /*def transformConstant(Constant constant, Logic2AlloyApiMapperTrace trace) { | ||
202 | val smtConstant = createSMTFunctionDeclaration => [ | ||
203 | name = constant.name.toID | ||
204 | range = transformTypeReference(constant.type, trace) | ||
205 | ] | ||
206 | trace.constants.put(constant,smtConstant) | ||
207 | return smtConstant | ||
208 | }*/ | ||
209 | |||
210 | def protected Expr transformAssertion(Assertion assertion, Logic2AlloyApiMapperTrace trace) { | ||
211 | |||
212 | return assertion.value.transformTerm(trace,emptyMap) | ||
213 | } | ||
214 | |||
215 | def dispatch protected Expr transformTerm(BoolLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
216 | throw new UnsupportedOperationException("Bool is not supported") | ||
217 | //open util/boolean, autoPay: Bool | ||
218 | //https://code.google.com/p/valloy2009/source/browse/trunk/src/models/util/boolean.als?r=142 | ||
219 | } | ||
220 | def dispatch protected Expr transformTerm(IntLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
221 | return ExprConstant.makeNUMBER(literal.value) | ||
222 | } | ||
223 | def dispatch protected Expr transformTerm(RealLiteral literal, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
224 | throw new UnsupportedOperationException("Real number is not supported") | ||
225 | } | ||
226 | def dispatch protected Expr transformTerm(Not not, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
227 | return not.operand.transformTerm(trace,variables).not} | ||
228 | def dispatch protected Expr transformTerm(And and, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
229 | val List<Expr> operands= and.operands.map[transformTerm(trace,variables)] | ||
230 | var andTerm=operands.get(0) | ||
231 | for(Integer i: 1..(operands.size-1)){ | ||
232 | andTerm=andTerm.and(operands.get(i)) | ||
233 | } | ||
234 | return andTerm | ||
235 | } | ||
236 | def dispatch protected Expr transformTerm(Or or, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
237 | val List<Expr> operands= or.operands.map[transformTerm(trace,variables)] | ||
238 | var orTerm=operands.get(0) | ||
239 | for(Integer i: 1..(operands.size-1)){ | ||
240 | orTerm=orTerm.or(operands.get(i)) | ||
241 | } | ||
242 | return orTerm | ||
243 | } | ||
244 | def dispatch protected Expr transformTerm(Impl impl, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
245 | return impl.leftOperand.transformTerm(trace,variables).implies(impl.rightOperand.transformTerm(trace,variables)) | ||
246 | } | ||
247 | def dispatch protected Expr transformTerm(Iff ifExpression, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
248 | return ifExpression.leftOperand.transformTerm(trace,variables).iff(ifExpression.rightOperand.transformTerm(trace,variables)) | ||
249 | } | ||
250 | def dispatch protected Expr transformTerm(MoreThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
251 | return moreThan.leftOperand.transformTerm(trace,variables).gt(moreThan.rightOperand.transformTerm(trace,variables)) | ||
252 | } | ||
253 | def dispatch protected Expr transformTerm(LessThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
254 | return lessThan.leftOperand.transformTerm(trace,variables).lt(lessThan.rightOperand.transformTerm(trace,variables)) | ||
255 | } | ||
256 | def dispatch protected Expr transformTerm(MoreOrEqualThan moreThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
257 | return moreThan.leftOperand.transformTerm(trace,variables).gte(moreThan.rightOperand.transformTerm(trace,variables)) | ||
258 | } | ||
259 | def dispatch protected Expr transformTerm(LessOrEqualThan lessThan, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
260 | return lessThan.leftOperand.transformTerm(trace,variables).lte(lessThan.rightOperand.transformTerm(trace,variables)) | ||
261 | } | ||
262 | def dispatch protected Expr transformTerm(Equals equals, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
263 | return equals.leftOperand.transformTerm(trace,variables).equal(equals.rightOperand.transformTerm(trace,variables)) | ||
264 | } | ||
265 | /*def dispatch protected Expr transformTerm(Distinct distinct, Logic2AlloyApiMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | ||
266 | createSMTDistinct => [ operands += distinct.operands.map[transformTerm(trace,variables)]]}*/ | ||
267 | def dispatch protected Expr transformTerm(Plus plus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
268 | return plus.leftOperand.transformTerm(trace,variables).plus(plus.rightOperand.transformTerm(trace,variables)) | ||
269 | } | ||
270 | def dispatch protected Expr transformTerm(Minus minus, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
271 | return minus.leftOperand.transformTerm(trace,variables).minus(minus.rightOperand.transformTerm(trace,variables)) | ||
272 | } | ||
273 | def dispatch protected Expr transformTerm(Multiply multiply, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
274 | return multiply.leftOperand.transformTerm(trace,variables).mul(multiply.rightOperand.transformTerm(trace,variables)) | ||
275 | } | ||
276 | def dispatch protected Expr transformTerm(Divison div, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
277 | return div.leftOperand.transformTerm(trace,variables).div(div.rightOperand.transformTerm(trace,variables)) | ||
278 | } | ||
279 | def dispatch protected Expr transformTerm(Mod mod, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
280 | throw new UnsupportedOperationException("Modulo is not supported.") | ||
281 | } | ||
282 | def dispatch protected Expr transformTerm(Forall forall, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
283 | return configureForall(forall,trace,variables) | ||
284 | } | ||
285 | def dispatch protected Expr transformTerm(Exists exists, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
286 | return configureExists(exists,trace,variables) | ||
287 | } | ||
288 | def dispatch protected Expr transformTerm(SymbolicValue symbolicValue, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
289 | symbolicValue.symbolicReference.transformSymbolicReference(symbolicValue.parameterSubstitutions,trace,variables) } | ||
290 | |||
291 | def private configureForall( | ||
292 | Forall quantifiedExpression, | ||
293 | Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) | ||
294 | { | ||
295 | val allVariables = new HashMap(variables) | ||
296 | val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size) | ||
297 | |||
298 | for(logicVariable: quantifiedExpression.quantifiedVariables) { | ||
299 | val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl | ||
300 | allVariables.put(logicVariable, newAlloyVariable) | ||
301 | newAlloyVariables += newAlloyVariable | ||
302 | } | ||
303 | val variable0=newAlloyVariables.get(0) | ||
304 | newAlloyVariables.remove(0) | ||
305 | return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forAll(variable0, newAlloyVariables) | ||
306 | } | ||
307 | |||
308 | def private configureExists( | ||
309 | Exists quantifiedExpression, | ||
310 | Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) | ||
311 | { | ||
312 | val allVariables = new HashMap(variables) | ||
313 | val newAlloyVariables = new ArrayList<Decl>(quantifiedExpression.quantifiedVariables.size) | ||
314 | |||
315 | for(logicVariable: quantifiedExpression.quantifiedVariables) { | ||
316 | val newAlloyVariable = (logicVariable.range.transformTypeReference(trace)).oneOf(logicVariable.name.toID) as Decl | ||
317 | allVariables.put(logicVariable, newAlloyVariable) | ||
318 | newAlloyVariables += newAlloyVariable | ||
319 | } | ||
320 | val variable0=newAlloyVariables.get(0) | ||
321 | newAlloyVariables.remove(0) | ||
322 | return (quantifiedExpression.expression.transformTerm(trace,allVariables)).forSome(variable0, newAlloyVariables) | ||
323 | } | ||
324 | |||
325 | def dispatch protected Expr transformSymbolicReference(DefinedElement referred, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
326 | return trace.elements.get(referred) | ||
327 | } | ||
328 | def dispatch protected Expr transformSymbolicReference(Variable variable, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
329 | return variables.get(variable).get | ||
330 | } | ||
331 | /*def dispatch protected Expr transformSymbolicReference(Function function, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
332 | val result = createSMTSymbolicValue => [sv | sv.symbolicReference = trace.functions.get(function)] | ||
333 | for(paramSubstitution : parameterSubstitutions) { | ||
334 | result.parameterSubstitutions.add(paramSubstitution.transformTerm(trace,variables)) | ||
335 | } | ||
336 | return result | ||
337 | }*/ | ||
338 | def dispatch protected Expr transformSymbolicReference(Relation relation, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
339 | return trace.relations.get(relation) | ||
340 | } | ||
341 | def dispatch protected Expr transformSymbolicReference(Constant constant, List<Term> parameterSubstitutions, Logic2AlloyApiMapperTrace trace, Map<Variable, Decl> variables) { | ||
342 | //createSMTSymbolicValue => [symbolicReference = trace.constants.get(constant)] | ||
343 | throw new UnsupportedOperationException("Constant is not supported") | ||
344 | } | ||
345 | } \ No newline at end of file | ||
diff --git a/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes new file mode 100644 index 00000000..5e349ac8 --- /dev/null +++ b/Solvers/Alloy-Solver/hu.bme.mit.inf.dlsreasoner.alloy.reasoner/unused/oldTypes | |||
@@ -0,0 +1,74 @@ | |||
1 | /*def dispatch boolean hasDeclaredElement(TypeDefinition type) { return false; } | ||
2 | def dispatch boolean hasDeclaredElement(TypeDeclaration type) { | ||
3 | if(type.isAbstract) { | ||
4 | type.subtypes.exists[it.hasDeclaredElement] | ||
5 | } else return true; | ||
6 | } | ||
7 | |||
8 | def dispatch List<TypeDefinition> allEnumSubtypes(TypeDefinition type) { return #[type] } | ||
9 | def dispatch List<TypeDefinition> allEnumSubtypes(TypeDeclaration type) { | ||
10 | return type.subtypes.map[it.allEnumSubtypes].flatten.toList | ||
11 | } | ||
12 | |||
13 | def protected transformTypes(List<Type> types, Logic2AlloyLanguageMapperTrace trace) { | ||
14 | val Map<TypeDeclaration,ALSSignatureDeclaration> signatureTrace = new HashMap; | ||
15 | |||
16 | // Creating the root type | ||
17 | val objectType = createALSSignatureDeclaration => [ name=#["util","object"].toID it.abstract = true ] | ||
18 | trace.objectSupperClass = objectType | ||
19 | trace.specification.typeDeclarations += objectType | ||
20 | |||
21 | // Creating the images of the types | ||
22 | for(type : types) { | ||
23 | if(type instanceof TypeDefinition) { | ||
24 | if(type.elements.empty) { | ||
25 | trace.type2ALSType.put(type,#[]); | ||
26 | } else { | ||
27 | val e = createALSEnumDeclaration => [ | ||
28 | it.name = type.name.toID | ||
29 | it.literal += type.elements.map[transformDefinedElement(trace)] | ||
30 | ] | ||
31 | trace.type2ALSType.put(type,#[e]) | ||
32 | trace.specification.typeDeclarations += e | ||
33 | } | ||
34 | } | ||
35 | else if(type instanceof TypeDeclaration) { | ||
36 | if(hasDeclaredElement(type)) { | ||
37 | val s = createALSSignatureDeclaration => [ | ||
38 | name=type.name.toID | ||
39 | it.abstract = type.isIsAbstract | ||
40 | ] | ||
41 | trace.type2ALSType.put(type,new LinkedList=>[add(s)]) | ||
42 | signatureTrace.put(type, s) | ||
43 | trace.specification.typeDeclarations += s | ||
44 | } | ||
45 | else { | ||
46 | signatureTrace.put(type, null) | ||
47 | trace.type2ALSType.put(type,new LinkedList);// empty | ||
48 | } | ||
49 | } | ||
50 | else throw new IllegalArgumentException('''Unknown type «type.class.name»''') | ||
51 | } | ||
52 | |||
53 | |||
54 | for(type: types.filter(TypeDeclaration)) { | ||
55 | // Adding inheritance | ||
56 | val s = type.lookup(signatureTrace) | ||
57 | if(s!=null) { | ||
58 | for(supertype : type.supertypes) { | ||
59 | s.supertype += (supertype as TypeDeclaration).lookup(signatureTrace) | ||
60 | } | ||
61 | if(type.supertypes.empty) { | ||
62 | s.supertype += objectType | ||
63 | } | ||
64 | } | ||
65 | // Adding enum subtypes | ||
66 | type.lookup(trace.type2ALSType)+=type.allEnumSubtypes.map[it.lookup(trace.type2ALSType)].flatten | ||
67 | } | ||
68 | } | ||
69 | |||
70 | def protected transformDefinedElement(DefinedElement element, Logic2AlloyLanguageMapperTrace trace) { | ||
71 | val result = createALSEnumLiteral => [name = element.name.toID] | ||
72 | trace.definedElement2EnumProperty.put(element,result) | ||
73 | return result | ||
74 | }*/ \ No newline at end of file | ||