SPECIFICATION Spec

CONSTANTS
    Deliveries = {delivery1, delivery2}
    Templates = {template1}
    Identities = {identity1}
    Revisions = {revision1, revision2}
    Others = {}
    InitialTemplateRef <- SharedTemplateRef
    InitialMode <- ContinuousMode

INVARIANTS TypeOK NoConcurrentRuns TemplateAvailable PreparedAvailable CollectedSaved
PROPERTIES TemplateStable AdmissionReady PublishDrained PublishLatest RecordOnce

CHECK_DEADLOCK FALSE