Skip to main content

__nondet__

Macro __nondet__ 

Source
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)))
}