From 4f0a474f5284bc97e9f509563d865424068b96fc Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Tue, 16 Feb 2021 00:55:15 +0100 Subject: Minor adjsutments to CrossScen ad FamTree local case studies --- Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig | 10 ++++++---- Domains/crossingScenario/inputs/csGenScale.vsconfig | 2 +- Domains/crossingScenario/plugin.xml | 11 ++++------- Domains/crossingScenario/queries/crossingScenarioQueries.vql | 4 ++++ .../src/crossingScenario/run/CrossingScenarioMain.java | 1 + .../case.study.familyTree.run/inputs/familytreeGen.vsconfig | 8 +++++--- .../case.study.familyTree.run/plugin.xml | 2 +- 7 files changed, 22 insertions(+), 16 deletions(-) diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig index 8ce9f6ee..db00ed7b 100644 --- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig +++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig @@ -21,7 +21,8 @@ generate { runtime = 10000, log-level = none, "numeric-solver" = "dreal-local", - "dreal-local-path" = "../../Solvers/dreal4/bazel-bin/dreal/dreal", + "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", + "strategy" = "crossingScenario", "ignored-attributes" = " Pedestrian.xPos=*, Pedestrian.yPos=*, @@ -35,11 +36,12 @@ generate { Vehicle.width=*, Vehicle.xSpeed=*, Vehicle.ySpeed=*, - CollisionExists.collisionTime=*", - "scopePropagator" = "polyhedral"} + CollisionExists.collisionTime=*" + //,"scopePropagator" = "polyhedral" + } runs = 1 - number = 3 + number = 1 debug = "outputs/debug" log = "outputs/debug/log.txt" output = "outputs/models" diff --git a/Domains/crossingScenario/inputs/csGenScale.vsconfig b/Domains/crossingScenario/inputs/csGenScale.vsconfig index d770986b..9ff2a10c 100644 --- a/Domains/crossingScenario/inputs/csGenScale.vsconfig +++ b/Domains/crossingScenario/inputs/csGenScale.vsconfig @@ -7,7 +7,7 @@ generate { partial-model = { "inputs/csInitScale.xmi"} solver = ViatraSolver scope = { - #node += 15..* + #node += 3..* ,# += 0 ,# += 0 //,# = 1 diff --git a/Domains/crossingScenario/plugin.xml b/Domains/crossingScenario/plugin.xml index 8e759f1f..c8846e1b 100644 --- a/Domains/crossingScenario/plugin.xml +++ b/Domains/crossingScenario/plugin.xml @@ -1,10 +1,7 @@ - - - - + + + + diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 0a28d774..5f35cd2b 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql @@ -94,6 +94,7 @@ pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { ////////////ADDED //to reduce overlap //NEEDED +/* @Constraint(severity="error", key={a}, message="5 Actor") pattern define_actor_wrtLane(a:Actor) { Actor.placedOn(a, lane); @@ -106,6 +107,7 @@ pattern define_actor_wrtLane(a:Actor) { Actor.xPos(a, xP); check(xP > 0.0-1.0); } +*/ ////////////ADDED //Minimum Distances @@ -437,6 +439,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { 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); @@ -453,6 +456,7 @@ pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { Actor.placedOn(a2, hl2); Lane_Horizontal(hl2); } +*/ ////////////ADDED //to make decision for ITE diff --git a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java index ad2c6d88..271a1cfb 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java +++ b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java @@ -24,6 +24,7 @@ public class CrossingScenarioMain { // Thread.sleep(2000); // System.out.println(System.getProperty("java.library.path")); // System.loadLibrary("z3java"); +// String errorMessages = StandaloneScriptExecutor.executeScript("inputs/csGenScale.vsconfig"); String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig"); if (errorMessages != null) { System.out.println(errorMessages); diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig index 7ead54af..bae32fca 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/inputs/familytreeGen.vsconfig @@ -12,9 +12,11 @@ generate { config = { runtime = 10000, - log-level = normal, - "numeric-solver" = "dreal", - "scopePropagator" = "typeHierarchy" + log-level = full, + "numeric-solver" = "dreal-local", + "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", + "scopePropagator" = "typeHierarchy", + "strategy" = "crossingScenario" } runs = 1 diff --git a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml index 2f4febdb..c760d4ef 100644 --- a/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml +++ b/Tests/MODELS2020-CaseStudies/case.study.familyTree.run/plugin.xml @@ -1 +1 @@ - + -- cgit v1.2.3-54-g00ecf