mirror of
https://github.com/pingcap/tla-plus.git
synced 2024-12-26 12:30:10 +08:00
21 lines
447 B
Plaintext
21 lines
447 B
Plaintext
---- MODULE MC ----
|
|
EXTENDS ResolvedTS, TLC
|
|
|
|
\* MV CONSTANT declarations@modelParameterConstants
|
|
CONSTANTS
|
|
k1, k2
|
|
----
|
|
|
|
\* MV CONSTANT definitions RM
|
|
const_1571478437097222000 ==
|
|
{k1, k2}
|
|
----
|
|
|
|
\* CONSTRAINT definition @modelParameterContraint:0
|
|
constr_1571478437097223000 ==
|
|
/\ nextTS < 106
|
|
----
|
|
=============================================================================
|
|
\* Modification History
|
|
\* Created Sat Oct 19 17:47:17 CST 2019 by neil
|