diff options
3 files changed, 16 insertions, 13 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java index d7268bb9..7dedfaeb 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDrealProblemSolver.java | |||
@@ -13,6 +13,7 @@ import java.util.Arrays; | |||
13 | import java.util.HashMap; | 13 | import java.util.HashMap; |
14 | import java.util.List; | 14 | import java.util.List; |
15 | import java.util.Map; | 15 | import java.util.Map; |
16 | import java.util.Map.Entry; | ||
16 | import java.util.UUID; | 17 | import java.util.UUID; |
17 | import java.util.concurrent.TimeUnit; | 18 | import java.util.concurrent.TimeUnit; |
18 | import java.util.regex.Matcher; | 19 | import java.util.regex.Matcher; |
@@ -35,7 +36,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
35 | 36 | ||
36 | private final String containerName; | 37 | private final String containerName; |
37 | private Map<Object, String> varMap; | 38 | private Map<Object, String> varMap; |
38 | private List<String> curVars; | 39 | private Map<String, String> curVar2Decl; |
39 | 40 | ||
40 | public NumericDrealProblemSolver() throws IOException, InterruptedException { | 41 | public NumericDrealProblemSolver() throws IOException, InterruptedException { |
41 | //setup docker | 42 | //setup docker |
@@ -64,6 +65,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
64 | //TODO timeout if needed | 65 | //TODO timeout if needed |
65 | if (!p.waitFor(5, TimeUnit.SECONDS)) { | 66 | if (!p.waitFor(5, TimeUnit.SECONDS)) { |
66 | p.destroy(); | 67 | p.destroy(); |
68 | System.err.println("TIMEOUT"); | ||
67 | } | 69 | } |
68 | return p; | 70 | return p; |
69 | } | 71 | } |
@@ -171,11 +173,11 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
171 | varMap.put(matchedObj, expr); | 173 | varMap.put(matchedObj, expr); |
172 | } | 174 | } |
173 | //Add variable declarations | 175 | //Add variable declarations |
174 | if(! curVars.contains(expr)) { | 176 | if(! curVar2Decl.keySet().contains(expr)) { |
175 | String varDecl = "(declare-fun " + expr + " () "; | 177 | String varDecl = "(declare-fun " + expr + " () "; |
176 | if (isInt) {varDecl += "Int)";} | 178 | if (isInt) {varDecl += "Int)";} |
177 | else {varDecl += "Real)";} | 179 | else {varDecl += "Real)";} |
178 | curVars.add(varDecl); | 180 | curVar2Decl.put(expr, varDecl); |
179 | } | 181 | } |
180 | } | 182 | } |
181 | // Constants | 183 | // Constants |
@@ -227,7 +229,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
227 | String tempFileName = tempFile.getName(); | 229 | String tempFileName = tempFile.getName(); |
228 | 230 | ||
229 | //STM2 FILE CONTENT CREATION | 231 | //STM2 FILE CONTENT CREATION |
230 | curVars = new ArrayList<String>(); | 232 | curVar2Decl = new HashMap<String, String>(); |
231 | List<String> curConstraints = new ArrayList<String>(); | 233 | List<String> curConstraints = new ArrayList<String>(); |
232 | 234 | ||
233 | PrintWriter printer = new PrintWriter(tempFile); | 235 | PrintWriter printer = new PrintWriter(tempFile); |
@@ -242,7 +244,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ | |||
242 | } | 244 | } |
243 | } | 245 | } |
244 | //Add Content to SMT2 file | 246 | //Add Content to SMT2 file |
245 | for (String varDecl : curVars) {printer.println(varDecl);} | 247 | for (String varDecl : curVar2Decl.values()) {printer.println(varDecl);} |
246 | for (String negAssert : curConstraints) {printer.println(negAssert);} | 248 | for (String negAssert : curConstraints) {printer.println(negAssert);} |
247 | printer.println("(check-sat)"); | 249 | printer.println("(check-sat)"); |
248 | printer.close(); | 250 | printer.close(); |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig index 01b7f040..7ead54af 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig | |||
@@ -6,7 +6,7 @@ generate { | |||
6 | constraints = { package queries} | 6 | constraints = { package queries} |
7 | solver = ViatraSolver | 7 | solver = ViatraSolver |
8 | scope = { | 8 | scope = { |
9 | #node = 6..15, | 9 | #node = 10..30, |
10 | #int = {} | 10 | #int = {} |
11 | } | 11 | } |
12 | 12 | ||
@@ -20,6 +20,7 @@ generate { | |||
20 | runs = 1 | 20 | runs = 1 |
21 | 21 | ||
22 | debug = "outputs/debug" | 22 | debug = "outputs/debug" |
23 | log = "outputs/log.txt" | 23 | log = "outputs/debug/log.txt" |
24 | output = "outputs/models" | 24 | output = "outputs/models" |
25 | statistics = "outputs/statistics.csv" | ||
25 | } \ No newline at end of file | 26 | } \ No newline at end of file |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql index f8650073..450107d4 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/queries/familyTreeConstraints.vql | |||
@@ -26,11 +26,11 @@ pattern negativeAge(m: Member) { | |||
26 | check(mage<0); | 26 | check(mage<0); |
27 | } | 27 | } |
28 | 28 | ||
29 | @Constraint(message="realisticAge", severity="error",key={m}) | 29 | //@Constraint(message="realisticAge", severity="error",key={m}) |
30 | pattern realisticAge(m: Member) { | 30 | //pattern realisticAge(m: Member) { |
31 | Member.age(m,mage); | 31 | // Member.age(m,mage); |
32 | check(mage>120); | 32 | // check(mage>120); |
33 | } | 33 | //} |
34 | 34 | ||
35 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) | 35 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) |
36 | pattern parentTooYoung(c: Member, p: Member) = { | 36 | pattern parentTooYoung(c: Member, p: Member) = { |