add some actor-related queries, solve minor Z3 issue

4 files changed, 154 insertions, 68 deletions

diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
index b216ed3f..c79c5775 100644
--- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
+++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig
@@ -9,8 +9,8 @@ generate {
         scope = {

                 #node = 15..100,

                 #int = {},

-                #<Lane> = 20..25//,

-                //#<Actor> = 1..10,

+                #<Lane> = 10..25,

+                #<Actor> = 10..25//,

                 //#<Relation> = 1..10

                 }

         

diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
index ee7c0b34..352c77c0 100644
--- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql
+++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql
@@ -11,6 +11,14 @@ import "http://www.eclipse.org/emf/2002/Ecore"
 //}
 
 //////////////
+//CrossingScenario
+/////////////
+
+//TODO Hard-code xSize?
+//TODO Hard-code ySize?
+//TODO Hard-code maxTime?
+
+//////////////
 //Lane
 //////////////
 
@@ -154,71 +162,103 @@ pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) {
 //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));
+}
 
-////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for vertical lanes")
-////pattern actorOnVerticalLane(a : Actor) {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Vertical);
-////    Actor.xPos(a, x);
-////    Lane.referenceCoord(l, r);
-////    check(x <= r);
-////} or {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Vertical);
-////    Actor.xPos(a, x);
-////    Lane.referenceCoord(l, r);
-////    Lane.numWidth(l, w);
-////    check(x >= (r + w));
-////}
-////
-////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation for horizontal lanes")
-////pattern actorOnHorizontalLane(a : Actor) {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Horizontal);
-////    Actor.yPos(a, y);
-////    Lane.referenceCoord(l, r);
-////    check(y <= r);
-////} or {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Horizontal);
-////    Actor.yPos(a, y);
-////    Lane.referenceCoord(l, r);
-////    Lane.numWidth(l, w);
-////    check(y >= (r + w));
-////}
-//
-////@Constraint(severity = "error", key = {a}, message = "this defines the placedOn relation")
-////pattern actorOnLane(a : Actor) {
-////    find actorOnVerticalLane(a);
-//////  neg find actorOnHorizontalLane(a);
-////}
-////
-////private pattern actorOnVerticalLane(a : Actor) {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Vertical);
-////    Actor.xPos(a, x);
-////    Lane.referenceCoord(l, r);
-////    Lane.numWidth(l, w);
-////    check(x >= r);
-////    check(x <= (r + w));
-////}
-//
-////@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
-////pattern widthSpec(l : Lane) {
-////    Lane.numWidth(l, w);
-////    check(w != 5);
-////}
-//
-////private pattern actorOnHorizontalLane(a : Actor) {
-////    Actor.placedOn(a, l);
-////    Lane.orientation(l, Orientation::Vertical);
-////    Actor.yPos(a, y);
-////    Lane.referenceCoord(l, r);
-////    Lane.widthNum(l, w);
-////    check(y >= r);
-////    check(y <= (r + w));
-////}
+@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));
+}
+
+//////////////
+//Actor
+//////////////
+
+////TODO
+/////////xPos of every actor mmust be within bounds defined in CS
+//@Constraint(severity="error", key={l}, message="1 Actor")
+//pattern define_actor_xPosWithinCSbounds(cs:CrossingScenario, a:Actor) {
+//      
+//}
 //
+////TODO
+/////////yPos of every actor mmust be within bounds defined in CS
+//@Constraint(severity="error", key={l}, message="2 Actor")
+//pattern define_actor_yPosWithinCSbounds(cs:CrossingScenario, a:Actor) {
+//      
+//}
+
+
+/////////pedestrian-width (3)
+pattern define_actor_pedestrianWidth(p:Pedestrian) {
+    Pedestrian.width(p, 1.0);
+}
+
+/////////pedestrian-width (4)
+pattern define_actor_pedestrianLength(p:Pedestrian) {
+    Pedestrian.length(p, 1.0);
+}
+
+/////////actor-width (5)
+pattern define_actor_actorWidth(a:Actor) {
+        Actor.placedOn(a, l);
+        Lane_Vertical(l);
+    Actor.width(p, 1.0);
+} or {
+        Actor.placedOn(a, l);
+        Lane_Horizontal(l);
+    Actor.width(p, 3.0);
+}
+
+/////////actor-width (6)
+pattern define_actor_actorLength(a:Actor) {
+        Actor.placedOn(a, l);
+        Lane_Vertical(l);
+    Actor.length(p, 3.0);
+} or {
+        Actor.placedOn(a, l);
+        Lane_Horizontal(l);
+    Actor.length(p, 1.0);
+}
+
+
+/////////xSpeed of actor on verticalLane is 0
+@Constraint(severity="error", key={a}, message="7 Actor")
+pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor, vl:Lane_Vertical) {
+        Actor.placedOn(a, vl);
+    Actor.xSpeed(a, xSpeed);
+    check(xSpeed != 0);
+}
+
+/////////ySpeed of actor on horizontalLane is 0
+@Constraint(severity="error", key={a}, message="8 Actor")
+pattern define_actor_actorOnHoriLaneHasySpeed0(a:Actor, hl:Lane_Horizontal) {
+        Actor.placedOn(a, hl);
+    Actor.ySpeed(a, ySpeed);
+    check(ySpeed != 0);
+}
+
 ////////////////
 ////CollisionExists
 ////////////////
diff --git a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java
index 9f9b939b..51ace4b8 100644
--- a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java
+++ b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java
@@ -16,14 +16,16 @@ import org.eclipse.emf.ecore.resource.ResourceSet;
 import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl;

 import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl;

 

+import crossingScenario.Actor;

 import crossingScenario.CrossingScenario;

 import crossingScenario.CrossingScenarioPackage;

 import crossingScenario.Lane;

 

 public class QueryDebug {

         public static void main(String[] args) throws FileNotFoundException {

-//              checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf");

-                testOnInstance();

+                checkPrevLanes("outputs/models/1.xmi", "outputs/simplePrevLane.tgf");

+//              testOnInstance();

+//              miniRETest("21/2");

         }

         

         public static void checkPrevLanes(String pathSrc, String pathTgt) throws FileNotFoundException {

@@ -35,6 +37,12 @@ public class QueryDebug {
                 PrintWriter printer = new PrintWriter(pathTgt);

                 

                 CrossingScenario cs = ((CrossingScenario) res.getContents().get(0));

+                

+                for (Actor o : cs.getActors()) {

+                        String nodeName = "(" + o.getXPos()+","+o.getYPos() + ")";

+                        printer.println(o.hashCode() + " " + nodeName);

+                }

+                

                 for (Lane o : cs.getLanes()) {

                         String prefix = "";

                         if (cs.getHorizontal_head().equals(o) || cs.getVertical_head().equals(o)) {

@@ -53,6 +61,13 @@ public class QueryDebug {
                                 printer.println(curName + " " + curPrev + " " + edgeLabel);

                         }

                 }

+                

+                for (Actor o : cs.getActors()) {

+                        int actName = o.hashCode();

+                        int lanName = o.getPlacedOn().hashCode();

+                        printer.println(actName + " " + lanName );

+                }

+                

                 printer.flush();

                 printer.close();

                 System.out.println("TGF CREATED");

@@ -168,5 +183,20 @@ public class QueryDebug {
                 }

                 return res;

         }

+        

+        public static void miniRETest(String in) {

+                Double oSol = 0.0;

+                String re = "([0-9]+)/([0-9]+)";

+                Pattern p = Pattern.compile(re);

+                Matcher ma = p.matcher(in);

+                if (ma.matches()) {

+                        int numerator = Integer.parseInt(ma.group(1));

+                        int denominator = Integer.parseInt(ma.group(2));

+                        oSol = (double) numerator / denominator;

+                        System.out.println(oSol);

+                } else {

+                        System.err.println("Problem converting string: " + in);

+                }

+        }

 

 }

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 db33804e..0b093859 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
@@ -4,6 +4,8 @@ import java.util.ArrayList;
 import java.util.HashMap;

 import java.util.List;

 import java.util.Map;

+import java.util.regex.Matcher;

+import java.util.regex.Pattern;

 

 import org.eclipse.xtext.common.types.JvmIdentifiableElement;

 import org.eclipse.xtext.xbase.XBinaryOperation;

@@ -98,7 +100,21 @@ public class NumericZ3ProblemSolver extends NumericProblemSolver{
                                                 sol.put(o, oSol);

                                         } else {

                                                 RealExpr val = (RealExpr) m.evaluate(varMap.get(o), false);

-                                                Double oSol = Double.parseDouble(val.toString());

+                                                Double oSol = 0.0;

+                                                if (val.toString().contains("/")) {

+                                                        String re = "([0-9]+)/([0-9]+)";

+                                                        Pattern p = Pattern.compile(re);

+                                                        Matcher ma = p.matcher(val.toString());

+                                                        if (ma.matches()) {

+                                                                int numerator = Integer.parseInt(ma.group(1));

+                                                                int denominator = Integer.parseInt(ma.group(2));

+                                                                oSol = (double) numerator / denominator;

+                                                        } else {

+                                                                System.err.println("Problem converting string: " + val.toString());

+                                                        }

+                                                } else {

+                                                        oSol = Double.parseDouble(val.toString());

+                                                }

                                                 sol.put(o, oSol);

                                         }

                                         //System.out.println("Solution:" + o + "->" + oSol);