From 43fcf6e297c4c305eb8f5cf3c91f8e507d440b83 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Wed, 6 Jan 2021 07:08:59 +0100 Subject: prepping measurement setup w/ dreal --- .../case.study.familyTree.run/plugin.xml | 1 + .../src/queries/familyTreeConstraints.vql | 6 ++++++ .../config/genericFamilyTree.vsconfig | 1 + .../config/genericFamilyTreeSMTEnd.vsconfig | 1 + .../config/genericFamilyTreeSMTQual.vsconfig | 1 + .../config/genericSatellite.vsconfig | 1 + .../case.study.pledge.run/config/genericTaxation.vsconfig | 1 + .../src/run/RunGeneratorConfig.xtend | 15 +++++++++++++-- 8 files changed, 25 insertions(+), 2 deletions(-) (limited to 'Tests') 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 @@ + 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) { check(mage<0); } +@Constraint(message="realisticAge", severity="error",key={m}) +pattern realisticAge(m: Member) { + Member.age(m,mage); + check(mage>120); +} + @Constraint(message="parentTooYoung", severity="error", key={c, p}) pattern parentTooYoung(c: Member, p: Member) = { 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 { config = { runtime = 10000, + "numeric-solver" = "z3", log-level = normal, "fitness-punishSize" = "false", "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 { config = { runtime = 10000, + "numeric-solver" = "z3", log-level = normal, "fitness-punishSize" = "false", "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 { config = { runtime = 10000, + "numeric-solver" = "z3", log-level = normal, "fitness-punishSize" = "false", "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 { config = { runtime = 10000, + "numeric-solver" = "z3", log-level = normal, "fitness-scope" = "3", "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 { config = { runtime = 10000, + "numeric-solver" = "z3", log-level = normal, "fitness-scope" = "1", "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 import org.apache.commons.cli.Options import org.apache.commons.cli.ParseException import org.eclipse.core.runtime.NullProgressMonitor +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.ConfigEntry +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.impl.ConfigEntryImpl +import hu.bme.mit.inf.dslreasoner.application.applicationConfiguration.CustomEntry class RunGeneratorConfig { static var SIZE_LB = 20 @@ -34,6 +37,7 @@ class RunGeneratorConfig { static var RUNS = 10 static var MODELS = 10 static var RUNTIME = 1500 + static var NUM_SOLVER = "z3" static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" static val QUERIES = true @@ -62,6 +66,9 @@ class RunGeneratorConfig { val rt = new Option("rt", "runtime", true, "runtime limit") options.addOption(rt) + + val ns = new Option("ns", "numericSolver", true, "what numeric solver to use") + options.addOption(ns) val d = new Option("d", "domain", true, "domain") options.addOption(d) @@ -91,6 +98,8 @@ class RunGeneratorConfig { if(nmIn !== null) MODELS = Integer.parseInt(nmIn) val rtIn = cmd.getOptionValue("runtime") if(rtIn !== null) RUNTIME = Integer.parseInt(rtIn) + val nsIn = cmd.getOptionValue("numericSolver") + if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal" val dIn = cmd.getOptionValue("domain") if(dIn !== null) DOMAIN = dIn val hhIn = cmd.getOptionValue("household") @@ -109,7 +118,7 @@ class RunGeneratorConfig { // ///////////////////////// // BEGIN RUN println( - "<>") if (isTaxation) println("<>") @@ -173,10 +182,12 @@ class RunGeneratorConfig { } } // workspace.writeModel(config, '''x.xmi''') - // Runtime + // Config val configScope = genTask.config as ConfigSpecification val runtimeEntry = configScope.entries.get(0) as RuntimeEntry runtimeEntry.millisecLimit = RUNTIME + val numSolverEntry = configScope.entries.get(1) as CustomEntry + numSolverEntry.value = NUM_SOLVER // Output locations val debug = genTask.debugFolder as FileSpecification -- cgit v1.2.3-54-g00ecf