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

[Hank Wang <wshengyu3001@xxxxxxxxx>]

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.