Enum Commands 

pub enum Commands {
    Check {
        input: SpecFileInput,
        config_file: Option<PathBuf>,
        model_checker: Option<ModelCheckerOption>,
        bdd: Option<BDDManagerOption>,
        smt_solver: Option<SMTSolverDefaultOptions>,
        compact_out: bool,
        abort_on_violation: bool,
        mode: CheckMode,
    },
    Visualize {
        input: SpecFileInput,
        output: VisualizationOutput,
    },
    Translate {
        input: SpecFileInput,
        output: TranslationOutput,
    },
}

Variants

Check

Read the specification file and check the specified properties

Fields

input: SpecFileInput

config_file: Option<PathBuf>

Configuration file for the model checker

model_checker: Option<ModelCheckerOption>

Request a specific model checker to be used

bdd: Option<BDDManagerOption>

Configure the BDD library to use

smt_solver: Option<SMTSolverDefaultOptions>

Select the SMT solver to be used

compact_out: bool

Enable compact output of error paths omitting locations with 0 processes and variables that are 0

abort_on_violation: bool

Abort the model checking on the first counter example that has been found

mode: CheckMode

Choose the mode with which to run the check

Visualize

Read the specification file and visualize the threshold automaton

Fields

input: SpecFileInput

output: VisualizationOutput

Translate

Translate from one specification file format to another one

Fields

input: SpecFileInput

output: TranslationOutput

Trait Implementations

impl Debug for Commands

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

Formats the value using the given formatter.

impl FromArgMatches for Commands

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from [ArgMatches], parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl Subcommand for Commands

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate Self via [FromArgMatches::from_arg_matches_mut]

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to [Command] so it can instantiate self via [FromArgMatches::update_from_arg_matches_mut]

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand