lunar-time-budget (rodzaj scenariusza)
Rodzaj scenariusza silnika v0.40.0, rodzina Przestrzeń księżycowa i cislunarna. Wyłącznie doradczo: wynik analizy z narzędzia badawczo-inżynieryjnego; nie jest to sprzęt nawigacyjny z zatwierdzeniem typu ani usługa bezpieczeństwa życia. Każda etykieta tutaj pochodzi od silnika lub z macierzy weryfikacji; rodzaj jest MODELLED, o ile macierz nie mówi inaczej (jak zdobywa się etykietę: sekcja Evidence w README).
Co robi#
MODELLED kompletny budżet błędu czasu Koordynowanego Czasu Księżycowego (LTC): siedem składników błędu LTC złożonych jako krzywe błędu czasu x_i(τ) po całej siatce czasów uśredniania, sumowanych pierwiastkowo do x_Σ(τ), oraz PUNKT PRZECIĘCIA zegar–układ odniesienia τ, w którym rosnący składnik zegara wyprzedza stały składnik realizacji układu odniesienia w czasie rzeczywistym (poniżej niego budżet jest ograniczony układem odniesienia, powyżej zegarem) — uczciwa odpowiedź na artefakt pojedynczego τ. Nachylenia względem τ są w postaci zamkniętej i można je sprawdzić analitycznie (zegar τ^{+1/2}/τ^{+1}, poziomy τ^0, pomiar τ^{-1/2}), a wiersze zegara odtwarzają opublikowane jednodobowe specyfikacje zegarów (crate::clock_specs); WIELKOŚCI poziomów łącza RF/optycznego, realizacji układu odniesienia, reszty relatywistycznej i efemeryd to modelowane przydziały budżetu (udokumentowane wartości domyślne, możliwe do nadpisania przez wywołującego), a nie pomiary. Wkładem jest odtwarzalny punkt przecięcia τ, a nie certyfikowana liczba dla poszczególnych składników; nie jest certyfikowane do operacyjnego pomiaru czasu.
Jeden przebieg scenarios/lunar-time-budget.toml podsumowuje się tak: lunar-time-budget | zegar passive-h-maser | 7-składnikowe x_Σ(τ) po 57 punktach τ (1–1e7 s) | punkt przecięcia τ 8.689e4 s (x 1.001e-9 s) | poziom układu odniesienia 1.001e-9 s | zegar x(1 d) 0,995 ns (MODELLED)
Wejścia#
Ze schematu (kshana kinds --json):
- Pola wymagane: brak
- Pola opcjonalne:
clock,tau_min_s,tau_max_s,points_per_decade,clocks,time_lab
Przykład scenarios/lunar-time-budget.toml ustawia między innymi:
| Pole | Wartość | Jednostka |
|---|---|---|
clock |
passive-h-maser | tekst |
kind |
lunar-time-budget | tekst |
Uruchom#
kshana scenarios/lunar-time-budget.toml
Tego rodzaju używa 2 dołączonych scenariuszy; pozostałe są w scenarios/.
Co daje#
Wyniki skalarne tego przebiegu, z jednostkami podanymi przez silnik:
| Wynik | Wartość | Jednostka |
|---|---|---|
clock |
passive-h-maser | tekst |
crossover_tau_s |
86894.284677 | s |
crossover_x_s |
1.0007e-9 | s |
evidence.id_rule |
stabilny identyfikator wiersza macierzy (ID | tekst |
evidence.matrix |
docs/VERIFICATION-MATRIX.md | tekst |
evidence.tier |
MODELLED | tekst |
frame_term_s |
1.0007e-9 | s |
Etykieta wyniku (silnika): MODELLED kompletny budżet błędu czasu LTC. Nachylenia względem τ są w postaci zamkniętej i można je sprawdzić analitycznie (zegar τ^{+1/2}/τ^{+1}, poziomy τ^0, pomiar τ^{-1/2}), a wiersze zegara odtwarzają opublikowane jednodobowe specyfikacje zegarów; WIELKOŚCI poziomów łącza RF/optycznego, realizacji układu odniesienia, reszty relatywistycznej i efemeryd
Dowody#
MODELLED: wiersze macierzy weryfikacji, które wymieniają ten rodzaj.
- MODELLED Jeden przebieg lunar-time-budget emituje wiersz punktu przecięcia zegar–układ odniesienia dla każdej klasy zegara względem jednego wspólnego składnika układu odniesienia, więc zegar jest jedyną zmienną w porównaniu; każdy wiersz niesie punkt przecięcia uzyskany dwoma sposobami -- wyznaczony przez bisekcję z
- MODELLED Opcjonalny blok [time_lab] scenariusza lunar-time-budget modeluje zegar księżycowej stacji referencyjnej (domyślnie klasa miniRAFS, dowolna nazwana klasa lub karta urządzenia dopasowana do podanych punktów stabilności) sterowany do Koordynowanego Czasu Księżycowego i Testy: lunar_station_time_lab.rs.
Wiersze, które sam przebieg wykorzystał, wraz z wyrocznią, jaką macierz podaje dla każdego (publiczne źródła są tam wymienione):
- MODELLED Deterministyczne, haszowane na poziomie scenariusza, bramki SBOM i złotych wyników między platformami. Wyrocznia (ExternalDataset): zgodność SBOM z oficjalnym schematem JSON CycloneDX 1,5 (+ prawidłowe identyfikatory SPDX): zewnętrzny opublikowany standard, zero błędów walidacji w całym grafie zależności; część dotycząca determinizmu wskaźników jakości i odtwarzalności bajt w bajt pozostaje przypiętą kontrolą samospójności, więc wiersz pozostaje MODELLED
- MODELLED Jeden przebieg lunar-time-budget emituje wiersz punktu przecięcia zegar–układ odniesienia dla każdej klasy zegara względem jednego wspólnego składnika układu odniesienia, więc zegar jest jedyną zmienną w por. Wyrocznia (InternalConsistency): dwa różne obliczenia tej samej wielkości w tej samej bazie kodu, a nie jedno powtórzone: bisekcja na krzywej potęgowej IEEE-1139 nic nie wie o typie szumu, podczas gdy postać zamknięta odwraca dominujący typ algebraicznie, więc błędnie sklasyfikowany typ szumu lub zły przedział objawia się niemałą różnicą względną. Cztery wartości odtwarzają też opublikowaną tabelę z pracy z dokładnością do połowy ostatniej wydrukowanej cyfry -- ale ta tabela była jej własną
- MODELLED Scenariusz lunar-time-budget publikuje swoje wyniki tablicowe jako tabelę w formie długiej (indeks siatki, czas uśredniania, składnik) obok raportu, więc siedem na. Wyrocznia (InternalConsistency): tylko samospójność: opublikowaną sumę sprawdzono względem pierwiastka z sumy kwadratów składników w tym samym pliku, a emitowana krzywa odtwarza opublikowany p3_time_budget_curve.csv we wszystkich 57 punktach. Obie kontrole dzielą własne definicje składników tego silnika, więc żadna nie jest niezależna. Składnik zegara opiera się na opublikowanych specyfikacjach zegarów, ale WIELKOŚCI poziomów łącza, układu odniesienia, relatywistycznego i efemeryd są udokumentowane
Ograniczenia#
Co raport samego przebiegu podaje jako niemodelowane lub niesprawdzone względem niezależnego wzorca:
- MODELLED kompletny budżet błędu czasu LTC. Nachylenia względem τ są w postaci zamkniętej i można je sprawdzić analitycznie (zegar τ^{+1/2}/τ^{+1}, poziomy τ^0, pomiar τ^{-1/2}), a wiersze zegara odtwarzają opublikowane jednodobowe specyfikacje zegarów; WIELKOŚCI poziomów łącza RF/optycznego, realizacji układu odniesienia, reszty relatywistycznej i efemeryd są modelowanymi przydziałami budżetu (udokumentowane wartości domyślne, możliwe do nadpisania przez wywołującego), a nie pomiarami. Wkładem (wynik
label) - MODELLED kompletny budżet błędu czasu Koordynowanego Czasu Księżycowego (LTC): siedem składników błędu LTC złożonych jako krzywe błędu czasu x_i(τ) po całej siatce czasów uśredniania, sumowanych pierwiastkowo do x_Σ(τ), oraz PUNKT PRZECIĘCIA zegar–układ odniesienia τ, w którym rosnący składnik zegara wyprzedza stały składnik realizacji układu odniesienia w czasie rzeczywistym (poniżej niego budżet jest ograniczony układem odniesienia, powyżej zegarem) — uczciwa odpowiedź na artefakt pojedynczego τ (katalog rodzajów (
kshana kinds --json)) - Rzetelność: MODELLED. Nachylenia względem tau są w postaci zamkniętej i można je sprawdzić analitycznie (zegar tau^{+1/2} lub tau^{+1}, poziomy tau^0, pomiar tau^{-1/2}), a wiersze zegara odtwarzają opublikowane jednodobowe specyfikacje zegarów; ale WIELKOŚCI poziomów łącza RF/optycznego, realizacji układu odniesienia, reszty relatywistycznej i efemeryd są modelowanymi przydziałami budżetu (udokumentowane wartości domyślne, możliwe do nadpisania przez wywołującego), a nie pomiarami. Wkładem jest (komentarz w pliku scenariusza, wiersze 13 do 18)
- Odtwarzalność i zapewnienie jakości oprogramowania jest MODELLED, nie jest sprawdzona względem niezależnego wzorca: jedno twierdzenie składowe jest sprawdzone zewnętrznie, ale cała możliwość składa się z elementów obliczonych na podstawie modelu, więc pozostaje obliczona na podstawie modelu. (macierz weryfikacji (docs/MODELLED-RATIONALE.md))
- Tabela księżycowych punktów przecięcia czasu dla poszczególnych klas zegarów ma poziom MODELLED, nie jest niezależnie sprawdzona względem wzorca zewnętrznego: sprawdzono ją względem jej własnej tożsamości w postaci zamkniętej / analitycznej; wychwytuje błędy przepisania i współczynników, ale nie jest zewnętrzną wyrocznią. (macierz weryfikacji (docs/MODELLED-RATIONALE.md))
- Odtwarzalność księżycowego budżetu błędu czasu ma poziom MODELLED, nie jest niezależnie sprawdzona względem wzorca zewnętrznego: sprawdzono ją względem jej własnej tożsamości w postaci zamkniętej / analitycznej; wychwytuje błędy przepisania i współczynników, ale nie jest zewnętrzną wyrocznią. (macierz weryfikacji (docs/MODELLED-RATIONALE.md))
Zobacz też#
- Strona rodziny: Przestrzeń księżycowa i cislunarna
- Wszystkie rodzaje: KINDS.md
- Strona tematu: LUNAR-REFERENCE-STATION.md
- Strona tematu: integrations.md