ravel::Simulation Class Reference

Top-level harness: owns the seed, virtual clock, RNG, trace and scheduler for one deterministic run. More...

#include <simulation.hpp>

Public Member Functions
	Simulation (std::uint64_t seed, SimulationOptions options={})
	A run for seed. Then add channels and disks, spawn tasks, add invariants, and run.
	Simulation (const Simulation &)=delete
	The scheduler refers to the members below, so a Simulation cannot move.
Simulation &	operator= (const Simulation &)=delete
VirtualClock &	clock () noexcept
	The virtual clock.
VirtualRng &	rng () noexcept
	The run's one source of randomness. Everything random in the code under test must come from here.
Scheduler &	scheduler () noexcept
	The scheduler: spawn tasks through it.
const Trace &	trace () const noexcept
	Everything that has happened so far.
const std::vector< VirtualRng::Choice > &	choices () const noexcept
	Every random choice made so far.
Channel &	add_channel (std::string from, std::string to, FaultSpec fault)
	Adds a one-way message channel from endpoint from to endpoint to.
Disk &	add_disk (std::string name, DiskFaultSpec fault={})
	Adds a virtual disk.
template<typename T , typename... Args>
T &	make_state (Args &&... args)
	Creates an object owned by the simulation and returns a reference to it.
void	add_invariant (std::string name, InvariantFn invariant)
	Invariants are checked once, after the scheduler has run to quiescence.
Result	run_until_quiescent ()
	Runs until nothing is left to happen (or a task throws, the step limit is hit, or the time limit passes), then checks the invariants.
void	write_trace (std::ostream &out) const
	Writes the trace as JSON Lines: a header line (format, versions, seed), then one line per event with its step, virtual time, kind, and the id and name of the task or channel it concerns.
std::string	describe (const TraceEvent &event) const
	One event in words, for messages: ‘TaskResumed 'client’ at t=40`.

Detailed Description

Top-level harness: owns the seed, virtual clock, RNG, trace and scheduler for one deterministic run.

Running the same code under the same seed gives the same Result, including the same trace_digest.

Member Function Documentation

add_invariant()

void ravel::Simulation::add_invariant	(	std::string	name,
		InvariantFn	invariant
	)

Invariants are checked once, after the scheduler has run to quiescence.

An invariant that throws counts as failed.

choices()

const std::vector< VirtualRng::Choice > & ravel::Simulation::choices ( ) const

inlinenoexcept

Every random choice made so far.

Passing this list back as SimulationOptions::replay_choices reproduces the run without the seed.

make_state()

template<typename T , typename... Args>

T & ravel::Simulation::make_state ( Args &&...  args )

inline

Creates an object owned by the simulation and returns a reference to it.

Use it for state shared by tasks and invariants: it outlives every task, and each run (say, each seed of run_seeds) gets its own fresh copy.

int& counter = sim.make_state<int>(0);

---

The documentation for this class was generated from the following file:

• include/ravel/simulation.hpp