Minor adjsutments to CrossScen ad FamTree local case studies

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..*

                 ,#<Lane> += 0

                 ,#<Relation> += 0

                 //,#<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 @@
 <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.0"?><!--
 --><plugin>
-   <extension point="org.eclipse.emf.ecore.generated_package">
-      <!-- @generated crossingScenario -->
-      <package
-            uri="http://www.example.com/crossingScenario"
-            class="crossingScenario.CrossingScenarioPackage"
-            genModel="model/crossingScenario.genmodel"/>
-   </extension>
+  <extension point="org.eclipse.emf.ecore.generated_package">
+    <!-- @generated crossingScenario -->
+    <package class="crossingScenario.CrossingScenarioPackage" genModel="model/crossingScenario.genmodel" uri="http://www.example.com/crossingScenario"/>
+  </extension>
 </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) {
 ////////////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 @@
-<?xml version="1.0" encoding="UTF-8"?><plugin/>

+<?xml version="1.0" encoding="UTF-8"?><plugin/>