Re: [tlaplus] Question about TLC error when running Bounded FIFO example

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Hank Wang,

You can find the TLA+ specifications from the book in the examples
repository [1]. The module you refer to is not there, so I would
assume that only MCInnerFIFO.{cfg,tla} are model checked. As far as I
remember, the hiding operator `\E` is not supported by TLC, but the
TLC experts may correct me. Since the hiding operator is applied in
the definition of Spec, you would have to write `SPECIFICATION Spec`
in the configuration file, instead of `NEXT BNext`. TLC expects no
arguments in the next-state relation.

[1] https://github.com/tlaplus/Examples/tree/master/specifications/SpecifyingSystems/FIFO


Best,
Igor

On Fri, Feb 13, 2026 at 4:53 AM Hank Wang <wshengyu3001@xxxxxxxxx> wrote:
>
> Hi all,
>
> I'm currently learning TLA+ using Specifying Systems, and I ran into an issue while working through the example in Chapter 4.4, A Bounded FIFO.
>
> I've translated the LaTeX specification from the book into the following TLA+ module:
>
> ```TLA
> ---- MODULE BoundedFIFO ----
> EXTENDS Naturals, Sequences
> VARIABLES in, out
> CONSTANT Message, N
> ASSUME (N \in Nat) /\ (N > 0)
> Inner(q) == INSTANCE innerFIFO
> BNext(q) == /\ Inner(q)!Next
>             /\ Inner(q)!BufRcv => (Len(q) < N)
> Spec == \E q : Inner(q)!Init /\ [][BNext(q)]_<<in, out, q>>
> ====
> ```
>
> My TLC configuration file is:
>
> ```
> CONSTANTS
>     Message = {m1, m2, m2}
>     N = 5
>
> NEXT BNext
> ```
>
> However, when I run TLC, I get the following error:
> Error: TLC requires next state action not to take any argument, but one was given: BNext
>
> I understand that this example involves a hidden variable (q), but I am having trouble figuring out how to structure the specification and the configuration so that TLC accepts it.
>
> Could someone explain how this example is intended to be run with TLC, or how to correctly handle the parameterized Next action in this setting?
>
> --
> 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ac075269-392a-4052-a53f-5c534d7cf7f7n%40googlegroups.com.

-- 
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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CACooHMCRtSNMfEWm2%2B9ZvwyGEr2_3M331m1Jb%2BTTBnd%3DFN66kQ%40mail.gmail.com.