From a620f07468780778bd55dcffc30245def37ece69 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <marussy@mit.bme.hu>
Date: Thu, 6 Aug 2020 16:07:16 +0200
Subject: MoDeS3 unit propagation WIP

---
 .../src/modes3/queries/Modes3Queries.vql           | 112 +++++++++++++++++++++
 1 file changed, 112 insertions(+)
 create mode 100644 Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql

(limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql')

diff --git a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql
new file mode 100644
index 00000000..982e6cec
--- /dev/null
+++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql
@@ -0,0 +1,112 @@
+package modes3.queries
+
+import "http://www.ece.mcgill.ca/wcet/modes3"
+
+@Constraint(message = "turnoutInSegments", severity = "error", key = { T })
+pattern turnoutInSegments(T : Turnout) {
+	Modes3ModelRoot.segments(_, T);
+}
+
+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 turnout(T : Turnout) {
+	Turnout(T);
+}
+
+pattern output(S1 : Segment, S2 : Segment) {
+	Segment.connectedTo(S1, S2);
+} or {
+	find turnoutOutput(S1, S2);
+}
+
+//@Constraint(message = "noInputOfSegment", severity = "error", key = { S })
+//pattern noInputOfSegment(S : Segment) {
+//	neg find turnout(S);
+//	neg find output(_, S);
+//}
+
+@Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S })
+pattern tooManyInputsOfSegment(S : Segment) {
+	neg find turnout(S);
+	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 extraInputOfTurnout(T : Turnout, S : Segment) {
+	Turnout.straight(T, Straight);
+	Turnout.divergent(T, Divergent);
+	find output(S, T);
+	S != Straight;
+	S != Divergent;
+}
+
+@Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T })
+pattern noExtraInputOfTurnout(T : Turnout) {
+	neg find extraInputOfTurnout(T, _);
+}
+
+@Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T })
+pattern tooManyExtraInputsOfTurnout(T : Turnout) {
+	find extraInputOfTurnout(T, I1);
+	find extraInputOfTurnout(T, I2);
+	I1 != I2;
+}
+
+pattern adjacent(S1 : Segment, S2 : Segment) {
+	find output(S1, S2);
+} or {
+	find turnoutOutput(S2, S1);
+}
+
+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);
+}
-- 
cgit v1.2.3-70-g09d2