Linear Temporal Logic over Finite Traces (LTLf) Model Checker. Faithful BEAM realization of De Giacomo and Vardi (2013, 2015).
Evaluates declarative process compliance constraints over finite execution sequences:
response(A, B): Whenever A occurs, B must eventually occur later (□(A → ◇B)).precedence(A, B): B cannot occur unless A has occurred previously (¬B W A).non_coexistence(A, B): A and B cannot both occur in the same trace (¬(◇A ∧ ◇B)).chain_response(A, B): Whenever A occurs, B must occur immediately in the next step (□(A → ○B)).exactly_once(A): Activity A must occur exactly once in the trace.absence(A): Activity A must never occur in the trace (□¬A).
Summary
Functions
Constructs an Absence(A) constraint: A must never occur in the trace.
Constructs a Chain-Response(A, B) constraint: whenever A occurs, B must occur immediately next.
Convenience evaluator returning a simple boolean satisfied? result.
Evaluates an LTLf formula or list of formulas against an observed trace.
trace is a list of activity strings.
Returns %{satisfied?: boolean(), violations: [tuple()]}.
Constructs an Exactly-Once(A) constraint: A must occur exactly once in the trace.
Constructs a Non-Coexistence(A, B) constraint: A and B cannot both occur in the same trace.
Constructs a Precedence(A, B) constraint: B cannot occur unless A has already occurred.
Constructs a Response(A, B) constraint: whenever A occurs, B must eventually occur.
Functions
Constructs an Absence(A) constraint: A must never occur in the trace.
Constructs a Chain-Response(A, B) constraint: whenever A occurs, B must occur immediately next.
Convenience evaluator returning a simple boolean satisfied? result.
Evaluates an LTLf formula or list of formulas against an observed trace.
trace is a list of activity strings.
Returns %{satisfied?: boolean(), violations: [tuple()]}.
Constructs an Exactly-Once(A) constraint: A must occur exactly once in the trace.
Constructs a Non-Coexistence(A, B) constraint: A and B cannot both occur in the same trace.
Constructs a Precedence(A, B) constraint: B cannot occur unless A has already occurred.
Constructs a Response(A, B) constraint: whenever A occurs, B must eventually occur.