Add satellite case study

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 @@
+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;
+//}
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 @@
+package hu.bme.mit.inf.dslreasoner.domains.satellite.runner
+
+import hu.bme.mit.inf.dslreasoner.application.execution.StandaloneScriptExecutor
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngineOptions
+import org.eclipse.viatra.query.runtime.rete.matcher.ReteBackendFactory
+
+final class SatelliteGeneratorMain {
+        private new() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly.")
+        }
+
+        public static def void main(String[] args) {
+                ViatraQueryEngineOptions.setSystemDefaultBackends(ReteBackendFactory.INSTANCE, ReteBackendFactory.INSTANCE,
+                        ReteBackendFactory.INSTANCE)
+                println(StandaloneScriptExecutor.executeScript("configs/generation.vsconfig"))
+        }
+}