__nondet__

Macro __nondet__ 

Source
macro_rules! __nondet__ {
    ($(#[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.

ยง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>, Unbounded> {
  singleton
    .sample_every(q!(Duration::from_secs(1)), nondet!(/**
        non-deterministic samples will eventually resolve to stable result
    */))
    .last()
}

Forwarded non-determinism:

use std::fmt::Debug;
use std::time::Duration;

/// ...
///
/// # 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(nondet!(
        /// non-deterministic duplicated logs are okay
        nondet_samples
    ))
    .for_each(q!(|v| println!("Sample: {:?}", v)))
}