Struct TraceValidatorConfig 

#[non_exhaustive]
pub struct TraceValidatorConfig {
    pub trace_spec: PathBuf,
    pub init: String,
    pub next: String,
    pub inv: String,
    pub cinit: String,
    pub apalache_bin: String,
    pub timeout: Option<Duration>,
}

Configuration for Apalache-based trace validation.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

trace_spec: PathBuf

Path to the TLA+ TraceSpec file.

init: String

INIT predicate name in the TraceSpec (default: “TraceInit”).

next: String

NEXT predicate name in the TraceSpec (default: “TraceNext”).

inv: String

Invariant that is violated when the trace is fully consumed (default: “TraceFinished”).

cinit: String

Constant initialization predicate (default: “TraceConstInit”).

apalache_bin: String

Path to the Apalache binary (default: “apalache-mc”).

timeout: Option<Duration>

Timeout for the Apalache subprocess. If None, no timeout is applied.

Implementations

impl TraceValidatorConfig

pub fn builder() -> TraceValidatorConfigBuilder

Trait Implementations

impl Clone for TraceValidatorConfig

fn clone(&self) -> TraceValidatorConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TraceValidatorConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for TraceValidatorConfig

fn default() -> Self

Returns the “default value” for a type.

impl From<&str> for TraceValidatorConfig

fn from(trace_spec: &str) -> Self

Converts to this type from the input type.

impl From<PathBuf> for TraceValidatorConfig

fn from(trace_spec: PathBuf) -> Self

Converts to this type from the input type.