API reference¶
The core checking API is exported from the top-level musil package — modelling (Model, Action),
the checks (check, check_all, explore, check_liveness, check_ltl), results and traces (Result,
Step, format_trace, witness, …), the LTL formula AST, and the test assertions (assert_ok,
assert_violates). Everything else lives in a submodule, imported directly — e.g.
from musil.probabilistic import reach_probability, from musil.env import check_open,
from musil.metrics import coverage. This reference is grouped the same way: the core first, then each layer
under the concern it serves. See migrating for the import-path changes from the pre-0.35 flat
namespace.
Core¶
The model, the safety/deadlock/reachability checker, traces, and the test assertions — the top-level API.
musil.core ¶
The explicit-state core: a model is (initial states, guarded actions, invariants), and check
does a breadth-first sweep of every reachable state, reporting the first invariant violation or
deadlock with the shortest trace that reaches it.
States are plain immutable, hashable Python values — a frozen dataclass is the idiomatic choice.
Actions are pure: enabled(state) decides whether the action can fire, apply(state) returns
the resulting NEW state. Because the sweep fires every enabled action from every state,
modelling several concurrent actors is just handing it all their actions — the interleaving is
explored for free. That's the whole point: the bugs that matter are races, and BFS over
interleavings finds them.
This module is dependency-free and knows nothing about any particular domain.
Action
dataclass
¶
A guarded, atomic transition. enabled decides if it can fire in a state; apply returns
the resulting new state (states are immutable, so it never mutates). Keep both pure — the checker
calls them many times and assumes no side effects.
fair tags this action's fairness for check_liveness: "weak" (weakly fair), "strong"
(strongly fair), or None (unfair — a fault). With no explicit fair= / fair_strong= tuple,
check_liveness derives its fairness sets from these tags, so the fair-ours / unfair-faults
distinction lives on the action that knows what it is, not in a parallel name list kept in sync by hand.
Source code in src/musil/core.py
Step
dataclass
¶
One link in a counterexample: the action that fired and the state it produced.
Source code in src/musil/core.py
Model
dataclass
¶
What to check: where to start, what can happen, and what must always hold.
init is one state or several. actions are the (possibly multi-actor) transitions — a STATIC
list. invariants map a name → predicate that must hold in every reachable state. terminal
marks states allowed to have no enabled action (an absorbing sink like deleted); any other
dead end is reported as a deadlock.
actions_fn, if given, supplies the actions available IN A GIVEN STATE (actions_fn(state) ->
Iterable[Action]) and takes precedence over the static actions. Use it for a STATE-DEPENDENT
action space — e.g. a possibleActions(state) / offered-menu enumerator, or a parameterized
bounded-action algebra whose enabled bindings depend on the state — instead of hand-guarding a large
static product. Each returned Action's own enabled still applies (return already-enabled actions,
or let their guards filter).
footprint, if given, is a state -> hashable PROJECTION of the sub-state that actions_fn
reads, and turns on MEMOIZATION: the enumerated action list is cached on footprint(state) and
reused across every state that shares a footprint. Use it when actions_fn is expensive (a menu
builder that constructs objects per call) but depends on only part of the state — the framework-level
version of the lru_cache such callers hand-write. It has effect only with actions_fn (there is
nothing to recompute for the static actions). Unlike canonicalize it does NOT quotient the
space, so an unsound footprint does not shrink the sweep — it feeds a state the WRONG memoized menu, so
successors go wrong and reachable states (and the violations only they reach) can be missed. The
obligation is that actions_fn yields the SAME menu for any two states with equal footprint; gate it
with footprint_sound before trusting it.
Source code in src/musil/core.py
ActionSchema
dataclass
¶
A PARAMETERIZED action: a name, typed parameter slots each with a BOUNDED domain, and pure
apply/enabled that take those parameters as keyword arguments. enumerate_actions expands it
into one concrete Action per binding in the cartesian product of the domains.
This makes the bounded-action-algebra pattern first-class: a closed union whose members declare typed
parameter slots with bounded domains, from which consumers construct concrete actions (the shape THE
ACTION LAW describes). params maps slot name → its finite domain; apply(state, **params) -> state
and enabled(state, **params) -> bool receive the bound arguments. A schema with no params yields a
single concrete action.
Source code in src/musil/core.py
Result
dataclass
¶
The outcome. ok is True when the whole reachable space satisfied every invariant with no
deadlock. Otherwise kind is "invariant" or "deadlock", invariant names the broken
one, and trace is the shortest path from an initial state to the offending state.
Source code in src/musil/core.py
action_names
property
¶
The action names along the counterexample trace, excluding the synthetic <init> step —
the sequence of steps that reproduces the violation (empty on success).
witness
property
¶
The offending state — the last state of the counterexample trace (the one that breaks the
invariant or deadlocks) — or None on success / an empty trace.
Verdict ¶
Bases: Protocol
What assert_ok needs from a result: a boolean verdict and a renderer. Every musil result
type satisfies it structurally -- Result, LivenessResult, ConformanceResult,
RefinementResult, OpenResult, SimReport.
Source code in src/musil/core.py
Graph
dataclass
¶
The full reachable state graph: initial states, every reachable state, and the labelled
transitions (edges[s] = the (action_name, next_state) pairs out of s). Built by
explore and consumed by liveness checking and graph export. truncated flags hitting the
max_states cap.
Source code in src/musil/core.py
FixedPoints
dataclass
¶
Where the system settles: for each initial state, the distinct terminal states (no outgoing
edge) reachable from it. Built by fixed_points; confluent is the headline question.
Source code in src/musil/core.py
confluent
property
¶
True when every single initial state settles in at most one place — the fixed point does
not depend on the order actions fired. A start with an empty set never settles at all (it
can only loop); that is a liveness question, not a confluence one, and does not count
against confluence. False whenever truncated (inconclusive).
StateViolation
dataclass
¶
One reachable state that breaks one invariant. reason carries the detail from a
string-returning invariant, if any.
Source code in src/musil/core.py
invariant_from_violations ¶
invariant_from_violations(
checker: Callable[[S], Sequence[object]],
*,
describe: Callable[[object], str] = str,
) -> Invariant[S]
Adapt an external checker into a musil invariant. checker(state) returns a sequence of
violation objects — empty means the state is fine. The resulting invariant returns True when
that sequence is empty, else the first violation's describe(...) string (a reason surfaced in
the counterexample). Use this to drive a real world -> [Violation] checker as an invariant
without the not checker(s) footgun (a truthy reason string would otherwise read as 'holds').
Source code in src/musil/core.py
enumerate_actions ¶
Expand parameterized ActionSchemas into concrete musil Actions — the cartesian product over
each schema's bounded parameter domains, one Action per binding (a zero-param schema → one Action). Each
argument tuple is bound BY VALUE so the generated closures don't capture the loop variable. The concrete
action's name encodes its binding (e.g. add_filter{field='status', value='active'}) so counterexample
traces read as filled actions. Pair with a static Model(actions=enumerate_actions(...)) for a bounded
parameterized algebra, or call it inside actions_fn to bound the domains per state.
Source code in src/musil/core.py
format_trace ¶
format_trace(
trace: Iterable[Step[S]],
*,
render: Callable[[S], str] | None = None,
loop: int | None = None,
) -> str
Render a counterexample as Init: <state> then → <action> <state> per step. render customises
how each state is shown (default str) — useful for rich states whose full repr is noisy. loop is
the index of a lasso's cycle start: a --- loops forever --- marker is emitted after that state, so an
infinite-run (LTL) counterexample shows where the repeating suffix begins.
Source code in src/musil/core.py
format_trace_diff ¶
Like format_trace but shows only the FIELDS THAT CHANGED between consecutive states — the init in
full, then per step the field=new deltas. Far more readable for rich states (dataclass / pydantic /
Mapping) where a full dump per step drowns the one thing the action changed. Falls back to the full state
repr for any state whose fields can't be introspected.
Source code in src/musil/core.py
assert_ok ¶
assert_ok(
result: Verdict,
message: str | None = None,
*,
truncated: Literal["fail", "ok"] = "fail",
) -> None
Assert a result is OK, failing with its rendered form -- the counterexample, not the repr.
assert check(model) inside a test runner reports the result's repr, and pytest shortens a
long one by eliding its middle: the trace comes out as
trace=(Step(action='<init>', s...Step(action='inc', state=S(n=3))), with the initial state
cut, followed by the whole Model repr (lambda addresses included) as assertion context. The
counterexample is not merely ugly there, it is incomplete. This raises AssertionError(str(result))
instead, so the failure message is the Init: ... -> action: ... rendering __str__ already
produces. message is prefixed when the same assertion runs over several models.
truncated governs a passing-but-TRUNCATED result — the max_states cap stopped the sweep before
the space was exhausted, so a green verdict proves nothing about the unexplored part. The default
"fail" rejects it (raise max_states, or pass truncated="ok" to accept an inconclusive pass);
this closes the quiet hole of a truncated green being read as proof.
Works on any musil result (they all carry ok and a meaningful __str__), and needs no test
framework -- it is a plain AssertionError, so unittest and bare assert get it too.
Source code in src/musil/core.py
assert_violates ¶
assert_violates(
result: Verdict,
message: str | None = None,
*,
kind: str | None = None,
invariant: str | None = None,
via: Iterable[str] | None = None,
where: Callable[[Any], bool] | None = None,
) -> None
Assert a check FOUND a violation — the red-side counterpart to assert_ok — optionally pinning the
details, rendering the full counterexample on any mismatch.
Fails if result.ok (no violation was found). Then, for each given constraint: kind must equal the
verdict kind ("invariant" / "deadlock" / "p-unreachable" / "fair-cycle" / "ltl");
invariant must equal the broken invariant name; every name in via must appear among the
counterexample's action_names; and where must hold on the witness (the offending state).
Works on Result and LivenessResult alike (both expose kind / action_names / witness);
message is prefixed as in assert_ok.
Source code in src/musil/core.py
actions_source ¶
The per-state action list the BFS loops iterate. With a Model.footprint and an actions_fn
the enumerated list is MEMOIZED on footprint(state) — states sharing a footprint reuse the tuple
instead of re-running actions_fn — so an expensive enumerator runs once per footprint, not once
per state (footprint_sound is the obligation). Without a footprint it is actions_fn itself;
with only static actions it is a constant. cache.get is disambiguated with is None so a
genuinely empty menu (()) is a hit, not re-enumerated.
Source code in src/musil/core.py
check ¶
check(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
) -> Result[S]
Breadth-first sweep of every reachable state. Returns the first invariant violation or
deadlock found (shortest trace, because BFS visits by increasing depth), else OK once the whole
reachable space is exhausted. max_states is a runaway guard for unbounded models.
canonicalize enables symmetry reduction (OPT-IN, soundness is the caller's obligation):
map each state to a canonical representative of its symmetry-equivalence class and only that
representative is explored — collapsing interchangeable components (e.g. sort the per-worker
slices) so the space stops blowing up combinatorially. SOUND only if it is a genuine symmetry of
the model: every action commutes with it and every invariant is constant across each class.
Getting that wrong silently drops reachable states (misses bugs), so VALIDATE it on small
instances with symmetry_reduction_sound before trusting it on large ones. Counterexample
traces are then witnesses up to symmetry (each step a real action followed by a renaming).
key maps a state to a HASHABLE identity used ONLY for the visited-set + trace bookkeeping. Supply
it when the state itself is NOT hashable (e.g. a pydantic model or a dataclass with list fields) so
it can be checked directly, with no wrapper type. Its result need not be a state — the rich states are
kept for the trace. It carries no SYMMETRY obligation (it does not quotient the space), but it DOES carry
an INJECTIVITY obligation: distinct reachable states (post-canonicalize) must map to distinct keys. A
collision prunes the second state AND all its successors from the sweep — silently dropping reachable
states and any violations only they reach, exactly the unsoundness canonicalize warns about, but with
no validator. When unsure, make key a lossless encoding of the whole state (e.g. every field). Unlike
canonicalize, a NON-injective key is never sound. (explore and the tools built on it still
require hashable states.) The model's actions_fn (if set) supplies the per-state action list;
otherwise the static actions are used.
Source code in src/musil/core.py
541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 | |
check_all ¶
check_all(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
distinct_by: str
| Callable[[str, str | None], Hashable] = "invariant",
) -> list[Result[S]]
Exhaustive check: instead of stopping at the FIRST problem, sweep the WHOLE reachable space and
return the SHORTEST witnessing trace for EACH DISTINCT violation (plus deadlock, once). For a review/audit
pass where you want the full list of what is broken, not one counterexample at a time.
distinct_by controls how violations are bucketed:
- "invariant" (default) — one entry per broken invariant NAME;
- "reason" — one entry per (invariant, reason) pair (finer);
- a CALLABLE (invariant_name, reason) -> hashable — bucket by a caller-defined CLASS. Use this when
the reason embeds variable detail (ids, counts) that would otherwise explode into many spurious
"distinct" entries: return e.g. the failure category so all instances collapse to one witness.
Results are ordered shortest-trace-first (BFS visits by increasing depth), so the most easily-triggered
problems lead. An EMPTY list means the model is fully correct (the analog of check(...).ok being True).
Unlike reachable_violations (one StateViolation per offending state, no path), each entry here is a
full Result with a reproducible trace. Shares check's invariant semantics, canonicalize
(symmetry reduction), key (hashable identity for non-hashable states — must be INJECTIVE over reachable
states; see check for the full contract), and the model's actions_fn.
Source code in src/musil/core.py
645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 | |
explore ¶
explore(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
) -> Graph[S]
Build the whole reachable state graph (no invariant checks). The shared exploration primitive
behind liveness and graph export; check stays separate so it can early-exit with the shortest
counterexample. canonicalize enables symmetry reduction (see check); validate it with
symmetry_reduction_sound before trusting it. Honours the model's actions_fn (per-state action
list) when set. States must be HASHABLE here (they key the graph); check/check_all accept a
key for non-hashable states, but the graph tools do not.
Source code in src/musil/core.py
reaches ¶
The states of graph from which a predicate-satisfying state is reachable (states
already satisfying it included) — plain reachability, by BFS over the reversed edges.
This is the weaker cousin of liveness: "can it still get there?", not "must it get there?".
reaches(g, p) == set(g.states) says the goal stays available from every reachable state
(in CTL terms: AG EF p) — e.g. "fmi3FreeInstance is legal in every mode" — whereas
check_liveness(..., everywhere=True) demands every run actually reach it (AG AF p): a
cycle that forever declines an available exit toward p violates the latter, never the former.
The complement set(graph.states) - reaches(graph, p) is the trap — reachable states from
which p is already lost.
Source code in src/musil/core.py
check_of ¶
Run the safety check over an ALREADY-explored graph instead of re-exploring — the graph-first
counterpart to check (as coverage_of is to coverage), so several analyses can share one
explore. Returns the same Result: the first invariant violation or deadlock in breadth-first
order (shortest trace), else OK.
Deadlock detection needs a COMPLETE graph: on a truncated one a cut-off frontier state looks like a sink,
so deadlocks are not reported there (invariant violations still are — a reachable violating state is a
real bug regardless), and a clean result carries truncated=True (inconclusive). check(model)
equals check_of(explore(model), model) on a complete graph, but check keeps its early-exit (it
stops at the first violation without building the whole graph), so prefer check when the verdict is
all you need. states_explored is the whole graph here, not check's partial count at early-exit.
Source code in src/musil/core.py
never ¶
An edge invariant that FORBIDS a transition: violated when action fires (optionally only from a
when before-state). The direct way to rule out an illegal step without a ghost flag on the state,
e.g. edge_invariants={"no-approve-unreviewed": never("approve", when=lambda s: not s.reviewed)}.
Source code in src/musil/core.py
path_to ¶
The shortest path from an initial state to state (a specific reachable state), as a Step
tuple, or None if state is not reachable. The positive counterpart to a counterexample trace — a
WITNESS that a state is reachable, and how. Render it with format_trace.
Source code in src/musil/core.py
witness ¶
The shortest path from an initial state to SOME reachable state satisfying predicate — a witness
that a good state is reachable and how to get there — or None if none is. Where reaches answers the
same question as a yes/no over the whole reachable set, this returns the concrete path. Render it with
format_trace.
Source code in src/musil/core.py
states_where ¶
The reachable states of graph satisfying predicate, in exploration order.
solution_cardinality counts these; this returns them (e.g. to inspect which states a goal holds
in, or feed to path_to).
Source code in src/musil/core.py
fixed_points ¶
fixed_points(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
) -> FixedPoints[S]
From each initial state separately: in which distinct terminal states can the runs end?
One start that can settle in two different places means the outcome depends on the order
actions fired — the bug this exists to catch (e.g. event iteration whose fixed point depends
on which pending event is applied first). Per initial state on purpose: different starts are
allowed to settle differently (that is what a latch is for); confluent only demands each
single start settle in at most one place.
Terminal here is structural — no outgoing edge — independent of model.terminal: the
question is where the dynamics stop, not which stops are declared legitimate. A start mapped
to an empty set never settles (every path loops); ask check_liveness about that instead.
canonicalize applies symmetry reduction (see check). If any exploration hits
max_states the result is inconclusive: truncated is set and confluent is False.
Source code in src/musil/core.py
fixed_points_of ¶
Graph-first fixed_points: the per-initial structural fixed points over an ALREADY-explored
graph instead of re-exploring from each initial — the graph-first counterpart to fixed_points (as
check_of is to check), so several analyses can share one explore. For each initial state, the
distinct STRUCTURAL terminals (a state with no outgoing edge) reachable from it, by forward BFS over the
graph's edges.
Equals fixed_points(model) on a graph built by explore(model) with the same canonicalize (the
corpus pins this), and carries the graph's truncated — a truncated graph is inconclusive, so
confluent is then False. Structural terminal is independent of model.terminal (the question is
where the dynamics STOP, not which stops are declared legitimate), which is why this needs only the graph.
Source code in src/musil/core.py
symmetry_reduction_sound ¶
symmetry_reduction_sound(
model: Model[S],
canonicalize: Callable[[S], S],
*,
max_states: int = 1000000,
) -> bool
Validate a symmetry-reduction canonicalize for model on a (bounded) instance — the
soundness gate that should pass before check(..., canonicalize=...) is trusted on larger
instances.
It explores the model fully and reduced and confirms two things agree:
(1) the reduced run visited exactly the canonical quotient of the full reachable set
({canonicalize(s) for s in full} == set(reduced)) — reachability coverage; and
(2) the SAME set of invariants is violable in both runs — which additionally certifies that every
invariant is constant across each symmetry class (a state and its representative agree).
Both matter: (1) alone passes for a lossy projection that merges non-equivalent states, but (2)
then catches it because an invariant violated on a dropped state is no longer violated on its
(information-losing) representative. Because the full run is the trusted reference, any unsound
canonicalize — not a real symmetry, or a real symmetry against a non-class-constant invariant —
makes one of these disagree and returns False. (Deadlock-freedom under reduction is NOT covered;
validate that separately.) Returns False if either run truncated at max_states (inconclusive).
Source code in src/musil/core.py
footprint_sound ¶
Sample-check a Model.footprint over the given states — the gate to pass before trusting
the footprint memoization (see Model.footprint).
footprint is a performance cache, not a quotient: it does not change WHICH states are explored,
only avoids re-running actions_fn for states that share a footprint. That makes it soundness-
critical the other way round from canonicalize — an unsound footprint does not shrink the space,
it hands a state the WRONG memoized menu, so the sweep follows wrong successors and can miss states
(and the violations only they reach). The obligation is that actions_fn yields the SAME menu for
any two states with equal footprint.
This groups states by footprint and returns False if any group holds two states whose
actions_fn menus differ, compared by the MULTISET OF ACTION NAMES (so a footprint that changes an
action's behaviour while keeping its name is out of scope — keep the name a faithful label). Returns
False if the model has no actions_fn or footprint to validate. Pass a representative sample:
for a hashable model, explore(model).states; for a non-hashable one (a pydantic state checked via
key=, exactly footprint's target case), a hand-picked or generated set. Like every sampling gate
it can only DISPROVE soundness on the states it sees, never prove it universally.
Source code in src/musil/core.py
reachable_violations ¶
reachable_violations(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
) -> list[StateViolation[S]]
Every (reachable state, broken invariant) pair — an exhaustive audit, where check stops
at the first. Use it to enumerate all the invalid states a model can reach — e.g. to derive the
exact set of cross-resource combinations that guards must exclude — instead of one shortest
counterexample. Deadlock is not considered (use check for that). Each invariant is evaluated
with the same semantics as check: a string return is a violation carrying that reason.
canonicalize applies symmetry reduction (see check).
Source code in src/musil/core.py
Temporal logic¶
Liveness and full linear-temporal-logic checking, plus the named pattern sugar.
musil.ltl ¶
Linear Temporal Logic — a formula AST plus a checker.
The nodes (Atom, Not, And, Or, Implies, Next, Eventually, Always,
Until, Release, WeakUntil) build an LTL formula as pure data. check_ltl checks ANY of them.
check_ltl first tries the shapes that reduce SOUNDLY to musil's proven primitives (fast, and they
carry a shortest-path counterexample trace):
Always(state)-> a safety invariant (check)Eventually(state)-><>P(check_liveness)Always(Eventually(state))->[]<>Precurrence (check_liveness(everywhere=True))Always(Implies(state, Eventually(state)))-> the response/leads-to property- a top-level conjunction of any of the above (checked conjunct by conjunct)
where state is any boolean combination of Atoms. Anything else — Next, Until, Release,
WeakUntil, arbitrary nesting — falls through to the GENERAL engine: model |= phi iff the Büchi
automaton for Not(phi) (GPVW, GeneralizedBuchi.from_ltl) has no accepting run over the
stutter-extended reachable graph (has_accepting_run, emptiness via SCC). The engine is sound over
infinite runs; terminal/deadlock states are stutter-extended so their finite runs are handled. Still to
come: a counterexample lasso from the engine, and re-expressing the fixed liveness forms / musil.patterns
as sugar over check_ltl. See LTL_NOTES.md.
LTL ¶
Atom
dataclass
¶
Buchi
dataclass
¶
A Büchi automaton over the alphabet of MODEL states — the sound back half of LTL model checking.
Automaton states are ints. transitions[q] is the tuple of (guard, q') edges out of q,
where guard(model_state) decides whether the edge fires from the model state currently being read
(the SOURCE of each model step). A run of the automaton over a model run is ACCEPTING iff it visits an
accepting automaton state infinitely often.
Built by hand today (for testing the emptiness check); constructed from Not(formula) by the GPVW
translation in a later step, at which point check_ltl runs it against explore(model) and an
accepting run is a counterexample to the formula. See LTL_NOTES.md.
Source code in src/musil/ltl.py
has_accepting_run ¶
True iff the product of graph and this automaton has an accepting run: a cycle reachable
from an initial product state that passes through an accepting automaton state. Emptiness via SCC
(musil's proven tarjan/has_internal_edge): an accepting run exists iff some reachable
non-trivial SCC of the product contains a product state whose automaton component is accepting.
Source code in src/musil/ltl.py
GeneralizedBuchi
dataclass
¶
A GENERALIZED Büchi automaton: like Buchi but with SEVERAL acceptance sets. A run is accepting
iff it visits EACH set in accepting_sets infinitely often. This is exactly the shape the GPVW
construction produces from an LTL formula (one acceptance set per Until subformula), so the engine
can run it directly without degeneralizing to a single-set Buchi.
Source code in src/musil/ltl.py
538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 | |
has_accepting_run ¶
True iff the product has a run visiting every acceptance set infinitely often. Emptiness via SCC: a reachable non-trivial SCC that intersects EVERY acceptance set contains such a run (being strongly connected, one cycle can visit all sets). With no acceptance sets, any non-trivial reachable SCC accepts (an unconstrained infinite run).
Source code in src/musil/ltl.py
accepting_lasso ¶
A concrete witness of an accepting run, as a lasso trace <init> -> ...(stem)... -> ...(cycle)
where the cycle repeats forever and visits every acceptance set, PLUS the index in that trace where
the cycle begins (the state reached, then repeated forever). Returns None when there is no accepting
run. Product states are mapped back to model states (the automaton component dropped); the looping
cycle is appended once.
Source code in src/musil/ltl.py
degeneralize ¶
The equivalent single-set :class:Buchi automaton, by the standard counter construction: one copy
of the automaton per acceptance set, advancing the counter when the current copy's acceptance set is
visited, and accepting in copy 0's set. A run visits accepting infinitely often iff it completes a
full counter cycle infinitely often iff it visits EVERY accepting_sets set infinitely often — so
the result recognises the same ω-language over every model: degeneralize().has_accepting_run(g) ==
has_accepting_run(g) for any graph g. With no acceptance sets, every infinite run accepts (all
states accepting). This is the front-end step toward a deterministic automaton for quantitative LTL
(an LDBA — see GENERAL_PLTL_NOTES.md).
Source code in src/musil/ltl.py
from_ltl
classmethod
¶
Build the automaton that accepts exactly the model runs satisfying formula, via the GPVW
(Gerth-Peled-Vardi-Wolper) tableau construction. To check model |= phi, build the automaton for
Not(phi) and ask whether it has_accepting_run(explore(model)) — an accepting run is a
counterexample to phi. The formula is put in negation normal form first (_push_negations);
each Until/Eventually subformula contributes one acceptance set (its eventuality must be
fulfilled, not deferred forever). See LTL_NOTES.md.
Source code in src/musil/ltl.py
check_ltl ¶
check_ltl(
model: Model[S],
formula: LTL[S],
*,
name: str = "ltl",
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] | None = None,
max_states: int = 1000000,
) -> Result[S] | LivenessResult[S]
Check formula against model, reducing the supported fragment onto check /
check_liveness (see the module docstring). Returns a Result for the safety reductions and a
LivenessResult for the liveness ones; both satisfy the Verdict protocol (.ok + __str__).
G p (Always of a state predicate) is PURE LTL safety: it holds iff p holds in every reachable
state and IGNORES deadlocks (an undeclared dead-end does not fail G p on its own; deadlock-freedom is a
separate property — use check or G(enabled) for that). So Always(p) agrees with its equivalent
false R p even on deadlocking models.
fair / fair_strong (weak / strong fairness by action NAME) apply everywhere: the reducible forms
(F / GF / G(a -> F b)) route through check_liveness, and any other formula is checked by the general
Büchi engine under fairness by reduction — model |=_fair phi iff model |= (fairness -> phi), with
the fairness assumption encoded as an LTL premise over the with_last_action model (where taken(a)
and enabled(a) are state atoms). A counterexample is then a FAIR run violating phi, its states
mapped back to the model's own. An unknown fair action name raises ValueError (validated against the
static action set). Any formula outside the reducible shapes is otherwise checked by the general engine
over the stutter-extended reachable graph (a Result with kind="ltl" on violation). On violation the Result carries a counterexample trace: the accepting
lasso of the Not(formula) automaton mapped back to model states — <init> -> ...(stem)... ->
...(cycle) — a concrete run that refutes the formula. Requires hashable states (the engine explores
the graph).
Source code in src/musil/ltl.py
355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 | |
musil.liveness ¶
Liveness: does the system eventually reach a goal, or can it loop forever short of it?
check_liveness(model, goal=P) proves the temporal property "eventually P" (<>P): on every run
from an initial state, P holds at some point. It fails in exactly two ways, and we report whichever
we find with a lasso counterexample (a stem into a recurring set, plus the loop):
- P unreachable — a reachable state from which P can never be reached (a dead end or a trap SCC with no exit to P). No scheduling fixes this.
- fair cycle — a reachable cycle of ¬P states that the system can follow forever. Whether
this counts depends on FAIRNESS: under weak fairness of an action set, an action that is
continuously enabled along the cycle must eventually be taken — so a cycle that starves a
continuously-enabled fair action is not a real counterexample (the fair scheduler would break
it). Pass
fair=[...]to rule those out; withfair=()you get strict (no-fairness) liveness.
Method: explore the reachable graph, restrict to ¬P states reachable through ¬P from a ¬P initial
state, then (1) flag any from which P is unreachable, (2) Tarjan-SCC the rest and report the first
non-trivial SCC that hosts a fair cycle. Strong fairness (fair_strong=[...]: an action enabled
infinitely often must be taken) is checked with sub-SCC refinement — a strongly-fair action enabled
somewhere in an SCC but never taken need not fire on a cycle that avoids the states enabling it, so
those states are removed and the remainder re-decomposed to a fixpoint (Emerson-Lei). Without that,
a fair cycle confined to a sub-SCC is missed and the property is wrongly reported to hold.
Dependency-free; for finite (bounded) models.
LivenessResult
dataclass
¶
Outcome of an "eventually P" check. ok True means every run reaches P. Otherwise kind
is "p-unreachable" or "fair-cycle"; stem is the shortest path from an initial state
to the offending state, and cycle is the recurring loop (empty for a P-unreachable sink).
Source code in src/musil/liveness.py
action_names
property
¶
The action names along the counterexample — the stem into the offending state then the
cycle it loops on — excluding the synthetic <init> step (empty on success).
witness
property
¶
The offending state — the last state of the stem (the P-unreachable trap, or the entry of the
fair cycle) — or None on success / an empty stem.
check_liveness ¶
check_liveness(
model: Model[S],
*,
goal: Callable[[S], bool],
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] | None = None,
everywhere: bool = False,
leadsto_from: Callable[[S], bool] | None = None,
goal_name: str = "goal",
max_states: int = 1000000,
) -> LivenessResult[S]
Prove a liveness property and return a lasso counterexample if it fails.
Default (everywhere=False) checks <>P — eventually P on every run from an initial
state. everywhere=True checks []<>P — on every run, always eventually P: past any
point of any run, P must actually be reached again. This is NOT reachability: a reachable
cycle that forever declines to move toward P is a violation even when P stays reachable from
every state on it — declare the exit in fair=[...] if a fair scheduler would eventually
take it. For the weaker "P merely remains reachable from every state" (AG EF, no state is ever
trapped), use reaches: reaches(g, goal) == set(g.states) with g = explore(model).
Use everywhere=True for convergence/recurrence properties whose model may start already
satisfying P.
leadsto_from=Q checks the response property [](Q -> <>P) — whenever Q holds, P
eventually follows. This is the untimed "no resource gets stuck" property: e.g. every service
that enters placed eventually reaches running or failed. It is weaker than
everywhere=True — only states triggered by Q must reach P, so a ¬P cycle that no Q-state can
reach is not a violation. (Implemented by seeding the same analysis from every reachable Q∧¬P
state; everywhere is ignored when leadsto_from is given.)
Fairness prunes cycles a fair scheduler would break. fair = weak fairness (an action
continuously enabled along a cycle must eventually be taken). fair_strong = strong fairness
(an action enabled infinitely often — i.e. in any state of the cycle — must be taken); strong
is the stronger assumption and rules out more cycles, so it can force a "flickering" action that
weak fairness cannot.
Each of fair / fair_strong is a tuple of action NAMES, OR left as None (the default) to
DERIVE the set from the actions' own fair="weak" / fair="strong" tags — so the fair-ours /
unfair-faults split lives on the actions, not in a parallel list kept in sync by hand. An explicit tuple
is validated: a name matching no action raises ValueError (a silent no-match fails in the unsound
direction). Tags and validation apply to a static actions list; with actions_fn pass names
explicitly (they are then used unchecked).
Source code in src/musil/liveness.py
check_liveness_of ¶
check_liveness_of(
graph: Graph[S],
*,
goal: Callable[[S], bool],
fair: Iterable[str] = (),
fair_strong: Iterable[str] = (),
everywhere: bool = False,
leadsto_from: Callable[[S], bool] | None = None,
goal_name: str = "goal",
) -> LivenessResult[S]
Run the liveness analysis over an ALREADY-explored graph instead of re-exploring — the graph-first
counterpart to check_liveness (as coverage_of is to coverage), so several analyses can share
one explore. Same properties, verdict, and lasso counterexample; see check_liveness for the full
semantics of goal / everywhere / leadsto_from and the fairness assumptions. check_liveness
is exactly check_liveness_of(explore(model, max_states=max_states), ...).
Source code in src/musil/liveness.py
has_internal_edge ¶
A non-trivial recurring set: >1 node, or a single node with a self-loop.
Source code in src/musil/liveness.py
tarjan ¶
Iterative Tarjan SCC over the subgraph induced by nodes (successors outside nodes are
ignored). Iterative to avoid Python recursion limits on deep graphs.
Source code in src/musil/liveness.py
musil.patterns ¶
musil.patterns — the Dwyer/Corbett specification patterns as one-call helpers.
These helpers name the well-known patterns so a team picks the pattern instead of encoding the temporal logic (issue #16):
always(p)— universality:pholds in every reachable state (safety, viacheck).absent(p)— absence:pholds in no reachable state (safety, viacheck).eventually(p)— existence:<>p, every run reachesp(liveness).recurs(p)— recurrence:[]<>p, every run reachespinfinitely often (liveness).responds(trigger, response)— response:[](trigger -> <>response)(liveness, leads-to).
The three LIVENESS patterns are SUGAR over check_ltl: each builds the corresponding Eventually /
Always(Eventually(...)) / Always(Implies(...)) formula and calls check_ltl, which owns the one
reduction of the temporal fragment onto check_liveness. So the lowering lives in a single place (fix or
extend it there and every pattern follows), and a pattern is by construction the same verdict as its LTL
formula (pinned in the corpus). The two SAFETY patterns stay direct check calls: G(state) is just an
invariant, and they expose canonicalize / key that the safety reduction inside check_ltl does
not forward, so routing them through it would drop those options for no gain. Because always / absent
go through check, they ALSO report a DEADLOCK (an undeclared dead-end) as a failure — the safety-check
surface, "p invariant AND no deadlock". This deliberately differs from the pure-LTL check_ltl(Always
(p)), which is a safety property that IGNORES deadlocks (deadlock-freedom is a separate concern; see
LTL_NOTES.md). Use the pattern for a safety check, check_ltl(Always(p)) for LTL G p.
Each returns whatever its underlying check returns (a Result for the safety patterns, a
LivenessResult for the liveness ones); both satisfy the Verdict protocol (.ok + __str__),
so assert_ok works uniformly.
Scope: these are the GLOBAL-scope patterns. The scoped variants (after / between / until a delimiter) and the precedence family (which need the state to carry history of what has happened) are deliberately not here yet — see issue #16 for the plan.
always ¶
always(
model: Model[S],
p: Callable[[S], bool],
*,
name: str = "always",
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
) -> Result[S]
Universality: p holds in EVERY reachable state. Lowers to check with p as the sole
invariant, so it ALSO reports a deadlock (an undeclared dead-end) as a failure — the safety-check surface.
This differs from check_ltl(Always(p)), the pure-LTL G p, which ignores deadlocks; use that for LTL
safety. The Result carries the shortest trace to a state where p fails (or to the deadlock).
Source code in src/musil/patterns.py
absent ¶
absent(
model: Model[S],
p: Callable[[S], bool],
*,
name: str = "absent",
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
) -> Result[S]
Absence: p holds in NO reachable state. Lowers to check with not p as the invariant, so
(like always) it also reports a deadlock as a failure — the safety-check surface, not pure LTL.
Source code in src/musil/patterns.py
eventually ¶
eventually(
model: Model[S],
p: Callable[[S], bool],
*,
name: str = "P",
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] | None = None,
max_states: int = 1000000,
) -> LivenessResult[S]
Existence: <>p — every run from an initial state eventually reaches a p-state. Sugar for
check_ltl(model, Eventually(p)); fair/fair_strong prune cycles a fair scheduler would break.
Source code in src/musil/patterns.py
recurs ¶
recurs(
model: Model[S],
p: Callable[[S], bool],
*,
name: str = "P",
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] | None = None,
max_states: int = 1000000,
) -> LivenessResult[S]
Recurrence: []<>p — every run reaches p infinitely often (past any point, p recurs).
Sugar for check_ltl(model, Always(Eventually(p))).
Source code in src/musil/patterns.py
responds ¶
responds(
model: Model[S],
trigger: Callable[[S], bool],
response: Callable[[S], bool],
*,
name: str = "response",
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] | None = None,
max_states: int = 1000000,
) -> LivenessResult[S]
Response: [](trigger -> <>response) — whenever trigger holds, response eventually
follows. The untimed "nothing gets stuck" property. Sugar for
check_ltl(model, Always(Implies(trigger, Eventually(response)))).
Source code in src/musil/patterns.py
Probabilistic & simulation¶
Exact DTMC/MDP verification (rational arithmetic, no floating point), and the sampling-based simulator for faulty distributed runs.
musil.probabilistic ¶
Bounded probabilistic verification — EXACT reachability probability over the reachable graph.
sim runs seeded Monte-Carlo (sampling, not verification). This asks the exact quantitative question a
stochastic system needs: what is the probability of eventually reaching a target set? Actions carry a
relative WEIGHT per state; the enabled actions' weights form a probability distribution over successors,
turning the reachable graph into a discrete-time Markov chain (DTMC). reach_probability returns the
exact answer as a fractions.Fraction — solved by Gaussian elimination over the rationals, so there is
no floating-point error and NO dependency (numpy is only ever an optional accelerator for large systems).
The standard three-way split (Baier & Katoen, Principles of Model Checking, ch. 10): target states have
probability 1; states that cannot reach the target have probability 0; the rest solve the linear system
x_s = sum_s' P(s, s') x_s'.
reach_probability_mdp adds NONDETERMINISTIC choice on top of the DTMC: a caller-supplied moves
function partitions each state's enabled actions into the moves a scheduler may pick between, and the
actions WITHIN a move form the probability distribution (via weight). This is a Markov decision
process (MDP); optimize="max" / "min" returns the maximal / minimal reachability probability over
all schedulers, solved EXACTLY by policy iteration (each policy's value is an exact DTMC solve; the policy
is improved until stable). Both functions take an optional steps=k for the exact probability of
reaching the target WITHIN k transitions (a finite unrolling, no fixed point). expected_reward
answers the dual quantitative question: the exact expected accumulated cost (default: number of steps) to
reach the target in a DTMC, finite only when the target is reached almost surely. long_run_probability
answers the steady-state question: the exact fraction of time the DTMC spends in a target set in the limit,
by decomposing into bottom SCCs and solving each one's stationary distribution exactly; long_run_reward
generalises it to the steady-state average of any per-state reward (a net rate, which may be negative).
probability_ltl
answers the exact probability that a random DTMC run satisfies an LTL formula, for the reducible F / G / GF /
FG fragment. See PROBABILISTIC_NOTES.md.
assert_probability ¶
assert_probability(
actual: Fraction,
*,
equals: Fraction | int | None = None,
at_least: Fraction | int | None = None,
at_most: Fraction | int | None = None,
label: str = "probability",
) -> None
Assert an exact probability or expected value meets a bound, raising AssertionError with the actual
value on failure — the quantitative analog of assert_ok / assert_violates. equals demands an
exact match; at_least / at_most demand a threshold (give both for a range). Bounds are int or
Fraction (NOT float — the whole point of the probabilistic layer is exact rational answers, and
Fraction(0.01) != 1/100; write Fraction(1, 100)). At least one bound is required.
Use it for the threshold properties a stochastic system needs::
assert_probability(reach_probability(model, is_bad), at_most=Fraction(1, 100), label="failure rate")
assert_probability(expected_reward(model, done), equals=Fraction(2), label="expected attempts")
Source code in src/musil/probabilistic.py
reach_probability ¶
reach_probability(
model: Model[S],
target: Callable[[S], bool],
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
avoid: Callable[[S], bool] | None = None,
steps: int | None = None,
max_states: int = 1000000,
) -> Fraction
The exact probability of eventually reaching a target state from the model's initial state,
treating the reachable graph as a DTMC.
At each state the enabled actions' weight(action_name, state) values are normalised into a
probability distribution over the successors (edges to the same successor sum); the default weight is
1 for every action, i.e. a uniform choice. A weight must be NON-NEGATIVE — a negative one raises
ValueError rather than silently producing a bogus probability (this holds for every function here that
takes a weight). States must be HASHABLE (the graph is explored). Returns a fractions.Fraction —
exact, no floating point.
avoid gives the CONSTRAINED (until) probability P(¬avoid U target): the probability of reaching
target WITHOUT first entering an avoid state. An avoid state that is not itself a target
becomes an absorbing failure (probability 0), so a run that touches it before the target does not count;
target takes precedence (a state in both counts as reached). With no avoid (the default) it is
plain reachability.
With steps=k the answer is the probability of reaching target WITHIN k transitions (an exact
finite unrolling; steps=0 is the indicator of target). With steps=None (the default) it is
the unbounded probability, solved by the exact linear system. Raises ValueError if the exploration
truncates at max_states (the probability would be inconclusive) or if steps is negative.
Source code in src/musil/probabilistic.py
transient_distribution ¶
transient_distribution(
model: Model[S],
steps: int,
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
max_states: int = 1000000,
) -> dict[S, Fraction]
The exact probability distribution over states AFTER EXACTLY steps transitions of the DTMC, from the
initial state — dict[state, Fraction] summing to 1 (PRISM's transient / instantaneous analysis). A
forward push: pi_0 puts all mass on the initial state (the first, if several); pi_{i+1}(s') = sum_s
pi_i(s) P(s, s'). Exact, no fixed point — steps=0 is the point mass on the initial state.
An absorbing / deadlock state (no outgoing edge) keeps its mass, so a run that has stopped there stays
counted. Point-in-time queries follow: sum(pi[s] for s in states if target(s)) is the probability of
being in the target set AT step k — distinct from reach_probability(steps=k), which is the
probability of reaching it WITHIN k. Raises ValueError if the exploration truncates or steps is
negative.
Source code in src/musil/probabilistic.py
expected_reward ¶
expected_reward(
model: Model[S],
target: Callable[[S], bool],
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
cost: Callable[[str, S], Fraction | int] | None = None,
steps: int | None = None,
max_states: int = 1000000,
) -> Fraction
The exact EXPECTED accumulated cost to first reach target from the model's initial state,
treating the reachable graph as a DTMC. With the default unit cost this is the expected number of
STEPS to reach the target.
weight normalises the enabled actions into a distribution over successors exactly as in
reach_probability; cost(action_name, state) is the cost charged for firing that action (default
1). Returns a fractions.Fraction — exact, no floating point, solving E(s) = 0 on the target
and E(s) = sum_s' P(s, s') (cost + E(s')) elsewhere.
With steps=k the answer is instead the expected cost accumulated until the target is reached OR k
steps elapse, whichever comes first — a finite backward induction (E_0 = 0; E_i(s) = cost(s) + sum_s'
P(s,s') E_{i-1}(s') off the target). Always finite, so it needs no almost-sure-reachability guard; a
bounded horizon is the natural "expected cost in the next k steps" question. With steps=None (the
default) it is the unbounded expected cost to reach the target, which is finite only if the target is
reached ALMOST SURELY; otherwise it is infinite, so this raises ValueError when reach_probability
from the initial state is not exactly 1. Also raises ValueError if the exploration truncates at
max_states or if steps is negative.
Source code in src/musil/probabilistic.py
long_run_reward ¶
long_run_reward(
model: Model[S],
reward: Callable[[S], Fraction | int],
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
max_states: int = 1000000,
) -> Fraction
The exact long-run AVERAGE reward per step of the DTMC (PRISM's steady-state reward R=? [S]): in the
limit, the mean of reward(state) over the run, as a Fraction.
The reachable graph is a DTMC (weight normalises each state's enabled actions into a distribution, as
in reach_probability). A finite DTMC is absorbed almost surely into a BOTTOM SCC; inside each BSCC the
long-run fraction of time in a state is its stationary probability pi_B(s), so the long-run average
reward is, over the BSCCs B, sum_B reach(B) * sum_{s in B} pi_B(s) * reward(s) — the reach-weighted
then stationary-weighted mean of the reward. reward MAY be negative (a net cost rate); it is not a
probability. Reachability to each BSCC reuses the exact DTMC solve, pi_B the exact stationary solve.
long_run_probability(model, target) is the special case reward = 1_target (the target's indicator).
Raises ValueError if the exploration truncates at max_states (the answer would be inconclusive).
Requires hashable states (the graph is explored).
Source code in src/musil/probabilistic.py
long_run_probability ¶
long_run_probability(
model: Model[S],
target: Callable[[S], bool],
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
max_states: int = 1000000,
) -> Fraction
The exact long-run (steady-state) fraction of time the DTMC spends in target states, from the
initial state — the answer to "in the limit, what proportion of the time is the system in a target
state?" (PRISM's steady-state / S operator). A Fraction, no floating point.
The reachable graph is a DTMC (each state's enabled actions' weight normalise into a distribution
over successors, as in reach_probability). A finite DTMC is absorbed almost surely into one of its
BOTTOM strongly-connected components (BSCCs); inside each BSCC — a finite irreducible chain — the long-run
fraction of time in each state is its stationary probability. So the answer is, over the BSCCs B, the
sum of P(the run is absorbed into B) times B's stationary mass on the target states:
sum_B reach(B) * sum_{s in B, target(s)} pi_B(s). Reachability to each BSCC reuses the exact DTMC
solve; pi_B is the exact stationary solve (_stationary). Transient states carry zero long-run
measure. An absorbing / deadlock state is treated as self-absorbing (it forms its own BSCC with mass 1).
Raises ValueError if the exploration truncates at max_states (the answer would be inconclusive).
Requires hashable states (the graph is explored). Equals long_run_reward with the target's indicator
as the reward (this delegates to it).
Source code in src/musil/probabilistic.py
long_run_reward_mdp ¶
long_run_reward_mdp(
model: Model[S],
reward: Callable[[S], Fraction | int],
*,
moves: Moves[S],
weight: Callable[[str, S], Fraction | int]
| None = None,
optimize: Literal["max", "min"] = "max",
max_policies: int = 100000,
max_states: int = 1000000,
) -> Fraction
The exact MAXIMAL (or MINIMAL) long-run average reward over all schedulers of the MDP — the steady-state
reward RATE a best/worst scheduler achieves. moves/weight describe the MDP as in
reach_probability_mdp; reward(state) is the per-state rate (may be negative).
This is the pure-Python REFERENCE ORACLE: a finite MDP has an average-optimal MEMORYLESS DETERMINISTIC
policy (Puterman), so the optimum over ALL schedulers equals the best/worst over the finitely many
memoryless deterministic policies — enumerate them, induce each one's DTMC, and take the extreme of
long_run_reward. Exact and dependency-free. It is EXPONENTIAL in the number of states with a genuine
choice (the product of their move-counts), so it is for SMALL MDPs; max_policies caps that product and
raises a loud ValueError past it rather than hanging. An efficient average-reward policy iteration is
the future accelerator (see PROBABILISTIC_NOTES.md), to be differential-tested against this oracle.
Raises ValueError if the exploration truncates, if the policy count exceeds max_policies, or if
optimize is not "max"/"min". Requires hashable states.
Source code in src/musil/probabilistic.py
long_run_probability_mdp ¶
long_run_probability_mdp(
model: Model[S],
target: Callable[[S], bool],
*,
moves: Moves[S],
weight: Callable[[str, S], Fraction | int]
| None = None,
optimize: Literal["max", "min"] = "max",
max_policies: int = 100000,
max_states: int = 1000000,
) -> Fraction
The exact MAXIMAL (or MINIMAL) long-run fraction of time the MDP spends in target over all
schedulers — the MDP analog of long_run_probability (as reach_probability_mdp is to
reach_probability). It is long_run_reward_mdp with the target's indicator as the reward and
delegates to it, so it shares the reference-oracle enumeration of memoryless deterministic policies and the
max_policies cap (see long_run_reward_mdp for the method and its small-MDP scope).
Source code in src/musil/probabilistic.py
probability_ltl ¶
probability_ltl(
model: Model[S],
formula: LTL[S],
*,
weight: Callable[[str, S], Fraction | int]
| None = None,
moves: Moves[S] | None = None,
optimize: Literal["max", "min"] = "max",
max_states: int = 1000000,
) -> Fraction
The exact probability that a run satisfies the LTL formula (PRISM's P operator), a Fraction.
With no moves (the default) the reachable graph is a DTMC (weight normalises each state's enabled
actions into a distribution; a negative weight raises), and the answer is the probability a RANDOM run
satisfies formula, for the fragment with a direct characterisation — a temporal operator on a STATE
predicate p:
F p→ the reachability probability ofp;X p(Next) → the probabilitypholds at the NEXT step (a one-step push of the initial distribution; an absorbing initial state self-loops, so it contributes[p(init)]);G p→1 - P(F ¬p);GF p(Always(Eventually p)) → the probability of absorption into a bottom SCC that CONTAINS apstate (a run visits every state of its absorbing BSCC infinitely often);FG p(Eventually(Always p)) → the probability of absorption into a bottom SCC ENTIRELY insidep.a U b(Until, both STATE predicates) → the CONSTRAINED (until) reachability: the probability of reaching abstate without first passing through a¬astate — exactlyreach_probabilitywithavoid=¬a, no automaton needed.a R b(Release, both STATE predicates) → the until dual1 - P(¬a U ¬b):bholds until (and including) the stepafirst holds, or forever ifanever does.G pis the special casefalse R p.a W b(WeakUntil, both STATE predicates) → the WEAK until(a U b) ∨ G a=b R (a∨b)=1 - P(reach ¬a∧¬b avoiding b).G pis also the special casep W false.
With moves (as in reach_probability_mdp) the model is an MDP and the answer is the OPTIMAL
probability over all schedulers, optimize="max" or "min", for the same F / X / G / GF / FG / U / R /
W fragment:
F p→ max / min reachability ofp;X p→ the max / min one-step probability ofp, over the initial state's moves;G p→1 - P_min(F ¬p)(max) /1 - P_max(F ¬p)(min);GF p(Büchi) → the max probability equals the max reachability to the states in a MAXIMAL END COMPONENT that contains apstate (reach such a component and cycle throughpforever); the min is the dual1 - P_max(FG ¬p);FG p(co-Büchi) → the max probability equals the max reachability to the region the scheduler can stay insidepforever (_stay_within); the min is the dual1 - P_max(GF ¬p).a U b→ the max / min constrained reachability ofbavoiding¬a(reach_probability_mdpwithavoid=¬a).a R b→1 - P_min(¬a U ¬b)(max) /1 - P_max(¬a U ¬b)(min), the until dual.a W b→1 - P_min(¬b U (¬a∧¬b))(max) /1 - P_max(¬b U (¬a∧¬b))(min), viab R (a∨b).
All exact, reusing the reachability solve, the BSCC / MEC / stay-within decompositions and (for the MDP)
policy iteration; NO linear programming (that is only for the long-run AVERAGE reward, see
PROBABILISTIC_NOTES.md). Any formula outside this fragment raises NotImplementedError — general
probabilistic LTL needs a DETERMINISTIC automaton for the formula (a Safra/Rabin construction), not yet
built. Raises ValueError if the exploration truncates.
Source code in src/musil/probabilistic.py
675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 | |
reach_probability_mdp ¶
reach_probability_mdp(
model: Model[S],
target: Callable[[S], bool],
*,
moves: Moves[S],
weight: Callable[[str, S], Fraction | int]
| None = None,
optimize: Literal["max", "min"] = "max",
avoid: Callable[[S], bool] | None = None,
steps: int | None = None,
max_states: int = 1000000,
) -> Fraction
The exact MAXIMAL (or MINIMAL) probability of eventually reaching target over all schedulers of
the MDP.
moves(state, enabled_actions) partitions the enabled actions into the moves a scheduler chooses
between at state; the actions within a move form one distribution over successors (their weight
normalised, default uniform). Grouping every enabled action into a single move recovers
reach_probability (a DTMC has no choice).
Solved EXACTLY by policy iteration: evaluate the current policy as a DTMC (an exact rational solve),
then switch each state to a strictly better move under those values, until the policy is stable — a
fractions.Fraction. For optimize="min" the states from which a scheduler can avoid the target
forever are found first (_s0_min) and pinned to 0, which is what stops min policy iteration from
stalling on a value-preserving self-loop (see PROBABILISTIC_NOTES.md).
avoid gives the CONSTRAINED (until) optimal probability P_opt(¬avoid U target): an avoid state
that is not a target becomes an absorbing failure (0), so a run that touches it before the target does
not count. The optimisation is still over all schedulers — e.g. optimize="max" is the best a scheduler
can do while steering clear of avoid until the target.
With steps=k the answer is instead the optimal probability of reaching target WITHIN k
transitions — an exact finite backward induction, so _s0_min is not needed (a bounded horizon cannot
stall). Raises ValueError if the exploration truncates at max_states or if steps is
negative.
Source code in src/musil/probabilistic.py
expected_reward_mdp ¶
expected_reward_mdp(
model: Model[S],
target: Callable[[S], bool],
*,
moves: Moves[S],
weight: Callable[[str, S], Fraction | int]
| None = None,
cost: Callable[[str, S], Fraction | int] | None = None,
optimize: str = "min",
steps: int | None = None,
max_states: int = 1000000,
) -> Fraction
The exact MINIMAL (optimize="min", default) or MAXIMAL (optimize="max") expected accumulated
cost to first reach target over all schedulers of the MDP — the stochastic shortest / longest path.
With steps=k the answer is instead the min/max expected cost accumulated until the target is reached OR
k steps elapse — a finite backward induction over the moves each step, always finite, so it needs no
reachability guard (the "expected cost in the next k steps under the best/worst scheduler").
With the default unit cost this is the min/max expected number of STEPS. moves/weight describe
the MDP exactly as in reach_probability_mdp; cost must be strictly POSITIVE off the target (the
default unit cost is), so that a scheduler which fails to reach the target a.s. has infinite cost — the
assumption both directions rest on. This is now ENFORCED: a zero- or negative-cost step off the target
raises ValueError (it would otherwise return a wrong finite value; the zero/negative-cost SSP is a
documented deferral). steps=k has NO such requirement (a bounded horizon is a well-defined finite sum
for any cost). Each policy is evaluated by an exact rational solve of E(s) = cost(s) + sum_s' P(s,s')
E(s').
MIN is the stochastic shortest path. A proper policy must EXIST for the min to be finite: the
max-reachability-optimal policy reaches the target almost surely from every state whose max reachability is
1 (a convex combination of values <= 1 equal to 1 forces every successor to 1), so it is proper there
and seeds the iteration, which then minimises over the moves whose successors are all proper.
MAX is the stochastic LONGEST path, finite only when EVERY policy is proper — otherwise a scheduler can loop away from the target forever and the max is infinite. So the guard is MIN reachability 1 from the initial state (no scheduler avoids the target); it implies min reachability 1 from every reachable state, hence every policy is proper and the max over the finite policy space is finite. Any policy is then a valid proper seed, and maximising policy iteration (each switch strictly RAISES a bounded, monotone value) converges to the optimum (Bertsekas & Tsitsiklis SSP, the all-proper case).
Raises ValueError if the required reachability guard fails from the initial state (the expectation is
then infinite: min — no scheduler reaches a.s.; max — some scheduler avoids the target with positive
probability), if optimize is not "min"/"max", or if the exploration truncates.
Source code in src/musil/probabilistic.py
976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 | |
musil.sim ¶
Deterministic simulation: run real, event-driven node code under a controlled world.
The expensive distributed bugs hide in timing -- message loss, reordering, a timeout racing a reply, a partition healing at the wrong moment. This runs your actual node logic against a virtual network and clock where all of that is controlled and seeded, so every run is reproducible from its seed (a found bug replays exactly). It's the FoundationDB/TigerBeetle "deterministic simulation testing" technique as a pure-Python library -- bug finding, not proof.
Model: nodes are event-driven actors (on_start / on_message / on_timer) that act through a
Context (send a message, set a timer, read the virtual clock, draw seeded randomness). The
Simulator owns a discrete-event queue ordered by (virtual time, sequence); the NetworkModel
decides per-message loss / duplication / latency, so reordering and delay emerge from latency spread.
A FaultSchedule layers on sustained faults -- network partitions and node crashes that hold for a
window then heal -- so simulate can check liveness: does the system converge once they lift?
All randomness comes from one seeded RNG. musil.refine + invariants are the oracle (next slice:
simulate).
Envelope
dataclass
¶
A message in flight: a unique sequence number, source, destination, and payload.
Source code in src/musil/sim.py
NetworkModel
dataclass
¶
How the virtual network treats each message. Defaults are a reliable, in-order channel; set
loss/duplicate (probabilities in [0, 1]) and a min_latency/max_latency spread
(virtual-time units) to inject drops, duplicates, and reordering. All draws use the sim's seed.
mutate is a Byzantine fault hook: mutate(src, dst, payload) -> object | None. The
returned value replaces the payload before delivery; returning None drops the message.
Applied after loss/duplicate decisions, so it targets messages that survive the network model.
Models wire-level corruption, wrong-answer injection, or selective drops (Castro & Liskov, OSDI
1999).
Source code in src/musil/sim.py
Partition
dataclass
¶
A sustained network fault: every directed link in links ((src, dst) pairs) drops ALL
traffic while active -- the window [start, end) in virtual time -- then heals. Unlike
NetworkModel.loss (independent per message, which a retrying sender papers over), a partition
cuts the link wholesale, so the system can only recover once it lifts. This is what makes a real
liveness test: does it converge after the partition heals?
Source code in src/musil/sim.py
Crash
dataclass
¶
A sustained process fault: node is down over [start, end) -- inbound messages are
dropped, its timers don't fire, it runs no handlers -- then restarts. lose_state=True is a cold
restart (a fresh node instance that re-runs on_start); the default is a warm resume that keeps
the instance's state (it simply missed everything while down).
Source code in src/musil/sim.py
FaultSchedule
dataclass
¶
A fixed set of sustained faults for one run. heal_time() is when the last fault lifts (the
world is clean again) -- the point after which a live system must converge to its goal. Build one
explicitly, or per-seed via a Callable[[Random], FaultSchedule] so randomized schedules stay
seed-reproducible.
Source code in src/musil/sim.py
RunResult
dataclass
¶
Outcome of a run. reason is "quiescent" (queue drained), "until" (goal predicate
met), or "max-steps" (step cap hit).
Source code in src/musil/sim.py
Context ¶
A node's handle on the world, passed to every handler. Lets the node send messages, arm/cancel
timers, read the virtual clock (now), and draw seeded randomness -- never use real time or the
global random module in a node, or runs stop being reproducible.
Source code in src/musil/sim.py
set_timer ¶
Arm (or re-arm) a timer; it fires delay virtual-time units from now via on_timer.
Re-arming a live timer of the same name replaces it.
Source code in src/musil/sim.py
Node ¶
Bases: Protocol
What the simulator needs from a node: three event handlers. Subclass BaseNode and override
only the ones you need.
Source code in src/musil/sim.py
BaseNode ¶
A node with no-op handlers; override what you need. Keep all mutable state on the instance.
Source code in src/musil/sim.py
AdversarialNode ¶
Bases: BaseNode
A simulation node that injects adversarial behavior via a prioritized behavior list.
Models an external component (a K8s node, an AWS service, a Byzantine peer) that sometimes
misbehaves. Each behavior is a (guard, response) pair:
guard(src, payload) -> bool— returns True when this behavior should fire.response(ctx, src, payload) -> None— the adversarial action: send wrong data, send nothing, send duplicate responses, violate the protocol.
On each on_message, behaviors are tried in order; the first matching guard fires and
no further behaviors are tried. If no guard matches, the message is silently dropped —
the default adversarial posture (an external service that ignores requests).
All randomness in behavior callbacks must go through ctx.random() / ctx.randint()
so runs stay reproducible across seeds. This is the simulation counterpart of
EnvironmentSpec: same contract theory, different execution model.
Source code in src/musil/sim.py
Simulator ¶
Runs a fixed set of named nodes under a virtual clock and network. Construct with the node
map, a seed, and an optional NetworkModel; call run. Determinism: identical
(nodes, seed, network) always produce the identical run.
Source code in src/musil/sim.py
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 | |
nodes
property
¶
The live node map -- the authoritative instances, which a cold restart swaps. The oracle snapshots through this so it always reads post-restart state.
random ¶
randint ¶
inject ¶
Send a message (from a node's ctx.send, or externally to kick the system). Subject to
the network model: it may be dropped, duplicated, or delayed.
Source code in src/musil/sim.py
schedule_timer ¶
Arm a timer for node that fires delay units from now (re-arming replaces it).
Source code in src/musil/sim.py
run ¶
run(
*,
max_steps: int = 10000,
until: Callable[[Simulator], bool] | None = None,
on_step: Callable[[Simulator], None] | None = None,
after_start: Callable[[Simulator], None] | None = None,
) -> RunResult
Drive the system to quiescence (queue empty), until until(sim) is true, or until
max_steps events have fired. after_start(sim) runs once after every node's
on_start (the initial world); on_step(sim) runs after each fired event -- the hooks
the oracle uses to snapshot and check the world.
Source code in src/musil/sim.py
SimFailure
dataclass
¶
A reproducible failure from simulate. kind is "invariant", "refinement",
"goal" (settled-but-goal-false with no faults), or "liveness" (under a FaultSchedule,
the system did not converge to the goal after the faults healed). detail names the broken
invariant / refinement violation / goal. world is the offending snapshot and history the
snapshots leading to it (a trace). Re-run with seeds=[seed] to reproduce exactly.
Source code in src/musil/sim.py
simulate ¶
simulate(
factory: Callable[[], Mapping[str, Node]],
*,
seeds: Iterable[int],
snapshot: Callable[[Mapping[str, Node]], W],
network: NetworkModel | None = None,
faults: FaultSchedule
| Callable[[Random], FaultSchedule]
| None = None,
invariants: Mapping[str, Callable[[W], bool]]
| None = None,
model: Model[S] | None = None,
abstraction: Callable[[W], S] | None = None,
goal: Callable[[W], bool] | None = None,
goal_name: str = "goal",
converge_within: int | None = None,
max_steps: int = 10000,
require_init: bool = True,
) -> SimReport[W]
Deterministic simulation testing of the real nodes. Runs the system once per seed under
network (independent per-message faults) and an optional faults schedule (sustained,
heal-able partitions / crashes -- a FaultSchedule or a per-seed Random -> FaultSchedule).
After every step it checks each invariant and (if a model + abstraction are given) that the
run refines the model -- safety holds during the chaos too. If a goal is given, the settled
final world must satisfy it: with a non-trivial faults schedule this is the liveness check
(did the system converge once the faults healed? -> kind="liveness"); with no faults it is the
plain convergence check (kind="goal"). converge_within (steps after the schedule's
heal_time) catches livelock early. Returns at the FIRST failing seed -- a reproducible repro
(report.failure.seed). factory builds a fresh node map per run (also reused to cold-restart
a crashed node); snapshot maps the live nodes to an immutable world value used by the oracle.
Source code in src/musil/sim.py
Systems & modelling¶
Open-system checking against adversarial environments, composition, and the model-building kits.
musil.env ¶
Open-system verification: check a system against adversarial external environments.
Real distributed systems do not operate in isolation. A service runs on Linux, inside K8s, talking
to AWS -- components that can crash, evict, throttle, or return wrong answers at any moment. musil's
closed-system check assumes the entire state space is under the model's control. check_open
lifts that restriction: each external component is an EnvironmentSpec -- a contract consisting of
the non-deterministic behaviors it can exhibit, the guarantees it commits to, and the
assumptions those guarantees rest on (following seL4's two-layer assurance model: Klein et al.,
SOSP 2009).
check_open composes by merging: env behaviors become additional actions (the BFS explores
every thing the environment can do), env guarantees become additional invariants. This is
Interface Automata composition (de Alfaro & Henzinger, ESEC/FSE 2001) -- the environment acts
adversarially within its contract; the system must handle all of it.
Assumptions are first-class: they are printed in the result, never silently swallowed. A guarantee that rests on an unverified assumption is weaker than one that rests on a verified proof -- the caller knows exactly what the verification is worth.
Assumption
dataclass
¶
A named proof obligation taken on faith or verified elsewhere.
status tracks where the assumption stands:
- "axiom" — taken as a foundation; not expected to be proved (e.g., hardware correctness)
- "verified" — machine-checked or formally proved (e.g., seL4 kernel proof)
- "unverified" — stated but not yet validated (the default; should be addressed)
source cites where the assumption comes from (paper, spec, URL).
predicate is an optional machine-checkable version of the assumption; None for
assumptions that cannot be expressed as a state predicate (e.g., "network eventually delivers").
Source code in src/musil/env.py
EnvironmentSpec
dataclass
¶
A contract for one external component: what it can do, what it promises, and what it assumes.
behaviors — the non-deterministic actions the environment can take. Each is an Action[S]
that fires from the same global state the system uses. The BFS in check_open explores
every possible environment action from every state, so the system is checked against the worst
possible environment (within the contract). Model each distinct failure mode -- crash, evict,
wrong-answer, timeout -- as a separate behavior.
guarantees — invariants the environment commits to hold in every reachable state. If the
environment breaks one, check_open reports it as "<env.name>:<guarantee_name>".
assumptions — named Assumption objects the guarantees rest on. Unverified assumptions
are surfaced in OpenResult.unverified_assumptions; they are never silently dropped.
Source code in src/musil/env.py
OpenResult
dataclass
¶
The outcome of check_open. Wraps the underlying Result and surfaces every
Assumption that is not yet "verified" -- these are the residual proof obligations
the caller must discharge for the verification to be unconditional.
bool(open_result) delegates to result.ok so it works in assertions.
Source code in src/musil/env.py
OpenLivenessResult
dataclass
¶
The outcome of check_liveness_open: the underlying LivenessResult plus every Assumption
from the environments that is not yet "verified" (the residual proof obligations). bool and
ok delegate to the liveness verdict, so it works in assertions.
Source code in src/musil/env.py
check_open ¶
check_open(
system: Model[S],
*envs: EnvironmentSpec[S],
max_states: int = 1000000,
) -> OpenResult[S]
Check system against adversarial external environments.
Composes the system and every environment by merging:
- all env.behaviors into the system's actions (the BFS explores every env action)
- all env.guarantees into the system's invariants (qualified as "<env.name>:<k>")
Then calls the standard check on the composed model.
check_open(system) with no environments is identical to check(system).
Unverified assumptions from all environments are collected and returned in
OpenResult.unverified_assumptions -- they are the residual proof obligations.
Source code in src/musil/env.py
check_liveness_open ¶
check_liveness_open(
system: Model[S],
*envs: EnvironmentSpec[S],
goal: Callable[[S], bool],
goal_name: str = "goal",
everywhere: bool = False,
leadsto_from: Callable[[S], bool] | None = None,
fair: Iterable[str] | None = None,
fair_strong: Iterable[str] = (),
max_states: int = 1000000,
) -> OpenLivenessResult[S]
Check a LIVENESS property of system under adversarial environments — the liveness counterpart
of check_open, so the same EnvironmentSpec faults are not written twice (once as env behaviors
for the safety check_open, once as hand-rolled unfair actions for check_liveness).
Composition: every env.behaviors action is merged into the model (the BFS explores every env
action), and by default fair is the SYSTEM's own action names only — so environment behaviors are
UNFAIR, i.e. an adversarial environment is never assumed to eventually 'help' reach the goal. Pass
fair explicitly to override (e.g. add an env behavior whose EnvironmentSpec guarantees it is
fairly scheduled, like "the network eventually delivers"); fair=() is strict no-fairness.
goal / goal_name / everywhere / leadsto_from / fair_strong pass straight through to
check_liveness (see there for <>P vs []<>P vs the response form). Environment SAFETY
guarantees are not re-checked here — they are safety, verified by check_open on the same envs; this
form verifies the liveness goal under the env's faults. Unverified assumptions from all environments are
surfaced in OpenLivenessResult.unverified_assumptions.
check_liveness_open(system, goal=...) with no environments matches check_liveness(system, goal=...)
with fair defaulting to the system's own moves.
Source code in src/musil/env.py
musil.compose ¶
Parallel composition of component models (I/O-automata style).
Specify each component independently as a Model (states + named actions), then compose them into
one Model whose state is the tuple of component states and whose actions are the interleaving of all
components' actions, each lifted to act on its own slice. This is the "specify per component, compose"
discipline from the methodology note (docs/specs/formal-modeling-distributed-systems.md): the joint
behaviour is every interleaving of the parts, which is exactly where concurrency bugs live.
Component actions are name-qualified ("<component>:<action>") and component invariants are lifted
(checked against that component's slice). Pass extra invariants to compose for joint properties
that span components. The composite is terminal only when every component is terminal.
Composite
dataclass
¶
A joint state: one component state per name, kept sorted by name so it hashes deterministically.
Read a component's slice with state["name"].
Source code in src/musil/compose.py
compose ¶
compose(
components: Mapping[str, Model[Any]],
*,
invariants: Mapping[str, Invariant[Composite]]
| None = None,
) -> Model[Composite]
Interleaving product of components (name -> Model). The result's reachable states are every
interleaving of the parts; component invariants are lifted ("<name>:<inv>") and invariants
adds joint properties over the whole composite.
Source code in src/musil/compose.py
musil.channels ¶
Generic message-channel modeling kit -- the "model the network explicitly" principle as a reusable building block (methodology doc section 3).
A channel's in-flight messages are held as a frozenset somewhere in your model's state. This kit
builds the channel's actions over that state: deliver a message (apply it to the receiver), and --
depending on the channel's reliability -- drop it (loss) or keep it after delivery (duplication).
Because the in-flight set is unordered and deliver may fire for ANY in-flight message, reordering
is modelled for free; lossy adds message loss; duplicating allows redelivery. (A set dedups a
re-send of the same message -- which matches an idempotent re-push. FIFO/ordered channels would need
a sequence instead; the realistic network is unordered, which is what this models.)
Domain-free: messages are any hashable values the caller supplies. Use send inside a sender's
action to inject a message, and channel_actions to add the channel's own steps to the model.
send ¶
send(
get: Callable[[S], frozenset[Message]],
put: Callable[[S, frozenset[Message]], S],
) -> Callable[[S, Message], S]
Return a helper send(state, msg) that injects msg into the channel's in-flight set
(idempotent: re-sending an in-flight message is a no-op, like an idempotent re-push).
Source code in src/musil/channels.py
fifo_send ¶
fifo_send(
get: Callable[[S], tuple[Message, ...]],
put: Callable[[S, tuple[Message, ...]], S],
) -> Callable[[S, Message], S]
Return a helper send(state, msg) that appends msg to the tail of an ORDERED channel
(a tuple, not a set). Unlike the unordered send, this is not idempotent — each call enqueues
another copy — so the caller must bound the queue (e.g. only send when it's empty, or guard on a
capacity) to keep the model finite.
Source code in src/musil/channels.py
fifo_channel_actions ¶
fifo_channel_actions(
*,
get: Callable[[S], tuple[Message, ...]],
put: Callable[[S, tuple[Message, ...]], S],
deliver: Callable[[S, Message], S],
lossy: bool = False,
name: str = "ch",
) -> list[Action[S]]
An ordered (FIFO) channel's steps over the caller's state, the order-preserving counterpart
to channel_actions. The in-flight messages are an ordered tuple (get/put read/write
it); only the head is deliverable, so messages arrive in send order — no reordering. lossy
adds a head-drop (loss). deliver(state, msg) applies the delivered head to the receiver; the
head is then removed. Use for sequence-number protocols (alternating-bit, sliding-window) and any
link whose correctness assumes order — where the unordered channel_actions would wrongly
explore reorderings. (Bound the queue from the sender side; see fifo_send.)
Source code in src/musil/channels.py
channel_actions ¶
channel_actions(
*,
messages: Iterable[Message],
get: Callable[[S], frozenset[Message]],
put: Callable[[S, frozenset[Message]], S],
deliver: Callable[[S, Message], S],
lossy: bool = False,
duplicating: bool = False,
name: str = "ch",
) -> list[Action[S]]
The channel's steps over the caller's state. get/put read/write the in-flight set;
deliver(state, msg) applies a delivered message to the receiver. messages is the (bounded)
universe of possible messages. lossy adds drop steps; duplicating lets a message be
delivered more than once. Delivery order is unconstrained (reordering).
Source code in src/musil/channels.py
musil.faults ¶
Fault-injection action factories for the EXPLICIT-STATE path (check / explore / check_open).
sim has a rich fault vocabulary (Crash, Partition, FaultSchedule), but it is reachable only
from the discrete-event Simulator. Models written for the explicit-state checker hand-roll the same
crash / revive / partition / heal edges over and over. This kit builds those edges over a caller-declared
projection of the state — the same lens style as channels (get / put) — so a distributed model
gets its standard faults from one call instead of a per-node copy-paste: crash_actions for node
liveness, partition_actions for network reachability.
Domain-free: nodes are any hashable ids, and the caller says how liveness is stored via get_up /
set_up. Splice the result into the model's actions alongside the protocol's own steps.
crash_actions ¶
crash_actions(
nodes: Iterable[Hashable],
*,
get_up: Callable[[S, Hashable], bool],
set_up: Callable[[S, Hashable, bool], S],
budget: int | None = None,
revive: bool = False,
name: str = "fault",
) -> list[Action[S]]
Crash (and optionally revive) actions over a caller-declared node-liveness projection.
get_up(state, node) -> bool reads whether node is up; set_up(state, node, up) -> S returns
the state with node's liveness set (a lens the caller owns — set_up then get_up must
round-trip). One {name}:crash:{node} action per node fires when the node is up and fewer than
budget nodes are already DOWN — so budget bounds the number of SIMULTANEOUS failures (None =
unbounded; with no revive a crash is permanent, so it also bounds the total). revive=True adds a
{name}:revive:{node} action that brings a down node back up (for heal-able faults / VOPR-style
liveness: after the faults clear, the system must reconverge).
Returns a list of Action to splice into the model's actions. Keep the fault actions UNFAIR (do
not tag them fair=, and do not name them in fair / fair_strong) so a liveness proof cannot
lean on a fault being scheduled.
Source code in src/musil/faults.py
partition_actions ¶
partition_actions(
splits: Iterable[Hashable],
*,
get_reach: Callable[[S], Hashable],
set_reach: Callable[[S, Hashable], S],
healed: Hashable,
name: str = "fault",
) -> list[Action[S]]
Partition (and heal) actions over a caller-declared reachability field.
The model stores a reachability CONFIGURATION somewhere in its state — whatever shape the caller uses (a
per-node reachable-set map, a partition of the nodes into groups, a split label...). get_reach(state)
reads it; set_reach(state, reach) -> S returns the state with it set (a lens the caller owns).
healed is the full-reachability configuration (typically the model's initial one; it must compare
equal via == to the healed state's field).
For each configuration in splits a {name}:partition:{i} action installs it — enabled only while
currently HEALED, so partitions do not stack — and a single {name}:heal action restores healed
from any partitioned configuration. This is the heal-able network-partition fault: the system runs
partitioned, then the partition clears and it must reconverge. Keep these actions UNFAIR (do not tag them
or name them in fair / fair_strong), like crash_actions, so a liveness proof cannot lean on a
partition healing on its own.
Source code in src/musil/faults.py
musil.fsm ¶
Build a model straight from a transition table — {from_state: {to_states}} — instead of
hand-writing one Action per edge. This is the zero-drift bridge: point it at the very table your
code enforces (e.g. a state machine's allowed-transitions map) and the model can never disagree
with the code, because it is the code's table. No separate spec file to keep in sync.
Generic over the state type: you supply get (read the status out of a state) and with_status
(return a new state with the status replaced), so the table can drive any state shape — typically a
frozen dataclass with a status field plus whatever other variables your invariants need.
transition_actions ¶
transition_actions(
table: Table,
*,
get: Callable[[S], str],
with_status: Callable[[S, str], S],
effect: Callable[[S, str, str], S] | None = None,
also: Callable[[S], bool] | None = None,
name: Callable[[str, str], str] = lambda src, dst: (
f"{src}->{dst}"
),
) -> list[Action[S]]
One Action per declared src -> dst edge. get reads the current status from a state;
with_status returns a new state with the status set to dst (states are immutable).
effect(state, src, dst) runs AFTER the status change and returns the state with any side effects on
OTHER fields applied (moving a balance, stamping a timestamp) — so a transition is not limited to
swapping the status field. also(state) is an extra guard ANDed with "currently in src", for a
cross-cutting precondition the table itself does not encode (e.g. only post while the period is open).
Source code in src/musil/fsm.py
replicated_transition_actions ¶
replicated_transition_actions(
table: Table,
instances: int | Iterable[Hashable],
*,
get: Callable[[S, Hashable], str],
set_status: Callable[[S, Hashable, str], S],
effect: Callable[[S, Hashable, str, str], S]
| None = None,
also: Callable[[S, Hashable], bool] | None = None,
name: Callable[
[Hashable, str, str], str
] = lambda key, src, dst: f"{key}:{src}->{dst}",
) -> list[Action[S]]
N copies of ONE transition table — one state machine per instance — over a FLAT state, for a
system of interchangeable entities (entries, replicas, jobs) that all obey the same lifecycle.
instances is either an int N (keys 0..N-1) or an explicit iterable of keys. Unlike
compose (which forces a Composite tuple state), the state stays a flat dataclass, so cross-
instance invariants (a + b == 0, "at most one entry posting") remain expressible. The projections are
per-instance: get(state, key) reads instance key's status; set_status(state, key, dst) sets
it. effect(state, key, src, dst) applies per-instance side effects after the status change, and
also(state, key) is a per-instance extra guard — exactly as in transition_actions but indexed by
the instance.
Source code in src/musil/fsm.py
status_field_actions ¶
Convenience for the common case: states are frozen dataclasses whose status lives in a single
field (default status). Builds actions that read/replace that field via dataclasses.replace.
Source code in src/musil/fsm.py
multi_status_field_actions ¶
For a dataclass with SEVERAL status fields, each driven by its own table (e.g. a control-plane
World whose node/service/cert fields each follow a different ALLOWED[...] map):
build every field's edge-actions at once. tables maps a field name to its table; action names
are namespaced "<field>:<src>-><dst>" so they stay distinct across fields. musil fires every
enabled action from every state, so the interleaved product of the per-field machines — every way
the resources can advance concurrently — is explored for free.
Source code in src/musil/fsm.py
protocol_actions ¶
protocol_actions(
table: Protocol[T],
*,
get: Callable[[S], T],
with_state: Callable[[S, T], S],
name: Callable[
[T, str], str
] = lambda state, operation: f"{operation} in {state}",
) -> list[Action[S]]
One Action per (state, operation) that moves, from a table of legal operations.
The zero-drift argument, one level up from :func:transition_actions: a protocol table is
what a guard needs anyway — "is this call legal where I am, and where does it leave me" —
so pointing the checker at the same table means the sequence being verified is the sequence
being enforced, not a second description of it.
Operations mapped to None produce no action. They are legal and they stay put, so they
add nothing to the reachable state space; a guard still has to know about them, which is why
they belong in the table rather than being left out of it.
get reads the protocol state out of your state; with_state returns a new one with it
replaced. For a model whose state is the protocol state, those are lambda s: s and
lambda _s, t: t.
Source code in src/musil/fsm.py
protocol_operations ¶
Every operation legal in state, moving or not — what a guard checks against.
declared_states ¶
terminal_states ¶
States with no outgoing transitions — absorbing sinks (a key mapped to an empty set, or a
target that's never a source). Use to build a model's terminal predicate so a legitimate
resting/sink state isn't reported as a deadlock.
Source code in src/musil/fsm.py
assert_covers_table ¶
assert_covers_table(
model: Model[S],
table: Table,
*,
get: Callable[[S], str],
max_states: int = 1000000,
message: str | None = None,
) -> None
Assert the model CONFORMS to the transition table — the zero-drift claim checked by musil instead
of a hand-rolled action-name test.
Over the whole reachable space, every step that CHANGES the status (read by get) must go from src
to some dst in table[src]: the model never makes a transition the table forbids. Actions built by
transition_actions / replicated_transition_actions cannot drift ABOVE the table by construction,
so this catches hand-written actions, a stale table, or an effect that produces an undeclared status
change. Raises AssertionError listing every undeclared (src -> dst) status transition found.
This checks CONFORMANCE (no forbidden transition), not completeness — a declared edge may be legitimately
unreachable or held off by an extra guard, so "every table edge is exercised" is left to the caller (who
knows which edges must be reachable); declared_states / terminal_states help build that check.
get is the same status projection you pass to transition_actions.
Source code in src/musil/fsm.py
musil.clock ¶
A bounded discrete clock for the explicit-state layer -- timeouts without an unbounded space.
sim has a virtual clock; Model/Action has none, so every timeout model (a wait with a
deadline, a retry ladder that gives up) hand-rolls the same two things: a tick action, and a bound to
stop it running forever. The bound is the part that is easy to get wrong, and getting it wrong is
quiet. An unbounded clock does not fail -- check hits max_states and returns
Result(ok=True, truncated=True), which reads as success to if result: and prints as
OK -- 1000000 states, no violations (TRUNCATED at cap). Nothing was proved and it looks like
something was.
bounded_clock makes the bound a declared number instead of an open-coded guard, and makes the
question it raises answerable: was the horizon binding? A green result under a binding horizon
means "no violation within horizon ticks", which is a weaker claim than "no violation" and should
not be quoted as the stronger one.
Domain-free, like the rest of the kit: the clock lives in a field of the caller's own state, read by
get and written by put.
clock = bounded_clock(get=lambda s: s.now, put=lambda s, t: replace(s, now=t), horizon=8)
model = Model(
init=World(),
actions=[*my_actions, clock.action],
invariants={...},
terminal=clock.at_horizon, # see below -- running out of time is a legitimate sink
)
graph = explore(model)
assert not clock.binding(graph) # or say so when reporting the result
terminal matters: at the horizon the tick is disabled, so a state whose only remaining move was
the tick has no enabled action and check calls it a deadlock. That is a false alarm -- the model
did not deadlock, time ran out -- so mark those states terminal (terminal=clock.at_horizon, or
lambda s: clock.at_horizon(s) or mine(s)). Forgetting it fails loudly, with a trace ending at the
horizon, which is the failure mode to prefer over a silent one.
BoundedClock
dataclass
¶
A clock that advances one tick at a time and stops at horizon. Built by bounded_clock.
action is the tick, to be added to the model's actions. now reads the clock out of a
state, at_horizon says whether a state sits at the bound, and binding answers the
question the bound raises.
Source code in src/musil/clock.py
horizon_states ¶
The reachable states sitting at the horizon -- where exploration stopped because the clock was not allowed to advance, not because the system had nowhere left to go.
Source code in src/musil/clock.py
binding ¶
Did the horizon cut the exploration? False means the model finished on its own with time
to spare, so the bound cost nothing and a green result is a result about the whole model.
True means the bound was reached, and a green result only says "no violation within
horizon ticks" -- raise the horizon until this goes False, or quote the weaker claim.
Source code in src/musil/clock.py
bounded_clock ¶
bounded_clock(
*,
get: Callable[[S], int],
put: Callable[[S, int], S],
horizon: int,
name: str = "clock",
) -> BoundedClock[S]
A tick action over the caller's clock field, bounded at horizon.
get(state) reads the current tick and put(state, t) returns a state with the clock at
t. The action is named f"{name}:tick" and is enabled exactly while get(state) <
horizon, so the clock contributes at most horizon + 1 values to the state space -- linear
in the horizon, and finite by construction rather than by hitting max_states.
horizon must be non-negative. horizon=0 is a clock that never ticks, which is a valid
(if pointless) model rather than an error -- the value is then always the initial one.
Deadlines are ordinary guards over get: a timeout fires when get(s) >= armed_at + delay,
a retry is enabled while get(s) < give_up_at. This helper does not model those, it only
supplies the time they are read from and the bound that keeps them finite.
Source code in src/musil/clock.py
musil.reconciler ¶
The controller / reconciler shape as a builder — desired↔actual convergence under faults.
A desired field set by the environment, an actual field the controller drives toward it, a fair
reconcile step, unfair faults (loss, crash, concurrent reconcilers), and the goal []<>converged: this is
the single most common shape in modern infrastructure (operators, sync engines, cache maintainers), and it
is the one musil had no builder for (it has channels for messaging and fsm for state tables).
reconciler produces the two pieces every such model writes by hand — the converged predicate and a
fair reconcile Action — and composes with the rest of the kit: attach faults.crash_actions /
channels as UNFAIR actions or env environments, and check []<>converged with
check_liveness(everywhere=True) (or check_liveness_open against an adversarial environment). The
reconcile action is tagged fair="weak" — the "ours" side of the fair-ours / unfair-faults discipline: a
liveness proof may assume the controller keeps reconciling, but not that a fault heals on its own.
reconciler ¶
reconciler(
*,
get_desired: Callable[[S], V],
get_actual: Callable[[S], V],
set_actual: Callable[[S, V], S],
name: str = "reconcile",
) -> tuple[Callable[[S], bool], Action[S]]
The canonical desired↔actual reconciler. get_desired / get_actual read the two fields (any
hashable values); set_actual(state, value) returns the state with actual set. Returns
(converged, reconcile):
converged(state)isget_actual(state) == get_desired(state)— the[]<>convergedgoal, typically fed tocheck_liveness(model, goal=converged, everywhere=True).reconcileis a fairAction(taggedfair="weak") that, while not converged, setsactualtodesiredin one step.
Splice reconcile into the model's actions next to the environment's desired-changing steps and your
UNFAIR faults (crash_actions, channel loss, extra reconcilers). For a controller that converges over
several steps rather than one, build your own reconcile Action and use only converged from here.
Source code in src/musil/reconciler.py
Reductions & proof¶
State-space reductions with their soundness gates, and proof by induction beyond the explored scope.
musil.por ¶
Partial-order reduction (POR) — explore only an ample set of actions per state, plus the soundness gate that makes any ample choice safe to trust.
musil explores every interleaving of concurrent actions, which is what finds races and also what blows the
state space up (N independent actions give N! orderings, most redundant). POR fires only a sufficient
subset — an ample set — at each state. An unsound ample set silently drops reachable states and the
violations only they reach, which is strictly worse than being slow, so POR ships with por_sound: the
gate that validates an ample function against the full exploration before it is trusted (the same
discipline as symmetry_reduction_sound / footprint_sound). See REDUCTION_NOTES.md.
This layer provides the MECHANISM (explore_por takes a caller-supplied ample) and the GATE
(por_sound); the automatic ample-set computation from the independence relation lands on top, validated
by the gate. independent is the concrete per-state independence test the computation rests on.
independent ¶
Whether actions a and b are INDEPENDENT at state: both enabled there, each still enabled
after the other fires (neither disables the other), and they COMMUTE
(apply(a, apply(b, s)) == apply(b, apply(a, s))). musil can test this concretely per state because
enabled/apply are pure functions — an advantage over tools that need a static independence
relation. (Independence is defined only for co-enabled actions; returns False otherwise.)
Source code in src/musil/por.py
explore_por ¶
explore_por(
model: Model[S],
*,
ample: Ample[S],
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
) -> Graph[S]
Build the reachable graph firing only ample(state, enabled_actions) at each state instead of
every enabled action. ample MUST return a subset of the enabled actions. SOUNDNESS is the caller's
obligation — validate the ample with por_sound before trusting the reduced graph. With
ample = lambda state, enabled: enabled this is exactly explore.
Source code in src/musil/por.py
por_sound ¶
Validate a POR ample for model on a (bounded) instance — the gate that should pass before
explore_por(..., ample=...) (and any check built on it) is trusted.
It explores the model FULL and REDUCED and confirms two things: (1) the reduced reachable set is a SUBSET of the full one (POR must not invent states); and (2) the SAME set of invariants is violable in both — an ample set that drops the only path to a violation makes these disagree and returns False.
This certifies preservation of SAFETY (invariant violability), which is what the standard ample-set conditions guarantee. Deadlock-freedom and liveness need the extra proviso (C3) and are NOT covered here — validate those separately. Returns False if either exploration truncated (inconclusive).
Source code in src/musil/por.py
musil.symmetry ¶
Building the canonicalize that check/explore take -- symmetry reduction you can derive
rather than hand-write.
check(model, canonicalize=...) has always accepted a symmetry reduction, and
symmetry_reduction_sound has always been able to grade one. What was missing is the step
between: turning "these N components are interchangeable" into the function. Hand-writing it is
where the mistakes live, and an unsound canonicalizer silently drops reachable states -- a checker
returning green for a question nobody asked.
Two constructions, and which one is correct depends on one question: does anything else in the state name a component?
canonical_by_sorting-- the components are anonymous. Their slices are sorted into a canonical order. O(N log N), so it is the one that scales, and the one to reach for by default. Sound only while no other field refers to a component by position or id: sorting the slices destroys that correspondence, and the state that said "worker 2 holds the lock" now says something else.canonical_by_permutations-- something does name a component (a leader, an owner, a route id in a message). The whole state is relabelled under each permutation of the identities and the smallest result wins, so every reference moves with the component it names. Correct where sorting is not, and factorial: usable for a handful of identities, not for 24.
Both still have to pass symmetry_reduction_sound on a small instance before being trusted on a
large one -- that gate is the point, and neither construction removes the obligation. The sorting
case is exactly where it earns its keep: a model that grows a leader field next year makes a
previously-sound sort unsound, and nothing about the sort itself changes to say so.
canonical_by_sorting ¶
canonical_by_sorting(
*,
get: Callable[[S], Sequence[T]],
put: Callable[[S, tuple[T, ...]], S],
key: Callable[[T], Any] | None = None,
) -> Callable[[S], S]
Canonicalize by sorting the interchangeable components' slices into a fixed order.
get(state) reads the per-component slices (one entry per component, in component order) and
put(state, slices) writes a reordered tuple back -- the same accessor pair the channel kit
uses. key orders slices that are not comparable with < (a frozen dataclass per component,
say); without it the slices are sorted directly.
Collapses the N! orderings of N anonymous components into one representative, so a space that was
V ** N becomes the multisets of size N over V. For 5 components over 3 values: 243 states
down to 21.
SOUND ONLY IF nothing outside these slices names a component. A leader: int field indexing
into them, an id inside a message, a per-component key elsewhere in the state -- any of those and
sorting breaks the reference while leaving the state well-formed, which is the quiet kind of
wrong. Use canonical_by_permutations there, and either way run symmetry_reduction_sound
on a small instance first.
Source code in src/musil/symmetry.py
canonical_by_permutations ¶
canonical_by_permutations(
identities: Sequence[I],
relabel: Callable[[S, Mapping[I, I]], S],
*,
order: Order[S] = repr,
max_permutations: int = 5040,
) -> Callable[[S], S]
Canonicalize by taking the smallest state in its orbit under every permutation of
identities -- the general construction, for when the identities are referenced.
relabel(state, mapping) applies one permutation to the WHOLE state: every place an identity
appears must be rewritten, not just the per-component slices. Missing one is precisely the bug
this construction exists to avoid, and it shows up as symmetry_reduction_sound returning
False rather than as a wrong answer.
order is the total order the minimum is taken under; any fixed one yields a canonical
representative, and the default repr works for arbitrary states without requiring <. It
must be stable for the duration of a check -- true for the frozen dataclasses states are normally
written as. (Ordering by repr of a frozenset field is stable within a process but varies
between runs under hash randomization: still canonical, just not reproducible across runs.)
The orbit has len(identities)! elements and all of them are built for every state, so this is
for a handful of identities. max_permutations (5040 = 7!) makes that a loud error instead of a
hang; raising it is a decision, not a default. For many anonymous components, canonical_by_sorting
is the construction that scales.
Source code in src/musil/symmetry.py
canonical_by_fields ¶
Declarative symmetry reduction: canonicalize by SORTING each named field -- each of which must hold
a collection of INTERCHANGEABLE items -- into a fixed order. The same thing canonical_by_sorting
builds, without hand-writing get/put, for the common case where the interchangeable components
already live in one field: a tuple of per-worker slices, a multiset of ids, a pool of domain values.
Works on frozen dataclass and pydantic v2 states; key orders items not comparable with <.
This is the symmetric_fields= declaration from the request, expressed as a canonicalize you
pass to check/explore -- the same shape as the other two constructions, rather than a new
Model field, so the soundness obligation stays visible at the call site.
SOUND ONLY IF nothing outside those fields names a component by position or id -- a leader: int
indexing into a sorted field, an id referenced elsewhere -- exactly as for canonical_by_sorting
(use canonical_by_permutations there). Declarative does NOT mean automatically sound: it removes
the boilerplate, not the obligation, so validate with symmetry_reduction_sound on a small instance
before trusting it on a large one.
Source code in src/musil/symmetry.py
musil.induction ¶
check_inductive — prove an invariant by INDUCTION instead of by enumerating the reachable set.
check is exhaustive up to a scope; a passing run proves the invariant only within that scope. An
INDUCTIVE proof discharges it without reference to reachability:
- base: no reachable state violates
Iwithin the firstk-1steps, and - step (k-induction): along every path
s0 -> ... -> skwhose firstkstates satisfyI, the(k+1)-th satisfiesItoo.
If both hold, I holds for every state the system can reach, at any scope. A failing step returns a
counterexample-to-induction (a state satisfying I with a successor that breaks it) so the author
strengthens I rather than widening the scope. This is what an SMT-backed inductive checker gives; we
make the "for all states s" concrete WITHOUT a solver by quantifying over a caller-supplied finite
domain -- the enumerable fragment, which is decidable by exhaustion and therefore sound.
The domain must be the FULL set of candidate states (every assignment of the state's bounded
variables), INCLUDING UNREACHABLE ONES. That is the whole point: 1-induction over only the reachable set
is trivially true for any model that already passes check (a reachable state's successors are
reachable, hence satisfy I), so a domain of just reachable states proves nothing new. The step only
ever follows ENABLED transitions, so a partial apply guarded correctly is never called out of bounds.
What this does NOT do: prove an unbounded number of components, or an infinite value domain, without a
domain to enumerate -- those need a symbolic decision procedure (a real SMT solver). See
INDUCTION_NOTES.md for what remains out of scope and why.
InductionResult
dataclass
¶
The verdict of check_inductive. proven is the headline. When it is False, failure is
"base" (a reachable state violates I within k-1 steps -- a genuine bug) or "step" (a
counterexample-to-induction: state satisfies I but firing action reaches successor,
which violates it). reason carries a string-invariant's message at the violating state.
Source code in src/musil/induction.py
check_inductive ¶
check_inductive(
model: Model[S],
invariant: Invariant[S],
domain: Iterable[S],
*,
k: int = 1,
) -> InductionResult[S]
Prove invariant inductive for model over the finite domain (see the module docstring).
invariant is a predicate with check's semantics (True holds; False/None/"" or a
reason string is a violation) -- pass one of model.invariants' values, or any predicate. domain
is the finite set of candidate states quantified over: it MUST include unreachable states (the full
bounded state space), or the check proves nothing beyond check. k is the induction depth
(k=1 is ordinary invariant induction; raise it when 1-induction reports a spurious, unreachable
counterexample). Returns an :class:InductionResult -- PROVEN, a base-case bug, or a
counterexample-to-induction.
Source code in src/musil/induction.py
Conformance to code¶
Checking that real code behaves like the model — trace replay and refinement.
musil.conformance ¶
Conformance: does the real implementation behave like the model?
Model checking proves the design is sound. Conformance testing checks the code matches the design: generate action traces from the model (sequences that cover the reachable graph), then replay each against the real system through a thin adapter, asserting the implementation lands in the state the model predicted after every step. It does not prove refinement (that's theorem-proving territory), but it checks it exhaustively over the model's traces against the running code — the practical "implementation faithful to spec" bridge (see docs/specs/RESEARCH.md: P, Stateright, ioco).
Two pieces
generate_traces(model)-> action sequences (lists of Steps,<init>first) that together cover every reachable edge (or state).replay(model, traces, step_fn, project, start)-> ConformanceResult.step_fn(real, action)drives the real system;project(real)maps it back to a model state to compare. The first divergence (real projected state != model-predicted state) is reported.
Divergence
dataclass
¶
The implementation departed from the model: after action (step step_index of trace
trace_index), the model predicted expected but the implementation projected to actual.
Source code in src/musil/conformance.py
generate_traces ¶
generate_traces(
model: Model[S],
*,
cover: str = "edges",
max_traces: int = 100000,
max_states: int = 1000000,
) -> list[tuple[Step[S], ...]]
Action sequences from the reachable graph (each a tuple of Steps, <init> first). With
cover='edges' (default) the set exercises every reachable transition at least once; with
cover='states', a shortest path to each reachable state. Each trace is a shortest stem, so
replays stay short.
Source code in src/musil/conformance.py
replay ¶
replay(
traces: Iterable[Sequence[Step[S]]],
*,
step_fn: Callable[[R, str], R],
project: Callable[[R], S],
start: R,
) -> ConformanceResult[S]
Replay each trace (from generate_traces) against the real system. start is the real
initial state (its projection must equal the model's initial state); step_fn(real, action)
applies an action to the real system; project maps a real state back to a model state for
comparison. Single-initial-state models; for multiple inits, project(start) must match each
trace's initial state. Use areplay when the real system is async.
Source code in src/musil/conformance.py
areplay
async
¶
areplay(
traces: Iterable[Sequence[Step[S]]],
*,
step_fn: Callable[[R, str], Awaitable[R]],
project: Callable[[R], S] | Callable[[R], Awaitable[S]],
start: R,
) -> ConformanceResult[S]
replay for an async implementation: step_fn is awaited, and project may be either
sync or a coroutine function (awaited when it returns an awaitable). Same arguments, same
ConformanceResult, same divergence indices -- it drives the same loop as replay.
This exists because the sync replay forces one asyncio.run per step, which cannot be
called from a running loop (so no async def test can use it) and, worse, gives every step its
own event loop: a connection pool or an open transaction created in one step is dead in the next.
Awaiting inside one loop keeps that loop-scoped state alive across a whole trace.
Source code in src/musil/conformance.py
musil.refine ¶
Refinement: hold real code to a model by checking its observed states, not its actions.
A run of the real system produces a sequence of concrete states (snapshots). An abstraction maps
each concrete state to a model state. The run refines the model iff every consecutive pair maps
to either the same abstract state (a stutter -- the real code took an internal step the model doesn't
care about) or to an abstract transition the model actually allows. The first observation must map to
a model initial state (unless require_init=False, for checking a mid-run fragment).
This is the runtime analog of refinement in the seL4/TLA+ sense (concrete behaviors are a subset of
abstract behaviors), done by checking against the explored model rather than proving -- the
practical bridge from a model-checked design to the running implementation. musil.sim feeds a
RefinementMonitor a snapshot after every step so the simulated real code is held to the spec.
Complement of conformance (which drives the real code with model-generated action labels); here
the real code drives itself and we watch where it goes.
RefinementViolation
dataclass
¶
The real run left the model. reason is "bad-init" (first state isn't a model initial
state), "unknown-state" (mapped to a state the model can't reach), or "no-model-step" (the
abstract transition isn't a model edge). index is the offending observation's position.
Source code in src/musil/refine.py
RefinementMonitor ¶
Streaming refinement check. Construct with a model and an abstraction; feed observed concrete
states one at a time to observe, which returns a RefinementViolation the first time the
run leaves the model (and None otherwise). The model is explored once, up front, so this is
for bounded models (the explicit-state regime musil lives in).
abstraction may be async (it has to read the real system rather than a captured snapshot); in
that case feed observations through aobserve, and observe raises TypeError rather than
silently abstracting everything to a coroutine object.
Source code in src/musil/refine.py
aobserve
async
¶
observe for an async abstraction -- one whose mapping to a model state has to await
(it reads the real system rather than a captured snapshot). A sync abstraction works here
too, so this is always the safe call inside a coroutine.
Source code in src/musil/refine.py
check_refinement ¶
check_refinement(
model: Model[S],
observations: Iterable[C],
abstraction: Callable[[C], S],
*,
require_init: bool = True,
max_states: int = 1000000,
) -> RefinementResult[C, S]
Check a whole observed run against the model. Returns at the first divergence (with the
offending observation), else OK once the run is exhausted. abstraction maps each observed
concrete state to a model state; require_init demands the first observation be a model initial
state (set False to check a mid-run fragment).
Source code in src/musil/refine.py
acheck_refinement
async
¶
acheck_refinement(
model: Model[S],
observations: AsyncIterable[C],
abstraction: Callable[[C], S]
| Callable[[C], Awaitable[S]],
*,
require_init: bool = True,
max_states: int = 1000000,
) -> RefinementResult[C, S]
check_refinement over an async source of observations, with an optionally async
abstraction. Same result, same first-divergence semantics.
The point is that the observations can be produced by awaiting -- polling a live service, reading a queue, draining an async generator -- without collecting the whole run into a list first. Collecting is the workaround it replaces, and it is not equivalent: a long or unbounded run has to be checked as it happens, and a violation should stop the polling rather than be found afterwards.
Source code in src/musil/refine.py
Analysis, tracing & tooling¶
Coverage and vacuity, counterexample tools, model diffing, caching, profiling, and the adoption helpers.
musil.metrics ¶
State-space metrics — how big and how branchy a design's reachable behaviour is.
Inspired by "expression cardinality" (given a semantic intent, how many valid programs express it?): for a design we don't have to guess a per-language score — musil already enumerates the whole reachable state graph, so we can MEASURE the exact analog on the behaviour itself.
state_space_metricsreports the size and branching of a model: reachable states, transitions, terminals, and per-state branching (distinct successors, self-loops excluded — anIdleaction shouldn't read as a choice). Lower branching + a tighter state space = a more deterministic, more reviewable design. A blow-up is the MDD "design for modelability" smell: behaviour you can't reason about, to reshape before it hides a bug.solution_cardinalityanswers the cardinality question directly: how many reachable states satisfy a goal. Exact over the explored space, not a guessed 1-10.
Deliberately NOT a single fabricated "determinism score" — these are honest counts on your model.
StateSpaceMetrics
dataclass
¶
The shape of a model's reachable behaviour. mean_branching/max_branching count DISTINCT
successor states (excluding self-loops) — the real fan-out of choices; terminal_states have
none. truncated means the max_states cap was hit, so the counts are lower bounds.
Source code in src/musil/metrics.py
Coverage
dataclass
¶
Which of a model's actions actually did anything over the reachable space.
A green check says no invariant broke; it does not say the behaviour you wrote was ever
explored. These are the three ways that goes wrong, as sets of names rather than accusations —
each has legitimate cases, and only the author knows which.
dead_actions: enabled in NO reachable state. The sharpest of the three: an action that can never fire is a guard bug or dead code, and it silently removes an interleaving the author believed was covered. A run that never explored it still reports OK.always_enabled_actions: enabled in EVERY reachable state, i.e. the guard never guards. Often intentional — anIdlestep, or an adversarialcrashthat may happen at any moment — so this is a smell to confirm, not a defect. Empty whenever the model has a terminal state, since nothing is enabled there.stutter_only_actions: enabled somewhere, but every firing lands back on the state it came from. The action fires and changes nothing.
truncated carries over from the graph and changes what dead_actions means: under a cap,
an action is only not yet seen enabled, which is a weaker claim than dead.
The names are action names for a static-actions model, or the key buckets ("kinds") for an
actions_fn model (see coverage/coverage_of).
Source code in src/musil/metrics.py
ok
property
¶
True when nothing was flagged. Not a verdict on the model — only the author can say whether an always-enabled action is intended — but a useful gate in a test suite.
InvariantCoverage
dataclass
¶
Which invariants are doing work — the dual of :class:Coverage (which is about actions).
A green check says every invariant held; it does not say any invariant was ever at risk. Over
the reachable space, each invariant is one of:
load_bearing: some GUARDED-OFF action, applied to a reachable state, WOULD violate it — a guard is what keeps it true. This is the spec constraining real behaviour: the near-miss the checker exists to certify.threatsmaps each such invariant to the actions that would break it.candidate_vacuous: NO guarded-off action ever produces a state that violates it, and no reachable state does either — it holds by CONSTRUCTION, so a passing check tells you nothing about it. A signal, not an accusation: an invariant true by construction can be intentional documentation.
This is the practical form of the vacuity idea that coverage deliberately dropped as too naive:
reachability + near-misses over the graph, rather than reasoning about opaque invariant antecedents.
It analyses the STATIC model.actions (it needs guarded-off actions to apply; an actions_fn that
only offers enabled actions exposes none, so those invariants read as candidate-vacuous by default).
Actions whose apply is partial — it relies on the guard and raises without it — are skipped for
the action that raised, since a state that cannot exist cannot witness a violation. truncated
carries over from the graph: under a cap, candidate_vacuous only means 'not yet threatened'.
Source code in src/musil/metrics.py
ok
property
¶
True when no invariant is candidate-vacuous. Not a verdict — an invariant true by construction may be intended — but a useful gate that every spec'd invariant is actually exercised.
PortfolioCoverage
dataclass
¶
How much of a declared transition table a whole PORTFOLIO of models exercises — read from state-field
VALUES across edges (action naming is irrelevant), unioned across every model, and diffed against the
declared table. The question a suite asks that per-model coverage cannot: "what does the whole
portfolio prove about the real state machine?"
covered_edges/dead_edges— declared(src, dst)field-transitions some model exercises / that NO model in the portfolio exercises.undeclared_edges— field-transitions a model DOES make that the table does not declare: the portfolio exercises a transition the external machine forbids (drift).covered_values/dead_values— declared field values seen / never seen across the portfolio.
ratio is covered declared edges over all declared edges (exact Fraction) — the number a ratchet
gate floors so coverage cannot rot as the denominator grows.
Source code in src/musil/metrics.py
ratio
property
¶
Covered declared edges over all declared edges (1 if the table declares no edge).
metrics_of ¶
Compute metrics from an already-explored :class:~musil.core.Graph.
Source code in src/musil/metrics.py
state_space_metrics ¶
Explore model and report the size + branching of its reachable behaviour (see
:class:StateSpaceMetrics).
Source code in src/musil/metrics.py
coverage_of ¶
coverage_of(
graph: Graph[S],
model: Model[S],
*,
key: Callable[[str], str] | None = None,
) -> Coverage
Compute coverage from an already-explored :class:~musil.core.Graph.
Reads the graph's recorded edges only — enabled is never called again, so this is O(edges) and,
unlike re-applying the actions, it stays correct under symmetry reduction (the edges are already
canonical). The report is over an "action universe": for a STATIC model.actions it is the declared
action names (in order); for an actions_fn model it is every action NAME the enumerator offers
across the reachable states (so a never-enabled kind is still counted, since it left no edge).
key maps an action NAME to a bucket ("kind") and coverage is reported over the buckets. This is how
actions_fn models report usefully: their per-state actions typically carry per-state unique names
(e.g. add_filter{field='status'}), so key=lambda name: name.split('{')[0] collapses them to
the kind. Without a key, names are used as-is (right for static models and for actions_fn models
whose action names are already a fixed set).
Source code in src/musil/metrics.py
coverage ¶
coverage(
model: Model[S],
*,
key: Callable[[str], str] | None = None,
max_states: int = 1000000,
) -> Coverage
Explore model and report which of its actions ever fired, always could, or never moved
(see :class:Coverage). key buckets action names into kinds — pass it for an actions_fn model
whose per-state action names are not a fixed set (see coverage_of).
Deliberately separate from check rather than a field on Result: check early-exits at
the first violation, so the graph it saw is partial and a coverage answer computed from it would
be wrong in the direction that matters — actions look dead because the sweep stopped, not because
they cannot fire. Run this on the whole space, next to check, not inside it.
Source code in src/musil/metrics.py
coverage_cached ¶
coverage_cached(
model: Model[S],
*,
version: str,
cache_dir: str | Path = DEFAULT_CACHE_DIR,
max_states: int = 1000000,
key: Callable[[str], str] | None = None,
) -> Coverage
Like coverage, but return a cached :class:Coverage when the model (identified by version plus
its readable structure) and options are unchanged; otherwise run coverage, store it, and return it —
the content-addressed parallel of check_cached (issue #41). A coverage regression test
(assert not coverage_cached(model, version="1").dead_actions) then skips the whole re-exploration on
every CI run and pre-push hook once the model is unchanged.
version is REQUIRED and carries the same obligation as in check_cached: bump it whenever an
action/invariant/guard BODY changes, since those callables are opaque to the structural digest (a
structural edit — a renamed/added action, changed options — invalidates the cache on its own). Unlike
check, coverage needs the whole reachable space, so the cached artifact is the final Coverage
computed once. Writing is best-effort. The entry is stored under a name distinct from check_cached's,
so a verdict cache and a coverage cache for the same model never collide.
Source code in src/musil/metrics.py
solution_cardinality ¶
solution_cardinality(
model: Model[S],
predicate: Callable[[S], bool],
*,
max_states: int = 1000000,
) -> int
How many REACHABLE states satisfy predicate — the design's "expression cardinality" for
that intent, counted exactly over the explored state space (not a guessed score). A large number
for a goal that should be reached one way is a redundancy/ambiguity smell; for a recovery goal,
more satisfying states can mean more resilience. Interpret in context.
Source code in src/musil/metrics.py
invariant_coverage_of ¶
Compute :class:InvariantCoverage from an already-explored :class:~musil.core.Graph.
For every reachable state and every STATIC model.actions that is GUARDED OFF there, it applies the
action anyway and asks whether the result violates each invariant — a guarded-off action that would
break an invariant is the guard doing its job, and marks that invariant load-bearing. An invariant no
guarded-off action ever threatens (and that no reachable state itself violates) is candidate-vacuous.
Enabled actions add no information here: their successors are already reachable, so in a passing model
they never violate. Cost is O(states x actions x invariants), so run it as an audit, next to check,
not inside it.
Source code in src/musil/metrics.py
invariant_coverage ¶
Explore model and report which of its invariants are load-bearing vs candidate-vacuous (see
:class:InvariantCoverage). Like coverage, kept separate from check and run over the whole
space: check early-exits at the first violation, so its graph is partial and this would misjudge
which invariants were ever threatened.
Source code in src/musil/metrics.py
portfolio_coverage ¶
portfolio_coverage(
portfolio: Iterable[Model[S] | Graph[S]],
*,
get: Callable[[S], str],
declared: Mapping[str, Iterable[str]],
max_states: int = 1000000,
) -> PortfolioCoverage
Union the state-field transitions exercised across a portfolio of models (or pre-built graphs) and
diff them against the declared transition table. get(state) reads the field whose values are the
external machine's states; declared maps each value to the values it may move to. A Model is explored;
a Graph is used as-is (share one explore across analyses). See :class:PortfolioCoverage.
Source code in src/musil/metrics.py
assert_covers ¶
assert_covers(
portfolio: Iterable[Model[S] | Graph[S]],
declared: Mapping[str, Iterable[str]],
*,
get: Callable[[S], str],
ratio: float = 0.0,
blind_spots: Iterable[tuple[str, str]] = (),
max_states: int = 1000000,
message: str | None = None,
) -> PortfolioCoverage
Ratchet gate on portfolio coverage — the fix for a numerator-only "N transitions covered" gate that
lets real coverage rot as the denominator grows (a suite once fell 67% -> 56% while staying green).
Computes :func:portfolio_coverage and asserts, in order:
- NO undeclared edge — the portfolio never exercises a transition the table forbids;
- the dead (uncovered) declared edges are EXACTLY the acknowledged
blind_spots— a new dead edge is a regression that must be covered or explicitly acknowledged, and a blind spot that is now covered must be removed (so the named set can only SHRINK, never grow); - the coverage
ratiois at least the floor.
Raises AssertionError on the first failure and returns the report on success. This is the doctrine
(ratio floor + named blind-spot set) as one gate.
Source code in src/musil/metrics.py
musil.counterexample ¶
Tools that turn a raw counterexample into a debugging artifact: minimize shrinks the violating
trace, and as_regression_test serialises it into a committable test.
minimize delta-debugs a violating trace: it drops actions and re-checks that replaying the reduced
sequence from the initial state still violates the SAME invariant, keeping only reductions that still
fail. The result is the minimal reproducer, the best debugging artifact and the seed for a fast
regression test (as_regression_test, issue #15).
Note on where it helps: a check/check_all counterexample is BFS-shortest, so no strict
subsequence of it can violate (BFS would have returned that shorter path first) and minimize returns
it essentially unchanged. Its value is on traces that are NOT step-minimal: a long simulation (VOPR) run,
an externally assembled action sequence, or any trace carrying actions irrelevant to the violation. On
those it strips the irrelevant actions down to the minimal failing subsequence.
minimize ¶
minimize(
model: Model[S],
result: Result[S],
*,
canonicalize: Callable[[S], S] | None = None,
) -> Result[S]
Delta-debug the counterexample in result to a minimal action sequence that still violates the
same invariant, and return a new Result carrying that shorter trace (all other fields preserved,
reason recomputed at the new final state). Greedy 1-minimization: repeatedly drop any single action
whose removal still reproduces the violation, until no single removal does.
Only invariant counterexamples are minimized; an ok result, a deadlock, or a result with no trace
is returned unchanged (there is no invariant to preserve). If the trace cannot be replayed
deterministically (same-named nondeterministic actions that pick differently), the original result is
returned unchanged rather than a possibly-wrong reduction. Pass the same canonicalize the check
used so replayed successors match the explored ones.
Source code in src/musil/counterexample.py
replay_actions ¶
replay_actions(
model: Model[S],
names: list[str],
*,
canonicalize: Callable[[S], S] | None = None,
) -> Result[S]
Replay a fixed sequence of ACTION NAMES from the model's first initial state, checking every
invariant at each state, and return the Result (the first invariant violation reached, else OK).
Unlike check it explores exactly one path -- no search -- so it is a cheap, deterministic replay of
a known counterexample, which is what a generated regression test runs. Raises ValueError if a
named action is not available/enabled at its step (the sequence no longer fits the model -- a stale
regression test should fail loudly rather than silently pass).
Source code in src/musil/counterexample.py
as_regression_test ¶
as_regression_test(
model: Model[S],
result: Result[S],
*,
test_name: str = "regression",
model_import: str = "from your_module import model # <-- point this at your Model",
minimize_first: bool = True,
) -> str
Emit committable pytest SOURCE that replays this counterexample and asserts the same invariant
breaks -- a fast, deterministic regression test that pins the exact interleaving without re-running the
exhaustive search. By default the trace is minimized first, so the emitted sequence is the minimal
reproducer. model_import is the line the test uses to obtain the Model (edit it to your module);
test_name names the function. Raises ValueError unless result is an invariant
counterexample -- there is nothing to pin otherwise.
Source code in src/musil/counterexample.py
musil.diffing ¶
diff — the behavioral delta between two model versions.
When a model is refactored (say, changing how actions are enumerated) the author wants to know behaviour
was preserved: the same reachable states, the same transitions, the same invariant outcomes. diff
explores both models and reports exactly that delta over the two reachable graphs, so a refactor is
reviewable as "the reachable states and their validity are unchanged" rather than a leap of faith
(issue #14).
States must be HASHABLE (diff runs explore on both, which keys the graph by state); pass the same
canonicalize to compare two models modulo the same symmetry.
ModelDiff
dataclass
¶
The behavioral delta between model A and model B over their reachable graphs.
states_only_in_a/states_only_in_b: reachable in one but not the other.transitions_only_in_a/transitions_only_in_b: labelled edges(from, action, to)present in one but not the other.invariant_changes: over states reachable in BOTH and invariant names defined in BOTH, the(state, invariant, holds_in_a, holds_in_b)where the outcome flipped.
equivalent is True when all four are empty — same reachable states, same transitions, same
invariant outcomes on the shared states.
Source code in src/musil/diffing.py
diff ¶
diff(
model_a: Model[S],
model_b: Model[S],
*,
canonicalize: Callable[[S], S] | None = None,
max_states: int = 1000000,
) -> ModelDiff[S]
Explore model_a and model_b and return their behavioral :class:ModelDiff (see there).
canonicalize is applied to both (compare modulo the same symmetry); max_states caps each
exploration. Reads only the reachable graphs, so it is O(states + transitions).
Source code in src/musil/diffing.py
musil.cache ¶
check_cached — content-addressed verdict caching, so an unchanged model is not re-checked.
Verification is expensive and pure: the verdict is a function of the model and the check options. In CI
an unchanged model is re-checked on every pipeline run — a ~5-20s exhaustive check that has not changed
since it last passed. check_cached stores the verdict on disk keyed by a stable digest and, on a hit,
returns it and skips the search. Same content-addressing a build system uses, applied to proofs
(issue #10).
The digest cannot be computed from the model alone: actions, invariants and terminal are opaque
Python callables, and a function's repr carries its address (different every run), so hashing it would
defeat every cache hit. So the identity of the model's LOGIC is a required version string the caller
bumps whenever an action/invariant/guard BODY changes — the one soundness obligation, and it is the
caller's, exactly as the issue frames it. On top of that the digest folds in the parts that CAN be read
stably — the action and invariant NAMES, the initial states' repr, the check options, and which opaque
hooks are present (actions_fn/footprint/canonicalize/key) — so a structural edit
invalidates the cache automatically even if version is not bumped. What it cannot see is a changed
lambda body under an unchanged name; that is what version is for.
The cache is a directory of pickle files, so it holds the FULL Result including a counterexample trace
over live state objects. Pickle means: load only a cache you produced (a CI workspace you control), and
the state classes must be importable at load time (module-level, as they are in real use). Writing is
best-effort — a read-only cache dir degrades to just running the check, never an error.
check_cached ¶
check_cached(
model: Model[S],
*,
version: str,
cache_dir: str | Path = DEFAULT_CACHE_DIR,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
) -> Result[S]
Like check, but return a cached verdict when the model (identified by version plus its
readable structure) and the options are unchanged; otherwise run check, store the Result, and
return it. version is REQUIRED: bump it whenever an action/invariant/guard BODY changes, since those
callables are opaque (see the module docstring for the full contract). canonicalize/key behave
as in check; changing one of THEM is a logic change too, so bump version for it as well.
Writing the cache is best-effort: a directory that cannot be created or written just means the check runs (and returns) normally, never an error.
Source code in src/musil/cache.py
clear_verdict_cache ¶
Delete every cached verdict under cache_dir and return how many files were removed. A missing
directory is fine (returns 0). Use it to invalidate everything when a global change (a musil upgrade,
a shared helper) makes bumping every model's version impractical.
Source code in src/musil/cache.py
musil.profiling ¶
profile — where a slow check spends its time.
When a check is slow, Result says nothing about WHERE the time went, so the honest answer used
to be a reverse-engineering session (a real case ran ~120s under CI coverage before anyone worked out
the guard was rebuilding an expensive menu ~100k times, amplified ~25x by line-tracing). profile
runs the same breadth-first sweep as check but timed, and reports:
- time split by PHASE — invariants, enumeration (
actions/actions_fn), enablement (enabled),apply,canonicalize, and the visited-set (identity + hashing + lookup); - the hottest ACTIONS by cumulative
enabled+applytime and call count; - states/second and which phase dominates, so the fix (footprint memoization, a cheaper guard, symmetry, a smaller scope) is obvious rather than guessed.
It profiles the FULL sweep, not check's early exit: it does not stop at the first violation, because
what you profile is a passing-but-slow check exhausting the space. Timing every call adds overhead, so
the absolute seconds are indicative and the RELATIVE split is the signal. Accepts canonicalize and
key exactly as check does, so a non-hashable (pydantic) model profiles the same way it checks.
An instrumented sibling of check's BFS: it deliberately duplicates the loop rather than threading
timing branches through the hot path of check itself.
Phase
dataclass
¶
ActionCost
dataclass
¶
Per-action cumulative cost: its enabled guard and its apply, timed separately.
Source code in src/musil/profiling.py
Profile
dataclass
¶
A timed breakdown of a check sweep. phases is ordered as executed; actions is sorted
hottest-first by total_seconds. truncated means the max_states cap was hit, so the counts
are lower bounds.
Source code in src/musil/profiling.py
dominant_phase
property
¶
The phase that took the most cumulative time — the thing to attack first.
profile ¶
profile(
model: Model[S],
*,
max_states: int = 1000000,
canonicalize: Callable[[S], S] | None = None,
key: Callable[[S], Hashable] | None = None,
) -> Profile
Run model's reachable sweep with per-phase and per-action timing; return a :class:Profile
(see the module docstring). Profiles the full space, not check's early exit. canonicalize and
key behave as in check.
Source code in src/musil/profiling.py
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 | |
musil.doctor ¶
musil.doctor — spot hand-rolled patterns a shipped musil API already covers.
The recurring finding across consumers is not missing features but SHIPPED features with zero adoption:
assert x.ok, str(x) written 290 times where assert_ok renders the counterexample; the trace-name
list-comprehension re-invented where Result.action_names exists; assert not x.ok where
assert_violates pins the verdict. scan reads Python source with the standard-library ast (so it
is dependency-free) and returns advisory :class:Findings — file positions plus the API to reach for. It is
a HINT, not a gate: heuristics match the common shapes, and a false positive costs only a suggestion.
Finding
dataclass
¶
One advisory hit: a hand-rolled pattern at line:col that message says how to replace.
pattern is a short stable id (e.g. "assert-ok") for filtering.
Source code in src/musil/doctor.py
scan ¶
Scan Python source for hand-rolled patterns a shipped musil API already covers, returning advisory
:class:Findings sorted by position. Pure stdlib ast — no dependency, and it never imports or runs
the code. Detected today:
assert X.ok, <msg>->assert_ok(X)(which renders the counterexample, so the message is unnecessary). The message is the tell that distinguishes musil's idiom from a bare truthiness assert.assert not X.ok->assert_violates(X, ...)(the red-side helper; optionally pinkind=/invariant=).[s.action for s in X.trace ...](list/set/generator) ->X.action_names.
Being advisory, it errs toward the specific shapes above rather than every possible match.
Source code in src/musil/doctor.py
musil.citations ¶
musil.citations — keep "the models are the spec" honest: model references must not dangle.
A good practice is for production code to CITE the model that justifies a non-obvious design ("the musil
model proved timer fairness alone cannot guarantee reconvergence — test_mesh_membership_musil"). The
practice fails silently when the pointer rots: a model cited by production code and a schema migration, whose
file no longer exists anywhere. find_citations locates the references (regex, so it sees comments and
prose, not only identifiers) and dangling_citations reports the ones that do not resolve against the set
of models that actually exist — the check a musil citations gate runs so a spec pointer cannot dangle.
Pure stdlib (re + pathlib), so it is dependency-free and never imports or runs the scanned code.
Citation
dataclass
¶
find_citations ¶
Every model reference in text (production code, comments, or prose), as Citations sorted by
position. pattern is a regex; the default matches test_*_musil names. One entry per distinct
(name, line).
Source code in src/musil/citations.py
dangling_citations ¶
dangling_citations(
text: str,
known: Iterable[str],
*,
pattern: str = DEFAULT_PATTERN,
) -> list[Citation]
The citations in text whose model name is NOT in known — spec pointers that dangle. known
is the set of model names that actually resolve (typically known_models over the test tree).
Source code in src/musil/citations.py
known_models ¶
The model names that RESOLVE under root: the stems of .py files whose stem matches pattern
(the existing test_*_musil.py model files). Feed this as known to dangling_citations.
Source code in src/musil/citations.py
musil.graph ¶
Render a model's reachable state graph as Graphviz DOT — the same artifact FizzBee emits, but
from the Python model. to_dot(model) explores the model and returns a DOT string you can pipe to
dot -Tsvg. Pass highlight (a sequence of states, e.g. the states of a counterexample trace)
to colour that path — handy for visualising why a check failed.
to_dot ¶
to_dot(
source: Model[S] | Graph[S],
*,
highlight: Iterable[S] = (),
name: str = "musil",
max_states: int = 1000000,
) -> str
Graphviz DOT for the reachable state graph. source is a Model (explored here) or a
pre-built Graph. Initial states are drawn bold; highlight states are filled and edges between
two highlighted states are red (e.g. highlight=[s.state for s in result.trace]).
Source code in src/musil/graph.py
musil.history ¶
with_last_action — put the action that produced a state INTO the state, so a temporal property can
name which action was taken.
A plain musil state says WHERE the system is, not HOW it got there. Some properties are about the action
sequence: "every request is eventually followed by a respond", "commit is never immediately
undone by rollback". A state-only predicate cannot say "request was just taken", and an edge invariant
(core.EdgeInvariant) can only make a SAFETY claim about a single step, not a liveness claim across a run.
with_last_action(model) augments the model so each state becomes LastAction(state, action) — the
original state plus the name of the action that produced it (None at an initial state). "which action was
taken" is now ordinary state data, so check_ltl and check_liveness express action-sequence properties
directly: G(action_taken('request') -> F action_taken('respond')). The transform lifts every field of the
model faithfully, so the augmented model is checked by exactly the same engines. Pure stdlib.
LastAction
dataclass
¶
A state paired with the name of the action that produced it (None at an initial state). The
element type of with_last_action(model), so a property can name WHICH action was taken.
Source code in src/musil/history.py
action_taken ¶
The predicate "the last action taken was name", for building an Atom / invariant over a
with_last_action model. False at an initial state (whose action is None).
Source code in src/musil/history.py
with_last_action ¶
Augment model so each state carries the action that produced it (LastAction = original state +
last action name). "Which action was taken" becomes STATE data, so check_ltl / check_liveness can
express properties over the ACTION SEQUENCE — e.g. "every request is eventually followed by a
respond" as G(action_taken('request') -> F action_taken('respond')) — which a state-only property
cannot say and a safety-only edge invariant cannot make a liveness claim about.
Every field is lifted faithfully: initial states get action=None; each action keeps its name and
fair tag and records itself on apply; invariants / terminal / edge_invariants / footprint
read the underlying .state; actions_fn is lifted per state. The reachable space grows only by
distinguishing states reached by different actions (a state reachable by two actions becomes two
LastAction states). Counterexample traces are over LastAction — read .state and .action.
Use action_taken(name) for the "the last action was name" predicate.
Source code in src/musil/history.py
musil.tracing ¶
no_trace — spare musil's hot loop from line-tracing overhead.
A model check spends most of its time in the explicit-state search (hashing, enablement dispatch, apply).
Under pytest-cov (or any sys.settrace-based tool) every executed line in that loop pays a tracing
cost, and nobody downstream measures musil's own line coverage — so it is pure waste. A real case: a check
that ran ~10s bare took ~120s under CI coverage and was killed, much of the amplification being coverage
tracing musil internals rather than the model logic under test.
no_trace() is a context manager that pauses the current thread's trace function for its block and
restores it after. It is dependency-free (only sys) and a no-op when nothing is tracing, so wrapping a
check costs nothing outside coverage/debugging runs::
with no_trace():
result = check(model)
It pauses ALL line tracing in the block (coverage, and any attached line-tracer), not coverage selectively — wrap only the check, not code whose coverage you want measured. For a coarser, whole-engine exclusion, prefer the config route in your own project instead::
# pyproject.toml
[tool.coverage.run]
omit = ["*/musil/*"] # do not measure the engine; your model code stays measured
Both target the same waste; the context manager is for a hot check inside an otherwise-measured test, the omit for skipping the engine everywhere.
no_trace ¶
Pause the current thread's trace function (e.g. coverage) for the duration of the block, then
restore it. A no-op when no trace function is installed. Pauses per-thread only (sys.settrace), so
run the check on the thread you wrap.