macro_rules! __nondet__ {
($(#[doc = $doc:expr])+ hook = $hook:expr $(,)?) => { ... };
($(#[doc = $doc:expr])+$($forward:ident),*) => { ... };
}Expand description
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.
The first argument must be a doc comment with the reason the non-determinism is okay. If forwarding a parent non-determinism, because the non-determinism is not handled internally, you should provide a short explanation of how the inner non-determinism is captured by the outer one. If the non-determinism is locally resolved, you should document why this is the case.
An optional trailing hook = ... argument attaches a simulator hook payload to
the guard (see hydro_lang::sim::hooks), letting a simulation test script the
decisions of the unsafe operator(s) that consume the guard. The expression is
converted with Into, so a raw handle can be passed where an optional one is
expected:
nondet!(/** reason */) // no hook attached (the payload default)
nondet!(/// reason
nondet_parent) // forwarded justification, no hook
nondet!(/** reason */ hook = my_hook) // attach a hook handle
nondet!(/** reason */ hook = part) // attach a payload split off a composite
// guard with `NonDet::take_hook`
nondet!(/** reason */ hook = (h1.into(), None)) // composite payload, hooking only `h1`Note that forwarding a guard without hook = never propagates a hook binding, even
if the forwarded guard carries one; every binding is visible at the exact
operator it controls. A guard whose type already matches an operator’s parameter is
passed to that operator directly; to attach a hook received as part of a composite
payload, split it off explicitly with
NonDet::take_hook and pass it via hook =.
§Examples
Locally resolved non-determinism:
use std::time::Duration;
fn singleton_with_delay<T, L>(
singleton: Singleton<T, Process<L>, Unbounded>
) -> Optional<T, Process<L>, InitNone> {
singleton
.sample_every(q!(Duration::from_secs(1)), nondet!(/**
non-deterministic samples will eventually resolve to stable result
*/))
.last()
.into()
}Forwarded non-determinism:
use std::fmt::Debug;
use std::time::Duration;
use hydro_lang::live_collections::stream::ExactlyOnce;
/// ...
///
/// # Non-Determinism
/// - `nondet_samples`: this function will non-deterministically print elements
/// from the stream according to a timer
fn print_samples<T: Debug, L>(
stream: Stream<T, Process<L>, Unbounded>,
nondet_samples: NonDet,
) {
stream
.sample_every(
q!(Duration::from_secs(1)),
nondet!(
/// non-deterministic timing will result in non-determistic samples printed
nondet_samples
),
)
.assume_retries::<ExactlyOnce>(nondet!(
/// non-deterministic duplicated logs are okay
nondet_samples
))
.for_each(q!(|v| println!("Sample: {:?}", v)))
}