danesabo/PWR-HYBRID-3
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
PWR-HYBRID-3/fret-pipeline/.archive/specs/DRC/DRCSpec_PWR-3001.smv
Dane Sabo cebf8c167a Initial umbrella repo: thesis + FRET pipeline + plant model with first controllers 
Folds three previously-separate pieces into one preliminary-example repo
for the HAHACS thesis:

- thesis/ (submodule) → gitea Thesis.git — the PhD proposal
- fret-pipeline/ — FRET requirements to AIGER controller (was
  ~/Documents/fret_processing/; prior single-commit history abandoned
  per user decision)
- plant-model/ — 10-state PKE + lumped T/H PWR model (was
  ~/Documents/PKE_Playground/; never version-controlled before)
- presentations/2026DICE/ (submodule) → gitea 2026DICE.git
- reachability/, hardware/ — empty placeholders for Thrust 3 and HIL
- docs/architecture.md — how the discrete and continuous layers compose
- claude_memory/ — session notes and scratch knowledge pattern

Plant model refactored to thesis naming (x, plant, u, ref); pke_th_rhs
now takes u as an explicit arg instead of reading rho_ext from the
params struct. First two controllers built to the contract
u = ctrl_<mode>(t, x, plant, ref): ctrl_null (baseline) and
ctrl_operation (stabilizing, proportional on T_avg). Validated under a
100% -> 80% Q_sg step: ctrl_operation reduces steady-state T_avg drift
~47% vs. the unforced plant.

Root CLAUDE.md emphasizes that CLAUDE.md files are living documents and
that any knowledge not captured before a session ends is lost forever;
claude_memory/ holds the session-level notes that haven't stabilized
enough to graduate into a CLAUDE.md.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-04-16 16:24:11 -04:00

113 lines
32 KiB
Plaintext
Raw Blame History

-- DRCSpec
MODULE main
VAR
t_dot_exceeded:boolean;
Heatup: boolean;
SCRAM: boolean;
DEFINE
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_0 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((Heatup & (X (! Heatup))) & (! (X SCRAM))))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_1 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((Heatup & (X (! Heatup))) & (! (X SCRAM))))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_2 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! (! Heatup)) & (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_3 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) & (! (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_4 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) & (! (X SCRAM)))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_5 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) & (! (X SCRAM)))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_6 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((! (X (! t_dot_exceeded))) & (Heatup & (X (! Heatup))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_7 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((! (X (! t_dot_exceeded))) & (Heatup & (X (! Heatup))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_8 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & (((Heatup & (X (! Heatup))) -> (Heatup & (X (! Heatup)))) U (! ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_9 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & (((Heatup & (X (! Heatup))) -> (Heatup & (X (! Heatup)))) U (! ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_10 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! Heatup) & (! (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_11 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((Heatup & (X (! Heatup))) & (! (X SCRAM))))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_12 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((Heatup & (X (! Heatup))) & (! (X SCRAM))))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_13 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! (! Heatup)) & (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_14 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) & (! (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_15 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) & (! (X SCRAM)))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_16 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((Heatup & (X (! Heatup))) & (! (X SCRAM)))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_17 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((! (X (! t_dot_exceeded))) & (Heatup & (X (! Heatup))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_18 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((! (X (! t_dot_exceeded))) & (Heatup & (X (! Heatup))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_19 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & (((Heatup & (X (! Heatup))) -> (Heatup & (X (! Heatup)))) U (! ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_20 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & (((Heatup & (X (! Heatup))) -> (Heatup & (X (! Heatup)))) U (! ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_21 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F (((! Heatup) & (X (! Heatup))) & (! (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_Heatup_22 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((Heatup & (! (X (! Heatup)))) & (! (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_0 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) & (! ((Heatup & (X (! Heatup))) | (X SCRAM))))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_1 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((X (! t_dot_exceeded)) & (! (Heatup & (X (! Heatup)))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_2 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((t_dot_exceeded & (! ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_3 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) & (! ((Heatup & (X (! Heatup))) | (X SCRAM))))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_4 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U (((! t_dot_exceeded) & ((X (! t_dot_exceeded)) & (! (Heatup & (X (! Heatup)))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_t_dot_exceeded_5 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((t_dot_exceeded & (! ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & (! ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_SCRAM_0 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((! (Heatup & (X (! Heatup)))) & (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_SCRAM_1 := (! ((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & ((! (! Heatup)) & ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((! (Heatup & (X (! Heatup)))) & (X SCRAM))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_SCRAM_2 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (! t_dot_exceeded)) & ((! (Heatup & (X (! Heatup)))) & (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
-- Req text: While Heatup if t_dot_exceeded DRC shall at the next timepoint satisfy SCRAM
LTLSPEC NAME PWR-3001_SCRAM_3 := (! (((G ((Heatup | (X (! Heatup))) | (X (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM))))))) & (F ((! (Heatup | (X (! Heatup)))) & (X ((((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! (Heatup & (X (! Heatup)))) U ((! (t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup)))))) & ((X ((! (Heatup & (X (! Heatup)))) & (X SCRAM))) & ((! Heatup) | (X Heatup)))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))))) & ((! Heatup) | (((Heatup & (X (! Heatup))) V ((t_dot_exceeded | ((X (! t_dot_exceeded)) | (Heatup & (X (! Heatup))))) | ((X ((Heatup & (X (! Heatup))) | (X SCRAM))) & ((! Heatup) | (X Heatup))))) & ((! t_dot_exceeded) | ((Heatup & (X (! Heatup))) | (X SCRAM)))))));
Reference in New Issue View Git Blame Copy Permalink