20 lines
381 B
INI
20 lines
381 B
INI
|
CONSTANTS
|
||
|
|
G1 = g1
|
||
|
|
G2 = g2
|
||
|
|
A1 = a1
|
||
|
|
NoArtifact = noArtifact
|
||
|
|
Generations <- GenerationsFixture
|
||
|
|
Artifact = a1
|
||
|
|
|
||
|
|
SPECIFICATION Spec
|
||
|
|
CHECK_DEADLOCK FALSE
|
||
|
|
|
||
|
|
INVARIANTS
|
||
|
|
TypeOK
|
||
|
|
LeaseBindingConsistent
|
||
|
|
MountedGenerationLeased
|
||
|
|
LeasedArtifactPublished
|
||
|
|
GCExcludesLeases
|
||
|
|
ReplacementOnlyDuringGC
|
||
|
|
ForeignStagePreserved
|
||
|
|
OwnedStageRequiresIntent
|