From bb6fa1913dc4eb0e9d3bfd680797ee38c77e77c8 Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Fri, 22 Jan 2021 04:27:36 +0100 Subject: Issue where blocker is not between source and target --- .../crossingScenario/CrossingScenario.java | 48 ++++ .../crossingScenario/CrossingScenarioPackage.java | 58 ++++- .../impl/CrossingScenarioImpl.java | 112 +++++++++ .../impl/CrossingScenarioPackageImpl.java | 24 ++ Domains/crossingScenario/inputs/cSinit4x4.xmi | 7 +- .../inputs/crossingScenarioGen.vsconfig | 2 +- .../crossingScenario/model/crossingScenario.aird | 42 +++- .../crossingScenario/model/crossingScenario.ecore | 4 + .../model/crossingScenario.genmodel | 2 + .../queries/crossingScenarioQueries.vql | 280 +++++++++++++++------ .../src/crossingScenario/run/DrawScenario.java | 23 +- .../InstanceModel2PartialInterpretation.xtend | 13 +- 12 files changed, 506 insertions(+), 109 deletions(-) diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenario.java b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenario.java index 0e9f4981..0f8eb79b 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenario.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenario.java @@ -21,6 +21,8 @@ import org.eclipse.emf.ecore.EObject; *
  • {@link crossingScenario.CrossingScenario#getLanes Lanes}
    • *
  • {@link crossingScenario.CrossingScenario#getMaxTime Max Time}
    • *
  • {@link crossingScenario.CrossingScenario#getRelations Relations}
    • + *
  • {@link crossingScenario.CrossingScenario#getMaxXSpeed Max XSpeed}
    • + *
  • {@link crossingScenario.CrossingScenario#getMaxYSpeed Max YSpeed}
    • * * * @see crossingScenario.CrossingScenarioPackage#getCrossingScenario() @@ -130,4 +132,50 @@ public interface CrossingScenario extends EObject { */ EList getRelations(); + /** + * Returns the value of the 'Max XSpeed' attribute. + * The default value is "0.0". + * + * + * @return the value of the 'Max XSpeed' attribute. + * @see #setMaxXSpeed(double) + * @see crossingScenario.CrossingScenarioPackage#getCrossingScenario_MaxXSpeed() + * @model default="0.0" + * @generated + */ + double getMaxXSpeed(); + + /** + * Sets the value of the '{@link crossingScenario.CrossingScenario#getMaxXSpeed Max XSpeed}' attribute. + * + * + * @param value the new value of the 'Max XSpeed' attribute. + * @see #getMaxXSpeed() + * @generated + */ + void setMaxXSpeed(double value); + + /** + * Returns the value of the 'Max YSpeed' attribute. + * The default value is "0.0". + * + * + * @return the value of the 'Max YSpeed' attribute. + * @see #setMaxYSpeed(double) + * @see crossingScenario.CrossingScenarioPackage#getCrossingScenario_MaxYSpeed() + * @model default="0.0" + * @generated + */ + double getMaxYSpeed(); + + /** + * Sets the value of the '{@link crossingScenario.CrossingScenario#getMaxYSpeed Max YSpeed}' attribute. + * + * + * @param value the new value of the 'Max YSpeed' attribute. + * @see #getMaxYSpeed() + * @generated + */ + void setMaxYSpeed(double value); + } // CrossingScenario diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java index 45443103..bafc5e69 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java @@ -121,6 +121,24 @@ public interface CrossingScenarioPackage extends EPackage { */ int CROSSING_SCENARIO__RELATIONS = 5; + /** + * The feature id for the 'Max XSpeed' attribute. + * + * + * @generated + * @ordered + */ + int CROSSING_SCENARIO__MAX_XSPEED = 6; + + /** + * The feature id for the 'Max YSpeed' attribute. + * + * + * @generated + * @ordered + */ + int CROSSING_SCENARIO__MAX_YSPEED = 7; + /** * The number of structural features of the 'Crossing Scenario' class. * @@ -128,7 +146,7 @@ public interface CrossingScenarioPackage extends EPackage { * @generated * @ordered */ - int CROSSING_SCENARIO_FEATURE_COUNT = 6; + int CROSSING_SCENARIO_FEATURE_COUNT = 8; /** * The number of operations of the 'Crossing Scenario' class. @@ -1067,6 +1085,28 @@ public interface CrossingScenarioPackage extends EPackage { */ EReference getCrossingScenario_Relations(); + /** + * Returns the meta object for the attribute '{@link crossingScenario.CrossingScenario#getMaxXSpeed Max XSpeed}'. + * + * + * @return the meta object for the attribute 'Max XSpeed'. + * @see crossingScenario.CrossingScenario#getMaxXSpeed() + * @see #getCrossingScenario() + * @generated + */ + EAttribute getCrossingScenario_MaxXSpeed(); + + /** + * Returns the meta object for the attribute '{@link crossingScenario.CrossingScenario#getMaxYSpeed Max YSpeed}'. + * + * + * @return the meta object for the attribute 'Max YSpeed'. + * @see crossingScenario.CrossingScenario#getMaxYSpeed() + * @see #getCrossingScenario() + * @generated + */ + EAttribute getCrossingScenario_MaxYSpeed(); + /** * Returns the meta object for class '{@link crossingScenario.Lane Lane}'. * @@ -1475,6 +1515,22 @@ public interface CrossingScenarioPackage extends EPackage { */ EReference CROSSING_SCENARIO__RELATIONS = eINSTANCE.getCrossingScenario_Relations(); + /** + * The meta object literal for the 'Max XSpeed' attribute feature. + * + * + * @generated + */ + EAttribute CROSSING_SCENARIO__MAX_XSPEED = eINSTANCE.getCrossingScenario_MaxXSpeed(); + + /** + * The meta object literal for the 'Max YSpeed' attribute feature. + * + * + * @generated + */ + EAttribute CROSSING_SCENARIO__MAX_YSPEED = eINSTANCE.getCrossingScenario_MaxYSpeed(); + /** * The meta object literal for the '{@link crossingScenario.impl.LaneImpl Lane}' class. * diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioImpl.java b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioImpl.java index b2b0d579..28667b0c 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioImpl.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioImpl.java @@ -37,6 +37,8 @@ import org.eclipse.emf.ecore.util.InternalEList; *
  • {@link crossingScenario.impl.CrossingScenarioImpl#getLanes Lanes}
    • *
  • {@link crossingScenario.impl.CrossingScenarioImpl#getMaxTime Max Time}
    • *
  • {@link crossingScenario.impl.CrossingScenarioImpl#getRelations Relations}
    • + *
  • {@link crossingScenario.impl.CrossingScenarioImpl#getMaxXSpeed Max XSpeed}
    • + *
  • {@link crossingScenario.impl.CrossingScenarioImpl#getMaxYSpeed Max YSpeed}
    • * * * @generated @@ -132,6 +134,46 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement */ protected EList relations; + /** + * The default value of the '{@link #getMaxXSpeed() Max XSpeed}' attribute. + * + * + * @see #getMaxXSpeed() + * @generated + * @ordered + */ + protected static final double MAX_XSPEED_EDEFAULT = 0.0; + + /** + * The cached value of the '{@link #getMaxXSpeed() Max XSpeed}' attribute. + * + * + * @see #getMaxXSpeed() + * @generated + * @ordered + */ + protected double maxXSpeed = MAX_XSPEED_EDEFAULT; + + /** + * The default value of the '{@link #getMaxYSpeed() Max YSpeed}' attribute. + * + * + * @see #getMaxYSpeed() + * @generated + * @ordered + */ + protected static final double MAX_YSPEED_EDEFAULT = 0.0; + + /** + * The cached value of the '{@link #getMaxYSpeed() Max YSpeed}' attribute. + * + * + * @see #getMaxYSpeed() + * @generated + * @ordered + */ + protected double maxYSpeed = MAX_YSPEED_EDEFAULT; + /** * * @@ -259,6 +301,52 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement return relations; } + /** + * + * + * @generated + */ + @Override + public double getMaxXSpeed() { + return maxXSpeed; + } + + /** + * + * + * @generated + */ + @Override + public void setMaxXSpeed(double newMaxXSpeed) { + double oldMaxXSpeed = maxXSpeed; + maxXSpeed = newMaxXSpeed; + if (eNotificationRequired()) + eNotify(new ENotificationImpl(this, Notification.SET, CrossingScenarioPackage.CROSSING_SCENARIO__MAX_XSPEED, oldMaxXSpeed, maxXSpeed)); + } + + /** + * + * + * @generated + */ + @Override + public double getMaxYSpeed() { + return maxYSpeed; + } + + /** + * + * + * @generated + */ + @Override + public void setMaxYSpeed(double newMaxYSpeed) { + double oldMaxYSpeed = maxYSpeed; + maxYSpeed = newMaxYSpeed; + if (eNotificationRequired()) + eNotify(new ENotificationImpl(this, Notification.SET, CrossingScenarioPackage.CROSSING_SCENARIO__MAX_YSPEED, oldMaxYSpeed, maxYSpeed)); + } + /** * * @@ -297,6 +385,10 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement return getMaxTime(); case CrossingScenarioPackage.CROSSING_SCENARIO__RELATIONS: return getRelations(); + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_XSPEED: + return getMaxXSpeed(); + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_YSPEED: + return getMaxYSpeed(); } return super.eGet(featureID, resolve, coreType); } @@ -331,6 +423,12 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement getRelations().clear(); getRelations().addAll((Collection)newValue); return; + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_XSPEED: + setMaxXSpeed((Double)newValue); + return; + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_YSPEED: + setMaxYSpeed((Double)newValue); + return; } super.eSet(featureID, newValue); } @@ -361,6 +459,12 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement case CrossingScenarioPackage.CROSSING_SCENARIO__RELATIONS: getRelations().clear(); return; + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_XSPEED: + setMaxXSpeed(MAX_XSPEED_EDEFAULT); + return; + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_YSPEED: + setMaxYSpeed(MAX_YSPEED_EDEFAULT); + return; } super.eUnset(featureID); } @@ -385,6 +489,10 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement return maxTime != MAX_TIME_EDEFAULT; case CrossingScenarioPackage.CROSSING_SCENARIO__RELATIONS: return relations != null && !relations.isEmpty(); + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_XSPEED: + return maxXSpeed != MAX_XSPEED_EDEFAULT; + case CrossingScenarioPackage.CROSSING_SCENARIO__MAX_YSPEED: + return maxYSpeed != MAX_YSPEED_EDEFAULT; } return super.eIsSet(featureID); } @@ -405,6 +513,10 @@ public class CrossingScenarioImpl extends MinimalEObjectImpl.Container implement result.append(ySize); result.append(", maxTime: "); result.append(maxTime); + result.append(", maxXSpeed: "); + result.append(maxXSpeed); + result.append(", maxYSpeed: "); + result.append(maxYSpeed); result.append(')'); return result.toString(); } diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java index b8261c86..292fcb9c 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java @@ -271,6 +271,26 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin return (EReference)crossingScenarioEClass.getEStructuralFeatures().get(5); } + /** + * + * + * @generated + */ + @Override + public EAttribute getCrossingScenario_MaxXSpeed() { + return (EAttribute)crossingScenarioEClass.getEStructuralFeatures().get(6); + } + + /** + * + * + * @generated + */ + @Override + public EAttribute getCrossingScenario_MaxYSpeed() { + return (EAttribute)crossingScenarioEClass.getEStructuralFeatures().get(7); + } + /** * * @@ -617,6 +637,8 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin createEReference(crossingScenarioEClass, CROSSING_SCENARIO__LANES); createEAttribute(crossingScenarioEClass, CROSSING_SCENARIO__MAX_TIME); createEReference(crossingScenarioEClass, CROSSING_SCENARIO__RELATIONS); + createEAttribute(crossingScenarioEClass, CROSSING_SCENARIO__MAX_XSPEED); + createEAttribute(crossingScenarioEClass, CROSSING_SCENARIO__MAX_YSPEED); laneEClass = createEClass(LANE); createEAttribute(laneEClass, LANE__REFERENCE_COORD); @@ -712,6 +734,8 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin initEReference(getCrossingScenario_Lanes(), this.getLane(), null, "lanes", null, 0, -1, CrossingScenario.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); initEAttribute(getCrossingScenario_MaxTime(), ecorePackage.getEDouble(), "maxTime", null, 0, 1, CrossingScenario.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); initEReference(getCrossingScenario_Relations(), this.getRelation(), null, "relations", null, 0, -1, CrossingScenario.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, IS_COMPOSITE, !IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); + initEAttribute(getCrossingScenario_MaxXSpeed(), ecorePackage.getEDouble(), "maxXSpeed", "0.0", 0, 1, CrossingScenario.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); + initEAttribute(getCrossingScenario_MaxYSpeed(), ecorePackage.getEDouble(), "maxYSpeed", "0.0", 0, 1, CrossingScenario.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); initEClass(laneEClass, Lane.class, "Lane", IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS); initEAttribute(getLane_ReferenceCoord(), ecorePackage.getEDouble(), "referenceCoord", null, 1, 1, Lane.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); diff --git a/Domains/crossingScenario/inputs/cSinit4x4.xmi b/Domains/crossingScenario/inputs/cSinit4x4.xmi index dd9b41de..24c29774 100644 --- a/Domains/crossingScenario/inputs/cSinit4x4.xmi +++ b/Domains/crossingScenario/inputs/cSinit4x4.xmi @@ -7,7 +7,9 @@ xsi:schemaLocation="http://www.example.com/crossingScenario ../model/crossingScenario.ecore" xSize="100.0" ySize="100.0" - maxTime="60.0"> + maxTime="60.0" + maxXSpeed="100.0" + maxYSpeed="100.0"> @@ -24,4 +26,7 @@ referenceCoord="15.0"/> + diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig index bee56db6..1d47952d 100644 --- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig +++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig @@ -23,7 +23,7 @@ generate { log-level = none, "numeric-solver" = "dreal-local", "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", - "ignored-attributes" = "CrossingScenario.maxTime=60", + "ignored-attributes" = "CollisionExists.collisionTime=*", "scopePropagator" = "polyhedral"} runs = 1 diff --git a/Domains/crossingScenario/model/crossingScenario.aird b/Domains/crossingScenario/model/crossingScenario.aird index 0a776802..d4aa8c13 100644 --- a/Domains/crossingScenario/model/crossingScenario.aird +++ b/Domains/crossingScenario/model/crossingScenario.aird @@ -5,7 +5,7 @@ crossingScenario.genmodel - + @@ -76,11 +76,19 @@ + + + + + + + + - + @@ -394,7 +402,7 @@ - + @@ -410,7 +418,7 @@ - + @@ -421,7 +429,7 @@ - + @@ -614,7 +622,7 @@ - + @@ -693,7 +701,7 @@ - + @@ -717,7 +725,7 @@ - + @@ -792,7 +800,7 @@ KEEP_LOCATION KEEP_SIZE KEEP_RATIO - + @@ -820,6 +828,22 @@ + + + + + + + + + + + + + + + + diff --git a/Domains/crossingScenario/model/crossingScenario.ecore b/Domains/crossingScenario/model/crossingScenario.ecore index c1aab2b8..05dba008 100644 --- a/Domains/crossingScenario/model/crossingScenario.ecore +++ b/Domains/crossingScenario/model/crossingScenario.ecore @@ -12,6 +12,10 @@ + + + + diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 2b67e14c..d1c72820 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql @@ -223,17 +223,23 @@ pattern define_placedOn_actorOnHorizLane(a : Actor, hl:Lane_Horizontal) { //Actor ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// +/////---------------- //Xpos and Ypos Bounds +/////---------------- -private pattern helper_getXAndBounds(cs:CrossingScenario, a:Actor, +private pattern helper_horiz_getXAndBounds(cs:CrossingScenario, a:Actor, xMax:java Double, xP:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); CrossingScenario.actors(cs, a); CrossingScenario.xSize(cs, xMax); Actor.xPos(a, xP); } -private pattern helper_getYAndBounds(cs:CrossingScenario, a:Actor, +private pattern helper_vert_getYAndBounds(cs:CrossingScenario, a:Actor, yMax:java Double, yP:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); CrossingScenario.actors(cs, a); CrossingScenario.ySize(cs, yMax); Actor.yPos(a, yP); @@ -241,87 +247,109 @@ private pattern helper_getYAndBounds(cs:CrossingScenario, a:Actor, @Constraint(severity="error", key={cs}, message="x") pattern define_actor_maxXp(cs:CrossingScenario, a:Actor) { - Actor.placedOn(a, hl); - Lane_Horizontal(hl); - find helper_getXAndBounds(cs, a, xMax, xP); + find helper_horiz_getXAndBounds(cs, a, xMax, xP); check(xP >= xMax);} @Constraint(severity="error", key={cs}, message="x") pattern define_actor_minXp(cs:CrossingScenario, a:Actor) { - Actor.placedOn(a, hl); - Lane_Horizontal(hl); - find helper_getXAndBounds(cs, a, xMax, xP); + find helper_horiz_getXAndBounds(cs, a, xMax, xP); check(xP <= 0-xMax);} @Constraint(severity="error", key={cs}, message="x") pattern define_actor_maxYp(cs:CrossingScenario, a:Actor) { - Actor.placedOn(a, vl); - Lane_Vertical(vl); - find helper_getYAndBounds(cs, a, yMax, yP); + find helper_vert_getYAndBounds(cs, a, yMax, yP); check(yP >= yMax);} @Constraint(severity="error", key={cs}, message="x") pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { - Actor.placedOn(a, vl); - Lane_Vertical(vl); - find helper_getYAndBounds(cs, a, yMax, yP); + find helper_vert_getYAndBounds(cs, a, yMax, yP); check(yP <= 0-yMax);} - + +/////---------------- //Xspeed and Yspeed bounds +/////---------------- //TODO THIS IS HARD_CODED -//@Constraint(severity="error", key={a}, message="x") -//pattern define_actor_maxXs(a:Actor) { -// Actor.xSpeed(a, xS); -// check(xS >= 100.0);} -// -//@Constraint(severity="error", key={a}, message="x") -//pattern define_actor_minXs(a:Actor) { -// Actor.xSpeed(a, xS); -// check(xS <= 0-100.0);} -// -////TODO THIS IS HARD_CODED -//@Constraint(severity="error", key={a}, message="x") -//pattern define_actor_maxYs(a:Actor) { -// Actor.ySpeed(a, yS); -// check(yS >= 100.0);} -// -//@Constraint(severity="error", key={a}, message="x") -//pattern define_actor_minYs(a:Actor) { -// Actor.ySpeed(a, yS); -// check(yS <= 0-100.0);} -//END Hard-coded stuff - -////TODO May be required -/////////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 May be required -/////////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) { -// -//} +/////////VERTICAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnVertLaneHasxSpeed0(a:Actor) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + Actor.xSpeed(a, xSpeed); + check(xSpeed != 0); +} + +private pattern helper_vert_getYSpeedAndBounds(cs:CrossingScenario, a:Actor, + ySpeedMax:java Double, ySpeed:java Double) { + Actor.placedOn(a, vl); + Lane_Vertical(vl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxYSpeed(cs, ySpeedMax); + Actor.ySpeed(a, ySpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMinYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS <= 0-ySMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnVertLaneMaxYs(cs:CrossingScenario, a:Actor) { + find helper_vert_getYSpeedAndBounds(cs, a, ySMax, yS); + check(yS >= ySMax); +} + +/////////HORIZONTAL LANE +@Constraint(severity="error", key={a}, message="7 Actor") +pattern define_actor_actorOnHorizLaneHasySpeed0(a:Actor) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + Actor.ySpeed(a, ySpeed); + check(ySpeed != 0); +} + +private pattern helper_horiz_getXSpeedAndBounds(cs:CrossingScenario, a:Actor, + xSpeedMax:java Double, xSpeed:java Double) { + Actor.placedOn(a, hl); + Lane_Horizontal(hl); + CrossingScenario.actors(cs, a); + CrossingScenario.maxXSpeed(cs, xSpeedMax); + Actor.xSpeed(a, xSpeed); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMinXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS <= 0-xSMax); +} + +@Constraint(severity="error", key={cs}, message="x") +pattern define_actor_actorOnHorizLaneMaxXs(cs:CrossingScenario, a:Actor) { + find helper_horiz_getXSpeedAndBounds(cs, a, xSMax, xS); + check(xS >= xSMax); +} + +/////---------------- +/////WIDTH and LENGTH +/////---------------- -///////pedestrian-width (3) //TODO Derived? +///////pedestrian-width (3) @Constraint(severity="error", key={p}, message="3 Actor") pattern define_actor_pedestrianWidth(p:Pedestrian) { Pedestrian.width(p, w); check(w != 1.0); } -/////////pedestrian-width (4) //TODO Derived? +/////////pedestrian-width (4) @Constraint(severity="error", key={p}, message="4 Actor") pattern define_actor_pedestrianLength(p:Pedestrian) { Pedestrian.length(p, l); check(l != 1.0); } -/////////actor-width (5) //TODO Derived? +/////////actor-width (5) @Constraint(severity="error", key={v}, message="5 Actor") pattern define_actor_vehicleWidth(v:Vehicle) { Vehicle.placedOn(v, lane); @@ -335,7 +363,7 @@ pattern define_actor_vehicleWidth(v:Vehicle) { check(w != 3.0); } -/////////actor-width (6) //TODO Derived? +/////////actor-width (6) @Constraint(severity="error", key={v}, message="6 Actor") pattern define_actor_vehicleLength(v:Vehicle) { Vehicle.placedOn(v, lane); @@ -349,23 +377,10 @@ pattern define_actor_vehicleLength(v:Vehicle) { check(l != 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); -} +/////---------------- +/////DERIVED FEATURES +/////---------------- -//<> Derived Features private pattern helper_getCoords(a1:Actor, a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { Actor.xPos(a1, x1); @@ -410,8 +425,6 @@ private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { //check(dx^2 + dy^2 > 20^2) check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); } - -//<> ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //Relation @@ -428,7 +441,57 @@ pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) { //////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //CollisionExists ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// - + + +//<> + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + CollisionExists.source(ce, a1); + CollisionExists.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} + +//<> +/* +//// +//VS VisionBlocked +//// +//TODO Very prone to corner cases + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern collisionExists_vsVisionBlocked(a1:Actor, a2:Actor) { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + neg find helper_collidingActors(a1, a2); +} or { + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + neg find helper_collidingActors(a2, a1); +} + +private pattern helper_collidingActors(a1:Actor, a2:Actor){ + CollisionExists.source(vb, a1); + CollisionExists.target(vb, a2); +} + +//<> + +//// +//CollisionExists - Time +//// + + @Constraint(severity="error", key={c}, message="x") pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) { CrossingScenario.relations(ss, c); @@ -441,6 +504,10 @@ pattern collisionExists_timeNotNegative(c:CollisionExists) { CollisionExists. collisionTime(c, cTime); check(cTime <= 0.0);} +//// +//CollisionExists - Physical Positioniung +//// + private pattern helper_getCollExistsTime(a1:Actor, a2: Actor, cTime:java Double) { CollisionExists.source(c, a1); CollisionExists.target(c, a2); @@ -459,6 +526,8 @@ private pattern helper_getAllYCoords(a1:Actor, a2: Actor, l1:java Double, l2:java Double, yPos1:java Double, yPos2:java Double, ySpeed1:java Double, ySpeed2:java Double) { + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); find helper_getYCoords(a1, l1, yPos1, ySpeed1); find helper_getYCoords(a2, l2, yPos2, ySpeed2); } @@ -474,9 +543,11 @@ private pattern helper_getXCoords(a:Actor, l:java Double, private pattern helper_getAllXCoords(a1:Actor, a2: Actor, w1:java Double, w2:java Double, xPos1:java Double, xPos2:java Double, xSpeed1:java Double, xSpeed2:java Double) { - - find helper_getYCoords(a1, w1, xPos1, xSpeed1); - find helper_getYCoords(a2, w2, xPos2, xSpeed2); + + CollisionExists.source(c, a1); + CollisionExists.target(c, a2); + find helper_getXCoords(a1, w1, xPos1, xSpeed1); + find helper_getXCoords(a2, w2, xPos2, xSpeed2); } @Constraint(severity="error", key={a1}, message="x") @@ -504,7 +575,7 @@ pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor) { pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor) { find helper_getCollExistsTime(a1, a2, cTime); - find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); //check(x_1_left > x_2_right) check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2)); @@ -515,13 +586,13 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 find helper_getCollExistsTime(a1, a2, cTime); - find helper_getAllYCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); + find helper_getAllXCoords(a1, a2, w1, w2, xPos1, xPos2, xSpeed1, xSpeed2); //check(x_1_right < x_2_left) check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2)); } - +*/ ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //VisionBlocked ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// @@ -545,6 +616,24 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { Actor.placedOn(a1, l); Actor.placedOn(a2, l); } + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, vl1); + Lane_Vertical(vl1); + Actor.placedOn(a2, vl2); + Lane_Vertical(vl2); +} or { + VisionBlocked.source(ce, a1); + VisionBlocked.target(ce, a2); + Actor.placedOn(a1, hl1); + Lane_Horizontal(hl1); + Actor.placedOn(a2, hl2); + Lane_Horizontal(hl2); +} + //<> @Constraint(severity="error", key={a1, a2}, message="x") @@ -571,8 +660,7 @@ pattern visionBlocked_ites_notOnSameVertLine(a1:Actor, a2:Actor, vb:VisionBlocke check(x1 == x2); } -//OPTIONS 1: everything is from a single check expression containing ITEs -//Currently unhandled bygenerator +//TODO refactor? @Constraint(severity="error", key={a1, vb}, message="x") pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 @@ -596,6 +684,7 @@ pattern visionBlocked_ites_top(a1:Actor, a2:Actor, vb:VisionBlocked) { < ((y1-y2)/(x1-x2))); } +//TODO refactor? @Constraint(severity="error", key={a1, vb}, message="x") pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 @@ -619,6 +708,35 @@ pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor, vb:VisionBlocked) { > ((y1-y2)/(x1-x2))); } +@Constraint(severity="error", key={a1, a2}, message="x") +pattern visionBlocked_blockerNotToRightOfBoth(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.xPos(a2, x2); + Actor.xPos(aBlocker, xBlocker); + + check( x1 < xBlocker && x2 < xBlocker); +} + +@Constraint(severity="error", key={a1, a2}, message="x") +pattern visionBlocked_blockerNotToLeftOfBoth(a1:Actor, a2:Actor) { + //This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1 + VisionBlocked.source(vb, a1); + VisionBlocked.target(vb, a2); + VisionBlocked.blockedBy(vb, aBlocker); + + Actor.xPos(a1, x1); + Actor.xPos(a2, x2); + Actor.xPos(aBlocker, xBlocker); + + check( x1 > xBlocker && x2 > xBlocker); +} + + /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //SeparationDistance /////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// diff --git a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java index 02abbd28..0ccfc4a1 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java +++ b/Domains/crossingScenario/src/crossingScenario/run/DrawScenario.java @@ -2,17 +2,11 @@ package crossingScenario.run; import java.awt.BasicStroke; import java.awt.Color; -import java.awt.Desktop; import java.awt.Graphics2D; import java.awt.image.BufferedImage; import java.io.File; import java.io.IOException; -import java.io.PrintWriter; -import java.nio.file.Path; -import java.util.ArrayList; -import java.util.List; -import java.util.regex.Matcher; -import java.util.regex.Pattern; +import java.util.stream.Collectors; import javax.imageio.ImageIO; @@ -29,6 +23,7 @@ import crossingScenario.CrossingScenarioPackage; import crossingScenario.Lane; import crossingScenario.Lane_Horizontal; import crossingScenario.Lane_Vertical; +import crossingScenario.VisionBlocked; public class DrawScenario { public static final int SIZE = 1000; @@ -71,9 +66,13 @@ public class DrawScenario { //lanes g.setPaint(Color.RED); + //origin g.drawRect(-5, -5, 10, 10); + //Axes + g.drawLine(-xSize/2, 0, xSize/2, 0); + g.drawLine(0, -ySize/2, 0, ySize/2); for (Lane l : cs.getLanes()) { - int ref = (int) (l.getReferenceCoord() * multiplier); + int ref = (int) ((l.getReferenceCoord() +5)* multiplier); if (l instanceof Lane_Horizontal) { g.drawLine(-xSize/2, ref, xSize/2, ref); } @@ -82,7 +81,6 @@ public class DrawScenario { } } - g.setPaint(Color.GREEN); for (Actor a : cs.getActors()) { //Draw actor int left = (int) ((a.getXPos()-a.getWidth()/2) * multiplier); @@ -94,6 +92,13 @@ public class DrawScenario { // System.out.println(width); // System.out.println(length); // System.out.println(); + if (!cs.getRelations().stream().filter(r -> r instanceof VisionBlocked) + .filter(r -> ((VisionBlocked) r).getBlockedBy().equals(a)). + collect(Collectors.toList()).isEmpty()) + g.setPaint(Color.BLACK); + else + g.setPaint(Color.GREEN); + g.drawRect(left, bot, width, length); //Draw Speed? diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend index f2f43aaa..f74c2ab4 100644 --- a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend +++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage/src/hu/bme/mit/inf/dslreasoner/viatrasolver/partialinterpretation2logic/InstanceModel2PartialInterpretation.xtend @@ -207,13 +207,12 @@ class InstanceModel2PartialInterpretation { } } // DEBUG -// println("DEBUG BEGINNING") -// println(object) -// println(attribute) -// println(value) -// -// println("MAYIGNORE " + mayIgnored) -// println("ISIGNORED " + isIgnored) + if (isIgnored) { + println("IGNORED") + println(object) + println(attribute) + println(object.eGet(attribute)) + } // END DEBUG return isIgnored } -- cgit v1.2.3-54-g00ecf