From 7adead25f3c8451a51a3f8fa1d45b0b8f93b3a69 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sun, 10 May 2020 22:09:17 +0200 Subject: Add satellite case study --- .../domains/satellite/queries/SatelliteQueries.vql | 325 +++++++++++++++++++++ 1 file changed, 325 insertions(+) create mode 100644 Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql (limited to 'Domains/hu.bme.mit.inf.dslreasoner.domains.satellite/src/hu/bme/mit/inf/dslreasoner/domains/satellite/queries/SatelliteQueries.vql') 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 @@ +package hu.bme.mit.inf.dslreasoner.domains.satellite.queries + +import "http://www.example.org/satellite" + +@Constraint(severity = "error", key = {Element}, + message = "A communicating element may not have two transmitting communication subsystems.") +pattern communicationLinkDoesNotStartAtContainingElement(Element : CommunicatingElement) { + find transmittingCommSubsystem(Element, Comm1); + find transmittingCommSubsystem(Element, Comm2); + Comm1 != Comm2; +} + +private pattern transmittingCommSubsystem(Element : CommunicatingElement, Comm : CommSubsystem) { + CommunicatingElement.commSubsystem(Element, Comm); + CommSubsystem.target(Comm, _); +} + +@Constraint(severity = "error", key = {Station}, + message = "The ground station network may not have outgoing communication links.") +pattern transmittingGroundStationNetwork(Station : GroundStationNetwork) { + find transmittingCommSubsystem(Station, _); +} + +@Constraint(severity = "error", key = {Station}, + message = "The ground station network may not have UHF communication subsystems.") +pattern roundStationNetworkUHF(Station : GroundStationNetwork) { + CommunicatingElement.commSubsystem(Station, Comm); + UHFCommSubsystem(Comm); +} + +// 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); +} + +//@Constraint(severity = "error", key = {Spacecraft}, message = "UNSAT") +//pattern unsat_linkToGroundStation(Spacecraft : Spacecraft) { +// ConstellationMission.groundStationNetwork(Mission, GroundStation); +// ConstellationMission.spacecraft(Mission, Spacecraft); +// find indirectCommunicationLink(Spacecraft, GroundStation); +//} + +@Constraint(severity = "error", key = {Mission}, message = "UNSAT") +pattern unsat_linkToGroundStation(Mission : InterferometryMission) { + InterferometryMission(Mission); + neg find noLinkToGroundStation(_); +} + +@Constraint(severity = "error", key = {Spacecraft}, + message = "Spacecraft has no potential communication path to the ground station.") +pattern noPotentialLinkToGroundStation(Spacecraft : Spacecraft) { + ConstellationMission.groundStationNetwork(Mission, GroundStation); + ConstellationMission.spacecraft(Mission, Spacecraft); + neg find indirectLinkAllowed(Spacecraft, GroundStation); +} + +private pattern indirectLinkAllowed(From : Spacecraft, To : CommunicatingElement) { + find linkAllowed+(From, To); +} + +private pattern linkAllowed(From : Spacecraft, To : CommunicatingElement) { + find matchingAntenna(From, To); + neg find cubeSat3U(From); +} or { + find matchingAntenna(From, To); + CubeSat3U(From); +} or { + find matchingAntenna(From, To); + CubeSat3U(From); + GroundStationNetwork(To); +} + +private pattern matchingAntenna(From : Spacecraft, To : CommunicatingElement) { + CommunicatingElement.commSubsystem(From, FromSys); + CommunicatingElement.commSubsystem(To, ToSys); + find matchingCommSubsystem(FromSys, ToSys); +} + +private pattern matchingCommSubsystem(From : CommSubsystem, To : CommSubsystem) { + UHFCommSubsystem(From); + UHFCommSubsystem(To); +} or { + XCommSubsystem(From); + XCommSubsystem(To); +} or { + KaCommSubsystem(From); + KaCommSubsystem(To); +} + +private pattern cubeSat3U(Sat : CubeSat3U) { + CubeSat3U(Sat); +} + +// 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) { + CommSubsystem.target(SourceSubsystem, TargetSubsystem); + CommunicatingElement.commSubsystem(Source, SourceSubsystem); + CommunicatingElement.commSubsystem(Target, TargetSubsystem); +} + +// Source and target communication systems must be compatible. + +@Constraint(severity = "error", key = {SourceSubsystem}, + message = "Two ends of a communication link must use the same band.") +pattern incompatibleSourceAndTargetBand(SourceSubsystem : CommSubsystem) { + CommSubsystem.target(SourceSubsystem, TargetSubsystem); + neg find matchingCommSubsystem(SourceSubsystem, TargetSubsystem); +} + +// 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); + CommSubsystem.target(SourceComm, TargetComm); + CommunicatingElement.commSubsystem(Target, TargetComm); + neg find groundStationNetwork(Target); +} + +private pattern commSubsystemBandUhf(Comm : UHFCommSubsystem) { + UHFCommSubsystem(Comm); +} + +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(Spacecraft, Comm); + KaCommSubsystem(Comm); + neg find smallSat(Spacecraft); +} + +pattern smallSat(Sat : SmallSat) { + SmallSat(Sat); +} + +//// +//// Metrics +//// +// +//// Coverage +// +//pattern coverageMetric(Coverage : java Double) { +// Coverage == sum find missionCoverage(_, #_); +//} +// +//private pattern missionCoverage(Mission : InterferometryMission, Coverage : java Double) { +// InterferometryMission.observationTime(Mission, ObservationTime); +// ObserverCount == count find spacecraftWithInterferometryPayload(Mission, _); +// Coverage == eval(Math.pow(1 - 2.0 / ObserverCount, 1 + 9 * (1.0 / ObservationTime)) + 0.05 * ObservationTime / 3); +//} +// +//// Time +// +//pattern timeMetric(Time : java Double) { +// Time == sum find missionTime(_, #_); +//} +// +//private pattern missionTime(Mission : InterferometryMission, Time : java Double) { +// InterferometryMission.observationTime(Mission, ObservationTime); +// TrasmitTime == sum find transmitTime(Mission, _, #_); +// Time == eval(TrasmitTime + 60.0 * ObservationTime); +//} +// +//private pattern transmitTime(Mission : InterferometryMission, Spacecraft : Spacecraft, TransmitTime : java Double) { +// ConstellationMission.spacecraft(Mission, Spacecraft); +// find scienceData(Spacecraft, ScienceData); +// IncomingData == sum find incomingData(Spacecraft, _, #_); +// find transmitRate(Spacecraft, TransmitRate); +// TransmitTime == eval((ScienceData + IncomingData) / (7.5 * TransmitRate)); +//} +// +//private pattern incomingData(Spacecraft : Spacecraft, Source : Spacecraft, Data : java Double) { +// find indirectCommunicationLink(Source, Spacecraft); +// find scienceData(Source, Data); +//} +// +//private pattern scienceData(Spacecraft : Spacecraft, Data : java Double) { +// ConstellationMission.spacecraft(Mission, Spacecraft); +// InterferometryMission.observationTime(Mission, ObservationTime); +// Data == eval(12.0 * ObservationTime); +//} +// +//private pattern transmitRate(Spacecraft : Spacecraft, TransmitRate : java Double) { +// find spacecraftUplink(Spacecraft, Comm, Target); +// UHFCommSubsystem(Comm); +// Spacecraft(Target); +// TransmitRate == 5.0; +//} or { +// find spacecraftUplink(Spacecraft, Comm, Target); +// XCommSubsystem(Comm); +// Spacecraft(Target); +// TransmitRate == 1.6; +//} or { +// find spacecraftUplink(Spacecraft, Comm, Target); +// XCommSubsystem(Comm); +// GroundStationNetwork(Target); +// TransmitRate == 0.7; +//} or { +// find spacecraftUplink(Spacecraft, Comm, Target); +// KaCommSubsystem(Comm); +// Spacecraft(Target); +// TransmitRate == 220.0; +//} or { +// find spacecraftUplink(Spacecraft, Comm, Target); +// KaCommSubsystem(Comm); +// GroundStationNetwork(Target); +// TransmitRate == 80.0; +//} +// +//private pattern spacecraftUplink(Spacecraft : Spacecraft, TargetSubsystem : CommSubsystem, Target : CommunicatingElement) { +// CommunicatingElement.commSubsystem.target(Spacecraft, TargetSubsystem); +// CommunicatingElement.commSubsystem(Target, TargetSubsystem); +//} +// +//// Cost +// +//pattern costMetric(Cost : java Double) { +// Cost == sum find missionCost(_, #_); +//} +// +//private pattern missionCost(Mission : InterferometryMission, Cost : java Double) { +// InterferometryMission.observationTime(Mission, ObservationTime); +// SpacecraftCost == sum find spacecraftCost(Mission, _, #_); +// Cost == eval(SpacecraftCost + 100000.0 * ObservationTime); +//} +// +//private pattern spacecraftCost(Mission : InterferometryMission, Spacecraft : Spacecraft, Cost : java Double) { +// ConstellationMission.spacecraft(Mission, Spacecraft); +// find spacecraftOfKindCount(Spacecraft, KindCount); +// find basePrice(Spacecraft, BasePrice); +// find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost); +// find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost); +// Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost); +//} +// +//private pattern spacecraftOfKindCount(Sat : Spacecraft, Count : java Integer) { +// CubeSat3U(Sat); +// Count == count find cubeSat3U(_); +//} or { +// CubeSat6U(Sat); +// Count == count find cubeSat6U(_); +//} or { +// SmallSat(Sat); +// Count == count find smallSat(_); +//} +// +//private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) { +// CubeSat3U(Spacecraft); +// BasePrice == 250000.0; +//} or { +// CubeSat6U(Spacecraft); +// BasePrice == 750000.0; +//} or { +// SmallSat(Spacecraft); +// BasePrice == 3000000.0; +//} +// +//private pattern interferometryPayloadCost(Spacecraft : Spacecraft, Cost : java Double) { +// find spacecraftWithInterferometryPayload(_, Spacecraft); +// Cost == 50000.0; +//} or { +// neg find spacecraftWithInterferometryPayload(_, Spacecraft); +// Cost == 0.0; +//} +// +//private pattern additionalCommSubsystemCost(Spacecraft : Spacecraft, Cost : java Double) { +// find spacecraftWithTwoCommSubsystems(Spacecraft); +// Cost == 100000.0; +//} or { +// neg find spacecraftWithTwoCommSubsystems(Spacecraft); +// Cost == 0.0; +//} +// +//private pattern spacecraftWithTwoCommSubsystems(Spacecraft : Spacecraft) { +// Spacecraft.commSubsystem(Spacecraft, Subsystem1); +// Spacecraft.commSubsystem(Spacecraft, Subsystem2); +// Subsystem1 != Subsystem2; +//} -- cgit v1.2.3-54-g00ecf