Машинний переклад, не перевірений носієм мови. Еталоном є англійська версія.

Сторінки видів сценаріївРедагувати на GitHubДжерело: docs/kinds/by-kind/aperture-duty-cycle.md

aperture-duty-cycle (різновид сценарію)

Різновид сценарію рушія v0.40.0, родина Аналіз місій, лінії та космічні операції. Лише консультативно: результат аналізу від дослідницького та інженерного інструмента; це не навігаційне обладнання із затвердженням типу і не послуга забезпечення безпеки життя. Кожна позначка тут — рушія або матриці верифікації; різновид є MODELLED, якщо матриця не каже іншого (як заслужити позначку: розділ README про докази).

Що він робить#

Робочий цикл апертур: розподіл часу між навігацією та зв'язком, який контактний план передбачає для пулу керованих апертур. Приймає контактний план (список вікон aos_s/los_s у [[contacts]], кожне з яких просить навігацію або зв'язок — той самий словник aos_s/los_s, який видає предиктор passes), кількість апертур і ПОЛІТИКУ АРБІТРАЖУ (за замовчуванням пріоритет навігації, або пріоритет зв'язку, або невитісний принцип «першим прийшов — першим обслужено») і повідомляє робочий цикл навігації, робочий цикл зв'язку, цикл простою та простій на сеанс — час контакту, який сеанс запитав і якого жодна апертура не обслужила. Точне зведення інтервалів за межами вікон, тож вікна, що торкаються, ніколи не конкурують і жодна секунда апертури не враховується двічі; секунди апертур навігації, зв'язку та простою накопичуються незалежно й замикаються на apertures*horizon_s. Звіт називає розв'язану політику, її повне визначення та визначення робочого циклу й простою, бо цифра робочого циклу, наведена без політики арбітражу, не є відтворюваною. MODELLED арифметика планування: жодного часу розвороту / перенастроювання / перемикання не нараховується, коли апертура змінює послугу чи сеанс, жоден обсяг даних, стан буфера, енергетичний бюджет чи замикання лінії не входить у рішення, а вікна контактів є входами — їхня геометрія така, яку створило те, що їх породило. Не продукт планування наземного сегмента.

Один прогін scenarios/aperture-duty-cycle.toml підсумовується так: aperture-duty-cycle: 6 сеансів на 2 апертурах за пріоритету навігації -> робочий цикл навігації 0,1167, робочий цикл зв'язку 0,2667, простій 0,6167; 0 с із 6900 с запитаних втрачено через конкуренцію (MODELLED)

Входи#

Зі схеми (kshana kinds --json):

  • Обов'язкові поля: немає
  • Необов'язкові поля: apertures, arbitration, horizon_start_s, horizon_end_s, contacts

Приклад scenarios/aperture-duty-cycle.toml задає, серед іншого:

Поле Значення Одиниця
apertures 2 кількість
arbitration navigation-priority text
contacts[0].aos_s 0 s
contacts[0].los_s 600 s
contacts[0].name nav-1 text
contacts[0].service navigation text
contacts[1].aos_s 300 s
contacts[1].los_s 1500 s
contacts[1].name comms-1 text
contacts[1].service communications text
contacts[2].aos_s 3600 s
contacts[2].los_s 4500 s

Запуск#

kshana scenarios/aperture-duty-cycle.toml

Що це дає#

Скалярні результати цього прогону з одиницями, які вказує рушій:

Результат Значення Одиниця
aperture_seconds_available 18000 aperture*s
apertures 2 кількість
arbitration_policy navigation-priority text
arbitration_policy_default navigation-priority text
communications_duty 0.266667 частка (безрозмірна)
communications_served_aperture_s 4800 aperture*s
contention_s 0 s
evidence.id_rule стабільний ідентифікатор рядка матриці (ID text
evidence.matrix docs/VERIFICATION-MATRIX.md text
evidence.tier MODELLED text

Позначка результату (рушія): MODELLED — арифметика планування апертур за наданим контактним планом: точне зведення інтервалів розподілу часу між навігацією та зв'язком і втрат від конкуренції на сеанс за іменованою політикою арбітражу. Жодного часу розвороту / перенастроювання / перемикання не нараховується, коли апертура змінює послугу чи сеанс,

Діаграма, яку рушій записує для scenarios/aperture-duty-cycle.toml, різновид aperture-duty-cycle

Докази#

MODELLED: рядки матриці верифікації, що називають цей різновид.

  • MODELLED Один прогін приймає контактний план (список вікон aos_s/los_s, кожне з яких просить апертуру для навігації або зв'язку — той самий словник вікон, який видає passes::predict_passes, перетворений через aperture_duty::windows_from_passes), кількість апертур

Рядки, які задіяв сам прогін, з оракулом, що його дає матриця кожному (публічні джерела названі там):

  • MODELLED Детерміновані, хешовані за сценарієм, SBOM + міжплатформні еталонні шлюзи. Оракул (ExternalDataset): відповідність SBOM офіційній схемі JSON CycloneDX 1,5 (+ дійсні ідентифікатори SPDX) — зовнішній опублікований стандарт, нуль помилок валідації на всьому графі залежностей; частина щодо детермінованості FoM / побайтової відтворюваності залишається закріпленою перевіркою самоузгодженості, тому рядок залишається MODELLED
  • MODELLED Один прогін приймає контактний план (список вікон aos_s/los_s, кожне з яких просить апертуру для навігації або зв'язку — той самий словник вікон, який видає `passes::pre. Оракул (InternalConsistency): внутрішня узгодженість, з трьох величин, обчислених різними виразами в тому самому зведенні й потім зобов'язаних замкнутися. Апертурні секунди навігації, апертурні секунди зв'язку та апертурні секунди простою накопичуються окремо — простій з (apertures − |served|) на елементарний інтервал, ніколи як залишок — і їхню суму перевіряють на рівність apertures × horizon_s, чого хибно розставлена межа, подвійний

Обмеження#

Що, за власним звітом прогону, не обчислено за моделлю або не перевірено за зовнішнім еталоном:

  • MODELLED — арифметика планування апертур за наданим контактним планом: точне зведення інтервалів розподілу часу між навігацією та зв'язком і втрат від конкуренції на сеанс за іменованою політикою арбітражу. Жодного часу розвороту / перенастроювання / перемикання не нараховується, коли апертура змінює послугу чи сеанс, жоден обсяг даних, стан буфера, енергетичний бюджет чи замикання лінії не входить у рішення, а вікна контактів є входами — їх (результат label)
  • MODELLED арифметика планування: жодного часу розвороту / перенастроювання / перемикання не нараховується, коли апертура змінює послугу чи сеанс, жоден обсяг даних, стан буфера, енергетичний бюджет чи замикання лінії не входить у рішення, а вікна контактів є входами — їхня геометрія така, яку створило те, що їх породило. (каталог різновидів (kshana kinds --json))
  • ЧЕСНИЙ ОБСЯГ: MODELLED арифметика планування над наданими вікнами. Жодного часу розвороту / перенастроювання / перемикання не нараховується, коли апертура змінює послугу чи сеанс; жоден обсяг даних, стан буфера, енергетичний бюджет чи замикання лінії не входить у рішення; а вікна контактів є входами -- їхня геометрія така, яку створило те, що їх породило (сценарій passes видає той самий словник aos_s / los_s). Не планування наземного (коментар у файлі сценарію, рядки 18–24)
  • Відтворюваність і гарантування якості програмного забезпечення — MODELLED, а не перевірено за зовнішнім еталоном: підтвердження частини вимоги перевірено зовні, але вся можливість складається з обчислених за моделлю частин, тому можливість залишається обчисленою за моделлю. (матриця верифікації (docs/MODELLED-RATIONALE.md))
  • Робочий цикл апертур між навігацією та зв'язком — MODELLED, а не перевірено за зовнішнім еталоном: звірено з власною замкненою / аналітичною тотожністю — ловить помилки транскрипції та коефіцієнтів, але не є зовнішнім оракулом. (матриця верифікації (docs/MODELLED-RATIONALE.md))

Див. також#