diff options
author | 2021-01-06 07:08:59 +0100 | |
---|---|---|
committer | 2021-01-06 07:08:59 +0100 | |
commit | 43fcf6e297c4c305eb8f5cf3c91f8e507d440b83 (patch) | |
tree | d4d9b610a46364982fb740309a8c2d6ae1ff899f /Tests/MODELS2020-CaseStudies | |
parent | Merge branch 'dreal-integration' of https://github.com/viatra/VIATRA-Generato... (diff) | |
download | VIATRA-Generator-43fcf6e297c4c305eb8f5cf3c91f8e507d440b83.tar.gz VIATRA-Generator-43fcf6e297c4c305eb8f5cf3c91f8e507d440b83.tar.zst VIATRA-Generator-43fcf6e297c4c305eb8f5cf3c91f8e507d440b83.zip |
prepping measurement setup w/ dreal
Diffstat (limited to 'Tests/MODELS2020-CaseStudies')
8 files changed, 25 insertions, 2 deletions
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml index 4297ec89..f5cda378 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml | |||
@@ -5,6 +5,7 @@ | |||
5 | <query-specification fqn="queries.twoMembersHaveNoParent"/> | 5 | <query-specification fqn="queries.twoMembersHaveNoParent"/> |
6 | <query-specification fqn="queries.memberHasParent"/> | 6 | <query-specification fqn="queries.memberHasParent"/> |
7 | <query-specification fqn="queries.negativeAge"/> | 7 | <query-specification fqn="queries.negativeAge"/> |
8 | <query-specification fqn="queries.realisticAge"/> | ||
8 | <query-specification fqn="queries.parentTooYoung"/> | 9 | <query-specification fqn="queries.parentTooYoung"/> |
9 | </group> | 10 | </group> |
10 | </extension> | 11 | </extension> |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql index fdbac640..f8650073 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/src/queries/familyTreeConstraints.vql | |||
@@ -26,6 +26,12 @@ pattern negativeAge(m: Member) { | |||
26 | check(mage<0); | 26 | check(mage<0); |
27 | } | 27 | } |
28 | 28 | ||
29 | @Constraint(message="realisticAge", severity="error",key={m}) | ||
30 | pattern realisticAge(m: Member) { | ||
31 | Member.age(m,mage); | ||
32 | check(mage>120); | ||
33 | } | ||
34 | |||
29 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) | 35 | @Constraint(message="parentTooYoung", severity="error", key={c, p}) |
30 | pattern parentTooYoung(c: Member, p: Member) = { | 36 | pattern parentTooYoung(c: Member, p: Member) = { |
31 | FamilyTree.members(_, c); | 37 | FamilyTree.members(_, c); |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig index 2e653776..a5fd3189 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTree.vsconfig | |||
@@ -33,6 +33,7 @@ generate { | |||
33 | 33 | ||
34 | config = { | 34 | config = { |
35 | runtime = 10000, | 35 | runtime = 10000, |
36 | "numeric-solver" = "z3", | ||
36 | log-level = normal, | 37 | log-level = normal, |
37 | "fitness-punishSize" = "false", | 38 | "fitness-punishSize" = "false", |
38 | "fitness-scope" = "3" | 39 | "fitness-scope" = "3" |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig index 7a22f760..e833397f 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTEnd.vsconfig | |||
@@ -33,6 +33,7 @@ generate { | |||
33 | 33 | ||
34 | config = { | 34 | config = { |
35 | runtime = 10000, | 35 | runtime = 10000, |
36 | "numeric-solver" = "z3", | ||
36 | log-level = normal, | 37 | log-level = normal, |
37 | "fitness-punishSize" = "false", | 38 | "fitness-punishSize" = "false", |
38 | "fitness-scope" = "3", | 39 | "fitness-scope" = "3", |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig index fa9cd6e2..36df7eef 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericFamilyTreeSMTQual.vsconfig | |||
@@ -33,6 +33,7 @@ generate { | |||
33 | 33 | ||
34 | config = { | 34 | config = { |
35 | runtime = 10000, | 35 | runtime = 10000, |
36 | "numeric-solver" = "z3", | ||
36 | log-level = normal, | 37 | log-level = normal, |
37 | "fitness-punishSize" = "false", | 38 | "fitness-punishSize" = "false", |
38 | "fitness-scope" = "3", | 39 | "fitness-scope" = "3", |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig index aad8f544..3ee164cd 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericSatellite.vsconfig | |||
@@ -31,6 +31,7 @@ generate { | |||
31 | 31 | ||
32 | config = { | 32 | config = { |
33 | runtime = 10000, | 33 | runtime = 10000, |
34 | "numeric-solver" = "z3", | ||
34 | log-level = normal, | 35 | log-level = normal, |
35 | "fitness-scope" = "3", | 36 | "fitness-scope" = "3", |
36 | "fitness-punishSize" = "true", | 37 | "fitness-punishSize" = "true", |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig index a3f1cd07..0f2657c1 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericTaxation.vsconfig | |||
@@ -34,6 +34,7 @@ generate { | |||
34 | 34 | ||
35 | config = { | 35 | config = { |
36 | runtime = 10000, | 36 | runtime = 10000, |
37 | "numeric-solver" = "z3", | ||
37 | log-level = normal, | 38 | log-level = normal, |
38 | "fitness-scope" = "1", | 39 | "fitness-scope" = "1", |
39 | "fitness-punishSize" = "inverse", | 40 | "fitness-punishSize" = "inverse", |
diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend index e4d6fe9f..e1d9b9d9 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/src/run/RunGeneratorConfig.xtend | |||
@@ -25,6 +25,9 @@ import org.apache.commons.cli.Option | |||
25 | import org.apache.commons.cli.Options | 25 | import org.apache.commons.cli.Options |
26 | import org.apache.commons.cli.ParseException | 26 | import org.apache.commons.cli.ParseException |
27 | import org.eclipse.core.runtime.NullProgressMonitor | 27 | import org.eclipse.core.runtime.NullProgressMonitor |
28 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigEntry | ||
29 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.impl.ConfigEntryImpl | ||
30 | import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CustomEntry | ||
28 | 31 | ||
29 | class RunGeneratorConfig { | 32 | class RunGeneratorConfig { |
30 | static var SIZE_LB = 20 | 33 | static var SIZE_LB = 20 |
@@ -34,6 +37,7 @@ class RunGeneratorConfig { | |||
34 | static var RUNS = 10 | 37 | static var RUNS = 10 |
35 | static var MODELS = 10 | 38 | static var MODELS = 10 |
36 | static var RUNTIME = 1500 | 39 | static var RUNTIME = 1500 |
40 | static var NUM_SOLVER = "z3" | ||
37 | 41 | ||
38 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" | 42 | static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" |
39 | static val QUERIES = true | 43 | static val QUERIES = true |
@@ -62,6 +66,9 @@ class RunGeneratorConfig { | |||
62 | 66 | ||
63 | val rt = new Option("rt", "runtime", true, "runtime limit") | 67 | val rt = new Option("rt", "runtime", true, "runtime limit") |
64 | options.addOption(rt) | 68 | options.addOption(rt) |
69 | |||
70 | val ns = new Option("ns", "numericSolver", true, "what numeric solver to use") | ||
71 | options.addOption(ns) | ||
65 | 72 | ||
66 | val d = new Option("d", "domain", true, "domain") | 73 | val d = new Option("d", "domain", true, "domain") |
67 | options.addOption(d) | 74 | options.addOption(d) |
@@ -91,6 +98,8 @@ class RunGeneratorConfig { | |||
91 | if(nmIn !== null) MODELS = Integer.parseInt(nmIn) | 98 | if(nmIn !== null) MODELS = Integer.parseInt(nmIn) |
92 | val rtIn = cmd.getOptionValue("runtime") | 99 | val rtIn = cmd.getOptionValue("runtime") |
93 | if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) | 100 | if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) |
101 | val nsIn = cmd.getOptionValue("numericSolver") | ||
102 | if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal" | ||
94 | val dIn = cmd.getOptionValue("domain") | 103 | val dIn = cmd.getOptionValue("domain") |
95 | if(dIn !== null) DOMAIN = dIn | 104 | if(dIn !== null) DOMAIN = dIn |
96 | val hhIn = cmd.getOptionValue("household") | 105 | val hhIn = cmd.getOptionValue("household") |
@@ -109,7 +118,7 @@ class RunGeneratorConfig { | |||
109 | // ///////////////////////// | 118 | // ///////////////////////// |
110 | // BEGIN RUN | 119 | // BEGIN RUN |
111 | println( | 120 | println( |
112 | "<<DOMAIN: " + DOMAIN + ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" + | 121 | "<<DOMAIN: " + DOMAIN + ", NumSolver=" + NUM_SOLVER + ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" + |
113 | MODELS + ", Runtime=" + RUNTIME + ">>") | 122 | MODELS + ", Runtime=" + RUNTIME + ">>") |
114 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") | 123 | if (isTaxation) println("<<Households: " + HOUSEHOLD + ">>") |
115 | 124 | ||
@@ -173,10 +182,12 @@ class RunGeneratorConfig { | |||
173 | } | 182 | } |
174 | } | 183 | } |
175 | // workspace.writeModel(config, '''x.xmi''') | 184 | // workspace.writeModel(config, '''x.xmi''') |
176 | // Runtime | 185 | // Config |
177 | val configScope = genTask.config as ConfigSpecification | 186 | val configScope = genTask.config as ConfigSpecification |
178 | val runtimeEntry = configScope.entries.get(0) as RuntimeEntry | 187 | val runtimeEntry = configScope.entries.get(0) as RuntimeEntry |
179 | runtimeEntry.millisecLimit = RUNTIME | 188 | runtimeEntry.millisecLimit = RUNTIME |
189 | val numSolverEntry = configScope.entries.get(1) as CustomEntry | ||
190 | numSolverEntry.value = NUM_SOLVER | ||
180 | 191 | ||
181 | // Output locations | 192 | // Output locations |
182 | val debug = genTask.debugFolder as FileSpecification | 193 | val debug = genTask.debugFolder as FileSpecification |