automation_structures/compositions/
mod.rs

1// Executable modules for the Signal and RateLimit compositions and for the
2// SelectThenActuate and TraversalBudgetComposition theorems. Each TLA+ action
3// maps to one exclusive mutable method. Concurrent realizations must provide
4// an equivalent atomic commit boundary.
5//
6//   signal              — Signal (named composition, Coordination family):
7//                         change-detecting notification channel;
8//                         PendingNotifiedDisjointness.
9//   rate_limit          — RateLimit (named composition, Coordination family):
10//                         per-window operation bound; WindowCountBound,
11//                         WindowStartNotFuture.
12//   select_then_actuate — SelectThenActuate composition theorem: argmax
13//                         selection coupled with actuation;
14//                         TypeInvariant, ActuationScope, WinnerOptimality,
15//                         CompositionInvariant.
16//   traversal_budget_composition — TraversalBudgetComposition theorem:
17//                         budgeted traversal with a
18//                         shared budget; TypeInvariant, CompositionInvariant
19//                         (total_cost + budget_remaining = MaxBudget),
20//                         AcceptedSubsetVisited.
21
22//! Named-composition carriers and their proof relations.
23
24/// Budget-coupled accepted-node snapshots.
25pub mod allocation_snapshot;
26/// Monotone-boundary bisection.
27pub mod bisection;
28/// Budgeted union-find equivalence classes.
29pub mod equivalence_class;
30/// Master and sub-pool budget federation.
31pub mod federated_budget;
32/// Fixed-window rate limiting.
33pub mod rate_limit;
34/// Ordered additive and maximum reductions.
35pub mod reduction;
36/// Registry-backed weighted relationship graphs.
37pub mod relationship_graph;
38/// Budgeted supported sampling.
39pub mod sampler;
40/// Selection coupled to governed actuation.
41pub mod select_then_actuate;
42/// Change notification with per-listener cursors.
43pub mod signal;
44/// Proof facade for traversal and budget coupling.
45pub mod traversal_budget_composition;
46/// Graph traversal assembled from shared structure owners.
47pub mod traversal_engine;
automation_structures/compositions/mod.rs

automation_structures/compositions/
mod.rs
