package queries

import "http://www.example.com/crossingScenario"
import "http://www.eclipse.org/emf/2002/Ecore"

//////Minimal Failing Example
//@Constraint(severity = "error", key = {l}, message = "this defines the placedOn relation")
//pattern patterThatOnlyWorksWithInt(l : Lane) {
//	Lane.referenceCoord(l, w);
//	check(w <= 0-10.0);
//}

//////////////
//CrossingScenario
/////////////

//TODO Hard-code xSize?
//TODO Hard-code ySize?

//TODO Hard-code maxTime?
//@Constraint(severity="error", key={l}, message="3 CrossingScenari")
//pattern define_cs_maxTime(cs:CrossingScenario) {
//	CrossingScenario.maxTime(cs, mt);
//	check(mt != 60.0);
//}


//////////////
//Lane
//////////////

@Constraint(severity="error", key={l}, message="1 Lane")
pattern define_numWidth_small(l : Lane) {
	Lane.width(l, Size::S_Small);
	Lane.numWidth(l, nw);
	check(nw <= 5.0);
} or {
	Lane.width(l, Size::S_Small);
	Lane.numWidth(l, nw);
	check(nw >= 10.0);
}

@Constraint(severity="error", key={l}, message="2 Lane")
pattern define_numWidth_medium(l : Lane) { 
	Lane.width(l, ::S_Med);
	Lane.numWidth(l, nw);
	check(nw <= 10.0);
}
or {
	Lane.width(l, Size::S_Med);
	Lane.numWidth(l, nw);
	check(nw >= 15.0);
}

@Constraint(severity="error", key={l}, message="3 Lane")
pattern define_numWidth_large(l : Lane) { 
	Lane.width(l, Size::S_Large);
	Lane.numWidth(l, nw);
	check(nw <= 15.0);
}
or {
	Lane.width(l, Size::S_Large);
	Lane.numWidth(l, nw);
	check(nw >= 20.0);
}

/////////////Prevlane

////////head lanes do not have prevLane
@Constraint(severity="error", key={l}, message="6.1 Lane")
pattern define_prevLane_headVertLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Vertical) {
	CrossingScenario.vertical_head(cs, l);
	Lane.prevLane(l, _);
}

@Constraint(severity="error", key={l}, message="6.2 Lane")
pattern define_prevLane_headHoriLaneDoesNotHavePrevLane(cs:CrossingScenario, l:Lane_Horizontal) {
	CrossingScenario.horizontal_head(cs, l);
	Lane.prevLane(l, _);
}

////////Non-head lanes must have prevLane
@Constraint(severity="error", key={l}, message="6.1 Lane")
pattern define_prevLane_nonheadVertLaneHasPrevLane(l:Lane_Vertical) {
	neg find find_headVertLane(l);
	neg find find_laneWithPrevLane(l);
}

@Constraint(severity="error", key={l}, message="6.1 Lane")
pattern define_prevLane_nonheadHoriLaneHasPrevLane(l:Lane_Horizontal) {
	neg find find_headHoriLane(l);
	neg find find_laneWithPrevLane(l);
}

private pattern find_headVertLane(l:Lane_Vertical) {
	CrossingScenario.vertical_head(_, l);
}
private pattern find_headHoriLane(l:Lane_Horizontal) {
	CrossingScenario.horizontal_head(_, l);
}
private pattern find_laneWithPrevLane(l:Lane) {
	Lane.prevLane(l, _);
}

/////////Lane cannot be its own recursive prevLane
@Constraint(severity="error", key={l}, message="6.1 Lane")
pattern define_prevLane_lanecannotBeItsOwnPrevLane(l:Lane) {
	Lane.prevLane(l, l);
}

@Constraint(severity="error", key={l}, message="6.2 Lane")
pattern define_prevLane_lanecannotBeItsOwnRecursivePrevLane(l:Lane) {
	find find_prevLane+(l, l);
}
private pattern find_prevLane(l1:Lane, l2:Lane) {
	Lane.prevLane(l1, l2);
}

//////Lane cannot be prevLane of >1 other lane
@Constraint(severity="error", key={l1, l2}, message="7 Lane")
pattern define_prevLane_lanecannotbeprevLaneof2lanes(l1:Lane, l2:Lane) {
	Lane.prevLane(l1, l);
	Lane.prevLane(l2, l);
	l1 != l2;
}

//////consecutive lanes must have same orientation
@Constraint(severity="error", key={l1, l2}, message="8 Lane")
pattern define_prevLane_consecutiveLanesMustHaveSameOrientation1(l1:Lane_Horizontal, l2:Lane_Vertical) {
	Lane.prevLane(l1, l2);
}

@Constraint(severity="error", key={l1, l2}, message="8 Lane")
pattern define_prevLane_consecutiveLanesMustHaveSameOrientation2(l1:Lane_Vertical, l2:Lane_Horizontal) {
	Lane.prevLane(l1, l2);
}

/////////////ReferenceCoord

/////refCoord of head lanes must be 0
@Constraint(severity="error", key={l}, message="6.2 Lane")
pattern define_prevLane_headHoriLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Horizontal) {
	CrossingScenario.horizontal_head(cs, l);
	Lane.referenceCoord(l, rc);
	check(rc != 0.0);
}

@Constraint(severity="error", key={l}, message="6.2 Lane")
pattern define_prevLane_headVertLaneHas0RefCoord(cs:CrossingScenario, l:Lane_Vertical) {
	CrossingScenario.vertical_head(cs, l);
	Lane.referenceCoord(l, rc);
	check(rc != 0.0);
}

//////refCoord of a lane is prevLane.rc + curLane.numWidth

@Constraint(severity="error", key={l}, message="6.2 Lane")
pattern define_referenceCoord_laneWithPrevHasCorrectRefCoord(l:Lane) {
	Lane.prevLane(l, prev);
	Lane.referenceCoord(l, rcCur);
	
	Lane.numWidth(prev, wPrev);
	Lane.referenceCoord(prev, rcPrev);
	check(rcCur != rcPrev + wPrev);
}


//////////////
//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 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
//////////////

//Hard-coded stuff
//TODO THIS IS HARD_CODED
@Constraint(severity="error", key={a}, message="x")
pattern define_actor_maxXp(a:Actor) {
	Actor.xPos(a, xP);
	check(xP >= 1000.0);}

@Constraint(severity="error", key={a}, message="x")
pattern define_actor_minXp(a:Actor) {
	Actor.xPos(a, xP);
	check(xP <= 0-1000.0);}
	
//TODO THIS IS HARD_CODED
@Constraint(severity="error", key={a}, message="x")
pattern define_actor_maxYp(a:Actor) {
	Actor.yPos(a, yP);
	check(yP >= 1000.0);}
	
@Constraint(severity="error", key={a}, message="x")
pattern define_actor_minYp(a:Actor) {
	Actor.yPos(a, yP);
	check(yP <= 0-1000.0);}
	
//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) {
//	
//}


///////pedestrian-width (3) //TODO Derived?
@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?
@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?
@Constraint(severity="error", key={v}, message="5 Actor")
pattern define_actor_vehicleWidth(v:Vehicle) {
	Vehicle.placedOn(v, lane);
	Lane_Vertical(lane);
    Vehicle.width(v, w);
    check(w != 1.0);
} or {
	Vehicle.placedOn(v, lane);
	Lane_Horizontal(lane);
    Vehicle.width(v, w);
    check(w != 3.0);
}

/////////actor-width (6) //TODO Derived?
@Constraint(severity="error", key={v}, message="6 Actor")
pattern define_actor_vehicleLength(v:Vehicle) {
	Vehicle.placedOn(v, lane);
	Lane_Vertical(lane);
    Vehicle.length(v, l);
    check(l != 3.0);
} or {
	Vehicle.placedOn(v, lane);
	Lane_Horizontal(lane);
    Vehicle.length(v, l);
    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);
}

//////////////
//Relation
//////////////
@Constraint(severity="error", key={a1, a2}, message="1 Relation")
pattern define_relation_noSelfRelation(a1:Actor, a2:Actor) {
	Actor.relations(a1, r);
	Relation.target(r, a2);
	a1 == a2;
}

//TODO do above but transitively?

//////////////
//CollisionExists
//////////////

//TODO THIS IS HARD_CODED
@Constraint(severity="error", key={c}, message="x")
pattern collisionExists_timeWithinBound(c:CollisionExists) {
	CollisionExists. collisionTime(c, cTime);
	check(cTime >= 60.0);}
	
//TODO replace above with this (more general)
//@Constraint(severity="error", key={c}, message="x")
//pattern collisionExists_timeWithinBound(ss:CrossingScenario, c:CollisionExists) {
//	CrossingScenario.actors.relations(ss, c);
//	CrossingScenario.maxTime(ss, maxTime);
//	CollisionExists. collisionTime(c, cTime);
//	check(cTime >= maxTime);}

@Constraint(severity="error", key={c}, message="x")
pattern collisionExists_timeNotNegative(c:CollisionExists) {
	CollisionExists. collisionTime(c, cTime);
	check(cTime <= 0.0);}

@Constraint(severity="error", key={a1, c}, message="x")
pattern collisionExists_defineCollision_y1(a1:Actor, a2:Actor, c:CollisionExists) {
	Actor.relations(a1, c);
	CollisionExists.target(c, a2);
	
	Actor.length(a1, l1);
	Actor.yPos(a1, yPos1);
	Actor.ySpeed(a1, ySpeed1);
	Actor.length(a2, l2);
	Actor.yPos(a2, yPos2);
	Actor.ySpeed(a2, ySpeed2);
	CollisionExists. collisionTime(c, cTime);
	//check(y_1_bottom > y_2_top
	check((yPos1 + (ySpeed1 * cTime)) - (l1/2) > (yPos2 + (ySpeed2 * cTime)) + (l2/2));	
}

@Constraint(severity="error", key={a1, c}, message="x")
pattern collisionExists_defineCollision_y2(a1:Actor, a2:Actor, c:CollisionExists) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, c);
	CollisionExists.target(c, a2);
	
	Actor.length(a1, l1);
	Actor.yPos(a1, yPos1);
	Actor.ySpeed(a1, ySpeed1);
	Actor.length(a2, l2);
	Actor.yPos(a2, yPos2);
	Actor.ySpeed(a2, ySpeed2);
	CollisionExists. collisionTime(c, cTime);
	//check(y_1_top < y_2_bottom)
	check((yPos1 + (ySpeed1 * cTime)) + (l1/2) < (yPos2 + (ySpeed2 * cTime)) - (l2/2));	
}

@Constraint(severity="error", key={a1, c}, message="x")
pattern collisionExists_defineCollision_x1(a1:Actor, a2:Actor, c:CollisionExists) {
	Actor.relations(a1, c);
	CollisionExists.target(c, a2);
	
	Actor.width(a1, w1);
	Actor.xPos(a1, xPos1);
	Actor.xSpeed(a1, xSpeed1);
	Actor.width(a2, w2);
	Actor.xPos(a2, xPos2);
	Actor.xSpeed(a2, xSpeed2);
	CollisionExists. collisionTime(c, cTime);
	//check(x_1_left > x_2_right)
	check((xPos1 + (xSpeed1 * cTime)) - (w1/2) > (xPos2 + (xSpeed2 * cTime)) + (w2/2));	
}

@Constraint(severity="error", key={a1, c}, message="x")
pattern collisionExists_defineCollision_x2(a1:Actor, a2:Actor, c:CollisionExists) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, c);
	CollisionExists.target(c, a2);
	
	Actor.width(a1, w1);
	Actor.xPos(a1, xPos1);
	Actor.xSpeed(a1, xSpeed1);
	Actor.width(a2, w2);
	Actor.xPos(a2, xPos2);
	Actor.xSpeed(a2, xSpeed2);
	CollisionExists. collisionTime(c, cTime);
	//check(x_1_right < x_2_left)
	check((xPos1 + (xSpeed1 * cTime)) + (w1/2) < (xPos2 + (xSpeed2 * cTime)) - (w2/2));	
}

//////////////
//SeparationDistance
//////////////
@Constraint(severity="error", key={a1, sd}, message="x")
pattern SeparationDistance_near_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, sd);
	SeparationDistance.target(sd, a2);
	SeparationDistance.distance(sd, Distance::D_Near);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	//check(dx^2 + dy^2 < 5^2)
	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 5*5);	
}

@Constraint(severity="error", key={a1, sd}, message="x")
pattern SeparationDistance_near_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, sd);
	SeparationDistance.target(sd, a2);
	SeparationDistance.distance(sd, Distance::D_Near);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	//check(dx^2 + dy^2 > 10^2)
	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 10*10);	
}

@Constraint(severity="error", key={a1, sd}, message="x")
pattern SeparationDistance_medium_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, sd);
	SeparationDistance.target(sd, a2);
	SeparationDistance.distance(sd, Distance::D_Med);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	//check(dx^2 + dy^2 < 10^2)
	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 10*10);	
}

@Constraint(severity="error", key={a1, sd}, message="x")
pattern SeparationDistance_medium_ub(a1:Actor, a2:Actor, sd:SeparationDistance) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, sd);
	SeparationDistance.target(sd, a2);
	SeparationDistance.distance(sd, Distance::D_Med);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	//check(dx^2 + dy^2 > 1^2)
	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) > 15*15);	
}

@Constraint(severity="error", key={a1, sd}, message="x")
pattern SeparationDistance_far_lb(a1:Actor, a2:Actor, sd:SeparationDistance) {
	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
	Actor.relations(a1, sd);
	SeparationDistance.target(sd, a2);
	SeparationDistance.distance(sd, Distance::D_Far);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	//check(dx^2 + dy^2 < 15^2)
	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);	
}

////////////////
////CollisionDoesNotExist
////////////////
//TODO
////@Constraint(severity="error", key={a1, cdne}, message="x")
////pattern collisionDoesNotExist(a1:Actor, a2:Actor, ss:CrossingScenario, cdne:CollisionDoesNotExist) {
////	//This second one is required because we do not want to enforce both a1->c->a2 and a2->c->a1
////	
////	CrossingScenario.actors(ss, a1);
////	CrossingScenario.actors(ss, a2);
////	Actor.relations(a1, cdne);
////	CollisionDoesNotExist.target(cdne, a2);
////	CrossingScenario.maxTime(ss, maxTime);
////	
////	Actor.width(a1, w1);
////	Actor.length(a1, l1);
////	Actor.xPos(a1, xPos1);
////	Actor.yPos(a1, yPos1);
////	Actor.xSpeed(a1, xSpeed1);
////	Actor.ySpeed(a1, ySpeed1);
////	
////	Actor.width(a2, w2);
////	Actor.length(a2, l2);
////	Actor.xPos(a2, xPos2);
////	Actor.yPos(a2, yPos2);
////	Actor.xSpeed(a2, xSpeed2);
////	Actor.ySpeed(a2, ySpeed2);
////	//check(dx^2 + dy^2 < 15^2)
////	check((x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) < 15*15);	
////}

//////////////
//VisionBlocked
//////////////

@Constraint(severity="error", key={a1, a2}, message="x")
pattern visionBlocked_invalidBlocker(a1:Actor, a2:Actor) {
	Actor.relations(a1, vb);
	VisionBlocked.target(vb, a2);
	VisionBlocked.blockedBy(vb, a1);
} or {	
	Actor.relations(a1, vb);
	VisionBlocked.target(vb, a2);
	VisionBlocked.blockedBy(vb, a1);
}

//OPTIONS 1: everything is from a single check expression containing ITEs
//Currently unhandled bygenerator
@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
	Actor.relations(a1, vb);
	VisionBlocked.target(vb, a2);
	VisionBlocked.blockedBy(vb, aBlocker);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	Actor.xPos(aBlocker, xBlocker);
	Actor.yPos(aBlocker, yBlocker);
	Actor.length(aBlocker, lenBlocker);
	Actor.width(aBlocker, widBlocker);
	
	//check(slope of a1-to-BlockerTop < slope of a1-to-a2)
	check(
		( yBlocker - y1 + (if(xBlocker > x1){lenBlocker/2}else{0-lenBlocker/2})) / 
		( xBlocker - x1 + (if(yBlocker > y1){0-widBlocker/2}else{widBlocker/2}))
		< ((y1-y2)/(x1-x2)));	
}

@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
	Actor.relations(a1, vb);
	VisionBlocked.target(vb, a2);
	VisionBlocked.blockedBy(vb, aBlocker);
	
	Actor.xPos(a1, x1);
	Actor.yPos(a1, y1);
	Actor.xPos(a2, x2);
	Actor.yPos(a2, y2);
	Actor.xPos(aBlocker, xBlocker);
	Actor.yPos(aBlocker, yBlocker);
	Actor.length(aBlocker, lenBlocker);
	Actor.width(aBlocker, widBlocker);
	
	//check(slope of a1-to-BlockerBottom > slope of a1-to-a2)
	check(
		( yBlocker - y1 + (if(xBlocker > x1){0-lenBlocker/2}else{lenBlocker/2})) / 
		( xBlocker - x1 + (if(yBlocker > y1){widBlocker/2}else{0-widBlocker/2}))
		> ((y1-y2)/(x1-x2)));	
}



////OPTION 2: 
////we handle ITE by seperating the constraints
//
////This will involve 1 constarint for each decision path, but will require multiple check expressions within the same pattern
//
////OPTION 3: 
////If this is nott working still, we will have to add some strctural components to the MM
////to differentiate the different cases and reduce the requirements of if, then, else
//
////This will involve more patterns, and some that are pstructural as well.