Module nondet 

Defines the NonDet type and nondet! macro for tracking non-determinism.

All safe APIs in Hydro guarantee determinism, even in the face of networking delays and concurrency across machines. But often it is necessary to do something non-deterministic, like generate events at a fixed wall-clock-time interval, or split an input into arbitrarily sized batches.

These non-deterministic APIs take additional parameters called non-determinism guards. These values, with type NonDet, help you reason about how non-determinism affects your application. To pass a non-determinism guard, you must invoke nondet!() with an explanation for how the non-determinism affects the application.

See the Hydro docs for more.

Macros

nondet

Fulfills a non-determinism guard parameter by declaring a reason why the non-determinism is tolerated or providing other non-determinism guards that forward the inner non-determinism.

Structs

NonDet

A non-determinism guard, which documents how a source of non-determinism affects the application.