// Voyager 1, modelled from public NASA/JPL sources and Gen-AI provided by https://apricot.tools. // Facts with a source: launch 1977-09-05, 815 kg launch / 721.9 kg dry, ten-sided bus, // 3.7 m high-gain dish (X 8.4 GHz / S 2.3 GHz), 3 MHW-RTGs (470 W at launch, 225 W in 2023, // about -4 W/year), 16 hydrazine thrusters, eleven investigations, instrument shutdown dates. // Not modelled (no verified source): masses and powers of each unit, bay assignment. package Voyager1 { private import ScalarValues::*; private import RealFunctions::*; metadata def SafetyCritical; // ---- Structure ---------------------------------------------------- port def PowerPort; port def DataPort; port def ControlPort; port def RadioPort; part def Unit { attribute offYear : Real = 0.0; // calendar year the unit was switched off; 0 = still on } // Power part def Rtg :> Unit { attribute launchWatts : Real = 157.0; // each of three; 470 W in total at launch port powerOut : PowerPort; } part def PowerDistribution :> Unit { port busIn : PowerPort; port busOut : PowerPort; } // Brains: each Voyager carries two of each computer (CCS, FDS, AACS). For most of the // mission the two CCS were used non-redundantly to add command capacity; which unit of the // FDS or AACS pair is in use is not public. part def CommandComputer :> Unit { attribute units : Integer = 2; attribute wordBits : Integer = 18; attribute memoryWords : Integer = 4096; // plated-wire, non-volatile, per unit port powerIn : PowerPort; port command : ControlPort; port telemetry : DataPort; } part def FlightDataSystem :> Unit { attribute units : Integer = 2; attribute wordBits : Integer = 16; attribute memoryWords : Integer = 8198; // per unit // Memory-chip fault: Nov 14 2023 all telemetry stopped, Apr 20 2024 engineering data // returned after code was relocated around the bad chip, science data came back from // May 2024 with full recovery of the powered instruments in June 2024. attribute faultFrom : Real = 2023.87; attribute engineeringFrom : Real = 2024.30; attribute scienceFrom : Real = 2024.50; port powerIn : PowerPort; port telemetry : DataPort; port storage : DataPort; port radio : DataPort; } part def AttitudeControl :> Unit { attribute units : Integer = 2; attribute wordBits : Integer = 18; attribute memoryWords : Integer = 4096; // per unit port powerIn : PowerPort; port command : ControlPort; port thrust : ControlPort; port scan : ControlPort; } part def TapeRecorder :> Unit { attribute capacityMB : Real = 64.0; attribute tracks : Integer = 8; attribute records : String = "plasma wave high-rate data, played back about every six months"; port record : DataPort; } // Telecom part def HighGainAntenna :> Unit { attribute diameter : Real = 3.7; // m, Cassegrain attribute gainXdB : Real = 47.0; // transmit boresight gain, PDS attribute gainSdB : Real = 36.0; attribute beamHalfWidthXDeg : Real = 0.32; // half-power half-width, PDS attribute beamHalfWidthSDeg : Real = 1.1; port feed : RadioPort; } part def RadioSubsystem :> Unit { attribute xBandGHz : Real = 8.4; attribute sBandGHz : Real = 2.3; attribute downlinkBps : Real = 160.0; // normal telemetry attribute uplinkBps : Real = 16.0; attribute xBandWatts : String = "12 or 22"; // selectable transmitter output, PDS attribute sBandWatts : String = "9 or 26"; port powerIn : PowerPort; port feed : RadioPort; port telemetry : DataPort; } // Propulsion part def HydrazineTank :> Unit { port feedLine : ControlPort; } part def Thruster :> Unit { port valve : ControlPort; } // One branch of thrusters. JPL: two attitude branches and one trajectory-correction (TCM) branch. part def ThrusterBranch :> Unit { attribute role : String; attribute pointingFrom : Real = 0.0; // calendar year the branch took over pointing; 0 = never used for it attribute pointingTo : Real = 0.0; // calendar year it handed pointing over; 0 = no end stated } // Science part def Instrument :> Unit { attribute acronym : String; attribute range : String; // what it measures, as NASA publishes it port data : DataPort; } part def ScanPlatform :> Unit { port drive : ControlPort; } // Mission milestones: calendar year and distance from the Sun (AU). Planet distances are // approximate (the planet's orbit radius); 94 AU for the termination shock is not verified. part def MissionEvent { attribute atYear : Real; attribute sunAU : Real; } part def GoldenRecord :> Unit { attribute diameterCm : Real = 30.0; // gold-plated copper disc in an aluminum cover attribute rpm : Real = 16.6667; // 16 2/3 rpm, played outside in attribute minutesPerSide : Real = 53.5; // 53 to 54 minutes attribute pulsarsOnCover : Integer = 14; } part def Spacecraft { part rtgs : Rtg[3]; part power : PowerDistribution; part ccs : CommandComputer; part fds : FlightDataSystem; part aacs : AttitudeControl; part dtr : TapeRecorder; part radio : RadioSubsystem; part hga : HighGainAntenna; part tank : HydrazineTank; part thrusters : Thruster[16]; part attitude1 : ThrusterBranch; part attitude2 : ThrusterBranch; part tcm : ThrusterBranch; part scanPlatform : ScanPlatform; part iss : Instrument; part iris : Instrument; part uvs : Instrument; part pps : Instrument; part mag : Instrument; part pws : Instrument; part pls : Instrument; part lecp : Instrument; part crs : Instrument; part pra : Instrument; part record : GoldenRecord; part liftoff : MissionEvent; part jupiter : MissionEvent; part saturn : MissionEvent; part paleBlueDot : MissionEvent; part shock : MissionEvent; part heliopause : MissionEvent; attribute launchMassKg : Real = 815.0; attribute dryMassKg : Real = 721.9; attribute launchYear : Real = 1977.68; // 1977-09-05 attribute launchWatts : Real = 470.0; attribute watts2023 : Real = 225.0; attribute wattsLostPerYear : Real = 4.0; attribute distanceAU : Real = 172.52; // October 2026 attribute lightMinutesPerAU : Real = 8.317; // Fuel burned over the mission (launch minus dry mass) attribute propellantKg : Real = launchMassKg - dryMassKg; // Light travel time to Earth, hours, one way attribute lightHours : Real = distanceAU * lightMinutesPerAU / 60.0; attribute roundTripHours : Real = 2.0 * lightHours; // Output after 2023: straight line at the quoted loss attribute watts2026 : Real = watts2023 - wattsLostPerYear * 3.0; connect rtgs.powerOut to power.busIn; connect power.busOut to ccs.powerIn; connect power.busOut to fds.powerIn; connect power.busOut to aacs.powerIn; connect power.busOut to radio.powerIn; connect ccs.command to aacs.command; connect ccs.telemetry to fds.telemetry; connect fds.storage to dtr.record; connect fds.radio to radio.telemetry; connect radio.feed to hga.feed; connect aacs.thrust to thrusters.valve; connect aacs.thrust to tank.feedLine; connect aacs.scan to scanPlatform.drive; connect iss.data to fds.telemetry; connect iris.data to fds.telemetry; connect uvs.data to fds.telemetry; connect pps.data to fds.telemetry; connect mag.data to fds.telemetry; connect pws.data to fds.telemetry; connect pls.data to fds.telemetry; connect lecp.data to fds.telemetry; connect crs.data to fds.telemetry; connect pra.data to fds.telemetry; } // The spacecraft, with the dates NASA publishes for each shutdown. part voyager1 : Spacecraft { part :>> rtgs { @SafetyCritical; } part :>> power { @SafetyCritical; } part :>> liftoff { attribute :>> atYear = 1977.68; attribute :>> sunAU = 1.0; } // Sep 5 1977 part :>> jupiter { attribute :>> atYear = 1979.18; attribute :>> sunAU = 5.2; } // closest approach Mar 5 1979 part :>> saturn { attribute :>> atYear = 1980.87; attribute :>> sunAU = 9.5; } // closest approach Nov 12 1980 part :>> paleBlueDot { attribute :>> atYear = 1990.12; attribute :>> sunAU = 40.0; } // Feb 14 1990, about six billion km part :>> shock { attribute :>> atYear = 2004.96; attribute :>> sunAU = 94.0; } // estimated Dec 15 2004 part :>> heliopause { attribute :>> atYear = 2012.65; attribute :>> sunAU = 121.0; } // announced Aug 25 2012 part :>> attitude1 { attribute :>> role = "attitude"; attribute :>> pointingFrom = 1977.68; attribute :>> pointingTo = 2002.0; } // first attitude branch until the 2002 switch part :>> attitude2 { attribute :>> role = "attitude"; attribute :>> pointingFrom = 2002.0; attribute :>> pointingTo = 2018.0; } // second attitude branch, 2002 to the 2018 switch part :>> tcm { attribute :>> role = "trajectory correction"; attribute :>> pointingFrom = 2018.0; attribute :>> pointingTo = 2024.65; } // pointing 2018 to Aug 27 2024 (swap back) part :>> aacs { @SafetyCritical; } part :>> hga { @SafetyCritical; } part :>> radio { @SafetyCritical; } part :>> iss { attribute :>> acronym = "ISS"; attribute :>> range = "two cameras, 8 filters each: wide-angle 200 mm f/3, narrow-angle 1500 mm f/8.5"; attribute :>> offYear = 1990.12; } // Feb 14 1990 part :>> iris { attribute :>> acronym = "IRIS"; attribute :>> range = "2.5-50 um and 0.3-2.0 um"; attribute :>> offYear = 1998.42; } // Jun 3 1998 part :>> uvs { attribute :>> acronym = "UVS"; attribute :>> range = "40-180 nm"; attribute :>> offYear = 2016.30; } // Apr 19 2016 part :>> pps { attribute :>> acronym = "PPS"; attribute :>> range = "0.2 m telescope, 8 wavelengths 235-750 nm"; attribute :>> offYear = 1980.08; } // Jan 29 1980 part :>> mag { attribute :>> acronym = "MAG"; attribute :>> range = "triaxial fluxgate, 4 sensors (2 high-field, 2 low-field)"; @SafetyCritical; } part :>> pws { attribute :>> acronym = "PWS"; attribute :>> range = "10 Hz to 56 kHz"; @SafetyCritical; } part :>> pls { attribute :>> acronym = "PLS"; attribute :>> range = "low-energy ions and electrons"; attribute :>> offYear = 2007.08; } // Feb 1 2007 part :>> lecp { attribute :>> acronym = "LECP"; attribute :>> range = "low-energy charged particles; its 0.5 W motor stays on"; attribute :>> offYear = 2026.29; } // Apr 17 2026 part :>> crs { attribute :>> acronym = "CRS"; attribute :>> range = "electrons 3-110 MeV, nuclei 1-500 MeV/nucleon"; attribute :>> offYear = 2025.15; } // Feb 25 2025 part :>> pra { attribute :>> acronym = "PRA"; attribute :>> range = "20.4-1300 kHz and 2.3-40.5 MHz"; attribute :>> offYear = 2008.04; } // Jan 15 2008 // Declared here rather than at package level (the editor's validator reads // a package-level satisfy as a second declaration of the requirement). satisfy pointing by voyager1; satisfy science by voyager1; satisfy talking by voyager1; } // ---- Requirements ------------------------------------------------- requirement def KeepScience { subject craft : Spacecraft; attribute minInstruments : Real; attribute running : Real; doc /* At least minInstruments science investigations keep returning data. */ require constraint enough { running >= minInstruments } } requirement def KeepTalking { subject craft : Spacecraft; attribute minBps : Real; doc /* The downlink keeps at least minBps through the high-gain dish. */ require constraint fast { craft.radio.downlinkBps >= minBps } } requirement def KeepPointing { subject craft : Spacecraft; doc /* Attitude control keeps the dish on Earth: it is a safety-critical unit. */ } requirement <'R-01'> pointing : KeepPointing; requirement <'R-02'> science : KeepScience { attribute :>> minInstruments = 1.0; attribute :>> running = 2.0; // MAG and PWS after April 2026 } requirement <'R-03'> talking : KeepTalking { attribute :>> minBps = 40.0; } assert constraint scienceCheck { 2.0 >= 1.0 } assert constraint downlinkCheck { voyager1.radio.downlinkBps >= 40.0 } assert constraint massBalance { voyager1.propellantKg >= 90.0 & voyager1.propellantKg <= 100.0 } // How the pointing requirement is verified: the telemetry carries the attitude error. verification def AttitudeTelemetry { subject craft : Spacecraft; VerificationCases::PassIf(craft.radio.downlinkBps >= 40.0) } verification checkAttitude : AttitudeTelemetry { subject craft = voyager1; objective { verify pointing; } } }