From 14afb998045e508b07633ea63c72b582084f8c4c Mon Sep 17 00:00:00 2001 From: Aren Babikian Date: Wed, 3 Feb 2021 02:35:39 +0100 Subject: major changes to CS case study, working example, few issues, major assumptions --- Domains/crossingScenario/.classpath | 7 +- .../ecore-gen/crossingScenario/Actor.java | 41 ---- .../crossingScenario/CrossingScenarioPackage.java | 140 +----------- .../ecore-gen/crossingScenario/impl/ActorImpl.java | 84 ------- .../impl/CrossingScenarioPackageImpl.java | 36 --- .../inputs/crossingScenarioGen.vsconfig | 5 +- .../crossingScenario/model/crossingScenario.ecore | 6 - .../model/crossingScenario.genmodel | 3 - .../crossingScenario/model/crossingScenario2.aird | 88 +------- Domains/crossingScenario/plugin.xml | 11 +- .../queries/crossingScenarioQueries.vql | 242 +++++++++++---------- .../crossingScenario/run/CrossingScenarioMain.java | 2 +- .../src/crossingScenario/run/QueryDebug.java | 30 +-- 13 files changed, 164 insertions(+), 531 deletions(-) diff --git a/Domains/crossingScenario/.classpath b/Domains/crossingScenario/.classpath index 5bc9ff04..b657c1bb 100644 --- a/Domains/crossingScenario/.classpath +++ b/Domains/crossingScenario/.classpath @@ -1,7 +1,12 @@ - + + + + + + diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/Actor.java b/Domains/crossingScenario/ecore-gen/crossingScenario/Actor.java index 1b570b6f..cbfc21cf 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/Actor.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/Actor.java @@ -2,8 +2,6 @@ */ package crossingScenario; -import org.eclipse.emf.common.util.EList; - import org.eclipse.emf.ecore.EObject; /** @@ -22,9 +20,6 @@ import org.eclipse.emf.ecore.EObject; *
  • {@link crossingScenario.Actor#getXSpeed XSpeed}
  • *
  • {@link crossingScenario.Actor#getPlacedOn Placed On}
  • *
  • {@link crossingScenario.Actor#getYSpeed YSpeed}
  • - *
  • {@link crossingScenario.Actor#getDist_near Dist near}
  • - *
  • {@link crossingScenario.Actor#getDist_med Dist med}
  • - *
  • {@link crossingScenario.Actor#getDist_far Dist far}
  • * * * @see crossingScenario.CrossingScenarioPackage#getActor() @@ -190,40 +185,4 @@ public interface Actor extends EObject { */ void setYSpeed(double value); - /** - * Returns the value of the 'Dist near' reference list. - * The list contents are of type {@link crossingScenario.Actor}. - * - * - * @return the value of the 'Dist near' reference list. - * @see crossingScenario.CrossingScenarioPackage#getActor_Dist_near() - * @model transient="true" volatile="true" derived="true" - * @generated - */ - EList getDist_near(); - - /** - * Returns the value of the 'Dist med' reference list. - * The list contents are of type {@link crossingScenario.Actor}. - * - * - * @return the value of the 'Dist med' reference list. - * @see crossingScenario.CrossingScenarioPackage#getActor_Dist_med() - * @model transient="true" volatile="true" derived="true" - * @generated - */ - EList getDist_med(); - - /** - * Returns the value of the 'Dist far' reference list. - * The list contents are of type {@link crossingScenario.Actor}. - * - * - * @return the value of the 'Dist far' reference list. - * @see crossingScenario.CrossingScenarioPackage#getActor_Dist_far() - * @model transient="true" volatile="true" derived="true" - * @generated - */ - EList getDist_far(); - } // Actor diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java index 9985f18a..b39553f9 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/CrossingScenarioPackage.java @@ -275,33 +275,6 @@ public interface CrossingScenarioPackage extends EPackage { */ int ACTOR__YSPEED = 6; - /** - * The feature id for the 'Dist near' reference list. - * - * - * @generated - * @ordered - */ - int ACTOR__DIST_NEAR = 7; - - /** - * The feature id for the 'Dist med' reference list. - * - * - * @generated - * @ordered - */ - int ACTOR__DIST_MED = 8; - - /** - * The feature id for the 'Dist far' reference list. - * - * - * @generated - * @ordered - */ - int ACTOR__DIST_FAR = 9; - /** * The number of structural features of the 'Actor' class. * @@ -309,7 +282,7 @@ public interface CrossingScenarioPackage extends EPackage { * @generated * @ordered */ - int ACTOR_FEATURE_COUNT = 10; + int ACTOR_FEATURE_COUNT = 7; /** * The number of operations of the 'Actor' class. @@ -549,33 +522,6 @@ public interface CrossingScenarioPackage extends EPackage { */ int PEDESTRIAN__YSPEED = ACTOR__YSPEED; - /** - * The feature id for the 'Dist near' reference list. - * - * - * @generated - * @ordered - */ - int PEDESTRIAN__DIST_NEAR = ACTOR__DIST_NEAR; - - /** - * The feature id for the 'Dist med' reference list. - * - * - * @generated - * @ordered - */ - int PEDESTRIAN__DIST_MED = ACTOR__DIST_MED; - - /** - * The feature id for the 'Dist far' reference list. - * - * - * @generated - * @ordered - */ - int PEDESTRIAN__DIST_FAR = ACTOR__DIST_FAR; - /** * The number of structural features of the 'Pedestrian' class. * @@ -667,33 +613,6 @@ public interface CrossingScenarioPackage extends EPackage { */ int VEHICLE__YSPEED = ACTOR__YSPEED; - /** - * The feature id for the 'Dist near' reference list. - * - * - * @generated - * @ordered - */ - int VEHICLE__DIST_NEAR = ACTOR__DIST_NEAR; - - /** - * The feature id for the 'Dist med' reference list. - * - * - * @generated - * @ordered - */ - int VEHICLE__DIST_MED = ACTOR__DIST_MED; - - /** - * The feature id for the 'Dist far' reference list. - * - * - * @generated - * @ordered - */ - int VEHICLE__DIST_FAR = ACTOR__DIST_FAR; - /** * The number of structural features of the 'Vehicle' class. * @@ -1022,39 +941,6 @@ public interface CrossingScenarioPackage extends EPackage { */ EAttribute getActor_YSpeed(); - /** - * Returns the meta object for the reference list '{@link crossingScenario.Actor#getDist_near Dist near}'. - * - * - * @return the meta object for the reference list 'Dist near'. - * @see crossingScenario.Actor#getDist_near() - * @see #getActor() - * @generated - */ - EReference getActor_Dist_near(); - - /** - * Returns the meta object for the reference list '{@link crossingScenario.Actor#getDist_med Dist med}'. - * - * - * @return the meta object for the reference list 'Dist med'. - * @see crossingScenario.Actor#getDist_med() - * @see #getActor() - * @generated - */ - EReference getActor_Dist_med(); - - /** - * Returns the meta object for the reference list '{@link crossingScenario.Actor#getDist_far Dist far}'. - * - * - * @return the meta object for the reference list 'Dist far'. - * @see crossingScenario.Actor#getDist_far() - * @see #getActor() - * @generated - */ - EReference getActor_Dist_far(); - /** * Returns the meta object for class '{@link crossingScenario.Relation Relation}'. * @@ -1358,30 +1244,6 @@ public interface CrossingScenarioPackage extends EPackage { */ EAttribute ACTOR__YSPEED = eINSTANCE.getActor_YSpeed(); - /** - * The meta object literal for the 'Dist near' reference list feature. - * - * - * @generated - */ - EReference ACTOR__DIST_NEAR = eINSTANCE.getActor_Dist_near(); - - /** - * The meta object literal for the 'Dist med' reference list feature. - * - * - * @generated - */ - EReference ACTOR__DIST_MED = eINSTANCE.getActor_Dist_med(); - - /** - * The meta object literal for the 'Dist far' reference list feature. - * - * - * @generated - */ - EReference ACTOR__DIST_FAR = eINSTANCE.getActor_Dist_far(); - /** * The meta object literal for the '{@link crossingScenario.impl.RelationImpl Relation}' class. * diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/ActorImpl.java b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/ActorImpl.java index 52d251e0..9ef288f0 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/ActorImpl.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/ActorImpl.java @@ -5,14 +5,8 @@ package crossingScenario.impl; import crossingScenario.Actor; import crossingScenario.CrossingScenarioPackage; import crossingScenario.Lane; - -import java.util.Collection; - import org.eclipse.emf.common.notify.Notification; import org.eclipse.emf.common.notify.NotificationChain; - -import org.eclipse.emf.common.util.EList; - import org.eclipse.emf.ecore.EClass; import org.eclipse.emf.ecore.InternalEObject; @@ -34,9 +28,6 @@ import org.eclipse.emf.ecore.impl.MinimalEObjectImpl; *
  • {@link crossingScenario.impl.ActorImpl#getXSpeed XSpeed}
  • *
  • {@link crossingScenario.impl.ActorImpl#getPlacedOn Placed On}
  • *
  • {@link crossingScenario.impl.ActorImpl#getYSpeed YSpeed}
  • - *
  • {@link crossingScenario.impl.ActorImpl#getDist_near Dist near}
  • - *
  • {@link crossingScenario.impl.ActorImpl#getDist_med Dist med}
  • - *
  • {@link crossingScenario.impl.ActorImpl#getDist_far Dist far}
  • * * * @generated @@ -391,48 +382,6 @@ public abstract class ActorImpl extends MinimalEObjectImpl.Container implements eNotify(new ENotificationImpl(this, Notification.SET, CrossingScenarioPackage.ACTOR__YSPEED, oldYSpeed, ySpeed)); } - /** - * - * - * @generated - */ - @Override - public EList getDist_near() { - // TODO: implement this method to return the 'Dist near' reference list - // Ensure that you remove @generated or mark it @generated NOT - // The list is expected to implement org.eclipse.emf.ecore.util.InternalEList and org.eclipse.emf.ecore.EStructuralFeature.Setting - // so it's likely that an appropriate subclass of org.eclipse.emf.ecore.util.EcoreEList should be used. - throw new UnsupportedOperationException(); - } - - /** - * - * - * @generated - */ - @Override - public EList getDist_med() { - // TODO: implement this method to return the 'Dist med' reference list - // Ensure that you remove @generated or mark it @generated NOT - // The list is expected to implement org.eclipse.emf.ecore.util.InternalEList and org.eclipse.emf.ecore.EStructuralFeature.Setting - // so it's likely that an appropriate subclass of org.eclipse.emf.ecore.util.EcoreEList should be used. - throw new UnsupportedOperationException(); - } - - /** - * - * - * @generated - */ - @Override - public EList getDist_far() { - // TODO: implement this method to return the 'Dist far' reference list - // Ensure that you remove @generated or mark it @generated NOT - // The list is expected to implement org.eclipse.emf.ecore.util.InternalEList and org.eclipse.emf.ecore.EStructuralFeature.Setting - // so it's likely that an appropriate subclass of org.eclipse.emf.ecore.util.EcoreEList should be used. - throw new UnsupportedOperationException(); - } - /** * * @@ -486,12 +435,6 @@ public abstract class ActorImpl extends MinimalEObjectImpl.Container implements return basicGetPlacedOn(); case CrossingScenarioPackage.ACTOR__YSPEED: return getYSpeed(); - case CrossingScenarioPackage.ACTOR__DIST_NEAR: - return getDist_near(); - case CrossingScenarioPackage.ACTOR__DIST_MED: - return getDist_med(); - case CrossingScenarioPackage.ACTOR__DIST_FAR: - return getDist_far(); } return super.eGet(featureID, resolve, coreType); } @@ -526,18 +469,6 @@ public abstract class ActorImpl extends MinimalEObjectImpl.Container implements case CrossingScenarioPackage.ACTOR__YSPEED: setYSpeed((Double)newValue); return; - case CrossingScenarioPackage.ACTOR__DIST_NEAR: - getDist_near().clear(); - getDist_near().addAll((Collection)newValue); - return; - case CrossingScenarioPackage.ACTOR__DIST_MED: - getDist_med().clear(); - getDist_med().addAll((Collection)newValue); - return; - case CrossingScenarioPackage.ACTOR__DIST_FAR: - getDist_far().clear(); - getDist_far().addAll((Collection)newValue); - return; } super.eSet(featureID, newValue); } @@ -571,15 +502,6 @@ public abstract class ActorImpl extends MinimalEObjectImpl.Container implements case CrossingScenarioPackage.ACTOR__YSPEED: setYSpeed(YSPEED_EDEFAULT); return; - case CrossingScenarioPackage.ACTOR__DIST_NEAR: - getDist_near().clear(); - return; - case CrossingScenarioPackage.ACTOR__DIST_MED: - getDist_med().clear(); - return; - case CrossingScenarioPackage.ACTOR__DIST_FAR: - getDist_far().clear(); - return; } super.eUnset(featureID); } @@ -606,12 +528,6 @@ public abstract class ActorImpl extends MinimalEObjectImpl.Container implements return placedOn != null; case CrossingScenarioPackage.ACTOR__YSPEED: return ySpeed != YSPEED_EDEFAULT; - case CrossingScenarioPackage.ACTOR__DIST_NEAR: - return !getDist_near().isEmpty(); - case CrossingScenarioPackage.ACTOR__DIST_MED: - return !getDist_med().isEmpty(); - case CrossingScenarioPackage.ACTOR__DIST_FAR: - return !getDist_far().isEmpty(); } return super.eIsSet(featureID); } diff --git a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java index 7f8f7357..887e02fe 100644 --- a/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java +++ b/Domains/crossingScenario/ecore-gen/crossingScenario/impl/CrossingScenarioPackageImpl.java @@ -360,36 +360,6 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin return (EAttribute)actorEClass.getEStructuralFeatures().get(6); } - /** - * - * - * @generated - */ - @Override - public EReference getActor_Dist_near() { - return (EReference)actorEClass.getEStructuralFeatures().get(7); - } - - /** - * - * - * @generated - */ - @Override - public EReference getActor_Dist_med() { - return (EReference)actorEClass.getEStructuralFeatures().get(8); - } - - /** - * - * - * @generated - */ - @Override - public EReference getActor_Dist_far() { - return (EReference)actorEClass.getEStructuralFeatures().get(9); - } - /** * * @@ -551,9 +521,6 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin createEAttribute(actorEClass, ACTOR__XSPEED); createEReference(actorEClass, ACTOR__PLACED_ON); createEAttribute(actorEClass, ACTOR__YSPEED); - createEReference(actorEClass, ACTOR__DIST_NEAR); - createEReference(actorEClass, ACTOR__DIST_MED); - createEReference(actorEClass, ACTOR__DIST_FAR); relationEClass = createEClass(RELATION); createEReference(relationEClass, RELATION__TARGET); @@ -632,9 +599,6 @@ public class CrossingScenarioPackageImpl extends EPackageImpl implements Crossin initEAttribute(getActor_XSpeed(), ecorePackage.getEDouble(), "xSpeed", "0.0", 1, 1, Actor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); initEReference(getActor_PlacedOn(), this.getLane(), this.getLane_Actors(), "placedOn", null, 1, 1, Actor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); initEAttribute(getActor_YSpeed(), ecorePackage.getEDouble(), "ySpeed", null, 1, 1, Actor.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_UNSETTABLE, !IS_ID, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); - initEReference(getActor_Dist_near(), this.getActor(), null, "dist_near", null, 0, -1, Actor.class, IS_TRANSIENT, IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, IS_DERIVED, IS_ORDERED); - initEReference(getActor_Dist_med(), this.getActor(), null, "dist_med", null, 0, -1, Actor.class, IS_TRANSIENT, IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, IS_DERIVED, IS_ORDERED); - initEReference(getActor_Dist_far(), this.getActor(), null, "dist_far", null, 0, -1, Actor.class, IS_TRANSIENT, IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, IS_DERIVED, IS_ORDERED); initEClass(relationEClass, Relation.class, "Relation", IS_ABSTRACT, !IS_INTERFACE, IS_GENERATED_INSTANCE_CLASS); initEReference(getRelation_Target(), this.getActor(), null, "target", null, 1, 1, Relation.class, !IS_TRANSIENT, !IS_VOLATILE, IS_CHANGEABLE, !IS_COMPOSITE, IS_RESOLVE_PROXIES, !IS_UNSETTABLE, IS_UNIQUE, !IS_DERIVED, IS_ORDERED); diff --git a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig index 7d329d18..8ce9f6ee 100644 --- a/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig +++ b/Domains/crossingScenario/inputs/crossingScenarioGen.vsconfig @@ -10,7 +10,6 @@ generate { scope = { #node += 0..* ,# += 0 - //,# = 25..* ,# += 0 //,# = 1 //,# = 0 @@ -22,7 +21,7 @@ generate { runtime = 10000, log-level = none, "numeric-solver" = "dreal-local", - "dreal-local-path" = "/home/models/dreal4/bazel-bin/dreal/dreal", + "dreal-local-path" = "../../Solvers/dreal4/bazel-bin/dreal/dreal", "ignored-attributes" = " Pedestrian.xPos=*, Pedestrian.yPos=*, @@ -40,7 +39,7 @@ generate { "scopePropagator" = "polyhedral"} runs = 1 - number = 10 + number = 3 debug = "outputs/debug" log = "outputs/debug/log.txt" output = "outputs/models" diff --git a/Domains/crossingScenario/model/crossingScenario.ecore b/Domains/crossingScenario/model/crossingScenario.ecore index 9f979b96..c5cddd7f 100644 --- a/Domains/crossingScenario/model/crossingScenario.ecore +++ b/Domains/crossingScenario/model/crossingScenario.ecore @@ -35,12 +35,6 @@ eType="#//Lane" eOpposite="#//Lane/actors"/> - - - - - - diff --git a/Domains/crossingScenario/model/crossingScenario2.aird b/Domains/crossingScenario/model/crossingScenario2.aird index f278e603..daf4df5b 100644 --- a/Domains/crossingScenario/model/crossingScenario2.aird +++ b/Domains/crossingScenario/model/crossingScenario2.aird @@ -5,7 +5,7 @@ crossingScenario.genmodel - + @@ -48,15 +48,6 @@ - - - - - - - - - @@ -364,54 +355,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - @@ -533,7 +476,7 @@ - + KEEP_LOCATION @@ -801,33 +744,6 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Domains/crossingScenario/plugin.xml b/Domains/crossingScenario/plugin.xml index c8846e1b..8e759f1f 100644 --- a/Domains/crossingScenario/plugin.xml +++ b/Domains/crossingScenario/plugin.xml @@ -1,7 +1,10 @@ - - - - + + + + diff --git a/Domains/crossingScenario/queries/crossingScenarioQueries.vql b/Domains/crossingScenario/queries/crossingScenarioQueries.vql index 32348399..0a28d774 100644 --- a/Domains/crossingScenario/queries/crossingScenarioQueries.vql +++ b/Domains/crossingScenario/queries/crossingScenarioQueries.vql @@ -91,6 +91,23 @@ pattern define_actor_minYp(cs:CrossingScenario, a:Actor) { find helper_vert_getYAndBounds(cs, a, yMax, yP); check(yP <= 0-yMax);} +////////////ADDED +//to reduce overlap +//NEEDED +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_actor_wrtLane(a:Actor) { + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yP); + check(yP > 0.0-1.0); +} or { + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xP); + check(xP > 0.0-1.0); +} +////////////ADDED + //Minimum Distances private pattern helper_getCoords(a1:Actor, a2: Actor, x1:java Double, x2:java Double, y1:java Double, y2:java Double) { @@ -105,8 +122,8 @@ private pattern helper_getCoords(a1:Actor, pattern define_actor_minimumDistance(a1: Actor, a2: Actor) { find helper_getCoords(a1, a2, x1, x2, y1, y2); a1 != a2; - //check(dx^2 + dy^2 < 5^2) - check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5); + //check(dx^2 + dy^2 < 3^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 3*3); } /////---------------- @@ -219,47 +236,38 @@ pattern define_actor_vehicleLength(v:Vehicle) { check(l != 2.0); } -///////---------------- -///////DERIVED FEATURES -///////---------------- -// -//@QueryBasedFeature -//pattern dist_near(a1: Actor, a2: Actor) { -// find helper_actorsAreNear(a1, a2); -// Actor.dist_near(a1, a2); -//} -// -//private pattern helper_actorsAreNear(a1: Actor, a2: Actor) { -// find helper_getCoords(a1, a2, x1, x2, y1, y2); -// //check(dx^2 + dy^2 < 10^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); -//} -// -//@QueryBasedFeature -//pattern dist_med(a1: Actor, a2: Actor) { -// find helper_actorsAreMed(a1, a2); -// Actor.dist_med(a1, a2); -//} -// -//private pattern helper_actorsAreMed(a1: Actor, a2: Actor) { -// find helper_getCoords(a1, a2, x1, x2, y1, y2); -// //check(10^2 < dx^2 + dy^2 < 15^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); -//} -// -//@QueryBasedFeature -//pattern dist_far(a1: Actor, a2: Actor) { -// find helper_actorsAreFar(a1, a2); -// Actor.dist_far(a1, a2); -//} -// -//private pattern helper_actorsAreFar(a1: Actor, a2: Actor) { -// find helper_getCoords(a1, a2, x1, x2, y1, y2); -// //check(dx^2 + dy^2 > 20^2) -// check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); -//} - +/////---------------- +/////DERIVED FEATURES +/////---------------- +/* +@QueryBasedFeature +pattern dist_near(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 < 10^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10); + Actor.dist_near(a1, a2); +} + +@QueryBasedFeature +pattern dist_med(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(10^2 < dx^2 + dy^2 < 15^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10); + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15); + Actor.dist_med(a1, a2); +} + +@QueryBasedFeature +pattern dist_far(a1: Actor, a2: Actor) { + find helper_getCoords(a1, a2, x1, x2, y1, y2); + + //check(dx^2 + dy^2 > 20^2) + check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 20*20); + Actor.dist_far(a1, a2); +} +*/ ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //Relation ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// @@ -278,7 +286,7 @@ pattern define_actor_vehicleLength(v:Vehicle) { //<> - +/* @Constraint(severity="error", key={a1, a2}, message="x") pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { CollisionExists.source(ce, a1); @@ -295,72 +303,9 @@ pattern collisionExists_qualAbstr(a1:Actor, a2:Actor) { Actor.placedOn(a2, hl2); Lane_Horizontal(hl2); } - +*/ //<> -//// -//VS VisionBlocked -//// -//TODO Very prone to corner cases -/* -@Constraint(severity="error", key={a1}, message="x") -pattern collisionExists_vsVisionBlockedX1(a1:Actor) { - VisionBlocked.blockedBy(_, a1); - CollisionExists.target(_, a1); -} -@Constraint(severity="error", key={a1}, message="x") -pattern collisionExists_vsVisionBlockedX2(a1:Actor) { - VisionBlocked.blockedBy(_, a1); - CollisionExists.source(_, a1); -} - -@Constraint(severity="error", key={a1}, message="x") -pattern collisionExists_vsVisionBlocked1(a1:Actor) { - VisionBlocked.source(_, a1); - neg find helper_source(a1); -} -private pattern helper_source(a1:Actor) { - CollisionExists.source(_, a1); -} - -@Constraint(severity="error", key={a1}, message="x") -pattern collisionExists_vsVisionBlocked2(a1:Actor) { - VisionBlocked.target(_, a1); - neg find helper_target(a1); -} -private pattern helper_target(a1:Actor) { - CollisionExists.target(_, a1); -} -*/ -/* -@Constraint(severity="error", key={a1}, message="x") -pattern collisionExists_vsVisionBlocked(a1:Actor) { - VisionBlocked.source(vb, a1); - VisionBlocked.target(vb, a2); - CollisionExists.source(ce, a1); - CollisionExists.target(ce, a3); - a2 != a3; -} or { - VisionBlocked.source(vb, a1); - VisionBlocked.target(vb, a2); - CollisionExists.source(ce, a3); - CollisionExists.target(ce, a1); - a2 != a3; -} or { - VisionBlocked.source(vb, a2); - VisionBlocked.target(vb, a1); - CollisionExists.source(ce, a3); - CollisionExists.target(ce, a1); - a2 != a3; -} or { - VisionBlocked.source(vb, a2); - VisionBlocked.target(vb, a1); - CollisionExists.source(ce, a1); - CollisionExists.target(ce, a3); - a2 != a3; -} -*/ -//<> //// //CollisionExists - Time @@ -407,10 +352,10 @@ private pattern helper_getAllYCoords(a1:Actor, a2: Actor, find helper_getYCoords(a2, l2, yPos2, ySpeed2); } -private pattern helper_getXCoords(a:Actor, l:java Double, +private pattern helper_getXCoords(a:Actor, w:java Double, xPos:java Double, xSpeed:java Double) { - Actor.length(a, l); + Actor.width(a, w); Actor.xPos(a, xPos); Actor.xSpeed(a, xSpeed); } @@ -473,7 +418,7 @@ pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor) { ///////*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*-_-*////// //<> - +/* @Constraint(severity="error", key={a1, a2}, message="on 3 different lanes") pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { VisionBlocked.source(vb, a1); @@ -491,7 +436,7 @@ pattern visionBlocked_qualAbstr(a1:Actor, a2:Actor) { Actor.placedOn(a1, l); 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); @@ -509,6 +454,30 @@ pattern visionBlocked_qualAbstr2(a1:Actor, a2:Actor) { Lane_Horizontal(hl2); } +////////////ADDED +//to make decision for ITE +//NOT NEEDED +/* +@Constraint(severity="error", key={a}, message="5 Actor") +pattern define_vb_blvssrc(a:Actor) { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Vertical(lane); + Actor.yPos(a, yPa); + Actor.yPos(b, yPb); + check(yPb <= yPa); +} or { + VisionBlocked.source(vb, a); + VisionBlocked.blockedBy(vb, b); + Actor.placedOn(a, lane); + Lane_Horizontal(lane); + Actor.xPos(a, xPa); + Actor.xPos(a, xPb); + check(xPb <= xPa); +} +*/ +////////////ADDED //<> @Constraint(severity="error", key={a1, a2}, message="x") @@ -582,6 +551,9 @@ pattern visionBlocked_ites_bottom(a1:Actor, a2:Actor) { > ((y1-y2)/(x1-x2))); } +/////// +//BLOCKER IN BETWEEN +/////// private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, x1:java Double, y1:java Double, @@ -600,6 +572,7 @@ private pattern helper_VB_getJustCoords(a1:Actor, a2: Actor, Actor.yPos(aBlocker, yBlocker); } +/* //INFO may use approximation instead @Constraint(severity="error", key={a1}, message="x") pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { @@ -621,4 +594,49 @@ pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { //check(dist(A2, ABlocker) > dist(A2, A1)) check((x2-xBlocker)*(x2-xBlocker) + (y2-yBlocker)*(y2-yBlocker) > (x2-x1)*(x2-x1) + (y2-y1)*(y2-y1)); } +*/ + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBSlargerThanxdistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((x1-xBlocker)*(x1-xBlocker) > (x1-x2)*(x1-x2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_xdistBTlargerThanxdistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + x1, _, x2, _, xBlocker, _); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((x2-xBlocker)*(x2-xBlocker) > (x2-x1)*(x2-x1)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBSlargerThanydistTS(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A1, ABlocker) > dist(A1, A2)) + check((y1-yBlocker)*(y1-yBlocker) > (y1-y2)*(y1-y2)); +} + +//INFO may use approximation instead +@Constraint(severity="error", key={a1}, message="x") +pattern visionBlocked_ydistBTlargerThanydistST(a1:Actor, a2:Actor) { + + find helper_VB_getJustCoords(a1, a2, + _, y1, _, y2, _, yBlocker); + + //check(dist(A2, ABlocker) > dist(A2, A1)) + check((y2-yBlocker)*(y2-yBlocker) > (y2-y1)*(y2-y1)); +} diff --git a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java index 5bf70b3a..ad2c6d88 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java +++ b/Domains/crossingScenario/src/crossingScenario/run/CrossingScenarioMain.java @@ -36,7 +36,7 @@ public class CrossingScenarioMain { // Files.copy(path, target, StandardCopyOption.REPLACE_EXISTING); printStats(pathStats); - for (int i = 1; i <= 10; i++) { + for (int i = 1; i <= 3; i++) { DrawScenario.drawScenario("outputs/models/"+i+".xmi", "outputs/drawnModel"+i+".png"); System.out.println("DONE " + i); } diff --git a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java index 3fea18de..e1830a2a 100644 --- a/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java +++ b/Domains/crossingScenario/src/crossingScenario/run/QueryDebug.java @@ -1,7 +1,6 @@ package crossingScenario.run; import java.io.FileNotFoundException; -import java.io.PrintWriter; import java.util.ArrayList; import java.util.HashMap; import java.util.List; @@ -16,10 +15,7 @@ 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 { @@ -84,18 +80,22 @@ public class QueryDebug { EPackage.Registry.INSTANCE.put(CrossingScenarioPackage.eNS_URI, CrossingScenarioPackage.eINSTANCE); ResourceSet rs = new ResourceSetImpl(); rs.getResource(URI.createFileURI("outputs/models/1.xmi"), true); + /* + ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(rs)); + // Access pattern matcher + Queries.instance().prepare(engine); -// ViatraQueryEngine engine = ViatraQueryEngine.on(new EMFScope(rs)); -// // Access pattern matcher -// Queries.instance().prepare(engine); -// -// X.Matcher matcher = X.Matcher.on(engine); -// // Get and iterate over all matches -// System.out.println("MATCHES:"); -// for (X.Match match : matcher.getAllMatches()) { -// // Print all the matches to the standard output -// System.out.println(match.getP()); -// } + for (IQuerySpecification q : Queries.instance().getSpecifications()) { + ViatraQueryMatcher matcher = q.getMatcher(engine); + System.out.println("MATCHES for " + matcher.getPatternName()); + for (Object match : matcher.getAllMatches()) { + // Print all the matches to the standard output + System.out.println(((IPatternMatch)match).get(0)); + System.out.println(((IPatternMatch)match).get(1)); + System.out.println("------"); + } + } + */ } -- cgit v1.2.3