Formal Reachability Graph & 1-Safe Soundness Prover for Workflow Nets. Faithful BEAM realization of Van der Aalst (1997, 2011).
A Workflow Net N = (P, T, F, M0, Mf) is 1-safe sound iff:
- Option to complete: ∀ M ∈ [M0⟩, ∃ σ : M [σ⟩ Mf
- Proper completion: ∀ M ∈ [M0⟩, M ≥ Mf ⟹ M = Mf (no lingering unconsumed tokens)
- No dead transitions: ∀ t ∈ T, ∃ M ∈ [M0⟩ : M [t⟩
- 1-Safety: ∀ M ∈ [M0⟩, ∀ p ∈ P, M(p) ≤ 1
Summary
Functions
Formally verifies the 1-safe soundness of a Workflow Net.
net_spec is a map with :places, :transitions, :initial_marking, and :final_marking.