TLC and parameterized INSTANCE

29 views
Skip to first unread message

Dmitry Kulagin

unread,
Jul 14, 2021, 2:14:54 PMJul 14
to tlaplus
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

unread,
Jul 15, 2021, 10:50:38 AMJul 15
to tlaplus
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

unread,
Jul 15, 2021, 11:05:04 AMJul 15
to tla...@googlegroups.com
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

unread,
Jul 16, 2021, 5:13:21 AMJul 16
to tlaplus
Oh, I see. Thank you, Markus
Reply all
Reply to author
Forward
0 new messages