Question about TLC error when running Bounded FIFO example

[Hank Wang]

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?

[Igor Konnov]

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

> --
> 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+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ac075269-392a-4052-a53f-5c534d7cf7f7n%40googlegroups.com.