Module cli 

Command Line Interface for TACO

TACO uses the clap crate to parse command line arguments and create the CLI interface. This module defines all available commands and options (and their documentation) as well as some utility functions to apply these options.

Modules

output_formats 🔒

This module contains the logic to output a GeneralThresholdAutomaton into a specific format

Structs

Cli 🔒

TACO toolsuite for threshold automata - Command Line Interface

LoggerConfig 🔒

SpecFileInput 🔒

TranslationOutput

VisualizationOutput

Enums

BDDManagerOption 🔒

CheckMode

Commands

ModelCheckerOption 🔒

OutputFormat

SMTSolverDefaultOptions

SMT solvers that are supported by default

SpecFileFormat 🔒

SymbolicModelCheckerHeuristics 🔒

Constants

DEFAULT_PREPROCESSORS

Preprocessors that will be used by default

Functions

create_coverability_expression

The coverability specification looks as follows: We want to find a path from an initial configuration to a configuration where the location is covered Thus the specification looks as follows: (expression_initial) => [](to_be_covered_loc = 0) Since the initial configuration is coded into the ta, there is no need for the implication. A counter example to this specification is exactly the path we are looking for

create_reachability_expression

The reachability specification looks as follows: We want to find a path from an initial configuration to a specific configuration Thus the specification looks as follows: (expression_initial) => []((pop_loc_1 = 0) || … || (pop_loc_p = 0) || (unpop_loc_1 > 0) || … || (unpop_loc_u > 0) Since the initial configuration is coded into the ta, there is no need for the implication. A counter example to this specification is exactly the path we are looking for

display_result

get_bdd_manager_cfg 🔒

Get BDD manager configuration based on selected BDD manager

get_preprocessors 🔒

Constructs the preprocessors, either from the configuration file or just uses the default preprocessors specified in DEFAULT_PREPROCESSORS

get_smt_solver 🔒

Get SMT solver configuration based on selected solver

get_zcs_model_checker_heuristic 🔒

Get the symbolic model checker heuristic based on the CLI option

initialize_cs_model_checker 🔒

initialize_logger 🔒

Initialize the logger as specified in cfg

initialize_smt_model_checker 🔒

initialize_zcs_model_checker 🔒

Initialize the symbolic model checker with the given options, threshold automaton and specifications

model_check_ta 🔒

parse_coverability

parse_initial_configuration 🔒

parse_input_file 🔒

Parse the input file into a threshold automaton

parse_reachability

translate_ta 🔒

Translate a threshold automaton into the specified format and write the resulting specification to the specified output file

visualize_ta 🔒

Visualize the threshold automaton in the given format