mirror of
https://github.com/pingcap/tla-plus.git
synced 2026-08-19 10:03:30 +08:00
22 lines
407 B
INI
22 lines
407 B
INI
\* MV CONSTANT declarations
|
|
CONSTANTS
|
|
k1 = k1
|
|
k2 = k2
|
|
\* MV CONSTANT definitions
|
|
CONSTANT
|
|
RM <- const_1571478437097222000
|
|
\* CONSTRAINT definition
|
|
CONSTRAINT
|
|
constr_1571478437097223000
|
|
\* SPECIFICATION definition
|
|
SPECIFICATION
|
|
RTSpec
|
|
\* INVARIANT definition
|
|
INVARIANT
|
|
RTTypeOK
|
|
CommitConsistency
|
|
ResolvedConsistency
|
|
\* PROPERTY definition
|
|
PROPERTY
|
|
ResolveLiveness
|
|
\* Generated on Sat Oct 19 17:47:17 CST 2019 |