TLC and parameterized INSTANCE

[Dmitry Kulagin]

Hello,

I try to use parameterized module instantiation:

M1(x) == INSTANCE M1 WITH X <- x

However, where I try to use it:

Prop == M1(Y)!Spec

I get an error: TLC cannot handle temporal formula

If I use non-parameterized version, everything works:

M1 == INSTANCE M1 WITH X <- Y

How should I use parameterized INSTANCE with TLC?

Thank you,

Dmitry

---------------- MODULE M0 ---------------------

VARIABLE Y

Init == Y = 0

Next == Y' = 1

Spec == Init /\ [][Next]_Y

M1(x) == INSTANCE M1 WITH X <- x

Prop == M1(Y)!Spec

==============================

---------------- MODULE M1 ----------------------

EXTENDS Integers

VARIABLE X

Init == X = 0

Next == X' = (X + 1) % 10

Spec == Init /\ [][Next]_X

===============================

[Andrew Helwer]

I tried this and actually got a more interesting error statement:

The configuration file did not specify the initial state predicate.
Can also be caused by trying to run TLC on a specification from
a module imported with a parameterized INSTANCE statement.

So perhaps TLC does not support this?

Andrew

[Markus Kuppe]

Hi,

please see section 2.1 of
https://lamport.azurewebsites.net/tla/current-tools.pdf and consider
helping with https://github.com/tlaplus/tlaplus/pull/441

Markus

[Dmitry Kulagin]

Oh, I see. Thank you, Markus