SPECIFICATION Spec

CONSTANTS
    Users = {u1, u2, u3}
    Tenants = {t1, t2}
    WorkflowTemplates = {wf1, wf2, wf3}
    WorkflowSteps = {step1, step2, step3}
    MaxRetries = 3
    MaxConcurrentRuns = 2

INVARIANTS
    TypeOK
    GodOnlyTemplateCreation
    AdminOnlyExecution
    TenantIsolation
    ConcurrencyLimit
    RetryLimit
    NoOverlap
    DependencyEnforcement
    AuditCompleteness

PROPERTIES
    EventualStepExecution
    EventualCompletion
    EventualScheduleTrigger

\* Constraint to limit state space for model checking
CONSTRAINT
    /\ Len(workflowAuditLog) <= 15
    /\ Cardinality(instances) <= 5
    /\ Cardinality(runningWorkflows) <= 3