I am a TLA+ newbie, and am in the process of writing my first spec. I'm getting this error when I run TLC on the spec.
Computing initial states...
Error: Attempted to check if the value:
TimerInactiveVal
is an element of the model value TimerInactiveVal
While working on the initial state:
/\ keepaliveTimers = [S1 |-> TimerInactiveVal, S2 |-> TimerInactiveVal]
/\ speakerStates = [S1 |-> "Idle", S2 |-> "Active"]
/\ holdTimers = [S1 |-> TimerInactiveVal, S2 |-> TimerInactiveVal]
/\ speakerConnectRetryCounters = [S1 |-> 0, S2 |-> 0]
/\ speakerConnectRetryTimers = [S1 |-> TimerInactiveVal, S2 |-> TimerInactiveVal]
Error: TLC was unable to fingerprint.
---- 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)
====
Any help will be greatly appreciated...
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.