[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] TLC and parameterized INSTANCE



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.