diff options
author | 2021-02-16 00:55:15 +0100 | |
---|---|---|
committer | 2021-02-16 00:55:15 +0100 | |
commit | 4f0a474f5284bc97e9f509563d865424068b96fc (patch) | |
tree | c99585c30dc85ac0bc2944b807a9dae988c8f363 /Domains/crossingScenario | |
parent | fix dreal call on solved problem imprecision issue (diff) | |
download | VIATRA-Generator-4f0a474f5284bc97e9f509563d865424068b96fc.tar.gz VIATRA-Generator-4f0a474f5284bc97e9f509563d865424068b96fc.tar.zst VIATRA-Generator-4f0a474f5284bc97e9f509563d865424068b96fc.zip |
Minor adjsutments to CrossScen ad FamTree local case studies
Diffstat (limited to 'Domains/crossingScenario')
5 files changed, 16 insertions, 12 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 { | |||
21 | runtime = 10000, | 21 | runtime = 10000, |
22 | log-level = none, | 22 | log-level = none, |
23 | "numeric-solver" = "dreal-local", | 23 | "numeric-solver" = "dreal-local", |
24 | "dreal-local-path" = "../../Solvers/dreal4/bazel-bin/dreal/dreal", | 24 | "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", |
25 | "strategy" = "crossingScenario", | ||
25 | "ignored-attributes" = " | 26 | "ignored-attributes" = " |
26 | Pedestrian.xPos=*, | 27 | Pedestrian.xPos=*, |
27 | Pedestrian.yPos=*, | 28 | Pedestrian.yPos=*, |
@@ -35,11 +36,12 @@ generate { | |||
35 | Vehicle.width=*, | 36 | Vehicle.width=*, |
36 | Vehicle.xSpeed=*, | 37 | Vehicle.xSpeed=*, |
37 | Vehicle.ySpeed=*, | 38 | Vehicle.ySpeed=*, |
38 | CollisionExists.collisionTime=*", | 39 | CollisionExists.collisionTime=*" |
39 | "scopePropagator" = "polyhedral"} | 40 | //,"scopePropagator" = "polyhedral" |
41 | } | ||
40 | 42 | ||
41 | runs = 1 | 43 | runs = 1 |
42 | number = 3 | 44 | number = 1 |
43 | debug = "outputs/debug" | 45 | debug = "outputs/debug" |
44 | log = "outputs/debug/log.txt" | 46 | log = "outputs/debug/log.txt" |
45 | output = "outputs/models" | 47 | 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 { | |||
7 | partial-model = { "inputs/csInitScale.xmi"} | 7 | partial-model = { "inputs/csInitScale.xmi"} |
8 | solver = ViatraSolver | 8 | solver = ViatraSolver |
9 | scope = { | 9 | scope = { |
10 | #node += 15..* | 10 | #node += 3..* |
11 | ,#<Lane> += 0 | 11 | ,#<Lane> += 0 |
12 | ,#<Relation> += 0 | 12 | ,#<Relation> += 0 |
13 | //,#<CollisionExists> = 1 | 13 | //,#<CollisionExists> = 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 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- | 1 | <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!-- |
2 | --><plugin> | 2 | --><plugin> |
3 | <extension point="org.eclipse.emf.ecore.generated_package"> | 3 | <extension point="org.eclipse.emf.ecore.generated_package"> |
4 | <!-- @generated crossingScenario --> | 4 | <!-- @generated crossingScenario --> |
5 | <package | 5 | <package class="crossingScenario.CrossingScenarioPackage" genModel="model/crossingScenario.genmodel" uri="http://www.example.com/crossingScenario"/> |
6 | uri="http://www.example.com/crossingScenario" | 6 | </extension> |
7 | class="crossingScenario.CrossingScenarioPackage" | ||
8 | genModel="model/crossingScenario.genmodel"/> | ||
9 | </extension> | ||
10 | </plugin> | 7 | </plugin> |
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) { | |||
94 | ////////////ADDED | 94 | ////////////ADDED |
95 | //to reduce overlap | 95 | //to reduce overlap |
96 | //NEEDED | 96 | //NEEDED |
97 | /* | ||
97 | @Constraint(severity="error", key={a}, message="5 Actor") | 98 | @Constraint(severity="error", key={a}, message="5 Actor") |
98 | pattern define_actor_wrtLane(a:Actor) { | 99 | pattern define_actor_wrtLane(a:Actor) { |
99 | Actor.placedOn(a, lane); | 100 | Actor.placedOn(a, lane); |
@@ -106,6 +107,7 @@ pattern define_actor_wrtLane(a:Actor) { | |||
106 | Actor.xPos(a, xP); | 107 | Actor.xPos(a, xP); |
107 | check(xP > 0.0-1.0); | 108 | check(xP > 0.0-1.0); |
108 | } | 109 | } |
110 | */ | ||
109 | ////////////ADDED | 111 | ////////////ADDED |
110 | 112 | ||
111 | //Minimum Distances | 113 | //Minimum Distances |
@@ -437,6 +439,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { | |||
437 | Actor.placedOn(a2, l); | 439 | Actor.placedOn(a2, l); |
438 | } | 440 | } |
439 | */ | 441 | */ |
442 | /* | ||
440 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") | 443 | @Constraint(severity="error", key={a1, a2}, message="on lanes with different orientation") |
441 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | 444 | pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { |
442 | VisionBlocked.source(ce, a1); | 445 | VisionBlocked.source(ce, a1); |
@@ -453,6 +456,7 @@ pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { | |||
453 | Actor.placedOn(a2, hl2); | 456 | Actor.placedOn(a2, hl2); |
454 | Lane_Horizontal(hl2); | 457 | Lane_Horizontal(hl2); |
455 | } | 458 | } |
459 | */ | ||
456 | 460 | ||
457 | ////////////ADDED | 461 | ////////////ADDED |
458 | //to make decision for ITE | 462 | //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 { | |||
24 | // Thread.sleep(2000); | 24 | // Thread.sleep(2000); |
25 | // System.out.println(System.getProperty("java.library.path")); | 25 | // System.out.println(System.getProperty("java.library.path")); |
26 | // System.loadLibrary("z3java"); | 26 | // System.loadLibrary("z3java"); |
27 | // String errorMessages = StandaloneScriptExecutor.executeScript("inputs/csGenScale.vsconfig"); | ||
27 | String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig"); | 28 | String errorMessages = StandaloneScriptExecutor.executeScript("inputs/crossingScenarioGen.vsconfig"); |
28 | if (errorMessages != null) { | 29 | if (errorMessages != null) { |
29 | System.out.println(errorMessages); | 30 | System.out.println(errorMessages); |