Sequences are currently not supported. This is because TLA does not allow us to declare a sequence type as [ Nat -> Datatype ]. Rather, we have to specify a fixed domain (See https://learntla.com/tla/functions/ regarding the Seq(S) operator); for instance, [ 1..5 -> Datatype ]. This is somewhat tricky to do.
One potential solution is to declare constants for the size of each sequence variable we declare, and then assign those constants in the CFG step.
Sequences are currently not supported. This is because TLA does not allow us to declare a sequence type as
[ Nat -> Datatype ]. Rather, we have to specify a fixed domain (See https://learntla.com/tla/functions/ regarding theSeq(S)operator); for instance,[ 1..5 -> Datatype ]. This is somewhat tricky to do.One potential solution is to declare constants for the size of each sequence variable we declare, and then assign those constants in the CFG step.