Re: [tlaplus] TLC and parameterized INSTANCE

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

--
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/7e7c7404-71a6-f066-bb70-0feca0f23e0f%40lemmster.de.