mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-25 14:25:02 +00:00
32 lines
695 B
INI
32 lines
695 B
INI
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
|