diff options
author | 2020-05-10 22:09:17 +0200 | |
---|---|---|
committer | 2020-05-10 22:09:17 +0200 | |
commit | 7adead25f3c8451a51a3f8fa1d45b0b8f93b3a69 (patch) | |
tree | 0b9b4ac2c58bf0535b27a447cae36335d5b9f503 /Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf | |
parent | Synthetic tokens for solver language (diff) | |
download | VIATRA-Generator-7adead25f3c8451a51a3f8fa1d45b0b8f93b3a69.tar.gz VIATRA-Generator-7adead25f3c8451a51a3f8fa1d45b0b8f93b3a69.tar.zst VIATRA-Generator-7adead25f3c8451a51a3f8fa1d45b0b8f93b3a69.zip |
Add satellite case study
Diffstat (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf')
2 files changed, 342 insertions, 0 deletions
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql new file mode 100644 index 00000000..ba12bbda --- /dev/null +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql | |||
@@ -0,0 +1,325 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.domains.satellite.queries | ||
2 | |||
3 | import "http://www.example.org/satellite" | ||
4 | |||
5 | @Constraint(severity = "error", key = {Element}, | ||
6 | message = "A communicating element may not have two transmitting communication subsystems.") | ||
7 | pattern communicationLinkDoesNotStartAtContainingElement(Element : CommunicatingElement) { | ||
8 | find transmittingCommSubsystem(Element, Comm1); | ||
9 | find transmittingCommSubsystem(Element, Comm2); | ||
10 | Comm1 != Comm2; | ||
11 | } | ||
12 | |||
13 | private pattern transmittingCommSubsystem(Element : CommunicatingElement, Comm : CommSubsystem) { | ||
14 | CommunicatingElement.commSubsystem(Element, Comm); | ||
15 | CommSubsystem.target(Comm, _); | ||
16 | } | ||
17 | |||
18 | @Constraint(severity = "error", key = {Station}, | ||
19 | message = "The ground station network may not have outgoing communication links.") | ||
20 | pattern transmittingGroundStationNetwork(Station : GroundStationNetwork) { | ||
21 | find transmittingCommSubsystem(Station, _); | ||
22 | } | ||
23 | |||
24 | @Constraint(severity = "error", key = {Station}, | ||
25 | message = "The ground station network may not have UHF communication subsystems.") | ||
26 | pattern roundStationNetworkUHF(Station : GroundStationNetwork) { | ||
27 | CommunicatingElement.commSubsystem(Station, Comm); | ||
28 | UHFCommSubsystem(Comm); | ||
29 | } | ||
30 | |||
31 | // At least two spacecraft must have the interferometry payload configured | ||
32 | |||
33 | @Constraint(severity = "error", key = {Mission}, | ||
34 | message = "Interferometry mission needs at least two spacecraft configured with the interferometry payload.") | ||
35 | pattern notEnoughInterferometryPayloads(Mission : InterferometryMission) { | ||
36 | InterferometryMission(Mission); | ||
37 | neg find atLeastTwoInterferometryPayloads(Mission); | ||
38 | } | ||
39 | |||
40 | private pattern atLeastTwoInterferometryPayloads(Mission : InterferometryMission) { | ||
41 | find spacecraftWithInterferometryPayload(Mission, Spacecraft1); | ||
42 | find spacecraftWithInterferometryPayload(Mission, Spacecraft2); | ||
43 | Spacecraft1 != Spacecraft2; | ||
44 | } | ||
45 | |||
46 | private pattern spacecraftWithInterferometryPayload(Mission : ConstellationMission, Spacecraft : Spacecraft) { | ||
47 | ConstellationMission.spacecraft(Mission, Spacecraft); | ||
48 | Spacecraft.payload(Spacecraft, Payload); | ||
49 | InterferometryPayload(Payload); | ||
50 | } | ||
51 | |||
52 | // All spacecraft must have some communication path to the ground station | ||
53 | |||
54 | @Constraint(severity = "error", key = {Spacecraft}, | ||
55 | message = "Spacecraft has no communication path to the ground station.") | ||
56 | pattern noLinkToGroundStation(Spacecraft : Spacecraft) { | ||
57 | ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
58 | ConstellationMission.spacecraft(Mission, Spacecraft); | ||
59 | neg find indirectCommunicationLink(Spacecraft, GroundStation); | ||
60 | } | ||
61 | |||
62 | //@Constraint(severity = "error", key = {Spacecraft}, message = "UNSAT") | ||
63 | //pattern unsat_linkToGroundStation(Spacecraft : Spacecraft) { | ||
64 | // ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
65 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
66 | // find indirectCommunicationLink(Spacecraft, GroundStation); | ||
67 | //} | ||
68 | |||
69 | @Constraint(severity = "error", key = {Mission}, message = "UNSAT") | ||
70 | pattern unsat_linkToGroundStation(Mission : InterferometryMission) { | ||
71 | InterferometryMission(Mission); | ||
72 | neg find noLinkToGroundStation(_); | ||
73 | } | ||
74 | |||
75 | @Constraint(severity = "error", key = {Spacecraft}, | ||
76 | message = "Spacecraft has no potential communication path to the ground station.") | ||
77 | pattern noPotentialLinkToGroundStation(Spacecraft : Spacecraft) { | ||
78 | ConstellationMission.groundStationNetwork(Mission, GroundStation); | ||
79 | ConstellationMission.spacecraft(Mission, Spacecraft); | ||
80 | neg find indirectLinkAllowed(Spacecraft, GroundStation); | ||
81 | } | ||
82 | |||
83 | private pattern indirectLinkAllowed(From : Spacecraft, To : CommunicatingElement) { | ||
84 | find linkAllowed+(From, To); | ||
85 | } | ||
86 | |||
87 | private pattern linkAllowed(From : Spacecraft, To : CommunicatingElement) { | ||
88 | find matchingAntenna(From, To); | ||
89 | neg find cubeSat3U(From); | ||
90 | } or { | ||
91 | find matchingAntenna(From, To); | ||
92 | CubeSat3U(From); | ||
93 | } or { | ||
94 | find matchingAntenna(From, To); | ||
95 | CubeSat3U(From); | ||
96 | GroundStationNetwork(To); | ||
97 | } | ||
98 | |||
99 | private pattern matchingAntenna(From : Spacecraft, To : CommunicatingElement) { | ||
100 | CommunicatingElement.commSubsystem(From, FromSys); | ||
101 | CommunicatingElement.commSubsystem(To, ToSys); | ||
102 | find matchingCommSubsystem(FromSys, ToSys); | ||
103 | } | ||
104 | |||
105 | private pattern matchingCommSubsystem(From : CommSubsystem, To : CommSubsystem) { | ||
106 | UHFCommSubsystem(From); | ||
107 | UHFCommSubsystem(To); | ||
108 | } or { | ||
109 | XCommSubsystem(From); | ||
110 | XCommSubsystem(To); | ||
111 | } or { | ||
112 | KaCommSubsystem(From); | ||
113 | KaCommSubsystem(To); | ||
114 | } | ||
115 | |||
116 | private pattern cubeSat3U(Sat : CubeSat3U) { | ||
117 | CubeSat3U(Sat); | ||
118 | } | ||
119 | |||
120 | // No communication loops may exist | ||
121 | // No spacecraft may directly communicate with itself | ||
122 | |||
123 | @Constraint(severity = "error", key = {Element}, | ||
124 | message = "Communication loop.") | ||
125 | pattern communicationLoop(Element : CommunicatingElement) { | ||
126 | find indirectCommunicationLink(Element, Element); | ||
127 | } | ||
128 | |||
129 | private pattern indirectCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) { | ||
130 | find directCommunicationLink+(Source, Target); | ||
131 | } | ||
132 | |||
133 | private pattern directCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) { | ||
134 | CommSubsystem.target(SourceSubsystem, TargetSubsystem); | ||
135 | CommunicatingElement.commSubsystem(Source, SourceSubsystem); | ||
136 | CommunicatingElement.commSubsystem(Target, TargetSubsystem); | ||
137 | } | ||
138 | |||
139 | // Source and target communication systems must be compatible. | ||
140 | |||
141 | @Constraint(severity = "error", key = {SourceSubsystem}, | ||
142 | message = "Two ends of a communication link must use the same band.") | ||
143 | pattern incompatibleSourceAndTargetBand(SourceSubsystem : CommSubsystem) { | ||
144 | CommSubsystem.target(SourceSubsystem, TargetSubsystem); | ||
145 | neg find matchingCommSubsystem(SourceSubsystem, TargetSubsystem); | ||
146 | } | ||
147 | |||
148 | // 3U CubeSats are assumed to only be able to downlink to Earth using an X-band trasmitter, | ||
149 | // but cross-link using UHF | ||
150 | |||
151 | @Constraint(severity = "error", key = {Sat}, | ||
152 | message = "3U CubeSats can only cross-link using UHF.") | ||
153 | pattern threeUCubeSatWithNonUhfCrossLink(Sat : CubeSat3U) { | ||
154 | CommunicatingElement.commSubsystem(Sat, SourceComm); | ||
155 | neg find commSubsystemBandUhf(SourceComm); | ||
156 | CommSubsystem.target(SourceComm, TargetComm); | ||
157 | CommunicatingElement.commSubsystem(Target, TargetComm); | ||
158 | neg find groundStationNetwork(Target); | ||
159 | } | ||
160 | |||
161 | private pattern commSubsystemBandUhf(Comm : UHFCommSubsystem) { | ||
162 | UHFCommSubsystem(Comm); | ||
163 | } | ||
164 | |||
165 | private pattern groundStationNetwork(Network : GroundStationNetwork) { | ||
166 | GroundStationNetwork(Network); | ||
167 | } | ||
168 | |||
169 | // Only a Small Satellite can be configured with a Ka-band communication system | ||
170 | |||
171 | @Constraint(severity = "error", key = {Spacecraft}, | ||
172 | message = "Only a Small Satellite can be configured with a Ka-band communication system.") | ||
173 | pattern cubeSatWithKaAntenna(Spacecraft : Spacecraft) { | ||
174 | CommunicatingElement.commSubsystem(Spacecraft, Comm); | ||
175 | KaCommSubsystem(Comm); | ||
176 | neg find smallSat(Spacecraft); | ||
177 | } | ||
178 | |||
179 | pattern smallSat(Sat : SmallSat) { | ||
180 | SmallSat(Sat); | ||
181 | } | ||
182 | |||
183 | //// | ||
184 | //// Metrics | ||
185 | //// | ||
186 | // | ||
187 | //// Coverage | ||
188 | // | ||
189 | //pattern coverageMetric(Coverage : java Double) { | ||
190 | // Coverage == sum find missionCoverage(_, #_); | ||
191 | //} | ||
192 | // | ||
193 | //private pattern missionCoverage(Mission : InterferometryMission, Coverage : java Double) { | ||
194 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
195 | // ObserverCount == count find spacecraftWithInterferometryPayload(Mission, _); | ||
196 | // Coverage == eval(Math.pow(1 - 2.0 / ObserverCount, 1 + 9 * (1.0 / ObservationTime)) + 0.05 * ObservationTime / 3); | ||
197 | //} | ||
198 | // | ||
199 | //// Time | ||
200 | // | ||
201 | //pattern timeMetric(Time : java Double) { | ||
202 | // Time == sum find missionTime(_, #_); | ||
203 | //} | ||
204 | // | ||
205 | //private pattern missionTime(Mission : InterferometryMission, Time : java Double) { | ||
206 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
207 | // TrasmitTime == sum find transmitTime(Mission, _, #_); | ||
208 | // Time == eval(TrasmitTime + 60.0 * ObservationTime); | ||
209 | //} | ||
210 | // | ||
211 | //private pattern transmitTime(Mission : InterferometryMission, Spacecraft : Spacecraft, TransmitTime : java Double) { | ||
212 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
213 | // find scienceData(Spacecraft, ScienceData); | ||
214 | // IncomingData == sum find incomingData(Spacecraft, _, #_); | ||
215 | // find transmitRate(Spacecraft, TransmitRate); | ||
216 | // TransmitTime == eval((ScienceData + IncomingData) / (7.5 * TransmitRate)); | ||
217 | //} | ||
218 | // | ||
219 | //private pattern incomingData(Spacecraft : Spacecraft, Source : Spacecraft, Data : java Double) { | ||
220 | // find indirectCommunicationLink(Source, Spacecraft); | ||
221 | // find scienceData(Source, Data); | ||
222 | //} | ||
223 | // | ||
224 | //private pattern scienceData(Spacecraft : Spacecraft, Data : java Double) { | ||
225 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
226 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
227 | // Data == eval(12.0 * ObservationTime); | ||
228 | //} | ||
229 | // | ||
230 | //private pattern transmitRate(Spacecraft : Spacecraft, TransmitRate : java Double) { | ||
231 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
232 | // UHFCommSubsystem(Comm); | ||
233 | // Spacecraft(Target); | ||
234 | // TransmitRate == 5.0; | ||
235 | //} or { | ||
236 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
237 | // XCommSubsystem(Comm); | ||
238 | // Spacecraft(Target); | ||
239 | // TransmitRate == 1.6; | ||
240 | //} or { | ||
241 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
242 | // XCommSubsystem(Comm); | ||
243 | // GroundStationNetwork(Target); | ||
244 | // TransmitRate == 0.7; | ||
245 | //} or { | ||
246 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
247 | // KaCommSubsystem(Comm); | ||
248 | // Spacecraft(Target); | ||
249 | // TransmitRate == 220.0; | ||
250 | //} or { | ||
251 | // find spacecraftUplink(Spacecraft, Comm, Target); | ||
252 | // KaCommSubsystem(Comm); | ||
253 | // GroundStationNetwork(Target); | ||
254 | // TransmitRate == 80.0; | ||
255 | //} | ||
256 | // | ||
257 | //private pattern spacecraftUplink(Spacecraft : Spacecraft, TargetSubsystem : CommSubsystem, Target : CommunicatingElement) { | ||
258 | // CommunicatingElement.commSubsystem.target(Spacecraft, TargetSubsystem); | ||
259 | // CommunicatingElement.commSubsystem(Target, TargetSubsystem); | ||
260 | //} | ||
261 | // | ||
262 | //// Cost | ||
263 | // | ||
264 | //pattern costMetric(Cost : java Double) { | ||
265 | // Cost == sum find missionCost(_, #_); | ||
266 | //} | ||
267 | // | ||
268 | //private pattern missionCost(Mission : InterferometryMission, Cost : java Double) { | ||
269 | // InterferometryMission.observationTime(Mission, ObservationTime); | ||
270 | // SpacecraftCost == sum find spacecraftCost(Mission, _, #_); | ||
271 | // Cost == eval(SpacecraftCost + 100000.0 * ObservationTime); | ||
272 | //} | ||
273 | // | ||
274 | //private pattern spacecraftCost(Mission : InterferometryMission, Spacecraft : Spacecraft, Cost : java Double) { | ||
275 | // ConstellationMission.spacecraft(Mission, Spacecraft); | ||
276 | // find spacecraftOfKindCount(Spacecraft, KindCount); | ||
277 | // find basePrice(Spacecraft, BasePrice); | ||
278 | // find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost); | ||
279 | // find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost); | ||
280 | // Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost); | ||
281 | //} | ||
282 | // | ||
283 | //private pattern spacecraftOfKindCount(Sat : Spacecraft, Count : java Integer) { | ||
284 | // CubeSat3U(Sat); | ||
285 | // Count == count find cubeSat3U(_); | ||
286 | //} or { | ||
287 | // CubeSat6U(Sat); | ||
288 | // Count == count find cubeSat6U(_); | ||
289 | //} or { | ||
290 | // SmallSat(Sat); | ||
291 | // Count == count find smallSat(_); | ||
292 | //} | ||
293 | // | ||
294 | //private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) { | ||
295 | // CubeSat3U(Spacecraft); | ||
296 | // BasePrice == 250000.0; | ||
297 | //} or { | ||
298 | // CubeSat6U(Spacecraft); | ||
299 | // BasePrice == 750000.0; | ||
300 | //} or { | ||
301 | // SmallSat(Spacecraft); | ||
302 | // BasePrice == 3000000.0; | ||
303 | //} | ||
304 | // | ||
305 | //private pattern interferometryPayloadCost(Spacecraft : Spacecraft, Cost : java Double) { | ||
306 | // find spacecraftWithInterferometryPayload(_, Spacecraft); | ||
307 | // Cost == 50000.0; | ||
308 | //} or { | ||
309 | // neg find spacecraftWithInterferometryPayload(_, Spacecraft); | ||
310 | // Cost == 0.0; | ||
311 | //} | ||
312 | // | ||
313 | //private pattern additionalCommSubsystemCost(Spacecraft : Spacecraft, Cost : java Double) { | ||
314 | // find spacecraftWithTwoCommSubsystems(Spacecraft); | ||
315 | // Cost == 100000.0; | ||
316 | //} or { | ||
317 | // neg find spacecraftWithTwoCommSubsystems(Spacecraft); | ||
318 | // Cost == 0.0; | ||
319 | //} | ||
320 | // | ||
321 | //private pattern spacecraftWithTwoCommSubsystems(Spacecraft : Spacecraft) { | ||
322 | // Spacecraft.commSubsystem(Spacecraft, Subsystem1); | ||
323 | // Spacecraft.commSubsystem(Spacecraft, Subsystem2); | ||
324 | // Subsystem1 != Subsystem2; | ||
325 | //} | ||
diff --git a/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/runner/SatelliteGeneratorMain.xtend b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/runner/SatelliteGeneratorMain.xtend new file mode 100644 index 00000000..5e4e4ef0 --- /dev/null +++ b/Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/runner/SatelliteGeneratorMain.xtend | |||
@@ -0,0 +1,17 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.domains.satellite.runner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor | ||
4 | import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions | ||
5 | import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory | ||
6 | |||
7 | final class SatelliteGeneratorMain { | ||
8 | private new() { | ||
9 | throw new IllegalStateException("This is a static utility class and should not be instantiated directly.") | ||
10 | } | ||
11 | |||
12 | public static def void main(String[] args) { | ||
13 | ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE, | ||
14 | ReteBackendFactory.INSTANCE) | ||
15 | println(StandaloneScriptExecutor.executeScript("configs/generation.vsconfig")) | ||
16 | } | ||
17 | } | ||