Ex4pmEngine.POWL.ChoiceGraph (ex4pm v26.9.9)

Copy Markdown View Source

POWL 2.0 Choice Graph — Exact Mathematical Realization:

  • Definition 1 [BPM25, p. 7]
  • Definition 2 & 3 [BPM25, p. 8]
  • Definition 3.6, 3.7 & 3.9 [PETRI25, pp. 8–10]

Mathematical Formalism

Let $X$ be a finite set of POWL sub-models (or transitions $T$). A choice graph over $X$ is a tuple: $$ G = (N, E) $$ where:

  1. $N = X \cup \{▷, □\}$ with $▷, □ \notin X$ (artificial start $▷$ and end $□$ delimiters).
  2. $E \subseteq N \times N$ is a directed binary relation over $N$.
  3. $\{▷\} = \{x \in N \mid (N \times \{x\}) \cap E = \emptyset\}$ (unique start node).
  4. $\{□\} = \{x \in N \mid (\{x\} \times N) \cap E = \emptyset\}$ (unique end node).
  5. $\forall n \in N, \exists$ a directed path in $E$ from $▷$ to $n$ and from $n$ to $□$.

Language Semantics (Definition 3 [BPM25, p. 8], Definition 3.9 [PETRI25, p. 10])

Let $\vec{G}$ denote the set of all directed paths from $▷$ to $□$ in $G$: $$ \vec{G} = \{\langle x_1, \dots, x_k \rangle \in X^* \mid (▷, x_1), (x_1, x_2), \dots, (x_k, □) \in E\} $$

The language of the choice graph is the union of path concatenations: $$ L(G) = \bigcup_{\langle x_1, \dots, x_k \rangle \in \vec{G}} L(x_1) \cdot L(x_2) \cdots L(x_k) $$

Summary

Types

node_id()
t()

Functions

end_delimiter()
enumerate_paths(choice_graph, opts \\ [])

Enumerates all paths $\vec{G} = \{\langle x_1, \dots, x_k \rangle \in X^* \mid (▷, x_1), \dots, (x_k, □) \in E\}$. For cyclic choice graphs, bounds depth by max_depth (default 20) and unrolls by max_unroll (default 2).

new(nodes, edges, metadata \\ %{})

Constructs a validated Choice Graph $G = (N, E)$. Accepts either "▷" / "□" or :start / :end as delimiter identifiers.

start_delimiter()

Types

node_id()

@type node_id() :: String.t()

t()

@type t() :: %Ex4pmEngine.POWL.ChoiceGraph{
  cyclic?: boolean(),
  edges: [{node_id(), node_id()}],
  metadata: map(),
  nodes: %{required(node_id()) => term()}
}

Functions

end_delimiter()

enumerate_paths(choice_graph, opts \\ [])

@spec enumerate_paths(t(), keyword()) :: [[node_id()]]

Enumerates all paths $\vec{G} = \{\langle x_1, \dots, x_k \rangle \in X^* \mid (▷, x_1), \dots, (x_k, □) \in E\}$. For cyclic choice graphs, bounds depth by max_depth (default 20) and unrolls by max_unroll (default 2).

new(nodes, edges, metadata \\ %{})

@spec new([term()], [{String.t(), String.t()}], map()) ::
  {:ok, t()} | {:error, String.t()}

Constructs a validated Choice Graph $G = (N, E)$. Accepts either "▷" / "□" or :start / :end as delimiter identifiers.

Doctests

iex> a = Ex4pmEngine.POWL.activity("a", "Triage")
iex> b = Ex4pmEngine.POWL.activity("b", "Approve")
iex> {:ok, cg} = Ex4pmEngine.POWL.ChoiceGraph.new([a, b], [{"▷", "a"}, {"a", "b"}, {"b", "□"}])
iex> cg.cyclic?
false
iex> Ex4pmEngine.POWL.ChoiceGraph.enumerate_paths(cg)
[["a", "b"]]

start_delimiter()