diff options
author | Kristóf Marussy <marussy@mit.bme.hu> | 2020-08-28 18:58:37 +0200 |
---|---|---|
committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-08-28 18:58:37 +0200 |
commit | 4fe7fce97aedbd516109ef81afc33e00112b7b68 (patch) | |
tree | 7eaa7c4e9b31b2a1488e49de48721b4dbad31fae /Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | |
parent | MoDeS3 unit propagation WIP (diff) | |
download | VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.tar.gz VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.tar.zst VIATRA-Generator-4fe7fce97aedbd516109ef81afc33e00112b7b68.zip |
Must unit propagation
Diffstat (limited to 'Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql')
-rw-r--r-- | Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | 54 |
1 files changed, 26 insertions, 28 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 index 982e6cec..b8841928 100644 --- a/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql +++ b/Domains/ca.mcgill.rtgmrt.example.modes3/src/modes3/queries/Modes3Queries.vql | |||
@@ -2,11 +2,6 @@ package modes3.queries | |||
2 | 2 | ||
3 | import "http://www.ece.mcgill.ca/wcet/modes3" | 3 | import "http://www.ece.mcgill.ca/wcet/modes3" |
4 | 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) { | 5 | pattern connectedTo(S1 : Segment, S2 : Segment) { |
11 | Segment.connectedTo(S1, S2); | 6 | Segment.connectedTo(S1, S2); |
12 | } | 7 | } |
@@ -39,10 +34,6 @@ pattern turnoutOutputsAreSame(T : Turnout) { | |||
39 | Turnout.divergent(T, S); | 34 | Turnout.divergent(T, S); |
40 | } | 35 | } |
41 | 36 | ||
42 | pattern turnout(T : Turnout) { | ||
43 | Turnout(T); | ||
44 | } | ||
45 | |||
46 | pattern output(S1 : Segment, S2 : Segment) { | 37 | pattern output(S1 : Segment, S2 : Segment) { |
47 | Segment.connectedTo(S1, S2); | 38 | Segment.connectedTo(S1, S2); |
48 | } or { | 39 | } or { |
@@ -56,8 +47,7 @@ pattern output(S1 : Segment, S2 : Segment) { | |||
56 | //} | 47 | //} |
57 | 48 | ||
58 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) | 49 | @Constraint(message = "tooManyInputsOfSegment", severity = "error", key = { S }) |
59 | pattern tooManyInputsOfSegment(S : Segment) { | 50 | pattern tooManyInputsOfSegment(S : SimpleSegment) { |
60 | neg find turnout(S); | ||
61 | find output(I1, S); | 51 | find output(I1, S); |
62 | find output(I2, S); | 52 | find output(I2, S); |
63 | find output(I3, S); | 53 | find output(I3, S); |
@@ -74,30 +64,38 @@ pattern turnoutConnectedToBothOutputs(T : Turnout) { | |||
74 | Segment.connectedTo(T, Divergent); | 64 | Segment.connectedTo(T, Divergent); |
75 | } | 65 | } |
76 | 66 | ||
77 | pattern extraInputOfTurnout(T : Turnout, S : Segment) { | 67 | pattern adjacent(S1 : Segment, S2 : Segment) { |
78 | Turnout.straight(T, Straight); | 68 | find output(S1, S2); |
79 | Turnout.divergent(T, Divergent); | 69 | } or { |
80 | find output(S, T); | 70 | find turnoutOutput(S2, S1); |
81 | S != Straight; | ||
82 | S != Divergent; | ||
83 | } | 71 | } |
84 | 72 | ||
85 | @Constraint(message = "noExtraInputOfTurnout", severity = "error", key = { T }) | 73 | @Constraint(message = "turnoutConnectedToBothOutputs", severity = "error", key = { T }) |
86 | pattern noExtraInputOfTurnout(T : Turnout) { | 74 | pattern tooManyInputsOfTurnout(T : Turnout) { |
87 | neg find extraInputOfTurnout(T, _); | 75 | find adjacent(I1, T); |
76 | find adjacent(I2, T); | ||
77 | find adjacent(I3, T); | ||
78 | find adjacent(I4, T); | ||
79 | I1 != I2; | ||
80 | I1 != I3; | ||
81 | I1 != I4; | ||
82 | I2 != I3; | ||
83 | I2 != I4; | ||
84 | I3 != I4; | ||
88 | } | 85 | } |
89 | 86 | ||
90 | @Constraint(message = "tooManyExtraInputsOfTurnout", severity = "error", key = { T }) | 87 | pattern inputsOfTurnout(T : Turnout) { |
91 | pattern tooManyExtraInputsOfTurnout(T : Turnout) { | 88 | find adjacent(I1, T); |
92 | find extraInputOfTurnout(T, I1); | 89 | find adjacent(I2, T); |
93 | find extraInputOfTurnout(T, I2); | 90 | find adjacent(I3, T); |
94 | I1 != I2; | 91 | I1 != I2; |
92 | I1 != I3; | ||
93 | I2 != I3; | ||
95 | } | 94 | } |
96 | 95 | ||
97 | pattern adjacent(S1 : Segment, S2 : Segment) { | 96 | @Constraint(message = "tooFewInputsOfTurnout", severity = "error", key = { T }) |
98 | find output(S1, S2); | 97 | pattern tooFewInputsOfTurnout(T : Turnout) { |
99 | } or { | 98 | neg find inputsOfTurnout(T); |
100 | find turnoutOutput(S2, S1); | ||
101 | } | 99 | } |
102 | 100 | ||
103 | pattern reachable(S1 : Segment, S2 : Segment) { | 101 | pattern reachable(S1 : Segment, S2 : Segment) { |