[tlaplus] TLC and parameterized INSTANCE

[Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>]

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

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

-- 
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 on the web visit https://groups.google.com/d/msgid/tlaplus/bd7f69ea-5676-4117-9b48-8ec81d3d4e8cn%40googlegroups.com.