Ex4pmEngine.WorkflowNet (ex4pm v26.9.9)

@type t() :: %Ex4pmEngine.WorkflowNet{
  arcs: [Ex4pmEngine.WorkflowNet.Arc.t()],
  id: String.t() | nil,
  metadata: map(),
  places: %{optional(String.t()) => Ex4pmEngine.WorkflowNet.Place.t()},
  sink_place: String.t(),
  source_place: String.t(),
  transitions: %{optional(String.t()) => Ex4pmEngine.WorkflowNet.Transition.t()}
}

Functions

enabled_transitions(net, marking)

Returns enabled transitions for a given marking.

fire(net, marking, transition_id)

Fires a transition from a marking, returning the new marking.

new(places, transitions, arcs, opts \\ [])

Constructs and structurally validates a Workflow Net.

simulate_traces(net, opts \\ [])

Simulates valid firing traces from source to sink up to max_depth and max_traces.

validate_structure(net)

Verifies Definition 3.3 formal WF-net structural rules:

Exactly one dedicated source place i with indegree 0.
Exactly one dedicated sink place o with outdegree 0.
Every node (place and transition) is on a path from i to o.

verify_soundness(net, opts \\ [])

Verifies Soundness of the Workflow Net:

1-Safe: No place holds > 1 tokens in any reachable marking.
Option to complete: From every reachable marking, the final marking [sink: 1] is reachable.
Proper completion: Whenever sink place has a token, it is the sole token in the marking.
No dead transitions: Every transition is enabled in at least one reachable marking.
Livelock detection: Detects terminal strongly connected components or cycles that cannot reach sink.