diff options
author | 2017-08-08 16:12:05 +0200 | |
---|---|---|
committer | 2017-08-08 16:12:05 +0200 | |
commit | 7443c0d1e88c1d6191d0074c27f81e2400bbd7fe (patch) | |
tree | 7fcc7ed30525c4fe12c71940e3388a91b432e50b /Framework | |
parent | Support for double and string attributes (diff) | |
parent | Fixed a typo (diff) | |
download | VIATRA-Generator-7443c0d1e88c1d6191d0074c27f81e2400bbd7fe.tar.gz VIATRA-Generator-7443c0d1e88c1d6191d0074c27f81e2400bbd7fe.tar.zst VIATRA-Generator-7443c0d1e88c1d6191d0074c27f81e2400bbd7fe.zip |
Merge branch 'master' of https://github.com/viatra/VIATRA-Generator
Diffstat (limited to 'Framework')
2 files changed, 189 insertions, 15 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend index 7b384bc4..fa277dbf 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.logic.model/src/hu/bme/mit/inf/dslreasoner/logic/model/builder/LogicSolver.xtend | |||
@@ -5,32 +5,139 @@ import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult |
6 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | 6 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace |
7 | import java.util.List | 7 | import java.util.List |
8 | import java.util.SortedSet | ||
9 | import java.util.TreeSet | ||
10 | import com.google.thirdparty.publicsuffix.PublicSuffixPatterns | ||
11 | import javax.xml.ws.soap.AddressingFeature.Responses | ||
12 | import java.util.Collection | ||
8 | 13 | ||
9 | abstract class LogicReasoner { | 14 | abstract class LogicReasoner { |
10 | def abstract LogicResult solve( | 15 | def abstract LogicResult solve(LogicProblem problem, LogicSolverConfiguration configuration, |
11 | LogicProblem problem, | ||
12 | LogicSolverConfiguration configuration, | ||
13 | ReasonerWorkspace workspace) throws LogicReasonerException | 16 | ReasonerWorkspace workspace) throws LogicReasonerException |
17 | |||
14 | def abstract List<? extends LogicModelInterpretation> getInterpretations(ModelResult modelResult) | 18 | def abstract List<? extends LogicModelInterpretation> getInterpretations(ModelResult modelResult) |
15 | } | 19 | } |
16 | 20 | ||
17 | public class LogicReasonerException extends Exception { | 21 | public class LogicReasonerException extends Exception { |
18 | new(String message, Exception cause) { super(message,cause) } | 22 | new(String message, Exception cause) { |
19 | new(Exception cause) { super("The reasoner has failed",cause)} | 23 | super(message, cause) |
20 | new(String message) { super(message) } | 24 | } |
25 | |||
26 | new(Exception cause) { | ||
27 | super("The reasoner has failed", cause) | ||
28 | } | ||
29 | |||
30 | new(String message) { | ||
31 | super(message) | ||
32 | } | ||
33 | } | ||
34 | |||
35 | /** | ||
36 | * Creates an interval. If the lowerLimit is greater than the upperLimit, the values will be swapped. | ||
37 | */ | ||
38 | class IntegerInterval { | ||
39 | private var int lowerLimit; | ||
40 | private var int upperLimit; | ||
41 | |||
42 | new(int lowerLimit, int upperLimit) { | ||
43 | if (lowerLimit <= upperLimit) { | ||
44 | this.lowerLimit = lowerLimit; | ||
45 | this.upperLimit = upperLimit; | ||
46 | } else { | ||
47 | this.upperLimit = lowerLimit; | ||
48 | this.lowerLimit = upperLimit; | ||
49 | } | ||
50 | } | ||
51 | |||
52 | def boolean equals(IntegerInterval interval) { | ||
53 | if (interval.lowerLimit == this.lowerLimit && interval.upperLimit == this.upperLimit) | ||
54 | return true | ||
55 | return false | ||
56 | } | ||
57 | |||
58 | def public int getLowerLimit() { | ||
59 | return lowerLimit; | ||
60 | } | ||
61 | |||
62 | def public int getUpperLimit() { | ||
63 | return upperLimit; | ||
64 | } | ||
65 | |||
66 | def public void setLimits(int lowerLimit, int upperLimit) { | ||
67 | if (lowerLimit <= upperLimit) { | ||
68 | this.lowerLimit = lowerLimit; | ||
69 | this.upperLimit = upperLimit; | ||
70 | } else { | ||
71 | this.upperLimit = lowerLimit; | ||
72 | this.lowerLimit = upperLimit; | ||
73 | } | ||
74 | } | ||
75 | } | ||
76 | |||
77 | /** | ||
78 | * Creates a range which represents the minimum and maximum length allowed for Strings. | ||
79 | * If the input for minimumLength is lower than 0, then the minimumLength will be set to 0. | ||
80 | * If the input for maximumLength is lower than 0, then the maximumLength will be set to 0. | ||
81 | * If minimumLength is greater than maximumLength, the values will be swapped | ||
82 | */ | ||
83 | class StringLengthInterval { | ||
84 | private var int minimumLength; | ||
85 | private var int maximumLength; | ||
86 | |||
87 | new(int minimumLength, int maximumLength) { | ||
88 | if (minimumLength < 0) { | ||
89 | this.minimumLength = 0 | ||
90 | } else if (maximumLength < 0) { | ||
91 | this.maximumLength = 0 | ||
92 | } else if (minimumLength >= maximumLength) { | ||
93 | this.maximumLength = minimumLength; | ||
94 | this.minimumLength = maximumLength; | ||
95 | } else { | ||
96 | this.maximumLength = maximumLength; | ||
97 | this.minimumLength = minimumLength; | ||
98 | } | ||
99 | } | ||
100 | |||
101 | def boolean equals(StringLengthInterval interval) { | ||
102 | if (interval.minimumLength == this.minimumLength && interval.maximumLength == this.maximumLength) | ||
103 | return true | ||
104 | return false | ||
105 | } | ||
106 | |||
107 | def public int getMinimumLength() { | ||
108 | return minimumLength; | ||
109 | } | ||
110 | |||
111 | def public int getMaximumLength() { | ||
112 | return maximumLength; | ||
113 | } | ||
114 | |||
115 | def public void setLimits(int minimumLength, int maximumLength) { | ||
116 | if (minimumLength < 0) { | ||
117 | this.minimumLength = 0 | ||
118 | } else if (maximumLength < 0) { | ||
119 | this.maximumLength = 0 | ||
120 | } else if (minimumLength >= maximumLength) { | ||
121 | this.maximumLength = minimumLength; | ||
122 | this.minimumLength = maximumLength; | ||
123 | } else { | ||
124 | this.maximumLength = maximumLength; | ||
125 | this.minimumLength = minimumLength; | ||
126 | } | ||
127 | } | ||
21 | } | 128 | } |
22 | 129 | ||
23 | abstract class LogicSolverConfiguration { | 130 | abstract class LogicSolverConfiguration { |
24 | public static val Unlimited = -1; | 131 | public static val Unlimited = -1; |
25 | public static val String UndefinedPath = null | 132 | public static val String UndefinedPath = null |
26 | 133 | ||
27 | /** The URI string to the independent solver application */ | 134 | /** The URI string to the independent solver application */ |
28 | public String solverPath = UndefinedPath | 135 | public String solverPath = UndefinedPath |
29 | /** Max runtime limit in seconds. */ | 136 | /** Max runtime limit in seconds. */ |
30 | public int runtimeLimit = Unlimited | 137 | public int runtimeLimit = Unlimited |
31 | /** Max runtime limit in seconds. */ | 138 | /** Max runtime limit in seconds. */ |
32 | public int memoryLimit = Unlimited | 139 | public int memoryLimit = Unlimited |
33 | 140 | ||
34 | public var TypeScopes typeScopes = new TypeScopes; | 141 | public var TypeScopes typeScopes = new TypeScopes; |
35 | public var SolutionScope solutionScope = new SolutionScope | 142 | public var SolutionScope solutionScope = new SolutionScope |
36 | } | 143 | } |
@@ -38,9 +145,76 @@ abstract class LogicSolverConfiguration { | |||
38 | /** | 145 | /** |
39 | * Defines the the size of the generated models. Constant <code>Unlimited</code> defines no upper limit to the type. | 146 | * Defines the the size of the generated models. Constant <code>Unlimited</code> defines no upper limit to the type. |
40 | */ | 147 | */ |
41 | public class TypeScopes{ | 148 | public class TypeScopes { |
42 | public static val Unlimited = -1; | 149 | public static val Unlimited = -1; |
43 | 150 | public var boolean ignoreIdDuringGeneration = true | |
151 | |||
152 | /** | ||
153 | * The domain of integers from which we can choose | ||
154 | */ | ||
155 | public var IntegerInterval intervalOfIntegers | ||
156 | /** | ||
157 | * The maximal and minimal length of strings | ||
158 | */ | ||
159 | public var StringLengthInterval intervalOfStrings | ||
160 | /** | ||
161 | * A set containing the integers that can be used to solve the problem. | ||
162 | */ | ||
163 | public TreeSet<Integer> allIntegers = new TreeSet<Integer> { | ||
164 | override boolean add(Integer element) { | ||
165 | if (element < intervalOfIntegers.lowerLimit || element > intervalOfIntegers.upperLimit) { | ||
166 | return false | ||
167 | } else { | ||
168 | return super.add(element) | ||
169 | } | ||
170 | } | ||
171 | |||
172 | override boolean addAll(Collection<? extends Integer> collectionToAdd) { | ||
173 | var boolean hasBeenModified = false | ||
174 | for (element : collectionToAdd) { | ||
175 | hasBeenModified = this.add(element); | ||
176 | } | ||
177 | return hasBeenModified | ||
178 | } | ||
179 | |||
180 | } | ||
181 | |||
182 | /** | ||
183 | * A set containing the strings that can be used to solve the problem. | ||
184 | */ | ||
185 | public TreeSet<String> allStrings = new TreeSet<String> { | ||
186 | override boolean add(String string) { | ||
187 | if (string.length < intervalOfStrings.minimumLength || string.length > intervalOfStrings.maximumLength) { | ||
188 | return false | ||
189 | } else { | ||
190 | return super.add(string) | ||
191 | } | ||
192 | } | ||
193 | |||
194 | override boolean addAll(Collection<? extends String> collectionToAdd) { | ||
195 | var boolean hasBeenModified = false | ||
196 | for (element : collectionToAdd) { | ||
197 | if (!(element.length < intervalOfStrings.minimumLength || | ||
198 | element.length > intervalOfStrings.maximumLength)) { | ||
199 | hasBeenModified = super.add(element); | ||
200 | } | ||
201 | } | ||
202 | return hasBeenModified | ||
203 | } | ||
204 | } | ||
205 | |||
206 | /** | ||
207 | * A set containing the doubles that can be used to solve the problem. | ||
208 | */ | ||
209 | public TreeSet<Double> allDoubles = new TreeSet<Double> | ||
210 | /** | ||
211 | * Sets the number of Strings that has to be used to solve the problem. | ||
212 | */ | ||
213 | public var numberOfUseableStrings = Unlimited | ||
214 | /** | ||
215 | * Sets the number of Integers that has to be used to solve the problem. | ||
216 | */ | ||
217 | public var numberOfUseableIntegers = Unlimited | ||
44 | /** | 218 | /** |
45 | * Defines a limit for integers in the logic problem. | 219 | * Defines a limit for integers in the logic problem. |
46 | */ | 220 | */ |
@@ -59,7 +233,7 @@ public class TypeScopes{ | |||
59 | * Defines the required number of solutions for the problem. | 233 | * Defines the required number of solutions for the problem. |
60 | * Constant <code>All</code> defines that all solution for the problem is requested. | 234 | * Constant <code>All</code> defines that all solution for the problem is requested. |
61 | */ | 235 | */ |
62 | public class SolutionScope{ | 236 | public class SolutionScope { |
63 | public static val All = -1; | 237 | public static val All = -1; |
64 | public var numberOfRequiredSolution = 1 | 238 | public var numberOfRequiredSolution = 1 |
65 | } \ No newline at end of file | 239 | } |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend index a4b6cc6d..86fc8537 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/Viatra2Logic.xtend | |||
@@ -227,15 +227,15 @@ class Viatra2Logic { | |||
227 | ecore2LogicTrace,viatra2LogicTrace,variable2Variable,config) | 227 | ecore2LogicTrace,viatra2LogicTrace,variable2Variable,config) |
228 | ].filterNull | 228 | ].filterNull |
229 | val allConstraintIsSatisfied = And(translatedConstraints) | 229 | val allConstraintIsSatisfied = And(translatedConstraints) |
230 | val allNetativeVariablesAreSatisfied = if(innerNegativeVariables.empty) { | 230 | val allNegativeVariablesAreSatisfied = if(innerNegativeVariables.empty) { |
231 | allConstraintIsSatisfied | 231 | allConstraintIsSatisfied |
232 | } else { | 232 | } else { |
233 | Forall(innerNegativeVariables,allConstraintIsSatisfied); | 233 | Forall(innerNegativeVariables,allConstraintIsSatisfied); |
234 | } | 234 | } |
235 | val allVariablesAreExisting = if(innerPositiveVariables.empty) { | 235 | val allVariablesAreExisting = if(innerPositiveVariables.empty) { |
236 | allNetativeVariablesAreSatisfied | 236 | allNegativeVariablesAreSatisfied |
237 | } else { | 237 | } else { |
238 | Exists(innerPositiveVariables,allNetativeVariablesAreSatisfied); | 238 | Exists(innerPositiveVariables,allNegativeVariablesAreSatisfied); |
239 | } | 239 | } |
240 | 240 | ||
241 | return allVariablesAreExisting | 241 | return allVariablesAreExisting |