Module lazy_balance_model_checker

Expand description

Model checker module for LazyBalance implementations.

Use LazyBalanceModelChecker as the entrypoint for all model checking operations.

This module exposes the required types:

These types are used to define the testing environment:

The execution engine is internal; interact with it only through the trait methods.

Structs§

BalanceExit: Represents a successful withdrawal where the lazy and manual models produce different outputs.
BalanceFailure: Represents a failure encountered during execution of an operation sequence.
BalanceModelResults: Aggregates results produced during state exploration.
BalanceState: Primary state container for executing and tracking a sequence of operations.
BalanceTraps: Defines trap behavior for state exploration.
LazyContainer: Convenience container holding the owned state required to operate on a LazyBalance instance.

BalanceOp: Operation descriptor for driving both LazyBalance and ManualBalanceModel executions in a consistent manner.

BalanceGuards: Defines validity checks for operations during state exploration.
BalanceStateHasher: Defines a primary hashing strategy for BalanceState instances.
LazyBalanceMarker: Convenience trait alias for a LazyBalance implementor used in model checking and testing.
LazyBalanceModelChecker: Unified model checker interface over the lazy balance model checker module.
ManualBalanceModel: A user-indexed eager balance model over a LazyBalance system, primarily intended for testing and validation.

balance_states_csv_reports 🔒: Writes model exploration results to CSV files.
compare_balances_values 🔒: Compares lazy and manual withdrawal results and evaluates drift.
deposit 🔒: Executes a deposit on the lazy balance model using the provided container.
drain 🔒: Executes a drain operation on the lazy balance model.
explore_balance_states 🔒: Core state exploration engine for LazyBalance.
explore_balance_trap_states_default 🔒: Extends explore_explore_balance_states_default by allowing controlled violations of BalanceGuards via BalanceTraps.
explore_explore_balance_states_default 🔒: Default state exploration entrypoint for LazyBalance.
mint 🔒: Executes a mint operation on the lazy balance model.
reap 🔒: Executes a reap operation on the lazy balance model.
record_err 🔒: Records a failed execution for the given trace.
record_exit 🔒: Records an exit (drift) between lazy and manual models.
record_pass 🔒: Records a successful execution for the given trace.
withdraw 🔒: Executes a withdrawal on the lazy balance model.