diff options
author | 2020-08-06 16:07:16 +0200 | |
---|---|---|
committer | 2020-08-06 16:07:16 +0200 | |
commit | a620f07468780778bd55dcffc30245def37ece69 (patch) | |
tree | 57189ad9c8bf15211a05a3cd50ee90e90f434557 /Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries | |
parent | Fix time measurement (diff) | |
download | VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.tar.gz VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.tar.zst VIATRA-Generator-a620f07468780778bd55dcffc30245def37ece69.zip |
MoDeS3 unit propagation WIP
Diffstat (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries')
-rw-r--r-- | Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | 112 |
1 files changed, 112 insertions, 0 deletions
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 @@ | |||
1 | package modes3.queries | ||
2 | |||
3 | import "http://www.ece.mcgill.ca/wcet/modes3" | ||
4 | |||
5 | @Constraint(message = "turnoutInSegments", severity = "error", key = { T }) | ||
6 | pattern turnoutInSegments(T : Turnout) { | ||
7 | Modes3ModelRoot.segments(_, T); | ||
8 | } | ||
9 | |||
10 | pattern connectedTo(S1 : Segment, S2 : Segment) { | ||
11 | Segment.connectedTo(S1, S2); | ||
12 | } | ||
13 | |||
14 | @Constraint(message = "connectedToNotSymmetric", severity = "error", key = { S1, S2 }) | ||
15 | pattern connectedToNotSymmetric(S1 : Segment, S2 : Segment) { | ||
16 | Segment.connectedTo(S1, S2); | ||
17 | neg find connectedTo(S2, S1); | ||
18 | } | ||
19 | |||
20 | @Constraint(message = "connectedToReflexive", severity = "error", key = { S }) | ||
21 | pattern connectedToReflexive(S : Segment) { | ||
22 | Segment.connectedTo(S, S); | ||
23 | } | ||
24 | |||
25 | pattern turnoutOutput(T : Turnout, S : Segment) { | ||
26 | Turnout.straight(T, S); | ||
27 | } or { | ||
28 | Turnout.divergent(T, S); | ||
29 | } | ||
30 | |||
31 | @Constraint(message = "outputReflexive", severity = "error", key = { T }) | ||
32 | pattern outputReflexive(T : Turnout) { | ||
33 | find turnoutOutput(T, T); | ||
34 | } | ||
35 | |||
36 | @Constraint(message = "turnoutOutputsAreSame", severity = "error", key = { T }) | ||
37 | pattern turnoutOutputsAreSame(T : Turnout) { | ||
38 | Turnout.straight(T, S); | ||
39 | Turnout.divergent(T, S); | ||
40 | } | ||
41 | |||
42 | pattern turnout(T : Turnout) { | ||
43 | Turnout(T); | ||
44 | } | ||
45 | |||
46 | pattern output(S1 : Segment, S2 : Segment) { | ||
47 | Segment.connectedTo(S1, S2); | ||
48 | } or { | ||
49 | find turnoutOutput(S1, S2); | ||
50 | } | ||
51 | |||
52 | //@Constraint(message = "noInputOfSegment", severity = "error", key = { S }) | ||
53 | //pattern noInputOfSegment(S : Segment) { | ||
54 | // neg find turnout(S); | ||
55 | // neg find output(_, S); | ||
56 | //} | ||
57 | |||
58 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) | ||
59 | pattern tooManyInputsOfSegment(S : Segment) { | ||
60 | neg find turnout(S); | ||
61 | find output(I1, S); | ||
62 | find output(I2, S); | ||
63 | find output(I3, S); | ||
64 | I1 != I2; | ||
65 | I1 != I3; | ||
66 | I2 != I3; | ||
67 | } | ||
68 | |||
69 | @Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T }) | ||
70 | pattern turnoutConnectedToBothOutputs(T : Turnout) { | ||
71 | Turnout.straight(T, Straight); | ||
72 | Turnout.divergent(T, Divergent); | ||
73 | Segment.connectedTo(T, Straight); | ||
74 | Segment.connectedTo(T, Divergent); | ||
75 | } | ||
76 | |||
77 | pattern extraInputOfTurnout(T : Turnout, S : Segment) { | ||
78 | Turnout.straight(T, Straight); | ||
79 | Turnout.divergent(T, Divergent); | ||
80 | find output(S, T); | ||
81 | S != Straight; | ||
82 | S != Divergent; | ||
83 | } | ||
84 | |||
85 | @Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T }) | ||
86 | pattern noExtraInputOfTurnout(T : Turnout) { | ||
87 | neg find extraInputOfTurnout(T, _); | ||
88 | } | ||
89 | |||
90 | @Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T }) | ||
91 | pattern tooManyExtraInputsOfTurnout(T : Turnout) { | ||
92 | find extraInputOfTurnout(T, I1); | ||
93 | find extraInputOfTurnout(T, I2); | ||
94 | I1 != I2; | ||
95 | } | ||
96 | |||
97 | pattern adjacent(S1 : Segment, S2 : Segment) { | ||
98 | find output(S1, S2); | ||
99 | } or { | ||
100 | find turnoutOutput(S2, S1); | ||
101 | } | ||
102 | |||
103 | pattern reachable(S1 : Segment, S2 : Segment) { | ||
104 | S1 == S2; | ||
105 | } or { | ||
106 | find adjacent+(S1, S2); | ||
107 | } | ||
108 | |||
109 | @Constraint(message = "unreachable", severity = "error", key = { S1, S2 }) | ||
110 | pattern unreachable(S1 : Segment, S2 : Segment) { | ||
111 | neg find reachable(S1, S2); | ||
112 | } | ||