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);
}

@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, TransceiverBand::UHF);
	CubeSat3U(From);
} or {
	find matchingAntenna(From, To, _);
	CubeSat3U(From);
	GroundStationNetwork(To);
}

private pattern matchingAntenna(From : Spacecraft, To : CommunicatingElement, Band : TransceiverBand) {
	CommunicatingElement.commSubsystem.band(From, Band);
	CommunicatingElement.commSubsystem.band(To, Band);
	CommunicatingElement.commSubsystem.gain(From, Gain);
	CommunicatingElement.commSubsystem.gain(To, Gain);
}

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) {
	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);
}

pattern smallSat(Sat : SmallSat) {
	SmallSat(Sat);
}

@QueryBasedFeature(feature = "kind")
pattern spacecraftOfKind(Spacecraft : Spacecraft, Kind : SpacecraftKind) {
	CubeSat3U(Spacecraft);
	Kind == SpacecraftKind::CubeSat3U;
} or {
	CubeSat6U(Spacecraft);
	Kind == SpacecraftKind::CubeSat6U;
} or {
	SmallSat(Spacecraft);
	Kind == SpacecraftKind::SmallSat;
}

/*
//
// 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, TransceiverBand::UHF, Target);
	Spacecraft(Target);
	TransmitRate == 5.0;
} or {
	find spacecraftUplink(Spacecraft, TransceiverBand::X, Target);
	Spacecraft(Target);
	TransmitRate == 1.6;
} or {
	find spacecraftUplink(Spacecraft, TransceiverBand::X, Target);
	GroundStationNetwork(Target);
	TransmitRate == 0.7;
} or {
	find spacecraftUplink(Spacecraft, TransceiverBand::Ka, Target);
	Spacecraft(Target);
	TransmitRate == 220.0;
} or {
	find spacecraftUplink(Spacecraft, TransceiverBand::Ka, Target);
	GroundStationNetwork(Target);
	TransmitRate == 80.0;
}

private pattern spacecraftUplink(Spacecraft : Spacecraft, Band : TransceiverBand, Target : CommunicatingElement) {
	CommunicatingElement.communicationLink(Spacecraft, Link);
	DirectedCommunicationLink.source.band(Link, Band);
	DirectedCommunicationLink.target(Link, 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);
	Spacecraft.kind(Spacecraft, Kind);
	KindCount == count find spacecraftOfKind(_, Kind);
	find basePrice(Spacecraft, BasePrice);
	find interferometryPayloadCost(Spacecraft, InterferometryPayloadCost);
	find additionalCommSubsystemCost(Spacecraft, AdditionalCommSubsystemCost);
	Cost == eval(BasePrice * Math.pow(KindCount, -0.25) + InterferometryPayloadCost + AdditionalCommSubsystemCost);
}

private pattern basePrice(Spacecraft : Spacecraft, BasePrice : java Double) {
	Spacecraft.kind(Spacecraft, SpacecraftKind::CubeSat3U);
	BasePrice == 250000.0;
} or {
	Spacecraft.kind(Spacecraft, SpacecraftKind::CubeSat6U);
	BasePrice == 750000.0;
} or {
	Spacecraft.kind(Spacecraft, SpacecraftKind::SmallSat);
	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;
}
*/