simulation.hpp

#pragma once
 
#include <cstdint>
#include <deque>
#include <filesystem>
#include <functional>
#include <iosfwd>
#include <limits>
#include <memory>
#include <optional>
#include <string>
#include <utility>
#include <vector>
 
#include "ravel/clock.hpp"
#include "ravel/disk.hpp"
#include "ravel/network.hpp"
#include "ravel/rng.hpp"
#include "ravel/scheduler.hpp"
#include "ravel/trace.hpp"
 
namespace ravel {
 
class Simulation;
 
using InvariantFn = std::function<bool()>;
 
using SimulationSetup = std::function<void(Simulation&)>;
 
struct SimulationOptions {
  std::uint64_t max_steps = 1'000'000;
 
  VirtualClock::Tick time_limit = std::numeric_limits<VirtualClock::Tick>::max();
 
  std::filesystem::path trace_dir;
 
  std::optional<std::vector<VirtualRng::Choice>> replay_choices;
};
 
struct Result {
  bool ok = false;
  std::uint64_t seed = 0;
  std::string failure;             
  std::uint64_t steps = 0;         
  std::uint64_t trace_digest = 0;  
  std::string trace_path;          
};
 
class Simulation {
 public:
  explicit Simulation(std::uint64_t seed, SimulationOptions options = {});
 
  Simulation(const Simulation&) = delete;
  Simulation& operator=(const Simulation&) = delete;
 
  VirtualClock& clock() noexcept { return clock_; }
  VirtualRng& rng() noexcept { return rng_; }
  Scheduler& scheduler() noexcept { return scheduler_; }
  const Trace& trace() const noexcept { return trace_; }
 
  const std::vector<VirtualRng::Choice>& choices() const noexcept { return rng_.choices(); }
 
  Channel& add_channel(std::string from, std::string to, FaultSpec fault);
  Disk& add_disk(std::string name, DiskFaultSpec fault = {});
 
  template <typename T, typename... Args>
  T& make_state(Args&&... args) {
    auto state = std::make_shared<T>(std::forward<Args>(args)...);
    T& reference = *state;
    owned_state_.push_back(std::move(state));
    return reference;
  }
 
  void add_invariant(std::string name, InvariantFn invariant);
 
  Result run_until_quiescent();
 
  void write_trace(std::ostream& out) const;
 
  std::string describe(const TraceEvent& event) const;
 
 private:
  struct NamedInvariant {
    std::string name;
    InvariantFn check;
  };
 
  std::string first_failed_invariant() const;
 
  std::string dump_trace() const;
 
  std::string subject_name(const TraceEvent& event) const;
 
  std::vector<std::shared_ptr<void>> owned_state_;
 
  std::uint64_t seed_;
  SimulationOptions options_;
  VirtualClock clock_;
  VirtualRng rng_;
  Trace trace_;
  Scheduler scheduler_;
 
  std::deque<Channel> channels_;
  std::deque<Disk> disks_;
  std::vector<NamedInvariant> invariants_;
};
 
}  // namespace ravel