From 6ac7f9bb5a9e8c2e98960cd56ca083741a709f3f Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Sun, 17 Jan 2021 03:13:47 -0500 Subject: add some actor-related queries, solve minor Z3 issue --- .../inputs/crossingScenarioGen.vsconfig | 4 +- .../queries/crossingScenarioQueries.vql | 166 +++++++++++++-------- .../src/crossingScenario/run/QueryDebug.java | 34 ++++- .../viatra2logic/NumericZ3ProblemSolver.java | 18 ++- 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 = {}, - # = 20..25//, - //# = 1..10, + # = 10..25, + # = 10..25//, //# = 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 @@ -10,6 +10,14 @@ import "http://www.eclipse.org/emf/2002/Ecore" // check(w <= 0-10.0); //} +////////////// +//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); -- cgit v1.2.3-54-g00ecf