Inductive Miner: the strict sequence cut and the every-pair test (Leemans 2017)

CHANGELOG.md

@@ -8,6 +8,21 @@ notice, not how it was done. Versions before 0.7.0 were released as CPNpy.
 
 ## 0.11.2
 
+- **The Inductive Miner's sequence cut now agrees with the reference
+  implementation.** Two changes to `sequence_cut`, both from Leemans'
+  thesis (*Robust Process Mining with Guarantees*, 2017), which is what
+  ProM and PM4Py follow: (1) a cut is accepted only when *every* activity of
+  an earlier group reaches *every* activity of a later one, as the
+  definition says, not when some pair does; (2) the *strict* step: groups
+  that can only be skipped together become one group, so an optional
+  stretch `a, c` is `×(τ, →(a, c))` rather than `×(τ, a), ×(τ, c)`, which
+  also allowed `<b, a>` and `<b, c>` that never happened. The How tab says
+  when the strict step merged groups, and Cite on the box lists the thesis.
+  The cross-check against PM4Py goes from 369 identical trees of 406 to
+  401; the five that remain are fall-throughs on logs with no cut, tried in
+  a different order, and the guarantees (a sound net, fitness 1) hold on
+  every log before and after. Models discovered from logs with skippable
+  stretches change; models of the textbook logs do not.
 - **Fixed: Describe log and Correlate failed with "No converter from
   EventLog to pandas.DataFrame" whenever pandas was installed.** A converter
   was registered under the class's defining module

openprocess/gui/studio/derivation_view.py

@@ -319,9 +319,11 @@ def _step_html(step) -> str:
     if step.kind == "cut":
         groups = "  |  ".join(_set(g) for g in step.groups or [])
         where = " <span style='color:%s'>(on the filtered DFG)</span>" % muted if step.filtered else ""
+        # A sequence cut says when the strict step merged groups (Leemans 2017).
+        detail = f"<br><span style='color:{muted}'>{escape(step.detail)}</span>" if step.detail else ""
         return (f"<b style='color:{accent}; font-size: 15px'>{step.operator}</b> "
                 f"<b>{OPERATOR_NAMES.get(step.operator, '')} cut</b>{where}<br>"
-                f"<span style='font-family:{MATH_FONT}'>{groups}</span>")
+                f"<span style='font-family:{MATH_FONT}'>{groups}</span>{detail}")
     if step.kind == "base":
         leaf = "<i>τ</i>" if step.result == "τ" else _activity(step.result or "")
         return f"<b>base case</b> → {leaf}"

openprocess/mining/discovery/inductive.py

@@ -1,7 +1,8 @@
 """The Inductive Miner (IM) and Inductive Miner – infrequent (IMf).
 
 Reading: Leemans, Fahland & van der Aalst, "Discovering block-structured
-process models from event logs" (course reading 4).
+process models from event logs" (course reading 4); the strict sequence cut
+is from Leemans, "Robust Process Mining with Guarantees" (PhD thesis, 2017).
 
 The idea: divide and conquer
 ----------------------------
@@ -22,6 +23,11 @@
     Every activity of an earlier group can reach every activity of a later
     group, and never the other way round.  Computed from the strongly
     connected components, merging components that are mutually unreachable.
+    Then the *strict* step (Leemans 2017, p. 233): groups that can only be
+    skipped together are merged, so an optional stretch ``a, c`` becomes
+    ``×(→(a,c), τ)`` rather than ``×(a,τ), ×(c,τ)``.  ProM and PM4Py do the
+    same, and ``tests/cross_check_inductive_miner.py`` checks that the trees
+    agree.
 ∧ parallel
     Between two different groups, *every* pair of activities directly
     follows each other in both directions, and every group contains a start
@@ -152,6 +158,15 @@ def mine(self, log: SimpleLog, depth: int) -> ProcessTree:
             self.note(depth, f"{operator.value} cut{' (on filtered DFG)' if filtered else ''}: "
                              f"{described}", "cut", operator=operator.value,
                       groups=[sorted(g) for g in groups], filtered=filtered)
+            if operator is Operator.SEQUENCE:
+                maximal = maximal_sequence_cut(dfg) or []
+                if len(maximal) != len(groups):
+                    merged = [sorted(g) for g in groups
+                              if not any(set(g) == m for m in maximal)]
+                    self.records[-1].detail = (
+                        "strict sequence cut: groups that can only be skipped together are "
+                        "one group: " + " ".join("{" + ", ".join(g) + "}" for g in merged))
+                    self.steps.append("  " * (depth + 1) + self.records[-1].detail)
             sublogs = split_log(log, operator, groups, dfg)
             children = [self.mine(sub, depth + 1) for sub in sublogs]
             if operator is Operator.LOOP and len(children) > 2:
@@ -269,51 +284,145 @@ def xor_cut(dfg: DFG) -> list[set[str]] | None:
 
 
 def sequence_cut(dfg: DFG) -> list[set[str]] | None:
+    """The *strict* sequence cut: the maximal sequence cut, then the groups
+    that can only be skipped together merged into one (Leemans 2017, p. 233).
+
+    The maximal cut puts every activity in the finest possible position of
+    the sequence.  That is correct but can be needlessly general: in
+    ``[<b>^4, <b,b,a,c>]`` the maximal cut is ``{b} | {a} | {c}``, and since
+    ``a`` and ``c`` are absent from four of the five traces, each becomes
+    optional on its own, ``→(↺(b,τ), ×(a,τ), ×(c,τ))``, a model that also
+    allows ``<b,a>`` and ``<b,c>``, which never happened.  ``c`` can only be
+    reached through ``a``, so whenever ``a`` is skipped ``c`` is skipped too:
+    merging them gives ``{b} | {a, c}`` and ``→(↺(b,τ), ×(→(a,c),τ))``.
+    """
+    groups = maximal_sequence_cut(dfg)
+    return None if groups is None else merge_skippable_groups(dfg, groups)
+
+
+def maximal_sequence_cut(dfg: DFG) -> list[set[str]] | None:
+    """The sequence cut with as many groups as the reachability relation
+    allows, ordered first to last.
+
+    The definition (Leemans, Fahland & van der Aalst 2013; Leemans 2017,
+    p. 188): a partition ``Σ1, …, Σn`` such that for every earlier group
+    ``Σi`` and later group ``Σj``, *every* ``a ∈ Σi`` reaches *every*
+    ``b ∈ Σj`` through the directly-follows graph, and no ``b`` reaches
+    any ``a``.  Two activities therefore belong to the same group exactly
+    when they reach each other (a loop) or when neither reaches the other
+    (two branches of a choice, or two concurrent activities): one of them
+    could not be put strictly before the other.
+
+    Computed as the thesis does it: start with one group per activity and
+    merge any two groups that hold such a pair, until nothing merges.  The
+    groups are then totally ordered by reachability.
+    """
     reach = _reachability(dfg)
-    nodes = sorted(dfg.activities)
-    # Strongly connected components: a and b together iff each reaches the other.
-    groups: list[set[str]] = []
-    for node in nodes:
-        for group in groups:
-            other = next(iter(group))
-            if (other in reach[node] and node in reach[other]):
-                group.add(node)
-                break
-        else:
-            groups.append({node})
+    groups: list[set[str]] = [{a} for a in sorted(dfg.activities)]
+    if not groups:
+        return None
 
-    def reaches(g1: set[str], g2: set[str]) -> bool:
-        return any(b in reach[a] for a in g1 for b in g2)
+    def must_share_a_group(g1: set[str], g2: set[str]) -> bool:
+        for a in g1:
+            for b in g2:
+                forward, backward = b in reach[a], a in reach[b]
+                if forward == backward:          # both ways (a loop) or neither
+                    return True
+        return False
 
-    # Merge groups that are mutually unreachable (neither can reach the other):
-    # they must sit in the same position of the sequence.
     merged = True
     while merged:
         merged = False
         for i in range(len(groups)):
             for j in range(i + 1, len(groups)):
-                if not reaches(groups[i], groups[j]) and not reaches(groups[j], groups[i]):
+                if must_share_a_group(groups[i], groups[j]):
                     groups[i] |= groups.pop(j)
                     merged = True
                     break
             if merged:
                 break
     if len(groups) < 2:
         return None
-    # Order: g1 before g2 iff g1 reaches g2.  Sorting by "number of groups
-    # reachable from me" (descending) gives a topological order.
-    # (Scores are computed first: during list.sort() the list looks empty to
-    # a key function that refers back to it.)
+
+    # After the fixpoint, for any two groups every pair reaches in exactly one
+    # direction, so "how many groups does this one reach" orders them.
+    def reaches(g1: set[str], g2: set[str]) -> bool:
+        return any(b in reach[a] for a in g1 for b in g2)
+
     score = [sum(1 for other in groups if other is not g and reaches(g, other)) for g in groups]
     groups = [g for _, g in sorted(zip(score, groups), key=lambda item: -item[0])]
-    # Validate: every earlier group reaches every later one and never back.
+    # Validate the definition literally: every pair, forward only.
     for i in range(len(groups)):
         for j in range(i + 1, len(groups)):
-            if not reaches(groups[i], groups[j]) or reaches(groups[j], groups[i]):
-                return None
+            for a in groups[i]:
+                for b in groups[j]:
+                    if b not in reach[a] or a in reach[b]:
+                        return None
     return groups
 
 
+def merge_skippable_groups(dfg: DFG, groups: list[set[str]]) -> list[set[str]]:
+    """Merge the groups of a sequence cut that can only be skipped together.
+
+    Follows the function on page 233 of S.J.J. Leemans, *Robust Process
+    Mining with Guarantees* (PhD thesis, 2017), which is also what ProM's and
+    PM4Py's Inductive Miner do, so the trees agree.
+
+    A group ``p`` is *skippable* when some trace gets past it without
+    visiting it: an edge from a group before ``p`` to one after it, a start
+    activity after ``p``, or an end activity before ``p``.  A skippable
+    group then absorbs
+
+    * the groups just before it whose edges never go past ``p`` (they can
+      only leave the sequence through ``p`` or earlier, so skipping ``p``
+      means skipping them), and
+    * the groups just after it that are only ever entered from ``p`` or
+      later (they can only be reached through ``p``, so skipping ``p``
+      skips them as well).
+
+    The merged group takes ``p``'s position, so the sequence order is kept.
+    Groups that do not merge are returned as they were.
+    """
+    n = len(groups)
+    index = {a: i for i, g in enumerate(groups) for a in g}
+    # comes_from[i]: the earliest group an edge into group i comes from; before
+    # everything (-1) when the group holds a start activity.  goes_to[i]: the
+    # latest group an edge out of group i goes to; past everything (n) when
+    # the group holds an end activity.
+    comes_from = [-1 if any(a in dfg.start for a in g) else n for g in groups]
+    goes_to = [n if any(a in dfg.end for a in g) else -1 for g in groups]
+    for a, b in dfg.edges:
+        comes_from[index[b]] = min(comes_from[index[b]], index[a])
+        goes_to[index[a]] = max(goes_to[index[a]], index[b])
+
+    merged = [set(g) for g in groups]
+    where = dict(index)                      # activity -> its group's current position
+
+    def skippable(p: int) -> bool:
+        if any(where[a] < p < where[b] for a, b in dfg.edges):
+            return True
+        return any(where[a] > p for a in dfg.start) or any(where[a] < p for a in dfg.end)
+
+    def absorb(p: int, q: int) -> None:
+        merged[p] |= merged[q]
+        for a in merged[q]:
+            where[a] = p
+        merged[q] = set()
+
+    for p in range(n):
+        if not merged[p] or not skippable(p):
+            continue
+        q = p - 1
+        while q >= 0 and goes_to[q] <= p:
+            absorb(p, q)
+            q -= 1
+        q = p + 1
+        while q < n and comes_from[q] >= p:
+            absorb(p, q)
+            q += 1
+    return [g for g in merged if g]
+
+
 def parallel_cut(dfg: DFG) -> list[set[str]] | None:
     nodes = sorted(dfg.activities)
     edges = set(dfg.edges)

openprocess/references.py

@@ -56,6 +56,8 @@ def url(self) -> str:
               "*Discovering Block-Structured Process Models from Event Logs Containing "
               "Infrequent Behaviour*. Business Process Management Workshops (BPM 2013), "
               "LNBIP 171, pp. 66–78. Springer, 2014.", "10.1007/978-3-319-06257-0_6"),
+    Reference("leemans2017", "S.J.J. Leemans. *Robust Process Mining with Guarantees*. PhD "
+              "thesis, Eindhoven University of Technology, 2017. ISBN 978-90-386-4257-4."),
     Reference("weijters2003", "A.J.M.M. Weijters and W.M.P. van der Aalst. *Rediscovering "
               "Workflow Models from Event-Based Data using Little Thumb*. Integrated "
               "Computer-Aided Engineering 10(2):151–162, 2003."),
@@ -175,8 +177,9 @@ class Topic:
         Topic("α-algorithm", "The eight steps from $T_L$ to $\\alpha(L)$, with $X_L$ and "
               "$Y_L$.", ("aalst2004", "aalst2013", "aalst2016"), "openprocess.mining.discovery.alpha"),
         Topic("Inductive Miner (IM) and IM – infrequent (IMf)",
-              "Cuts, base cases and fall-throughs on the directly-follows graph; IMf filters "
-              "infrequent behaviour.", ("leemans2013", "leemans2014"),
+              "Cuts, base cases and fall-throughs on the directly-follows graph; the strict "
+              "sequence cut; IMf filters infrequent behaviour.",
+              ("leemans2013", "leemans2014", "leemans2017"),
               "openprocess.mining.discovery.inductive"),
         Topic("Heuristics Miner",
               "Dependency measures $a \\Rightarrow b$, length-one and length-two loops, and "

tests/cross_check_inductive_miner.py

@@ -21,13 +21,20 @@
    token-based precision) of the two models on the same log, so a difference
    can be read as "ours is less precise", "equal" or "more precise".
 
-Baseline, OpenProcess 0.11.1 against PM4Py 2.7.23, seed 2026, 400 random logs:
-406 logs, guarantees hold on 406, identical trees on 369 (all six textbook logs
-among them), 37 differ, of which 30 less precise, 4 equal, 3 more precise.
-Every one of the 37 is the same choice: after a sequence cut, groups that are
-always skipped *together* (``<b>, <b,b,a,c>``: ``a`` and ``c`` never appear
-without each other) are modelled as skippable *separately*,
-``→(…, ×(a,τ), ×(c,τ))``, where the reference gives ``→(…, ×(→(a,c),τ))``.
+Baseline against PM4Py 2.7.23, seed 2026, 400 random logs:
+
+* OpenProcess 0.11.1: guarantees hold on 406, identical trees on 369 (all six
+  textbook logs among them), 37 differ, of which 30 less precise.  Every one
+  of the 37 came from the sequence cut: groups that are only ever skipped
+  *together* (``<b>, <b,b,a,c>``: ``a`` and ``c`` never appear without each
+  other) were modelled as skippable *separately*, ``→(…, ×(a,τ), ×(c,τ))``,
+  where the reference gives ``→(…, ×(→(a,c),τ))``; and a cut was accepted
+  when *some* pair of activities reached across it rather than *every* pair.
+* After the strict sequence cut (Leemans 2017, p. 233) and the every-pair
+  test: guarantees hold on 406, identical trees on 401, 5 differ (2 less
+  precise, 2 equal, 1 more precise), all of them fall-throughs on logs that
+  have no cut at all, where the two implementations try the fall-throughs
+  in a different order.
 """
 
 from __future__ import annotations

tests/test_mining.py

@@ -148,6 +148,41 @@ def test_inductive_miner_on_course_log_matches_pm4py():
     assert "stow bag" in tree
 
 
+def test_sequence_cut_follows_the_definition_for_every_pair():
+    """Every activity of an earlier group must reach every activity of a later
+    one.  In [<b,b,c,c,c,c>, <b,a,d,d>] c reaches nothing and d is reached
+    only from a, so c and d (and a) must share a group: {b} | {a, c, d}, not
+    {b} | {a, c} | {d}, which the old any-pair test accepted."""
+    from openprocess.mining.dfg import dfg_from_simple_log
+    from openprocess.mining.discovery.inductive import maximal_sequence_cut
+    dfg = dfg_from_simple_log(parse_simple_log("[<b,b,c,c,c,c>^2, <b,a,d,d>^3]"))
+    assert maximal_sequence_cut(dfg) == [{"b"}, {"a", "c", "d"}]
+    tree = str(inductive_miner(parse_simple_log("[<b,b,c,c,c,c>^2, <b,a,d,d>^3]")).tree)
+    assert tree == "→(↺(b, τ), ×(→(a, ↺(d, τ)), ↺(c, τ)))"      # × is commutative
+
+
+def test_strict_sequence_cut_merges_groups_skipped_together():
+    """Leemans 2017, p. 233: a and c never occur without each other, so the
+    optional stretch is ×(τ, →(a, c)), not two separate choices ×(τ, a),
+    ×(τ, c) that would also allow <b, a> and <b, c>."""
+    from openprocess.mining.dfg import dfg_from_simple_log
+    from openprocess.mining.discovery.inductive import (maximal_sequence_cut,
+                                                        merge_skippable_groups, sequence_cut)
+    log = parse_simple_log("[<b>^4, <b,b,a,c>]")
+    dfg = dfg_from_simple_log(log)
+    assert maximal_sequence_cut(dfg) == [{"b"}, {"a"}, {"c"}]
+    assert merge_skippable_groups(dfg, [{"b"}, {"a"}, {"c"}]) == [{"b"}, {"a", "c"}]
+    assert sequence_cut(dfg) == [{"b"}, {"a", "c"}]
+    result = inductive_miner(log)
+    assert str(result.tree) == "→(↺(b, τ), ×(τ, →(a, c)))"
+    assert any("skipped together" in s.text or "skipped together" in (s.detail or "")
+               for s in result.steps)
+    # The textbook log is a plain sequence cut: nothing to merge, nothing said.
+    plain = inductive_miner(parse_simple_log("[<a,b,c,d>^3, <a,c,b,d>^2, <a,e,d>]"))
+    assert str(plain.tree) == "→(a, ×(∧(b, c), e), d)"
+    assert not any("skipped together" in (s.detail or "") for s in plain.steps)
+
+
 def test_inductive_miner_always_fits_randomised():
     rng = random.Random(7)
     for _ in range(15):