campaign (тип сценарію)

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

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

Кампанія: наявні типи сценаріїв, складені в один прогін, де кожне число зчитано з реального прогону названого типу. Чотири розділи в будь-якому поєднанні. PHASES: ланцюгова місія на спільній часовій шкалі -- кожна фаза запускає один або кілька сценаріїв (наприклад, глушіння, потім спуфінг, потім годинник у режимі holdover з інерціальною навігаційною системою, що іде поруч за інерцією, потім тривога цілісності, потім відновлення), їхні виходи зчитуються в іменовані канали (похибка часу годинника проти її межі, відношення потужності несівної до спектральної густини шуму проти порога стеження, рівень захисту проти межі тривоги, похибка позиції, супутники, що стежать, прапорці тривог) за пресетом для кожного типу або за явними шляхами результатів і передискретизуються на спільну сітку утриманням нульового порядку, з межами фаз і подіями; стан передається далі через carry (канал продовжується від кінцевого значення попередньої фази), handoff (число попередньої фази, записане у сценарій цієї фази) та end_at (фаза завершується в момент, який обчислив прогін, наприклад час виявлення монітором спуфінгу). SWEEP: сітка за одним–трьома ключами сценарію через крапку будь-якого типу (цілочисельний сегмент індексує масив таблиць, як у system.2.sisre_m), з метриками, що зчитуються за шляхом результату, і, якщо прогонів більше одного, із засіяним ансамблем Монте-Карло в кожному вузлі. MONTE_CARLO: реалізація k виконується із base_seed + k; кожна метрика повідомляє середнє, стандартне відхилення, перцентилі 5/50/95 за найближчим рангом і бутстреп-довірчий інтервал 95% для середнього із фіксованим зерном. COMPOSE: кілька сценаріїв зі спільними значеннями (потужність і позиція одного глушника, записані в морський і дорожній приймачі), із комбінованим підсумком найкращого/найгіршого. Результат містить хеш кампанії, дайджест за всіма результатами учасників і запис одиниць для кожного виданого числа; експорти інтероперабельності записують кожен сценарій-учасник, що має геометрію, як окремий набір файлів. Тотожності композиції перевірено тестами: кампанія з однієї фази відтворює окремий прогін біт у біт, ансамбль із фіксованим зерном байт-стабільний, а на годиннику з білим частотним шумом середнє ансамблю потрапляє в повідомлений інтервал, а розкид відповідає sqrt(q_wf * tau). MODELLED: адитивне перенесення та утримання нульового порядку є модельними виборами, і кожна фаза несе позначку типу, що її виконав.

Один прогін scenarios/campaign-sweep-jammer-power.toml підсумовується так: кампанія 46aa07cb58fb | Перебір потужності глушника: доступність і J/S залежно від потужності передавача | перебір за jamming: 13 вузлів за [jammer_power] | 13 прогонів учасників (MODELLED)

Входи#

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

• Обов'язкові поля: немає
• Необов'язкові поля: title, seed, timeline, phases, sweep, monte_carlo, compose

Приклад scenarios/campaign-sweep-jammer-power.toml задає, серед іншого:

Запуск#

kshana scenarios/campaign-sweep-jammer-power.toml

Цей тип використовують 22 вбудованих сценаріїв; решта — у scenarios/.

Що це дає#

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

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

Докази#

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

• MODELLED iq::campaign::detect і виконавець кампанії: необов'язкова таблиця [monitors] запускає монітори IQ на кожній комірці за єдиний прохід виконавця. Тести: iq_campaign.rs.
• MODELLED iq::campaign::detect (windows, roc) та iq::campaign::report::rocs: кожна комірка кампанії з моніторами зберігає для кожного типу тривоги й каналу максимум власної тестової статистики монітора за кожне заявлене вікно події (додатне) та за
• MODELLED iq::labfit (campaign, cn0, iqfit, iqreport) та [input] campaign у kshana iq labfit, Python kshana.iq_labfit і інструмент labfit для MCP (лише теки кампаній у його робочому каталозі): зчитує вихідну теку kshana iq campaign за її Тести: iq_labfit_followup.rs.
• MODELLED Фази типу campaign: кожна фаза запускає один або кілька сценаріїв наявних типів через run_toml, зчитує їхні виходи в іменовані канали (похибка часу годинника та межа, середнє ефективне відношення потужності несівної до спектральної густини шуму та поріг стеження, v Тести: campaign_composition_reference.rs.
• і ще 4 у матриці.

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

• MODELLED Геометричний бюджет лінії J/S, протизавадове C/N₀, втрата захоплення для кожного супутника. Оракул (InternalConsistency): Рівняння бюджету лінії протизавадового C/N₀, перехресно перевірене незалежним повторним виведенням у numpy (використовує ту саму замкнену форму → InternalConsistency), а також характеристика деградації C/N₀ за реальним JammerTest-2024. 0,30 раунд 2, заблоковано (залишається MODELLED): виміряне зниження C/N0 у JammerTest 2024 порівняно з прогнозом бюджету лінії (попередньо зареєстровано 6a66994b, у межах 3 дБ) не виконано, бо позиція та напрямок антени F8.1 на
• MODELLED Детерміновані, хешовані за сценарієм, SBOM + міжплатформні еталонні шлюзи. Оракул (ExternalDataset): відповідність SBOM офіційній схемі JSON CycloneDX 1,5 (+ дійсні ідентифікатори SPDX) — зовнішній опублікований стандарт, нуль помилок валідації на всьому графі залежностей; частина щодо детермінованості FoM / побайтової відтворюваності залишається закріпленою перевіркою самоузгодженості, тому рядок залишається MODELLED
• PARTNER Не надається — Kshana моделює характеристики сигналу, а не корисне навантаження чи антенне обладнання. Оракул (NoneKind): немає: дисципліна, якою володіє партнер, за задумом без модуля і без тесту
• MODELLED Перебір типу campaign (один–три ключі через крапку будь-якого типу, за значеннями осей узагальненого перебору, за потреби з ансамблем у кожному вузлі) та розділи monte_carlo. Оракул (InternalConsistency): Замкнена форма випадкового блукання фази при білому частотному шумі, дисперсія q_wf tau (NIST Technical Note 1337), для статистичного апарату та байтова рівність з окремими прогонами для засівання. Вона перевіряє арифметику ансамблю на власній моделі годинника рушія, а не на зовнішньому наборі даних

Обмеження#

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

• MODELLED композиція наявних типів сценаріїв. Кожне число зчитано з реального прогону названого типу; ланцюгування (адитивне перенесення каналу через межу фази, утримання нульового порядку на сітці часової шкали, фаза, що завершується в обчислений момент) є модельним вибором, і кожна фаза несе позначку типу, що її створив. (результат label)
• MODELLED: адитивне перенесення та утримання нульового порядку є модельними виборами, і кожна фаза несе позначку типу, що її виконав. (каталог типів (kshana kinds --json))
• MODELLED: так само, як у типу jamming. (коментар у файлі сценарію, рядок 14)
• Стійкість до глушіння в умовах відсутності GNSS є MODELLED, а не перевіреною (validated): звірено з власною замкненою / аналітичною тотожністю — виявляє помилки перенесення та коефіцієнтів, але не є зовнішнім оракулом. (матриця верифікації (docs/MODELLED-RATIONALE.md))
• Відтворюваність і гарантування якості програмного забезпечення — MODELLED, а не перевірено за зовнішнім еталоном: підтвердження частини вимоги перевірено зовні, але вся можливість складається з обчислених за моделлю частин, тому можливість залишається обчисленою за моделлю. (матриця верифікації (docs/MODELLED-RATIONALE.md))
• Перебори параметрів і засіяні ансамблі Монте-Карло за будь-яким типом сценарію є MODELLED, а не перевіреними (validated): звірено з власною замкненою / аналітичною тотожністю — виявляє помилки перенесення та коефіцієнтів, але не є зовнішнім оракулом. (матриця верифікації (docs/MODELLED-RATIONALE.md))

Див. також#

• Сторінка родини: Кампанії
• Усі різновиди: KINDS.md
• Тематична сторінка: LEO-PNT.md
• Тематична сторінка: RESILIENCE-CROSSWALK.md