TraceForge’s wrapper for an assertion. It behaves similarly to the system’s assert!
but allows the underlying model checker to continue exploration even if an assertion
violation has been found.
There is no way to write a counterexample file without using this function.
There is a good question though about what name we should offer this to
customers under.
Same as estimate_execs but with a user-defined number of
samples
The return value can be Inf to denote the estimate is too large for a f64 representation
verify tries to systematically explore the state space until completion. For preliminary analysis,
parallel_test provides an incomplete exploration strategy. parallel_test spins up a configurable number of threads,
and runs TraceForge on each thread using different random scheduling orders on each thread but otherwise running
the ODPOR algorithm. parallel_test is not meant to be comprehensive and usually runs with an upper bound on the number
of executions explored in each thread or an upper bound on the time
(both can be configured—see with_samples and with_time_bound)
verify tries to systematically explore the state space until completion. For preliminary analysis,
test provides an incomplete exploration strategy. test is not meant to be comprehensive and usually runs with an upper bound on the number
of executions explored