dynamis-specs/GPCTController.tla at main · DynamisNetwork/dynamis-specs · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
-------------------------- MODULE GPCTController --------------------------
EXTENDS Integers, Sequences, TLC

(*
    Formal Specification of the Dynamo GPCT Controller

    This Module verifies the "Smart Fluid" State Machine logic:
    1. Regimes: LAMINAR, TRANSITION, TURBULENT, CIRCUIT
    2. Hysteresis: Transitions should be dampended
    3. Safety: High Turbulence MUST trigger Circuit Breaker
    4. Safety: Hard Rug Protection (Exit Gate)
*)

CONSTANTS
    MaxEpochs,       (* Limit verification depth *)
    TurbulenceLevels (* discrete levels of turbulence q_t for checking *)

VARIABLES
    currentRegime,   (* LAMINAR, TRANSITION, TURBULENT, CIRCUIT *)
    turbulenceQ,     (* Current turbulence quantile 0..100 *)
    epoch            (* Current time step *)

vars == <<currentRegime, turbulenceQ, epoch>>

(* Regimes as Integers for simplicity *)
LAMINAR    == 1
TRANSITION == 2
TURBULENT  == 3
CIRCUIT    == 4

(* Thresholds (scaled by 100 for integer math) *)
Q_LAMINAR_MAX    == 50
Q_TRANSITION_MAX == 70
Q_TURBULENT_MAX  == 90

(*
   Hysteresis (Damping)
   To downgrade, we must drop BELOW the threshold by a buffer
*)
BUFFER == 5

-----------------------------------------------------------------------------

(* Initial State *)
Init ==
    /\ currentRegime = LAMINAR
    /\ turbulenceQ = 0
    /\ epoch = 0

(* Next State Logic - The core Controller physics *)
NextRegime(q, oldRegime) ==
    CASE
      (* Escalation Logic (Instant Up) *)
      q >= Q_TURBULENT_MAX -> CIRCUIT
      [] q >= Q_TRANSITION_MAX /\ oldRegime < TURBULENT -> TURBULENT
      [] q >= Q_LAMINAR_MAX    /\ oldRegime < TRANSITION -> TRANSITION

      (* De-escalation Logic (Hysteresis Down) *)
      (* Must drop below threshold - BUFFER to downgrade *)
      [] oldRegime = CIRCUIT    /\ q < Q_TURBULENT_MAX - BUFFER -> TURBULENT
      [] oldRegime = TURBULENT  /\ q < Q_TRANSITION_MAX - BUFFER -> TRANSITION
      [] oldRegime = TRANSITION /\ q < Q_LAMINAR_MAX - BUFFER -> LAMINAR

      (* Stay same *)
      [] OTHER -> oldRegime

(* State Transitions *)
Next ==
    \/  /\ epoch < MaxEpochs
        /\ \E newQ \in TurbulenceLevels :
            /\ turbulenceQ' = newQ
            /\ currentRegime' = NextRegime(newQ, currentRegime)
            /\ epoch' = epoch + 1
    \/  /\ epoch = MaxEpochs
        /\ UNCHANGED vars

-----------------------------------------------------------------------------

(* SAFETY INVARIANTS *)

(* 1. Safety: If Turbulence is Critical (95+), we MUST be in CIRCUIT *)
(* Note: We allow 1 epoch lag if simulating lag, but here logic is instantaneous *)
CircuitBreakerSafety ==
    (turbulenceQ >= Q_TURBULENT_MAX) => (currentRegime = CIRCUIT)

(* 2. Safety: Exit Gate logic. If in Circuit, Exit Penalty is 99% *)
(* Modeled as a property check *)
ExitGateActive ==
    (currentRegime = CIRCUIT) => (turbulenceQ >= Q_TURBULENT_MAX - BUFFER)
    (* i.e., We shouldn't be in CIRCUIT if input is low, unless draining from hysteresis *)

(* 3. Liveness / Reversibility (Not a safety invariant, but a property) *)
(* If q stays 0, we eventually return to LAMINAR *)
(* Hard to prove in simple safety spec, but implied by de-escalation logic *)

Spec == Init /\ [][Next]_vars

=============================================================================