1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
package hu.bme.mit.inf.dslreasoner.domains.satellite.queries
import "http://www.example.org/satellite"
@Constraint(severity = "error", key = {Link},
message = "Communication links must start from the containing element.")
pattern communicationLinkDoesNotStartAtContainingElement(Link : DirectedCommunicationLink) {
CommunicatingElement.communicationLink(Element, Link);
DirectedCommunicationLink.source(Link, SourceComm);
CommunicatingElement.commSubsystem(SourceElement, SourceComm);
Element != SourceElement;
}
// At least two spacecraft must have the interferometry payload configured
//@Constraint(severity = "error", key = {Mission},
// message = "Interferometry mission needs at least two spacecraft configured with the interferometry payload.")
pattern notEnoughInterferometryPayloads(Mission : InterferometryMission) {
InterferometryMission(Mission);
neg find atLeastTwoInterferometryPayloads(Mission);
}
private pattern atLeastTwoInterferometryPayloads(Mission : InterferometryMission) {
find spacecraftWithInterferometryPayload(Mission, Spacecraft1);
find spacecraftWithInterferometryPayload(Mission, Spacecraft2);
Spacecraft1 != Spacecraft2;
}
private pattern spacecraftWithInterferometryPayload(Mission : ConstellationMission, Spacecraft : Spacecraft) {
ConstellationMission.spacecraft(Mission, Spacecraft);
Spacecraft.payload(Spacecraft, Payload);
InterferometryPayload(Payload);
}
// All spacecraft must have some communication path to the ground station
@Constraint(severity = "error", key = {Spacecraft},
message = "Spacecraft has no communication path to the ground station.")
pattern noLinkToGroundStation(Spacecraft : Spacecraft) {
ConstellationMission.groundStationNetwork(Mission, GroundStation);
ConstellationMission.spacecraft(Mission, Spacecraft);
neg find indirectCommunicationLink(Spacecraft, GroundStation);
}
// No communication loops may exist
// No spacecraft may directly communicate with itself
@Constraint(severity = "error", key = {Element},
message = "Communication loop.")
pattern communicationLoop(Element : CommunicatingElement) {
find indirectCommunicationLink(Element, Element);
}
private pattern indirectCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) {
find directCommunicationLink+(Source, Target);
}
private pattern directCommunicationLink(Source : CommunicatingElement, Target : CommunicatingElement) {
DirectedCommunicationLink.source(Link, SourceSubsystem);
DirectedCommunicationLink.target(Link, TargetSubsystem);
CommunicatingElement.commSubsystem(Source, SourceSubsystem);
CommunicatingElement.commSubsystem(Target, TargetSubsystem);
}
// Source and target communication systems must be compatible.
@Constraint(severity = "error", key = {Link},
message = "Two ends of a communication link must use the same band.")
pattern incompatibleSourceAndTargetBand(Link : DirectedCommunicationLink) {
DirectedCommunicationLink.source(Link, SourceSubsystem);
DirectedCommunicationLink.target(Link, TargetSubsystem);
CommSubsystem.band(SourceSubsystem, Band);
neg find commSubsystemBand(TargetSubsystem, Band);
}
private pattern commSubsystemBand(Comm : CommSubsystem, Band : TransceiverBand) {
CommSubsystem.band(Comm, Band);
}
@Constraint(severity = "error", key = {Link},
message = "Two ends of a communication link must use the same antenna gain.")
pattern incompatibleSourceAndTargetGain(Link : DirectedCommunicationLink) {
DirectedCommunicationLink.source(Link, SourceSubsystem);
DirectedCommunicationLink.target(Link, TargetSubsystem);
CommSubsystem.gain(SourceSubsystem, Gain);
neg find commSubsystemGain(TargetSubsystem, Gain);
}
private pattern commSubsystemGain(Comm : CommSubsystem, Gain : AntennaGain) {
CommSubsystem.gain(Comm, Gain);
}
// UHF-band transmitters may only be combined with a low gain antenna
@Constraint(severity = "error", key = {Comm},
message = "UHF transceiver must be combined with a low gain antenna.")
pattern uhfAntennaGainNotLow(Comm : CommSubsystem) {
CommSubsystem.band(Comm, TransceiverBand::UHF);
// VIATRA will fail to infer a type constraint for the virtual variable introduced
// when an enum literal appears in a negative pattern call, so we use a helper pattern
// instead of neg find commSubsystemGain(Comm, AntennaGain::LOW);
neg find commSubsystemGainLow(Comm);
}
private pattern commSubsystemGainLow(Comm : CommSubsystem) {
CommSubsystem.gain(Comm, AntennaGain::LOW);
}
// X-band transmitters may only be combined with a medium gain antenna
@Constraint(severity = "error", key = {Comm},
message = "X-band transceiver must be combined with a medium gain antenna.")
pattern xAntennaGainNotMedium(Comm : CommSubsystem) {
CommSubsystem.band(Comm, TransceiverBand::X);
neg find commSubsystemGainMedium(Comm);
}
private pattern commSubsystemGainMedium(Comm : CommSubsystem) {
CommSubsystem.gain(Comm, AntennaGain::MEDIUM);
}
// Ka-band transmitters may only be combined with a medium or high gain antenna
@Constraint(severity = "error", key = {Comm},
message = "Ka-band transceiver must be combined with a medium or high gain antenna.")
pattern kaAntennaGainLow(Comm : CommSubsystem) {
CommSubsystem.band(Comm, TransceiverBand::Ka);
CommSubsystem.gain(Comm, AntennaGain::LOW);
}
// 3U CubeSats are assumed to only be able to downlink to Earth using an X-band trasmitter,
// but cross-link using UHF
@Constraint(severity = "error", key = {Sat},
message = "3U CubeSats can only cross-link using UHF.")
pattern threeUCubeSatWithNonUhfCrossLink(Sat : CubeSat3U) {
CommunicatingElement.commSubsystem(Sat, SourceComm);
neg find commSubsystemBandUhf(SourceComm);
DirectedCommunicationLink.source(Link, SourceComm);
DirectedCommunicationLink.target(Link, TargetComm);
CommunicatingElement.commSubsystem(Target, TargetComm);
neg find groundStationNetwork(Target);
}
private pattern commSubsystemBandUhf(Comm : CommSubsystem) {
CommSubsystem.band(Comm, TransceiverBand::UHF);
}
private pattern groundStationNetwork(Network : GroundStationNetwork) {
GroundStationNetwork(Network);
}
// Only a Small Satellite can be configured with a Ka-band communication system
@Constraint(severity = "error", key = {Spacecraft},
message = "Only a Small Satellite can be configured with a Ka-band communication system.")
pattern cubeSatWithKaAntenna(Spacecraft : Spacecraft) {
CommunicatingElement.commSubsystem.band(Spacecraft, TransceiverBand::Ka);
neg find smallSat(Spacecraft);
}
private pattern smallSat(Sat : SmallSat) {
SmallSat(Sat);
}
|
