From bc403272d867f82edd623179d82c080e57154c1a Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 09:01:25 +0100 Subject: CrossingScenario case study is ready for server --- .../src/crossingScenario/run/DrawScenario.java | 10 +- .../viatra2logic/ExpressionEvaluation2Logic.xtend | 2 +- .../viatra2logic/NumericDrealProblemSolver.java | 3 +- .../viatra2logic/NumericDynamicProblemSolver.java | 4 +- .../viatra2logic/NumericTranslator.xtend | 6 +- .../viatra2logic/NumericZ3ProblemSolver.java | 15 +- .../dse/BestFirstStrategyForModelGeneration.java | 1 + .../viatrasolver/reasoner/dse/NumericSolver.xtend | 10 +- .../impl/ModelQueriesGlobalConstraint.java | 2 + .../viatra/dse/solutionstore/SolutionStore.java | 3 +- .../case.study.pledge.run/RunGeneratorConfig.jar | Bin 78139397 -> 78169348 bytes .../config/genericCrossScenario.vsconfig | 51 ++ .../config/genericStrategyNo.vsconfig | 64 ++ .../config/genericStrategyNoWithHints.vsconfig | 64 ++ .../config/genericStrategyYes.vsconfig | 65 +++ .../inputs/crossScen4Strat.xmi | 38 ++ .../case.study.pledge.run/inputs/crossScen5.xmi | 31 + .../queries/csQueriesScale.vql | 220 +++++++ .../queries/csQueriesStrategy.vql | 646 +++++++++++++++++++++ .../queries/csQueriesStrategyHints.vql | 646 +++++++++++++++++++++ .../case.study.pledge.run/runCrossScenario.sh | 21 + .../runCrossScenarioStrategy.sh | 15 + .../case.study.pledge.run/runTestCrossScenario.sh | 11 + .../src/run/RunGeneratorConfig.xtend | 18 +- 24 files changed, 1925 insertions(+), 21 deletions(-) create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql create mode 100644 Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql create mode 100755 Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh create mode 100755 Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh create mode 100755 Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh diff --git a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java index cce2b3f2..61fa51a2 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java +++ b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java @@ -32,10 +32,12 @@ public class DrawScenario { public static final int SIZE = 1000; public static void main(String[] args) throws IOException { - for (int i = 1; i <= 10; i++) { - drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png"); - System.out.println("DONE " + i); - } + drawScenario("/home/models/VIATRA-Generator/Tests/MODELS2020-CaseStudies/case.study.pledge.run/measurements/models/StrategyNo/size01to-1r1n1rt300nsdreal-localdrto10000_16-0823/1.xmi" + , "outputs/drawnModelMisc.png"); +// for (int i = 1; i <= 10; i++) { +// drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png"); +// System.out.println("DONE " + i); +// } } public static File drawScenario(String pathToXmi, String saveToPath) throws IOException { diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend index ae94c327..f8d3e3bd 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/ExpressionEvaluation2Logic.xtend @@ -21,7 +21,7 @@ class ExpressionEvaluation2Logic { def getNumericSolver() { if(_numericSolver === null) { // it seems like this getter has no use - _numericSolver = (new NumericTranslator(null)).selectProblemSolver("z3") + _numericSolver = (new NumericTranslator(null, 0)).selectProblemSolver("z3") } return _numericSolver } 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 eb63d96a..cecd3623 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 @@ -44,7 +44,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private final int TIMEOUT_DOCKER = 5000; private int TIMEOUT_LOCAL = -1; - private final int DEBUG_PRINT = 2; + private final int DEBUG_PRINT = 0; public NumericDrealProblemSolver(boolean useDocker, String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { this.useDocker = useDocker; @@ -72,6 +72,7 @@ public class NumericDrealProblemSolver extends NumericProblemSolver{ private Process runProcess(List cmd, int timeout) throws IOException, InterruptedException { // String s = String.join(" ", cmd); // Process p = Runtime.getRuntime().exec(s); + Runtime.getRuntime().exec("killall -9 dreal").waitFor(); Process p = (new ProcessBuilder(cmd)).start(); // p.waitFor(); //TODO timeout if needed diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java index 1e5c1f29..e8c20138 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericDynamicProblemSolver.java @@ -13,16 +13,18 @@ public class NumericDynamicProblemSolver extends NumericProblemSolver{ // private NumericZ3ProblemSolver z3Solver; private NumericDrealProblemSolver drealSolver; + private int timeout; public NumericDynamicProblemSolver(String drealLocalPath, int drealTimeout) throws IOException, InterruptedException { // this.z3Solver = new NumericZ3ProblemSolver(); this.drealSolver = new NumericDrealProblemSolver(false, drealLocalPath, drealTimeout); + this.timeout = drealTimeout; } public NumericProblemSolver selectSolver(String selection) { switch (selection) { case "z3": - return new NumericZ3ProblemSolver(); + return new NumericZ3ProblemSolver(timeout); case "dreal": return this.drealSolver; default: diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index 791dd644..a11ae8a8 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend @@ -17,6 +17,7 @@ class NumericTranslator { private XExpressionExtractor extractor = new XExpressionExtractor(); private NumericProblemSolver numericSolver; + private int timeout; long formingProblemTime=0; long solvingProblemTime=0; @@ -29,8 +30,9 @@ class NumericTranslator { } } - new(NumericProblemSolver numericProblemSolver){ + new(NumericProblemSolver numericProblemSolver, int timeout){ this.numericSolver = numericProblemSolver + this.timeout = timeout; } def Map arrayToMap(Object[] tuple, ArrayList variablesInOrder) { @@ -63,7 +65,7 @@ class NumericTranslator { val NumericDynamicProblemSolver dynamicSolver = numericSolver as NumericDynamicProblemSolver return dynamicSolver.selectSolver(selection); } else{ - if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver + if (numericSolver instanceof NumericZ3ProblemSolver) return new NumericZ3ProblemSolver(this.timeout) return numericSolver; } } diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java index 612e93a6..0799953f 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericZ3ProblemSolver.java @@ -1,6 +1,5 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; -import java.io.File; import java.util.ArrayList; import java.util.HashMap; import java.util.List; @@ -20,6 +19,7 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Model; +import com.microsoft.z3.Params; import com.microsoft.z3.RealExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; @@ -36,7 +36,7 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ private Solver s; private Map varMap; - public NumericZ3ProblemSolver() { + public NumericZ3ProblemSolver(int timeout) { //FOR LINUX VM //Not Elegant, but this is working for now // String root = "/home/models/VIATRA-Generator"; @@ -50,6 +50,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ ctx = new Context(cfg); ctx.setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB_FULL); s = ctx.mkSolver(); + if (timeout != -1) { + Params p = ctx.mkParams(); + p.add("timeout", timeout); + s.setParameters(p); + } varMap = new HashMap(); } @@ -82,7 +87,11 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{ s.add(problemInstance); endformingProblem = System.nanoTime()-startformingProblem; long startSolvingProblem = System.nanoTime(); - boolean result = (s.check() == Status.SATISFIABLE); +// System.out.print("start - "); + Status soln = s.check(); + boolean result = (soln == Status.SATISFIABLE); + if (soln == Status.UNKNOWN) System.err.println("TIMEOUT"); +// System.out.println("end"); endSolvingProblem = System.nanoTime()-startSolvingProblem; this.ctx.close(); return result; diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java index a8d2381c..c62d124a 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/BestFirstStrategyForModelGeneration.java @@ -222,6 +222,7 @@ public class BestFirstStrategyForModelGeneration implements IStrategy { // } // } +// System.out.println("--------NEXT"); boolean consistencyCheckResult = checkConsistency(currentTrajectoryWithFitness); if(consistencyCheckResult == true) { continue mainLoop; } diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend index 8281c3c3..a228afc6 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.reasoner/src/hu/bme/mit/inf/dslreasoner/viatrasolver/reasoner/dse/NumericSolver.xtend @@ -55,7 +55,7 @@ class NumericSolver { this.caching = caching this.drealLocalPath = config.drealLocalPath this.strategy = config.strategy - this.t = new NumericTranslator(createNumericTranslator(config)) + this.t = new NumericTranslator(createNumericTranslator(config), config.drealTimeout) } def createNumericTranslator(ViatraReasonerConfiguration config) { @@ -77,7 +77,7 @@ class NumericSolver { System.load(root + "/Solvers/SMT-Solver/com.microsoft.z3/lib/libz3java.so"); // System.load("libz3.so"); // System.load("libz3java.so"); - return new NumericZ3ProblemSolver + return new NumericZ3ProblemSolver(config.drealTimeout) } } else { @@ -150,9 +150,9 @@ class NumericSolver { //Filter constraints if there are phase-related restricutions //null whitelist means accept everything - println("<<<>>> (" + phase + ")") +// println("<<<>>> (" + phase + ")") if (phase == -2) { - println("Skipping numeric check") +// println("Skipping numeric check") //TODO Big assumption return true } @@ -235,7 +235,7 @@ class NumericSolver { def selectSolver(int phase) { if (strategy === ExplorationStrategy.CrossingScenario){ - if (phase == 1) return "dreal" + if (phase == 1) return "z3" else return "dreal" } return "irrelevant" diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java index 7616b4a2..3a990a1e 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/objectives/impl/ModelQueriesGlobalConstraint.java @@ -87,6 +87,8 @@ public class ModelQueriesGlobalConstraint implements IGlobalConstraint { for (ViatraQueryMatcher matcher : matchers) { if ((type.equals(ModelQueryType.NO_MATCH) && matcher.countMatches() > 0) || (type.equals(ModelQueryType.MUST_HAVE_MATCH) && matcher.countMatches() == 0)) { +// System.out.println(type + " " + matcher.countMatches()); +// System.out.println(matcher.getSpecification().getSimpleName()); return false; } } diff --git a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java index 578ae277..6e0abd0b 100644 --- a/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java +++ b/Solvers/VIATRA-Solver/org.eclipse.viatra.dse/src/org/eclipse/viatra/dse/solutionstore/SolutionStore.java @@ -208,10 +208,11 @@ public class SolutionStore { solutionTrajectory.setFitness(fitness); if (acceptOnlyGoalSolutions && !fitness.isSatisifiesHardObjectives()) { +// System.out.println("NOT SAVING"); unsavedSolutionCallbacks(context, solutionTrajectory); return; } - + System.out.println("SAVING SOLUTION"); boolean solutionSaved = solutionSaver.saveSolution(context, id, solutionTrajectory); if (solutionSaved) { diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar index 8d981fde..b97ebf5c 100644 Binary files a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar and b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/RunGeneratorConfig.jar differ diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig new file mode 100644 index 00000000..290b8835 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericCrossScenario.vsconfig @@ -0,0 +1,51 @@ +import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" +import viatra "queries/csQueriesScale.vql" +import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" +import viatra "queries/SatelliteQueries.vql" + +generate { + metamodel = { package satellite } + constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } + partial-model = { "inputs/SatelliteInstance.xmi"} + solver = ViatraSolver + scope = { + #node += 10..* + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + log-level = none + } + + runs = 1 + + output = "measurements/debug/warmup" +} + +generate { + metamodel = { package crossingScenario } + constraints = { package queries} + partial-model = { "inputs/crossScen5.xmi"} + solver = ViatraSolver + scope = { + #node += 3..* + ,# += 0 + ,# += 0 + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + "dreal-local-path" = "enterPathHere", + "dreal-timeout" = "10000", + log-level = none, + "scopePropagator" = "polyhedral"} + + runs = 1 + number = 10 + debug = "outputs/debug" + log = "outputs/debug/log.txt" + output = "outputs/models" + statistics = "outputs/debug/statistics.csv" +} diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig new file mode 100644 index 00000000..836b6b76 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNo.vsconfig @@ -0,0 +1,64 @@ +import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" +import viatra "queries/csQueriesStrategy.vql" +import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" +import viatra "queries/SatelliteQueries.vql" + +generate { + metamodel = { package satellite } + constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } + partial-model = { "inputs/SatelliteInstance.xmi"} + solver = ViatraSolver + scope = { + #node += 10..* + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + log-level = none + } + + runs = 1 + + output = "measurements/debug/warmup" +} + +generate { + metamodel = { package crossingScenario } + constraints = { package queries} + partial-model = { "inputs/crossScen4Strat.xmi"} + solver = ViatraSolver + scope = { + #node += 0..* + ,# += 0 + ,# += 0 + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + "dreal-local-path" = "enterPathHere", + "dreal-timeout" = "10000", + log-level = none, + "ignored-attributes" = " + Pedestrian.xPos=*, + Pedestrian.yPos=*, + Pedestrian.length=*, + Pedestrian.width=*, + Pedestrian.xSpeed=*, + Pedestrian.ySpeed=*, + Vehicle.xPos=*, + Vehicle.yPos=*, + Vehicle.length=*, + Vehicle.width=*, + Vehicle.xSpeed=*, + Vehicle.ySpeed=*, + CollisionExists.collisionTime=*"} + + runs = 1 + number = 10 + debug = "outputs/debug" + log = "outputs/debug/log.txt" + output = "outputs/models" + statistics = "outputs/debug/statistics.csv" +} diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig new file mode 100644 index 00000000..ebb2c4ca --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyNoWithHints.vsconfig @@ -0,0 +1,64 @@ +import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" +import viatra "queries/csQueriesStrategyHints.vql" +import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" +import viatra "queries/SatelliteQueries.vql" + +generate { + metamodel = { package satellite } + constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } + partial-model = { "inputs/SatelliteInstance.xmi"} + solver = ViatraSolver + scope = { + #node += 10..* + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + log-level = none + } + + runs = 1 + + output = "measurements/debug/warmup" +} + +generate { + metamodel = { package crossingScenario } + constraints = { package queries} + partial-model = { "inputs/crossScen4Strat.xmi"} + solver = ViatraSolver + scope = { + #node += 0..* + ,# += 0 + ,# += 0 + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + "dreal-local-path" = "enterPathHere", + "dreal-timeout" = "10000", + log-level = none, + "ignored-attributes" = " + Pedestrian.xPos=*, + Pedestrian.yPos=*, + Pedestrian.length=*, + Pedestrian.width=*, + Pedestrian.xSpeed=*, + Pedestrian.ySpeed=*, + Vehicle.xPos=*, + Vehicle.yPos=*, + Vehicle.length=*, + Vehicle.width=*, + Vehicle.xSpeed=*, + Vehicle.ySpeed=*, + CollisionExists.collisionTime=*"} + + runs = 1 + number = 10 + debug = "outputs/debug" + log = "outputs/debug/log.txt" + output = "outputs/models" + statistics = "outputs/debug/statistics.csv" +} diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig new file mode 100644 index 00000000..5c2077c2 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/config/genericStrategyYes.vsconfig @@ -0,0 +1,65 @@ +import epackage "../../../Domains/crossingScenario/model/crossingScenario.ecore" +import viatra "queries/csQueriesStrategy.vql" +import epackage "../../../Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/model/satellite.ecore" +import viatra "queries/SatelliteQueries.vql" + +generate { + metamodel = { package satellite } + constraints = { package hu.bme.mit.inf.dslreasoner.domains.satellite.queries } + partial-model = { "inputs/SatelliteInstance.xmi"} + solver = ViatraSolver + scope = { + #node += 10..* + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + log-level = none + } + + runs = 1 + + output = "measurements/debug/warmup" +} + +generate { + metamodel = { package crossingScenario } + constraints = { package queries} + partial-model = { "inputs/crossScen4Strat.xmi"} + solver = ViatraSolver + scope = { + #node += 0..* + ,# += 0 + ,# += 0 + } + + config = { + runtime = 10000, + "numeric-solver" = "z3", + "dreal-local-path" = "enterPathHere", + "dreal-timeout" = "10000", + log-level = none, + "strategy" = "crossingScenario", + "ignored-attributes" = " + Pedestrian.xPos=*, + Pedestrian.yPos=*, + Pedestrian.length=*, + Pedestrian.width=*, + Pedestrian.xSpeed=*, + Pedestrian.ySpeed=*, + Vehicle.xPos=*, + Vehicle.yPos=*, + Vehicle.length=*, + Vehicle.width=*, + Vehicle.xSpeed=*, + Vehicle.ySpeed=*, + CollisionExists.collisionTime=*"} + + runs = 1 + number = 10 + debug = "outputs/debug" + log = "outputs/debug/log.txt" + output = "outputs/models" + statistics = "outputs/debug/statistics.csv" +} diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi new file mode 100644 index 00000000..08cde1e8 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen4Strat.xmi @@ -0,0 +1,38 @@ + + + + + + + + + + + + + + + diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi new file mode 100644 index 00000000..5eee1734 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/inputs/crossScen5.xmi @@ -0,0 +1,31 @@ + + + + + + + + + + + + + diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql new file mode 100644 index 00000000..d3afa775 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesScale.vql @@ -0,0 +1,220 @@ +package queries + +import "http://www.example.com/crossingScenario" +import "http://www.eclipse.org/emf/2002/Ecore" + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Lane+Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + check(x <= r); +} or { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); +// //<<<>>> +// Lane.numWidth(vl, w); +// check(x >= (r + w)); + + //<<<>>>: lanes all have width=3 + check(x >= (r + 3.0)); +} + +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + check(y <= r); +} or { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); +// //<> +// Lane.numWidth(hl, w); +// check(y >= (r + w)); + + //<>: lanes all have width=3 + check(y >= (r + 3.0)); + +} + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////---------------- +//Xpos and Ypos Bounds +/////---------------- + +private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, + xMax:java Double, xP:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.xSize(cs, xMax); + Actor.xPos(a, xP); +} + +private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, + yMax:java Double, yP:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.ySize(cs, yMax); + Actor.yPos(a, yP); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP >= xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP <= 0-xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP >= yMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP <= 0-yMax);} + +//Minimum Distances +private pattern helper_getCoords(a1:Actor, + a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); +} + +//INFO may remove? +@Constraint(severity="error", key={a1, a2}, message="x") +pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + a1 != a2; + //check(dx^2 + dy^2 < 4^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 4*4); +} + +/////---------------- +//Xspeed and Yspeed bounds +/////---------------- +/* +/////////VERTICAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0.0); +} + +private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, + ySpeedMax:java Double, ySpeed:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxYSpeed(cs, ySpeedMax); + Actor.ySpeed(a, ySpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS <= 0.0-ySMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS >= ySMax); +} + +/////////HORIZONTAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0.0); +} + +private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, + xSpeedMax:java Double, xSpeed:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxXSpeed(cs, xSpeedMax); + Actor.xSpeed(a, xSpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS <= 0.0-xSMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS >= xSMax); +} +*/ +/////---------------- +/////WIDTH and LENGTH +/////---------------- + +///////pedestrian-width (3) +@Constraint(severity="error", key={p}, message="3 Actor") +pattern define_actor_pedestrianWidth(p:Pedestrian) { + Pedestrian.width(p, w); + check(w != 1.0); +} + +/////////pedestrian-width (4) +@Constraint(severity="error", key={p}, message="4 Actor") +pattern define_actor_pedestrianLength(p:Pedestrian) { + Pedestrian.length(p, l); + check(l != 1.0); +} + +/////////actor-width (5) +@Constraint(severity="error", key={v}, message="5 Actor") +pattern define_actor_vehicleWidth(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.width(v, w); + check(w != 2.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.width(v, w); + check(w != 3.0); +} + +/////////actor-width (6) +@Constraint(severity="error", key={v}, message="6 Actor") +pattern define_actor_vehicleLength(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.length(v, l); + check(l != 3.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.length(v, l); + check(l != 2.0); +} diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql new file mode 100644 index 00000000..5f35cd2b --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategy.vql @@ -0,0 +1,646 @@ +package queries + +import "http://www.example.com/crossingScenario" +import "http://www.eclipse.org/emf/2002/Ecore" + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Lane+Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + check(x <= r); +} or { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); +// //<<<>>> +// Lane.numWidth(vl, w); +// check(x >= (r + w)); + + //<<<>>>: lanes all have width=3 + check(x >= (r + 3.0)); +} + +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + check(y <= r); +} or { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); +// //<> +// Lane.numWidth(hl, w); +// check(y >= (r + w)); + + //<>: lanes all have width=3 + check(y >= (r + 3.0)); + +} + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////---------------- +//Xpos and Ypos Bounds +/////---------------- + +private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, + xMax:java Double, xP:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.xSize(cs, xMax); + Actor.xPos(a, xP); +} + +private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, + yMax:java Double, yP:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.ySize(cs, yMax); + Actor.yPos(a, yP); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP >= xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP <= 0-xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP >= yMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP <= 0-yMax);} + +////////////ADDED +//to reduce overlap +//NEEDED +/* +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_actor_wrtLane(a:Actor) { + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yP); + check(yP > 0.0-1.0); +} or { + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xP); + check(xP > 0.0-1.0); +} +*/ +////////////ADDED + +//Minimum Distances +private pattern helper_getCoords(a1:Actor, + a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); +} + +//INFO may remove? +@Constraint(severity="error", key={a1, a2}, message="x") +pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + a1 != a2; + //check(dx^2 + dy^2 < 3^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); +} + +/////---------------- +//Xspeed and Yspeed bounds +/////---------------- + +/////////VERTICAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0.0); +} + +private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, + ySpeedMax:java Double, ySpeed:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxYSpeed(cs, ySpeedMax); + Actor.ySpeed(a, ySpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS <= 0.0-ySMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS >= ySMax); +} + +/////////HORIZONTAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0.0); +} + +private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, + xSpeedMax:java Double, xSpeed:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxXSpeed(cs, xSpeedMax); + Actor.xSpeed(a, xSpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS <= 0.0-xSMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS >= xSMax); +} + +/////---------------- +/////WIDTH and LENGTH +/////---------------- + +///////pedestrian-width (3) +@Constraint(severity="error", key={p}, message="3 Actor") +pattern define_actor_pedestrianWidth(p:Pedestrian) { + Pedestrian.width(p, w); + check(w != 1.0); +} + +/////////pedestrian-width (4) +@Constraint(severity="error", key={p}, message="4 Actor") +pattern define_actor_pedestrianLength(p:Pedestrian) { + Pedestrian.length(p, l); + check(l != 1.0); +} + +/////////actor-width (5) +@Constraint(severity="error", key={v}, message="5 Actor") +pattern define_actor_vehicleWidth(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.width(v, w); + check(w != 2.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.width(v, w); + check(w != 3.0); +} + +/////////actor-width (6) +@Constraint(severity="error", key={v}, message="6 Actor") +pattern define_actor_vehicleLength(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.length(v, l); + check(l != 3.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.length(v, l); + check(l != 2.0); +} + +/////---------------- +/////DERIVED FEATURES +/////---------------- +/* +@QueryBasedFeature +pattern dist_near(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 < 10^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); + Actor.dist_near(a1, a2); +} + +@QueryBasedFeature +pattern dist_med(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(10^2 < dx^2 + dy^2 < 15^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); + Actor.dist_med(a1, a2); +} + +@QueryBasedFeature +pattern dist_far(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 > 20^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); + Actor.dist_far(a1, a2); +} +*/ +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Relation +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +//@Constraint(severity="error", key={a1, a2}, message="1 Relation") +//pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { +// Relation.source(r, a1); +// Relation.target(r, a2); +// a1 == a2; +//} + +//TODO do above but transitively?/ +//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//CollisionExists +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + + +//<> +/* +@Constraint(severity="error", key={a1, a2}, message="x") +pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} +*/ +//<> + + +//// +//CollisionExists - Time +//// + + +@Constraint(severity="error", key={c}, message="x") +pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { + CrossingScenario.relations(ss, c); + CrossingScenario.maxTime(ss, maxTime); + CollisionExists.collisionTime(c, cTime); + check(cTime >= maxTime);} + +@Constraint(severity="error", key={c}, message="x") +pattern collisionExists_timeNotNegative(c:CollisionExists) { + CollisionExists. collisionTime(c, cTime); + check(cTime <= 0.0);} + +//// +//CollisionExists - Physical Positioniung +//// + +private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + CollisionExists. collisionTime(c, cTime); +} + +private pattern helper_getYCoords(a:Actor, l:java Double, + yPos:java Double, ySpeed:java Double) { + + Actor.length(a, l); + Actor.yPos(a, yPos); + Actor.ySpeed(a, ySpeed); +} + +private pattern helper_getAllYCoords(a1:Actor, a2: Actor, + l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, + ySpeed1:java Double, ySpeed2:java Double) { + + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + find helper_getYCoords(a1, l1, yPos1, ySpeed1); + find helper_getYCoords(a2, l2, yPos2, ySpeed2); +} + +private pattern helper_getXCoords(a:Actor, w:java Double, + xPos:java Double, xSpeed:java Double) { + + Actor.width(a, w); + Actor.xPos(a, xPos); + Actor.xSpeed(a, xSpeed); +} + +private pattern helper_getAllXCoords(a1:Actor, a2: Actor, + w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, + xSpeed1:java Double, xSpeed2:java Double) { + + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + find helper_getXCoords(a1, w1, xPos1, xSpeed1); + find helper_getXCoords(a2, w2, xPos2, xSpeed2); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); + + //check(y_1_bottom > y_2_top + check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); + + //check(y_1_top < y_2_bottom) + check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + + //check(x_1_left > x_2_right) + check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + + //check(x_1_right < x_2_left) + check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); +} + + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//VisionBlocked +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +//<> +/* +@Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") +pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} or { + VisionBlocked.source(vb, a1); + VisionBlocked.blockedBy(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} or { + VisionBlocked.blockedBy(vb, a1); + VisionBlocked.target(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} +*/ +/* +@Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") +pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} +*/ + +////////////ADDED +//to make decision for ITE +//NOT NEEDED +/* +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_vb_blvssrc(a:Actor) { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yPa); + Actor.yPos(b, yPb); + check(yPb <= yPa); +} or { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xPa); + Actor.xPos(a, xPb); + check(xPb <= xPa); +} +*/ +////////////ADDED +//<> + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, a2); +} or { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, a1); +} + +@Constraint(severity="error", key={a1, vb}, message="x") +pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { + //REQUIRED to avoid division by 0 in next 2 queries + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + + Actor.xPos(a1, x1); + Actor.xPos(a2, x2); + + //check(slope of a1-to-BlockerTop < slope of a1-to-a2) + check(x1 == x2); +} + +private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, + x1:java Double, y1:java Double, + x2:java Double, y2:java Double, + xBlocker:java Double, yBlocker:java Double, + lenBlocker:java Double, widBlocker:java Double) { + + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); + Actor.xPos(aBlocker, xBlocker); + Actor.yPos(aBlocker, yBlocker); + Actor.length(aBlocker, lenBlocker); + Actor.width(aBlocker, widBlocker); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { + + find helper_VB_getAllCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); + + //check(slope of a1-to-BlockerTop < slope of a1-to-a2) + check( + ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / + ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) + < ((y1-y2)/(x1-x2))); +} + + +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { + + find helper_VB_getAllCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); + + //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) + check( + ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / + ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) + > ((y1-y2)/(x1-x2))); +} + +/////// +//BLOCKER IN BETWEEN +/////// + +private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, + x1:java Double, y1:java Double, + x2:java Double, y2:java Double, + xBlocker:java Double, yBlocker:java Double) { + + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); + Actor.xPos(aBlocker, xBlocker); + Actor.yPos(aBlocker, yBlocker); +} + +/* +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); +} +*/ + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); +} + diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql new file mode 100644 index 00000000..6a9f106c --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/queries/csQueriesStrategyHints.vql @@ -0,0 +1,646 @@ +package queries + +import "http://www.example.com/crossingScenario" +import "http://www.eclipse.org/emf/2002/Ecore" + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Lane+Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////////Actor (a) on vertical lane (l) must have a.xPos=[l.rc, l.rc + l.nw] +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnVerticalLane(a : Actor, vl:Lane_Vertical) { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); + check(x <= r); +} or { + Actor.placedOn(a, vl); + Actor.xPos(a, x); + Lane.referenceCoord(vl, r); +// //<<<>>> +// Lane.numWidth(vl, w); +// check(x >= (r + w)); + + //<<<>>>: lanes all have width=3 + check(x >= (r + 3.0)); +} + +@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes") +pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); + check(y <= r); +} or { + Actor.placedOn(a, hl); + Actor.yPos(a, y); + Lane.referenceCoord(hl, r); +// //<> +// Lane.numWidth(hl, w); +// check(y >= (r + w)); + + //<>: lanes all have width=3 + check(y >= (r + 3.0)); + +} + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Actor +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +/////---------------- +//Xpos and Ypos Bounds +/////---------------- + +private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, + xMax:java Double, xP:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.xSize(cs, xMax); + Actor.xPos(a, xP); +} + +private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, + yMax:java Double, yP:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.ySize(cs, yMax); + Actor.yPos(a, yP); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP >= xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXAndBounds(cs, a, xMax, xP); + check(xP <= 0-xMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP >= yMax);} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { + find helper_vert_getYAndBounds(cs, a, yMax, yP); + check(yP <= 0-yMax);} + +////////////ADDED +//to reduce overlap +//NEEDED + +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_actor_wrtLane(a:Actor) { + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yP); + check(yP > 0.0-1.0); +} or { + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xP); + check(xP > 0.0-1.0); +} + +////////////ADDED + +//Minimum Distances +private pattern helper_getCoords(a1:Actor, + a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); +} + +//INFO may remove? +@Constraint(severity="error", key={a1, a2}, message="x") +pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + a1 != a2; + //check(dx^2 + dy^2 < 3^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); +} + +/////---------------- +//Xspeed and Yspeed bounds +/////---------------- + +/////////VERTICAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0.0); +} + +private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, + ySpeedMax:java Double, ySpeed:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxYSpeed(cs, ySpeedMax); + Actor.ySpeed(a, ySpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS <= 0.0-ySMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS >= ySMax); +} + +/////////HORIZONTAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0.0); +} + +private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, + xSpeedMax:java Double, xSpeed:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxXSpeed(cs, xSpeedMax); + Actor.xSpeed(a, xSpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS <= 0.0-xSMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS >= xSMax); +} + +/////---------------- +/////WIDTH and LENGTH +/////---------------- + +///////pedestrian-width (3) +@Constraint(severity="error", key={p}, message="3 Actor") +pattern define_actor_pedestrianWidth(p:Pedestrian) { + Pedestrian.width(p, w); + check(w != 1.0); +} + +/////////pedestrian-width (4) +@Constraint(severity="error", key={p}, message="4 Actor") +pattern define_actor_pedestrianLength(p:Pedestrian) { + Pedestrian.length(p, l); + check(l != 1.0); +} + +/////////actor-width (5) +@Constraint(severity="error", key={v}, message="5 Actor") +pattern define_actor_vehicleWidth(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.width(v, w); + check(w != 2.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.width(v, w); + check(w != 3.0); +} + +/////////actor-width (6) +@Constraint(severity="error", key={v}, message="6 Actor") +pattern define_actor_vehicleLength(v:Vehicle) { + Vehicle.placedOn(v, lane); + Lane_Vertical(lane); + Vehicle.length(v, l); + check(l != 3.0); +} or { + Vehicle.placedOn(v, lane); + Lane_Horizontal(lane); + Vehicle.length(v, l); + check(l != 2.0); +} + +/////---------------- +/////DERIVED FEATURES +/////---------------- +/* +@QueryBasedFeature +pattern dist_near(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 < 10^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); + Actor.dist_near(a1, a2); +} + +@QueryBasedFeature +pattern dist_med(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(10^2 < dx^2 + dy^2 < 15^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); + Actor.dist_med(a1, a2); +} + +@QueryBasedFeature +pattern dist_far(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 > 20^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); + Actor.dist_far(a1, a2); +} +*/ +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//Relation +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +//@Constraint(severity="error", key={a1, a2}, message="1 Relation") +//pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { +// Relation.source(r, a1); +// Relation.target(r, a2); +// a1 == a2; +//} + +//TODO do above but transitively?/ +//////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//CollisionExists +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + + +//<> + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} + +//<> + + +//// +//CollisionExists - Time +//// + + +@Constraint(severity="error", key={c}, message="x") +pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { + CrossingScenario.relations(ss, c); + CrossingScenario.maxTime(ss, maxTime); + CollisionExists.collisionTime(c, cTime); + check(cTime >= maxTime);} + +@Constraint(severity="error", key={c}, message="x") +pattern collisionExists_timeNotNegative(c:CollisionExists) { + CollisionExists. collisionTime(c, cTime); + check(cTime <= 0.0);} + +//// +//CollisionExists - Physical Positioniung +//// + +private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + CollisionExists. collisionTime(c, cTime); +} + +private pattern helper_getYCoords(a:Actor, l:java Double, + yPos:java Double, ySpeed:java Double) { + + Actor.length(a, l); + Actor.yPos(a, yPos); + Actor.ySpeed(a, ySpeed); +} + +private pattern helper_getAllYCoords(a1:Actor, a2: Actor, + l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, + ySpeed1:java Double, ySpeed2:java Double) { + + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + find helper_getYCoords(a1, l1, yPos1, ySpeed1); + find helper_getYCoords(a2, l2, yPos2, ySpeed2); +} + +private pattern helper_getXCoords(a:Actor, w:java Double, + xPos:java Double, xSpeed:java Double) { + + Actor.width(a, w); + Actor.xPos(a, xPos); + Actor.xSpeed(a, xSpeed); +} + +private pattern helper_getAllXCoords(a1:Actor, a2: Actor, + w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, + xSpeed1:java Double, xSpeed2:java Double) { + + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + find helper_getXCoords(a1, w1, xPos1, xSpeed1); + find helper_getXCoords(a2, w2, xPos2, xSpeed2); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor) { + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); + + //check(y_1_bottom > y_2_top + check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllYCoords(a1, a2, l1, l2, yPos1, yPos2, ySpeed1, ySpeed2); + + //check(y_1_top < y_2_bottom) + check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + + //check(x_1_left > x_2_right) + check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + + find helper_getCollExistsTime(a1, a2, cTime); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + + //check(x_1_right < x_2_left) + check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); +} + + +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +//VisionBlocked +///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// + +//<> +/* +@Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") +pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} or { + VisionBlocked.source(vb, a1); + VisionBlocked.blockedBy(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} or { + VisionBlocked.blockedBy(vb, a1); + VisionBlocked.target(vb, a2); + Actor.placedOn(a1, l); + Actor.placedOn(a2, l); +} +*/ + +@Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") +pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} + + +////////////ADDED +//to make decision for ITE +//NOT NEEDED +/* +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_vb_blvssrc(a:Actor) { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yPa); + Actor.yPos(b, yPb); + check(yPb <= yPa); +} or { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xPa); + Actor.xPos(a, xPb); + check(xPb <= xPa); +} +*/ +////////////ADDED +//<> + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, a2); +} or { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, a1); +} + +@Constraint(severity="error", key={a1, vb}, message="x") +pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocked) { + //REQUIRED to avoid division by 0 in next 2 queries + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + + Actor.xPos(a1, x1); + Actor.xPos(a2, x2); + + //check(slope of a1-to-BlockerTop < slope of a1-to-a2) + check(x1 == x2); +} + +private pattern helper_VB_getAllCoords(a1:Actor, a2: Actor, + x1:java Double, y1:java Double, + x2:java Double, y2:java Double, + xBlocker:java Double, yBlocker:java Double, + lenBlocker:java Double, widBlocker:java Double) { + + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); + Actor.xPos(aBlocker, xBlocker); + Actor.yPos(aBlocker, yBlocker); + Actor.length(aBlocker, lenBlocker); + Actor.width(aBlocker, widBlocker); +} + +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ites_top(a1:Actor, a2:Actor) { + + find helper_VB_getAllCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); + + //check(slope of a1-to-BlockerTop < slope of a1-to-a2) + check( + ( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / + ( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2})) + < ((y1-y2)/(x1-x2))); +} + + +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { + + find helper_VB_getAllCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker, lenBlocker, widBlocker); + + //check(slope of a1-to-BlockerBottom > slope of a1-to-a2) + check( + ( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / + ( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2})) + > ((y1-y2)/(x1-x2))); +} + +/////// +//BLOCKER IN BETWEEN +/////// + +private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, + x1:java Double, y1:java Double, + x2:java Double, y2:java Double, + xBlocker:java Double, yBlocker:java Double) { + + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.yPos(a1, y1); + Actor.xPos(a2, x2); + Actor.yPos(a2, y2); + Actor.xPos(aBlocker, xBlocker); + Actor.yPos(aBlocker, yBlocker); +} + +/* +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((x1-xBlocker)*(x1-xBlocker) + (y1-yBlocker)*(y1-yBlocker) > (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, y1, x2, y2, xBlocker, yBlocker); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); +} +*/ + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); +} + diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh new file mode 100755 index 00000000..8a6a30be --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenario.sh @@ -0,0 +1,21 @@ +#!/usr/bin/bash +NODE="$1" +./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 4 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns z3 -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 6 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 12 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 15 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 16 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 18 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 + +./run.sh "${NODE}" -d CrossScenario -lb 8 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 20 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 + +./run.sh "${NODE}" -d CrossScenario -lb 21 -nm 1 -nr 10 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 9 -nm 1 -nr 10 -rt 300 -ns z3 -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 + diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh new file mode 100755 index 00000000..5ceda582 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runCrossScenarioStrategy.sh @@ -0,0 +1,15 @@ +#!/usr/bin/bash +NODE="$1" +./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 + +./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 +./run.sh "${NODE}" -d StrategyNo -lb 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 + +./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 +./run.sh "${NODE}" -d StrategyNo -lb 1 -ub 1 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 + +./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 +./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 + +./run.sh "${NODE}" -d StrategyNoWithHints -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d StrategyNo -lb 0 -nr 10 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 diff --git a/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh new file mode 100755 index 00000000..64a72200 --- /dev/null +++ b/Tests/MODELS2020-CaseStudies/case.study.pledge.run/runTestCrossScenario.sh @@ -0,0 +1,11 @@ +#!/usr/bin/bash +NODE="$1" + +./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns z3 -drto 300000 +./run.sh "${NODE}" -d CrossScenario -lb 3 -nm 1 -nr 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 + +./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns z3 -drto 2000 +./run.sh "${NODE}" -d CrossScenario -lb 300 -nm 1 -nr 1 -rt 10 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 2000 + +./run.sh "${NODE}" -d StrategyYes -lb 0 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 300000 +./run.sh "${NODE}" -d StrategyNoWithHints -lb 1 -ub 1 -nr 1 -nm 1 -rt 300 -ns dreal -drp /home/models/dreal4/bazel-bin/dreal/dreal -drto 10000 \ No newline at end of file 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 eddb8bb5..78d86504 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 @@ -39,6 +39,7 @@ class RunGeneratorConfig { static var RUNTIME = 1500 static var NUM_SOLVER = "z3" static var DREAL_PATH = "" + static var DREAL_TIMEOUT = "-2" // static var SCOPE_PROPAGATOR = "typeHierarchy" static var DOMAIN = "FamilyTree" // "FamilyTree", "Satellite", "Taxation" @@ -75,6 +76,9 @@ class RunGeneratorConfig { val drp = new Option("drp", "drealPath", true, "path to dreal executeable") options.addOption(drp) + val drto = new Option("drto", "drealTimeout", true, "drealTimeout") + options.addOption(drto) + // val sp = new Option("sp", "scopePropagator", true, "scope Propagator") // options.addOption(sp) // @@ -82,7 +86,7 @@ class RunGeneratorConfig { options.addOption(d) val hh = new Option("hh", "household", true, "number of households") - options.addOption(hh) + options.addOption(hh) val CommandLineParser parser = new BasicParser val formatter = new HelpFormatter() @@ -110,6 +114,8 @@ class RunGeneratorConfig { if(nsIn !== null && nsIn.equals("dreal")) NUM_SOLVER = "dreal-local" val drpIn = cmd.getOptionValue("drealPath") if(drpIn !== null) DREAL_PATH = drpIn + val drtoIn = cmd.getOptionValue("drealTimeout") + if(drtoIn !== null) DREAL_TIMEOUT = drtoIn // val spIn = cmd.getOptionValue("scopePropagator") // if(spIn !== null ) SCOPE_PROPAGATOR = spIn val dIn = cmd.getOptionValue("domain") @@ -136,14 +142,16 @@ class RunGeneratorConfig { ", SIZE=" + SIZE_LB + "to" + SIZE_UB + ", Runs=" + RUNS + ", ModelsPerRun=" + MODELS + - ", Runtime=" + RUNTIME + ">>") + ", Runtime=" + RUNTIME + + ", dreal-timeout=" + DREAL_TIMEOUT + ">>") if (isTaxation) println("<>") var naming = DOMAIN + "/size" + toStr(SIZE_LB) + "to" + toStr(SIZE_UB) + "r" + RUNS + "n" + MODELS + "rt" + RUNTIME + - "ns" + NUM_SOLVER + "ns" + NUM_SOLVER + + "drto" + DREAL_TIMEOUT if (isTaxation) naming = naming + "hh" + HOUSEHOLD val outputPath = "measurements/" + "models/" + naming + "_" + formattedDate val debugPath = "measurements/" + "debug/" + naming + "_" + formattedDate @@ -211,6 +219,10 @@ class RunGeneratorConfig { numSolverEntry.value = NUM_SOLVER val drealPathEntry = configScope.entries.get(2) as CustomEntry drealPathEntry.value = DREAL_PATH + if (DREAL_TIMEOUT != "-2") { + val drealTimeoutEntry = configScope.entries.get(3) as CustomEntry + drealTimeoutEntry.value = DREAL_TIMEOUT + } // val scopePropEntry = configScope.entries.get(3) as CustomEntry // scopePropEntry.value = SCOPE_PROPAGATOR -- cgit v1.2.3-54-g00ecf