[tlaplus] TLC error: <Constant> is an element of the model value <Constant>

---- MODULE BgpConnectionFsmTwoSpeakers ----
(*
Specification of the BGP connection FSM (Finite State Machine) for two speakers.
See https://datatracker.ietf.org/doc/html/rfc4271#section-8.
*)
EXTENDS Integers

VARIABLES speakerStates, speakerConnectRetryCounters, speakerConnectRetryTimers,
holdTimers, keepaliveTimers

\* Various grouping of variables.
allVars == <<speakerStates, speakerConnectRetryCounters,
speakerConnectRetryTimers, holdTimers, keepaliveTimers>>

\* The set of BGP Speakers. Eventually we should test with more than two speakers.
\* We will assume, S1 initiates the connection for simplicity.
\* I.e., this spec does not handle the case where both ends can initiate
\* connections.
Speakers == {"S1", "S2"}

\* The set of states of the FSM. Eventually, we may want to convert this
\* into a sequence if the ordering is important.
States == {"Idle", "Connect", "Active", "OpenSent", "OpenConfirm",
"Established"}

\* Indicates the amount of time remaining for an active timer to expire.
TimerActiveVals == Nat \union {0}

\* Indicates an inactive timer.
TimerInactiveVal == CHOOSE t: t \notin TimerActiveVals

\* A timer can be active or inactive.
TimerAllVals == TimerActiveVals \union TimerInactiveVal

\* ConnectRetryTime for each speaker.
SpeakerConnectRetryTimes == [speaker \in Speakers |-> 10]

\* Holdtime is common to the session between the two speakers.
HoldTime == 10

\* Keepalive time for each speaker. It's usually set to one-third of
\* the holdtime.
KeepaliveTimes == [speaker \in Speakers |-> HoldTime \div 3]

TypeInvariant == \* Specify constraints on what values
\* each variable can take. In other words,
\* specify type of each variable.
/\ speakerStates \in [Speakers -> States]
\* speakerStates is a function that
\* maps each Speaker to a value in
\* States.
/\ speakerConnectRetryCounters \in [Speakers -> Nat \union {0}]
\* speakerConnectRetryCounters is
\* a function that maps each speaker to
\* a valid timer value.
/\ speakerConnectRetryTimers \in [Speakers -> TimerAllVals]
/\ holdTimers \in [Speakers -> TimerAllVals]
/\ keepaliveTimers \in [Speakers -> TimerAllVals]
\* Each of the timers is
\* a function that maps each speaker to
\* a non-negative integer indicating the
\* remaining time for the timer expiry.

Init ==
\* The initial predicate
/\ speakerStates = [S1 |-> "Idle", S2 |-> "Active"]
\* Initial states for each speaker.
\* S1 initiates the connection while
\* S2 waits for an incoming connection
\* That's why S2's state is Active as per
\* https://www.rfc-editor.org/rfc/rfc4271.html#section-8.2.2.
/\ speakerConnectRetryCounters = [speaker \in Speakers |-> 0]
\* Initial value of the connectRetryCounter
\* for each speaker.
/\ speakerConnectRetryTimers = [speaker \in Speakers |-> TimerInactiveVal]
/\ holdTimers = [speaker \in Speakers |-> TimerInactiveVal]
/\ keepaliveTimers = [speaker \in Speakers |-> TimerInactiveVal]
\* Initialization of various
\* timers for each speaker.

StartS1 ==
\* Represents a manual or automatic start Event
\* at S1. Note in this Specification
\* only S1 is allowed to initiate
\* the connection.
/\ speakerStates["S1"] = "Idle" \* The state of S2 does not matter.
/\ speakerConnectRetryCounters' =
[speakerConnectRetryCounters EXCEPT !["S1"] = 0]
\* Reset S1's connectRetryCounter.
/\ speakerConnectRetryTimers' =
[speakerConnectRetryTimers EXCEPT !["S1"] =
SpeakerConnectRetryTimes["S1"]]
\* Reset S1's connectRetryTimer.

/\ speakerStates' = [speakerStates EXCEPT !["S1"] = "Connect"]
\* Move S1 to the Connect state.
/\ UNCHANGED <<holdTimers, keepaliveTimers>>

Next == StartS1
\* All possible actions of the
\* specification.

Spec == Init /\ [][Next]_allVars
----
THEOREM Spec => [](TypeInvariant)
====