mirror of
https://github.com/aljazceru/turso.git
synced 2026-01-14 05:34:20 +01:00
191b586f05
better counterexample minimization. - it separates interaction plans from their state of execution - it removes closures from the property definitions, encoding properties as an enum variant, and deriving the closures from the variants. - it adds some naive counterexample minimization capabilities to the Limbo simulator and reduces the plan sizes considerably. - it makes small changes to various points of the simulator for better error reporting, enhancing code readability, small fixes to handle previously missed cases
45 lines
1.3 KiB
Rust
45 lines
1.3 KiB
Rust
use clap::{command, Parser};
|
|
|
|
#[derive(Parser)]
|
|
#[command(name = "limbo-simulator")]
|
|
#[command(author, version, about, long_about = None)]
|
|
pub struct SimulatorCLI {
|
|
#[clap(short, long, help = "set seed for reproducible runs", default_value = None)]
|
|
pub seed: Option<u64>,
|
|
#[clap(short, long, help = "set custom output directory for produced files", default_value = None)]
|
|
pub output_dir: Option<String>,
|
|
#[clap(
|
|
short,
|
|
long,
|
|
help = "enable doublechecking, run the simulator with the plan twice and check output equality"
|
|
)]
|
|
pub doublecheck: bool,
|
|
#[clap(
|
|
short = 'n',
|
|
long,
|
|
help = "change the maximum size of the randomly generated sequence of interactions",
|
|
default_value_t = 1024
|
|
)]
|
|
pub maximum_size: usize,
|
|
#[clap(
|
|
short = 'k',
|
|
long,
|
|
help = "change the minimum size of the randomly generated sequence of interactions",
|
|
default_value_t = 1
|
|
)]
|
|
pub minimum_size: usize,
|
|
#[clap(
|
|
short = 't',
|
|
long,
|
|
help = "change the maximum time of the simulation(in seconds)",
|
|
default_value_t = 60 * 60 // default to 1 hour
|
|
)]
|
|
pub maximum_time: usize,
|
|
#[clap(
|
|
short = 'm',
|
|
long,
|
|
help = "minimize(shrink) the failing counterexample"
|
|
)]
|
|
pub shrink: bool,
|
|
}
|