GPCTControllerInductive.tla

------------------- MODULE GPCTControllerInductive -------------------
EXTENDS Integers, TLAPS

Q_LAMINAR == 500
Q_TRANSITION == 700
Q_TURBULENT == 900
HYSTERESIS == 50
FEE_MIN == 3
FEE_MAX == 50

VARIABLES
    q,              \* [0, 1000]
    state,          \* 0 (LAMINAR), 1 (TRANSITION), 2 (TURBULENT), 3 (CIRCUIT)
    fee,            \* Scaled fee
    w               \* Scaled weight

vars == <<q, state, fee, w>>

(* -- State Logic -- *)

TypeOK ==
    /\ q \in Int
    /\ 0 <= q /\ q <= 1000
    /\ state \in {0, 1, 2, 3}
    /\ fee \in Int
    /\ w \in Int

Init ==
    /\ q = 0
    /\ state = 0
    /\ fee = FEE_MIN
    /\ w = 800

Next ==
    \E newQ \in 0..1000 :
        /\ q' = newQ
        /\ state' = IF state = 0 THEN (IF newQ >= Q_LAMINAR THEN 1 ELSE 0)
                    ELSE IF state = 1 THEN 
                        (IF newQ >= Q_TRANSITION THEN 2
                         ELSE IF newQ <= Q_LAMINAR - HYSTERESIS THEN 0
                         ELSE 1)
                    ELSE IF state = 2 THEN
                        (IF newQ >= Q_TURBULENT THEN 3
                         ELSE IF newQ <= Q_TRANSITION - HYSTERESIS THEN 1
                         ELSE 2)
                    ELSE (IF newQ <= Q_TURBULENT - HYSTERESIS THEN 2 ELSE 3)
        /\ fee' = IF state' = 0 THEN FEE_MIN
                  ELSE IF state' = 1 THEN FEE_MIN
                  ELSE FEE_MAX
        /\ w' = IF state' = 0 THEN 800
                ELSE IF state' = 1 THEN 400
                ELSE IF state' = 2 THEN 0
                ELSE 1000

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

\* Type Correctness Invariant
TypeInvariant ==
    /\ q \in 0..1000
    /\ state \in {0, 1, 2, 3}
    /\ fee \in {FEE_MIN, FEE_MAX}
    /\ w \in {0, 400, 800, 1000}

(* -- Inductive Proofs -- *)

THEOREM InitProperty == Init => TypeInvariant
  BY DEF Init, TypeInvariant, FEE_MIN

THEOREM InductiveStep == TypeInvariant /\ [Next]_vars => TypeInvariant'
<1>1. ASSUME TypeInvariant, Next
      PROVE  TypeInvariant'
  BY <1>1 DEF Next, TypeInvariant, FEE_MIN, FEE_MAX
<1>2. ASSUME TypeInvariant, vars' = vars
      PROVE  TypeInvariant'
  BY <1>2 DEF TypeInvariant, vars
<1>3. QED
  BY <1>1, <1>2

THEOREM SafetyProperty == Spec => []TypeInvariant
<1>1. Init => TypeInvariant
  BY InitProperty
<1>2. TypeInvariant /\ [Next]_vars => TypeInvariant'
  BY InductiveStep
<1>3. QED
  BY <1>1, <1>2, PTL DEF Spec

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