mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-25 06:14:59 +00:00
596 lines
23 KiB
Plaintext
596 lines
23 KiB
Plaintext
---------------------------- MODULE workflow_system ----------------------------
|
|
(***************************************************************************
|
|
* Workflow System Specification for MetaBuilder *
|
|
* *
|
|
* This specification models workflow execution, scheduling, and state *
|
|
* management for MetaBuilder's advanced workflow features. *
|
|
* *
|
|
* Features modeled: *
|
|
* - Workflow definition and validation *
|
|
* - Scheduled and manual workflow execution *
|
|
* - Step dependencies and parallel execution *
|
|
* - Error handling and retry logic *
|
|
* - Workflow templates and instances *
|
|
* - God-level (Level 5+) permission requirements *
|
|
***************************************************************************)
|
|
|
|
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
|
|
|
CONSTANTS
|
|
Users, \* Set of all users
|
|
Tenants, \* Set of tenants
|
|
WorkflowTemplates, \* Set of workflow templates
|
|
WorkflowSteps, \* Set of possible workflow steps
|
|
MaxRetries, \* Maximum retry attempts for failed steps
|
|
MaxConcurrentRuns \* Maximum concurrent workflow executions per tenant
|
|
|
|
VARIABLES
|
|
userLevels, \* User -> Permission Level
|
|
userTenants, \* User -> Tenant
|
|
templates, \* WorkflowTemplate -> Template Definition
|
|
instances, \* WorkflowInstance -> Instance State
|
|
scheduledRuns, \* Set of scheduled workflow runs
|
|
runningWorkflows, \* Set of currently executing workflow instances
|
|
completedWorkflows, \* Set of completed workflow instances
|
|
workflowAuditLog \* Sequence of workflow events
|
|
|
|
vars == <<userLevels, userTenants, templates, instances, scheduledRuns,
|
|
runningWorkflows, completedWorkflows, workflowAuditLog>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Type Definitions *)
|
|
|
|
PermissionLevel == 1..6
|
|
|
|
WorkflowStatus == {"draft", "active", "paused", "archived"}
|
|
StepStatus == {"pending", "running", "success", "failed", "skipped", "retrying"}
|
|
InstanceStatus == {"queued", "running", "completed", "failed", "cancelled"}
|
|
|
|
TemplateRecord == [
|
|
id: WorkflowTemplates,
|
|
name: STRING,
|
|
tenantId: Tenants,
|
|
status: WorkflowStatus,
|
|
steps: Seq(WorkflowSteps),
|
|
dependencies: [WorkflowSteps -> SUBSET WorkflowSteps], \* Step dependencies
|
|
trigger: {"manual", "scheduled", "event"}
|
|
]
|
|
|
|
InstanceRecord == [
|
|
id: Nat,
|
|
templateId: WorkflowTemplates,
|
|
tenantId: Tenants,
|
|
status: InstanceStatus,
|
|
startedBy: Users,
|
|
startTime: Nat,
|
|
stepStates: [WorkflowSteps -> StepStatus],
|
|
retryCount: [WorkflowSteps -> Nat],
|
|
result: STRING
|
|
]
|
|
|
|
TypeOK ==
|
|
/\ userLevels \in [Users -> PermissionLevel]
|
|
/\ userTenants \in [Users -> Tenants]
|
|
/\ templates \subseteq TemplateRecord
|
|
/\ instances \subseteq InstanceRecord
|
|
/\ scheduledRuns \subseteq (WorkflowTemplates \X Tenants \X Nat) \* (template, tenant, timestamp)
|
|
/\ runningWorkflows \subseteq Nat \* Instance IDs
|
|
/\ completedWorkflows \subseteq Nat
|
|
/\ workflowAuditLog \in Seq([
|
|
user: Users \cup {"system"},
|
|
action: STRING,
|
|
templateId: WorkflowTemplates \cup {0},
|
|
instanceId: Nat,
|
|
tenant: Tenants,
|
|
timestamp: Nat
|
|
])
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Permission Checks *)
|
|
|
|
\* God level (5+) required for workflow authoring
|
|
CanAuthorWorkflow(user, tenant) ==
|
|
/\ userLevels[user] >= 5
|
|
/\ userTenants[user] = tenant
|
|
|
|
\* Admin level (4+) required for workflow execution
|
|
CanExecuteWorkflow(user, tenant) ==
|
|
/\ userLevels[user] >= 4
|
|
/\ userTenants[user] = tenant
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Helper Functions *)
|
|
|
|
\* Get template by ID
|
|
GetTemplate(tid) ==
|
|
CHOOSE t \in templates : t.id = tid
|
|
|
|
\* Get instance by ID
|
|
GetInstance(iid) ==
|
|
CHOOSE i \in instances : i.id = iid
|
|
|
|
\* Check if all dependencies of a step are satisfied
|
|
StepDependenciesSatisfied(instance, step) ==
|
|
LET
|
|
template == GetTemplate(instance.templateId)
|
|
deps == template.dependencies[step]
|
|
IN
|
|
\A dep \in deps :
|
|
instance.stepStates[dep] \in {"success", "skipped"}
|
|
|
|
\* Count running workflows for a tenant
|
|
CountRunningForTenant(tenant) ==
|
|
Cardinality({i \in runningWorkflows : GetInstance(i).tenantId = tenant})
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Initial State *)
|
|
|
|
Init ==
|
|
/\ userLevels \in [Users -> PermissionLevel]
|
|
/\ userTenants \in [Users -> Tenants]
|
|
/\ templates = {}
|
|
/\ instances = {}
|
|
/\ scheduledRuns = {}
|
|
/\ runningWorkflows = {}
|
|
/\ completedWorkflows = {}
|
|
/\ workflowAuditLog = <<>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Workflow Template Operations *)
|
|
|
|
\* God user creates a new workflow template
|
|
CreateTemplate(user, tid, tenant, steps, deps, trigger) ==
|
|
/\ CanAuthorWorkflow(user, tenant)
|
|
/\ tid \in WorkflowTemplates
|
|
/\ tid \notin {t.id : t \in templates}
|
|
/\ steps \in Seq(WorkflowSteps)
|
|
/\ Len(steps) > 0
|
|
/\ trigger \in {"manual", "scheduled", "event"}
|
|
/\ LET newTemplate == [
|
|
id |-> tid,
|
|
name |-> "WorkflowTemplate",
|
|
tenantId |-> tenant,
|
|
status |-> "draft",
|
|
steps |-> steps,
|
|
dependencies |-> deps,
|
|
trigger |-> trigger
|
|
] IN
|
|
/\ templates' = templates \cup {newTemplate}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "create_template",
|
|
templateId |-> tid,
|
|
instanceId |-> 0,
|
|
tenant |-> tenant,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* God user activates a template
|
|
ActivateTemplate(user, tid) ==
|
|
/\ \E t \in templates :
|
|
/\ t.id = tid
|
|
/\ CanAuthorWorkflow(user, t.tenantId)
|
|
/\ t.status = "draft"
|
|
/\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "active"]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "activate_template",
|
|
templateId |-> tid,
|
|
instanceId |-> 0,
|
|
tenant |-> t.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* God user archives a template
|
|
ArchiveTemplate(user, tid) ==
|
|
/\ \E t \in templates :
|
|
/\ t.id = tid
|
|
/\ CanAuthorWorkflow(user, t.tenantId)
|
|
/\ t.status \in {"active", "paused"}
|
|
/\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "archived"]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "archive_template",
|
|
templateId |-> tid,
|
|
instanceId |-> 0,
|
|
tenant |-> t.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Workflow Execution *)
|
|
|
|
\* Admin user manually starts a workflow
|
|
StartWorkflow(user, tid, iid) ==
|
|
/\ \E t \in templates :
|
|
/\ t.id = tid
|
|
/\ CanExecuteWorkflow(user, t.tenantId)
|
|
/\ t.status = "active"
|
|
/\ CountRunningForTenant(t.tenantId) < MaxConcurrentRuns
|
|
/\ iid \notin {i.id : i \in instances}
|
|
/\ LET
|
|
initialStepStates == [s \in WorkflowSteps |->
|
|
IF s \in {t.steps[i] : i \in 1..Len(t.steps)}
|
|
THEN "pending"
|
|
ELSE "skipped"]
|
|
initialRetryCount == [s \in WorkflowSteps |-> 0]
|
|
newInstance == [
|
|
id |-> iid,
|
|
templateId |-> tid,
|
|
tenantId |-> t.tenantId,
|
|
status |-> "running",
|
|
startedBy |-> user,
|
|
startTime |-> Len(workflowAuditLog),
|
|
stepStates |-> initialStepStates,
|
|
retryCount |-> initialRetryCount,
|
|
result |-> "in_progress"
|
|
]
|
|
IN
|
|
/\ instances' = instances \cup {newInstance}
|
|
/\ runningWorkflows' = runningWorkflows \cup {iid}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "start_workflow",
|
|
templateId |-> tid,
|
|
instanceId |-> iid,
|
|
tenant |-> t.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
|
completedWorkflows>>
|
|
|
|
\* System executes a workflow step
|
|
ExecuteStep(iid, step) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.status = "running"
|
|
/\ instance.stepStates[step] = "pending"
|
|
/\ StepDependenciesSatisfied(instance, step)
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT !.stepStates[step] = "running"]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "execute_step",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* Step completes successfully
|
|
CompleteStep(iid, step) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.stepStates[step] = "running"
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT !.stepStates[step] = "success"]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "complete_step",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* Step fails (may retry)
|
|
FailStep(iid, step) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.stepStates[step] = "running"
|
|
/\ LET
|
|
newRetryCount == instance.retryCount[step] + 1
|
|
shouldRetry == newRetryCount < MaxRetries
|
|
newStatus == IF shouldRetry THEN "retrying" ELSE "failed"
|
|
IN
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT
|
|
!.stepStates[step] = newStatus,
|
|
!.retryCount[step] = newRetryCount
|
|
]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "fail_step",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* Retry a failed step
|
|
RetryStep(iid, step) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.stepStates[step] = "retrying"
|
|
/\ instance.retryCount[step] < MaxRetries
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT !.stepStates[step] = "pending"]}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "retry_step",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* Complete entire workflow
|
|
CompleteWorkflow(iid) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.status = "running"
|
|
/\ LET
|
|
template == GetTemplate(instance.templateId)
|
|
allStepsComplete == \A step \in {template.steps[i] : i \in 1..Len(template.steps)} :
|
|
instance.stepStates[step] \in {"success", "skipped"}
|
|
IN
|
|
/\ allStepsComplete
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT
|
|
!.status = "completed",
|
|
!.result = "success"
|
|
]}
|
|
/\ runningWorkflows' = runningWorkflows \ {iid}
|
|
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "complete_workflow",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
|
|
|
\* Fail entire workflow
|
|
FailWorkflow(iid) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ instance.status = "running"
|
|
/\ LET
|
|
template == GetTemplate(instance.templateId)
|
|
hasFailedStep == \E step \in {template.steps[i] : i \in 1..Len(template.steps)} :
|
|
/\ instance.stepStates[step] = "failed"
|
|
/\ instance.retryCount[step] >= MaxRetries
|
|
IN
|
|
/\ hasFailedStep
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT
|
|
!.status = "failed",
|
|
!.result = "failure"
|
|
]}
|
|
/\ runningWorkflows' = runningWorkflows \ {iid}
|
|
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "fail_workflow",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
|
|
|
\* Admin user cancels a running workflow
|
|
CancelWorkflow(user, iid) ==
|
|
/\ iid \in runningWorkflows
|
|
/\ \E instance \in instances :
|
|
/\ instance.id = iid
|
|
/\ CanExecuteWorkflow(user, instance.tenantId)
|
|
/\ instance.status = "running"
|
|
/\ instances' = (instances \ {instance}) \cup
|
|
{[instance EXCEPT
|
|
!.status = "cancelled",
|
|
!.result = "cancelled"
|
|
]}
|
|
/\ runningWorkflows' = runningWorkflows \ {iid}
|
|
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "cancel_workflow",
|
|
templateId |-> instance.templateId,
|
|
instanceId |-> iid,
|
|
tenant |-> instance.tenantId,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Scheduling *)
|
|
|
|
\* Schedule a workflow run
|
|
ScheduleWorkflow(user, tid, tenant, scheduledTime) ==
|
|
/\ \E t \in templates :
|
|
/\ t.id = tid
|
|
/\ t.tenantId = tenant
|
|
/\ CanExecuteWorkflow(user, tenant)
|
|
/\ t.status = "active"
|
|
/\ t.trigger \in {"scheduled", "manual"}
|
|
/\ scheduledRuns' = scheduledRuns \cup {<<tid, tenant, scheduledTime>>}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> user,
|
|
action |-> "schedule_workflow",
|
|
templateId |-> tid,
|
|
instanceId |-> 0,
|
|
tenant |-> tenant,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, instances,
|
|
runningWorkflows, completedWorkflows>>
|
|
|
|
\* System triggers a scheduled workflow
|
|
TriggerScheduled(tid, tenant, scheduledTime, iid) ==
|
|
/\ <<tid, tenant, scheduledTime>> \in scheduledRuns
|
|
/\ Len(workflowAuditLog) >= scheduledTime
|
|
/\ \E t \in templates :
|
|
/\ t.id = tid
|
|
/\ t.tenantId = tenant
|
|
/\ t.status = "active"
|
|
/\ CountRunningForTenant(tenant) < MaxConcurrentRuns
|
|
/\ iid \notin {i.id : i \in instances}
|
|
/\ LET
|
|
initialStepStates == [s \in WorkflowSteps |->
|
|
IF s \in {t.steps[i] : i \in 1..Len(t.steps)}
|
|
THEN "pending"
|
|
ELSE "skipped"]
|
|
initialRetryCount == [s \in WorkflowSteps |-> 0]
|
|
newInstance == [
|
|
id |-> iid,
|
|
templateId |-> tid,
|
|
tenantId |-> tenant,
|
|
status |-> "running",
|
|
startedBy |-> CHOOSE u \in Users : userTenants[u] = tenant /\ userLevels[u] >= 5,
|
|
startTime |-> Len(workflowAuditLog),
|
|
stepStates |-> initialStepStates,
|
|
retryCount |-> initialRetryCount,
|
|
result |-> "in_progress"
|
|
]
|
|
IN
|
|
/\ instances' = instances \cup {newInstance}
|
|
/\ runningWorkflows' = runningWorkflows \cup {iid}
|
|
/\ scheduledRuns' = scheduledRuns \ {<<tid, tenant, scheduledTime>>}
|
|
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
|
user |-> "system",
|
|
action |-> "trigger_scheduled",
|
|
templateId |-> tid,
|
|
instanceId |-> iid,
|
|
tenant |-> tenant,
|
|
timestamp |-> Len(workflowAuditLog)
|
|
])
|
|
/\ UNCHANGED <<userLevels, userTenants, templates, completedWorkflows>>
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Next State Relation *)
|
|
|
|
Next ==
|
|
\/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants,
|
|
steps \in Seq(WorkflowSteps),
|
|
deps \in [WorkflowSteps -> SUBSET WorkflowSteps],
|
|
trigger \in {"manual", "scheduled", "event"}:
|
|
CreateTemplate(u, tid, t, steps, deps, trigger)
|
|
\/ \E u \in Users, tid \in WorkflowTemplates: ActivateTemplate(u, tid)
|
|
\/ \E u \in Users, tid \in WorkflowTemplates: ArchiveTemplate(u, tid)
|
|
\/ \E u \in Users, tid \in WorkflowTemplates, iid \in Nat:
|
|
StartWorkflow(u, tid, iid)
|
|
\/ \E iid \in Nat, step \in WorkflowSteps: ExecuteStep(iid, step)
|
|
\/ \E iid \in Nat, step \in WorkflowSteps: CompleteStep(iid, step)
|
|
\/ \E iid \in Nat, step \in WorkflowSteps: FailStep(iid, step)
|
|
\/ \E iid \in Nat, step \in WorkflowSteps: RetryStep(iid, step)
|
|
\/ \E iid \in Nat: CompleteWorkflow(iid)
|
|
\/ \E iid \in Nat: FailWorkflow(iid)
|
|
\/ \E u \in Users, iid \in Nat: CancelWorkflow(u, iid)
|
|
\/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants, time \in Nat:
|
|
ScheduleWorkflow(u, tid, t, time)
|
|
\/ \E tid \in WorkflowTemplates, t \in Tenants, time \in Nat, iid \in Nat:
|
|
TriggerScheduled(tid, t, time, iid)
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Safety Properties *)
|
|
|
|
\* Only God-level users can create templates
|
|
GodOnlyTemplateCreation ==
|
|
\A event \in 1..Len(workflowAuditLog):
|
|
workflowAuditLog[event].action = "create_template" =>
|
|
userLevels[workflowAuditLog[event].user] >= 5
|
|
|
|
\* Only Admin+ users can execute workflows
|
|
AdminOnlyExecution ==
|
|
\A event \in 1..Len(workflowAuditLog):
|
|
workflowAuditLog[event].action \in {"start_workflow", "cancel_workflow"} =>
|
|
userLevels[workflowAuditLog[event].user] >= 4
|
|
|
|
\* Workflow instances belong to exactly one tenant
|
|
TenantIsolation ==
|
|
\A i1, i2 \in instances:
|
|
i1.id = i2.id => i1.tenantId = i2.tenantId
|
|
|
|
\* Running workflows don't exceed concurrency limit
|
|
ConcurrencyLimit ==
|
|
\A t \in Tenants:
|
|
CountRunningForTenant(t) <= MaxConcurrentRuns
|
|
|
|
\* Failed steps don't exceed retry limit
|
|
RetryLimit ==
|
|
\A i \in instances, s \in WorkflowSteps:
|
|
i.retryCount[s] <= MaxRetries
|
|
|
|
\* Completed workflows are not in running set
|
|
NoOverlap ==
|
|
runningWorkflows \cap completedWorkflows = {}
|
|
|
|
\* Step dependencies are respected
|
|
DependencyEnforcement ==
|
|
\A i \in instances, step \in WorkflowSteps:
|
|
i.stepStates[step] \in {"running", "success"} =>
|
|
StepDependenciesSatisfied(i, step)
|
|
|
|
\* All workflow events are audited
|
|
AuditCompleteness ==
|
|
Len(workflowAuditLog) >= Cardinality(instances)
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Liveness Properties *)
|
|
|
|
\* Pending steps eventually execute (if dependencies are met)
|
|
EventualStepExecution ==
|
|
\A i \in instances, step \in WorkflowSteps:
|
|
(i.stepStates[step] = "pending" /\ StepDependenciesSatisfied(i, step)) ~>
|
|
i.stepStates[step] \in {"running", "success", "failed"}
|
|
|
|
\* Running workflows eventually complete or fail
|
|
EventualCompletion ==
|
|
\A iid \in Nat:
|
|
iid \in runningWorkflows ~> iid \in completedWorkflows
|
|
|
|
\* Scheduled workflows eventually trigger
|
|
EventualScheduleTrigger ==
|
|
\A tid \in WorkflowTemplates, t \in Tenants, time \in Nat:
|
|
<<tid, t, time>> \in scheduledRuns ~>
|
|
(<<tid, t, time>> \notin scheduledRuns \/ CountRunningForTenant(t) >= MaxConcurrentRuns)
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* System Specification *)
|
|
|
|
Spec ==
|
|
/\ Init
|
|
/\ [][Next]_vars
|
|
/\ \A iid \in Nat: WF_vars(CompleteWorkflow(iid))
|
|
/\ \A iid \in Nat: WF_vars(FailWorkflow(iid))
|
|
/\ \A iid \in Nat, step \in WorkflowSteps: WF_vars(ExecuteStep(iid, step))
|
|
|
|
-----------------------------------------------------------------------------
|
|
(* Invariants *)
|
|
|
|
Invariants ==
|
|
/\ TypeOK
|
|
/\ GodOnlyTemplateCreation
|
|
/\ AdminOnlyExecution
|
|
/\ TenantIsolation
|
|
/\ ConcurrencyLimit
|
|
/\ RetryLimit
|
|
/\ NoOverlap
|
|
/\ DependencyEnforcement
|
|
/\ AuditCompleteness
|
|
|
|
=============================================================================
|