On Thursday, July 15, 2021 at 6:05:04 PM UTC+3 Markus Alexander Kuppe wrote:
On 7/14/21 11:14 AM, Dmitry Kulagin wrote:
> 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
> ===============================
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