package modes3.queries

import "http://www.ece.mcgill.ca/wcet/modes3"

pattern connectedTo(S1 : Segment, S2 : Segment) {
	Segment.connectedTo(S1, S2);
}

@Constraint(message = "connectedToNotSymmetric", severity = "error", key = { S1, S2 })
pattern connectedToNotSymmetric(S1 : Segment, S2 : Segment) {
	Segment.connectedTo(S1, S2);
	neg find connectedTo(S2, S1);
}

@Constraint(message = "connectedToReflexive", severity = "error", key = { S })
pattern connectedToReflexive(S : Segment) {
	Segment.connectedTo(S, S);
}

pattern turnoutOutput(T : Turnout, S : Segment) {
	Turnout.straight(T, S);
} or {
	Turnout.divergent(T, S);
}

@Constraint(message = "outputReflexive", severity = "error", key = { T })
pattern outputReflexive(T : Turnout) {
	find turnoutOutput(T, T);
}

@Constraint(message = "turnoutOutputsAreSame", severity = "error", key = { T })
pattern turnoutOutputsAreSame(T : Turnout) {
	Turnout.straight(T, S);
	Turnout.divergent(T, S);
}

pattern output(S1 : Segment, S2 : Segment) {
	Segment.connectedTo(S1, S2);
} or {
	find turnoutOutput(S1, S2);
}

@Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S })
pattern tooManyInputsOfSegment(S : SimpleSegment) {
	find output(I1, S);
	find output(I2, S);
	find output(I3, S);
	I1 != I2;
	I1 != I3;
	I2 != I3;
}

@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
pattern turnoutConnectedToBothOutputs(T : Turnout) {
	Turnout.straight(T, Straight);
	Turnout.divergent(T, Divergent);
	Segment.connectedTo(T, Straight);
	Segment.connectedTo(T, Divergent);
}

pattern adjacent(S1 : Segment, S2 : Segment) {
	find output(S1, S2);
} or {
	find turnoutOutput(S2, S1);
}

@Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T })
pattern tooManyInputsOfTurnout(T : Turnout) {
	find adjacent(I1, T);
	find adjacent(I2, T);
	find adjacent(I3, T);
	find adjacent(I4, T);
	I1 != I2;
	I1 != I3;
	I1 != I4;
	I2 != I3;
	I2 != I4;
	I3 != I4;
}

pattern inputsOfTurnout(T : Turnout) {
	find adjacent(I1, T);
	find adjacent(I2, T);
	find adjacent(I3, T);
	I1 != I2;
	I1 != I3;
	I2 != I3;
}

@Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T })
pattern tooFewInputsOfTurnout(T : Turnout) {
	neg find inputsOfTurnout(T);
}

pattern reachable(S1 : Segment, S2 : Segment) {
	S1 == S2;
} or {
	find adjacent+(S1, S2);
}

@Constraint(message = "unreachable", severity = "error", key = { S1, S2 })
pattern unreachable(S1 : Segment, S2 : Segment) {
	neg find reachable(S1, S2);
}

//
// closeTrains
//

pattern closeTrains_step_2(in train : Train) {
//    frame->t1 = model->trains[i0];
//    frame->start = frame->t1->location;
//    if(frame->start != 0){
// ...
//    }
//    + OUTER FOR LOOP COUNTER INCREMENT
	Train(train);
}

pattern closeTrains_step_3(in train : Train, in start : Segment) {
//      int loop_bound1 = frame->start->connected_to_count;
//      for (int i1 = 0; i1 < loop_bound1; i1++) { LOOP COUNTER INCREMENT IS NOT INCLUDED HERE
// ...
//      }
	Train.location(train, start);
}

pattern closeTrains_step_4(in train : Train, in start : Segment, in middle : Segment) {
//          frame->middle = frame->start->connected_to[i1];
//        int loop_bound2 = frame->middle->connected_to_count;

//        for (int i2 = 0; i2 < loop_bound2; i2++) { LOOP COUNTER INCREMENT IS NOT INCLUDED HERE
// ...
//        }
//        + OUTER FOR LOOP COUNTER INCREMENT
	Train.location(train, start);
	Segment.connectedTo(start, middle);
}

pattern closeTrains_step_5(in train : Train, in start : Segment, in middle : Segment, in end : Segment) {
//           frame->end = frame->middle->connected_to[i2];
//          if (frame->start != frame->end) {
// ...
//          }
//          + OUTER FOR LOOP COUNTER INCREMENT
	Train.location(train, start);
	Segment.connectedTo(start, middle);
	Segment.connectedTo(middle, end);
}

pattern closeTrains_step_6(in train : Train, in start : Segment, in middle : Segment, in end : Segment) {
//            frame->t2 = frame->end->train;
//            if (frame->t2 != 0) {
// ...
//            }
	Train.location(train, start);
	Segment.connectedTo(start, middle);
	Segment.connectedTo(middle, end);
	start != end;
}

pattern closeTrains_step_7(in train : Train, in start : Segment, in middle : Segment, in end : Segment, in otherTrain : Train) {
//              results->matches[match_cntr].start = frame->start;
//              results->matches[match_cntr++].end = frame->end;
	Train.location(train, start);
	Segment.connectedTo(start, middle);
	Segment.connectedTo(middle, end);
	start != end;
	Segment.occupiedBy(end, otherTrain);
}

//
// trainLocations
//

pattern trainLocations_step_2(in train : Train) {
//   frame->train = model->trains[i0];
//   frame->location = frame->train->location;
//   if (frame->location != NULL) {
//     ...
//   }

	Train(train);
}

pattern trainLocations_step_3(in train : Train, in location : Segment) {
//     results->matches[match_cntr].location = frame->location;
//     results->matches[match_cntr++].train = frame->train;
	Train(train);
    Train.location(train, location);
}

//
// misalignedTurnout
//

pattern misalignedTurnout_step_2(in turnout : Turnout) {
//    frame->turnout = model->turnouts[i0];
//    frame->location = frame->turnout->straight;
//    if (frame->location != NULL) {
// ...
//    }
	Turnout(turnout);
}

pattern misalignedTurnout_step_3(in turnout : Turnout, in location : Segment) {
//      Segment *disconnected = ((Segment *)frame->turnout);
//      if (disconnected->connected_to[0] != frame->location &&
//          disconnected->connected_to[1] != frame->location) {
// ...
//      }
	Turnout(turnout);
	Turnout.straight(turnout, location);
}

pattern misalignedTurnout_step_4(in turnout : Turnout, in location : Segment) {
//        frame->train = frame->location->train;
//        if (frame->train != NULL) {
// ...
//        }
	Turnout(turnout);
	Turnout.straight(turnout, location);
	neg find connectedSegmentsDirected(turnout, location);	
}

pattern misalignedTurnout_step_5(in turnout : Turnout, in location : Segment, in train : Train) {
//              results->matches[match_cntr].start = frame->start;
//              results->matches[match_cntr++].end = frame->end;
	Turnout(turnout);
	Turnout.straight(turnout, location);
	neg find connectedSegmentsDirected(turnout, location);
	Segment.occupiedBy(location, train);
}

pattern connectedSegmentsDirected(s1 : Segment, s2 : Segment) {
	Segment.connectedTo(s1, s2);
}

//
// endOfSiding
//

pattern endOfSiding_step_2(in train : Train) {
//   frame->train = model->trains[i0];
//   frame->location = frame->train->location;
//   if (frame->location != NULL) {
//     ...
//   }

	Train(train);
}

pattern endOfSiding_step_3(in train : Train, in location : Segment) {
//     int loop_bound1 = frame->location->connected_to_count;
//     for (int i1 = 0; i1 < loop_bound1; i1++) {
//       ...
//     }
	Train(train);
    Train.location(train, location);
}

pattern endOfSiding_step_4(in train : Train, in location : Segment, in end : Segment) {
//       frame->end = frame->location->connected_to[i1];
//       if (frame->end != NULL &&
//			 frame->end->connected_to[1] == frame->location &&
//           frame->end->connected_to[0] == NULL) {
//         ...
//       } 
//     	 if (frame->end != NULL &&
//			 frame->end->connected_to[0] == frame->location &&
//           frame->end->connected_to[1] == NULL) {
//         ...
//       }
	Train(train);
    Train.location(train, location);
    Segment.connectedTo(location, end);
}

pattern endOfSiding_step_5(in train : Train, in location : Segment, in end : Segment) {
//         results->matches[match_cntr].location = frame->location;
//         results->matches[match_cntr++].train = frame->train;
//         ...OR...
//         results->matches[match_cntr].location = frame->location;
//         results->matches[match_cntr++].train = frame->train;
	Train(train);
    Train.location(train, location);
    Segment.connectedTo(location, end);
	neg find multipleConnectedTo(end);
}

pattern multipleConnectedTo(s : Segment) {
	Segment.connectedTo(s, n1);
	Segment.connectedTo(s, n2);
	n1 != n2;
}