Concept index

• `!' (LTL formula operator): Random LTL formulas
• `!' (operator semantics in LTL): LTL formulas
• `->' (LTL formula operator): Random LTL formulas
• `->' (operator semantics in LTL): LTL formulas
• `/\' (LTL formula operator): Random LTL formulas
• `/\' (operator semantics in LTL): LTL formulas
• `<->' (LTL formula operator): Random LTL formulas
• `<->' (operator semantics in LTL): LTL formulas
• `\/' (LTL formula operator): Random LTL formulas
• `\/' (operator semantics in LTL): LTL formulas
• and (LTL formula operator): Random LTL formulas
• and (operator semantics in LTL): LTL formulas
• not (LTL formula operator): Random LTL formulas
• or (LTL formula operator): Random LTL formulas
• or (operator semantics in LTL): LTL formulas
• abbreviated LTL formula operators: LTL formula options
• abbreviated LTL formula operators: FormulaOptions section
• `Algorithm' section (configuration file): Translator section
• always (LTL formula operator): Random LTL formulas
• always (operator semantics in LTL): LTL formulas
• analyzing test failures, Büchi automata intersection emptiness check: Failure analysis commands
• analyzing test failures, model checking result consistency check: Failure analysis commands
• analyzing test failures, model checking result cross-comparison test: Failure analysis commands
• atomic proposition: Random input generation
• atomic propositions, computing probabilities for: The formula generation algorithm
• atomic propositions, priorities for: LTL formula options
• atomic propositions, priorities for: FormulaOptions section
• atomic propositions, priorities for: The formula generation algorithm
• atomic propositions, priorities for: Random LTL formulas
• `B' (LTL formula operator): Random LTL formulas
• `B' (operator semantics in LTL): LTL formulas
• before (LTL formula operator): Random LTL formulas
• before (operator semantics in LTL): LTL formulas
• Büchi automata intersection emptiness check: Automata intersection emptiness check
• Büchi automata intersection emptiness check, failure analysis: Failure analysis commands
• Büchi automata, formal definition: Generalized automata
• Büchi automata, LTL-to-Büchi translator output file format: Format for automata
• changing verbosity of output: Test control commands
• changing verbosity of output: Global options
• changing verbosity of output: GlobalOptions section
• commands, abbreviating: Command conventions
• commands, conventions for entering: Command conventions
• commands, entering lists of numbers: Command conventions
• commands, getting help: Getting help
• commands, invoking external programs: Command conventions
• commands, LTL formula identifiers: Command conventions
• commands, redirecting output: Command conventions
• commands, test control: Test control commands
• commands, writing output to a pipe: Command conventions
• comments in configuration file: Configuration file
• configuration file, `Algorithm' section: Translator section
• configuration file, changing the name of: Special options
• configuration file, comments: Configuration file
• configuration file, example: Sample configuration file
• configuration file, formatting: Configuration file
• configuration file, `FormulaOptions' section: FormulaOptions section
• configuration file, `GlobalOption' section: GlobalOptions section
• configuration file, `Implementation' section: Translator section
• configuration file, minimal requirements: Translator section
• configuration file, minimal requirements: Configuration file
• configuration file, option values: Configuration file
• configuration file, `StateSpaceOptions' section: StateSpaceOptions section
• configuration file, `Translator' section: Translator section
• configuration information: Configuration information
• conjunction (LTL formula operator): Random LTL formulas
• conjunction (operator semantics in LTL): LTL formulas
• constants, computing probabilities for: The formula generation algorithm
• constants, priorities for: LTL formula options
• constants, priorities for: FormulaOptions section
• constants, priorities for: The formula generation algorithm
• constants, priorities for: Random LTL formulas
• conventions for entering commands: Command conventions
• conventions for writing configuration files: Configuration file
• default operator priority: LTL formula options
• default operator priority: FormulaOptions section
• density (of a state space): StateSpaceOptions section
• density (of a state space): Random state spaces
• disabling LTL-to-Büchi translators: Test control commands
• disabling LTL-to-Büchi translators: Global options
• disabling LTL-to-Büchi translators: Translator section
• disjunction (LTL formula operator): Random LTL formulas
• disjunction (operator semantics in LTL): LTL formulas
• enabling and disabling tests: Global options
• enabling and disabling tests: Special options
• enabling and disabling tests: GlobalOptions section
• enabling LTL-to-Büchi translators: Test control commands
• enabling LTL-to-Büchi translators: Global options
• enabling LTL-to-Büchi translators: Translator section
• enumerated path: State space options
• enumerated path: StateSpaceOptions section
• enumerated path: Random state spaces
• equivalence (LTL formula operator): Random LTL formulas
• equivalence (operator semantics in LTL): LTL formulas
• eventually (LTL formula operator): Random LTL formulas
• eventually (operator semantics in LTL): LTL formulas
• exclusive or (LTL formula operator): Random LTL formulas
• exclusive or (operator semantics in LTL): LTL formulas
• exiting lbtt: Invocation
• `f' (Boolean constant semantics in LTL): LTL formulas
• `F' (LTL formula operator): Random LTL formulas
• `F' (operator semantics in LTL): LTL formulas
• failure analysis, Büchi automata intersection check: Failure analysis commands
• failure analysis, model checking result consistency check: Failure analysis commands
• failure analysis, model checking result cross-comparison test: Failure analysis commands
• false (Boolean constant semantics in LTL): LTL formulas
• file formats, formula input file for lbtt: Special options
• file formats, LTL-to-Büchi translator input file: Format for LTL formulas
• file formats, LTL-to-Büchi translator output file: Format for automata
• finally (LTL formula operator): Random LTL formulas
• finally (operator semantics in LTL): LTL formulas
• formula size: Random LTL formulas
• `FormulaOptions' section (configuration file): FormulaOptions section
• `G' (LTL formula operator): Random LTL formulas
• `G' (operator semantics in LTL): LTL formulas
• generalized Büchi automata, formal definition: Generalized automata
• generalized Büchi automata, LTL-to-Büchi translator output file format: Format for automata
• global model checking: Global options
• global model checking: GlobalOptions section
• global model checking: Model checking result consistency check
• global model checking: Model checking result cross-comparison test
• globally (LTL formula operator): Random LTL formulas
• globally (operator semantics in LTL): LTL formulas
• `GlobalOptions' section (configuration file): GlobalOptions section
• graph density: StateSpaceOptions section
• graph density: Random state spaces
• GraphViz: Data display commands
• henceforth (LTL formula operator): Random LTL formulas
• henceforth (operator semantics in LTL): LTL formulas
• identifiers for LTL-to-Büchi translators: Translator section
• `Implementation' section (configuration file): Translator section
• implication (LTL formula operator): Random LTL formulas
• implication (operator semantics in LTL): LTL formulas
• interactivity modes: Global options
• interactivity modes: GlobalOptions section
• interfacing LTL-to-Büchi translators with lbtt: The lbtt-translate utility
• interfacing LTL-to-Büchi translators with lbtt: Interfacing with lbtt
• internal model checking algorithm: Test round messages
• internal model checking algorithm: StateSpaceOptions section
• internal model checking algorithm: Model checking result cross-comparison test
• invoking lbtt: Invocation
• lbt: The lbtt-translate utility
• lbtt (executable file): Invocation
• lbtt-translate (executable file): The lbtt-translate utility
• local model checking: Global options
• local model checking: GlobalOptions section
• local model checking: Model checking result consistency check
• local model checking: Model checking result cross-comparison test
• log file for test failures: Special options
• LTL formula operators, abbreviated: LTL formula options
• LTL formula operators, abbreviated: FormulaOptions section
• LTL formula operators, supported: Random LTL formulas
• LTL formula, displaying with user command: Data display commands
• LTL formula, generation algorithm: The formula generation algorithm
• LTL formula, identifiers in commands: Command conventions
• LTL formula, LTL-to-Büchi translator input file format: Format for LTL formulas
• LTL formula, output modes: LTL formula options
• LTL formula, output modes: FormulaOptions section
• LTL formula, parameters for generation algorithm: LTL formula options
• LTL formula, parameters for generation algorithm: FormulaOptions section
• LTL formula, parameters for generation algorithm: Random LTL formulas
• LTL formula, random: Random LTL formulas
• LTL formula, reading from a file or standard input: Special options
• LTL formula, size: Random LTL formulas
• LTL-to-Büchi translators, automaton output file format: Format for automata
• LTL-to-Büchi translators, disabling: Test control commands
• LTL-to-Büchi translators, disabling: Global options
• LTL-to-Büchi translators, disabling: Translator section
• LTL-to-Büchi translators, enabling: Test control commands
• LTL-to-Büchi translators, enabling: Global options
• LTL-to-Büchi translators, enabling: Translator section
• LTL-to-Büchi translators, identifiers: Translator section
• LTL-to-Büchi translators, interface requirements: Translator interface
• LTL-to-Büchi translators, interfacing with: The lbtt-translate utility
• LTL-to-Büchi translators, interfacing with: Interfacing with lbtt
• LTL-to-Büchi translators, LTL formula input file format: Format for LTL formulas
• `M' (LTL formula operator): Random LTL formulas
• `M' (operator semantics in LTL): LTL formulas
• minimal requirements for configuration files: Configuration file
• model checking: Overview
• model checking modes: Global options
• model checking modes: GlobalOptions section
• model checking modes: Model checking result consistency check
• model checking modes: Model checking result cross-comparison test
• model checking result consistency check: Model checking result consistency check
• model checking result consistency check, failure analysis: Failure analysis commands
• model checking result cross-comparison test: Model checking result cross-comparison test
• model checking result cross-comparison test, failure analysis: Failure analysis commands
• negation (LTL formula operator): Random LTL formulas
• negation (operator semantics in LTL): LTL formulas
• negation normal form: LTL formula options
• negation normal form: FormulaOptions section
• next time (LTL formula operator): Random LTL formulas
• next time (operator semantics in LTL): LTL formulas
• numeric values in configuration file: Configuration file
• operators, abbreviated: LTL formula options
• operators, abbreviated: FormulaOptions section
• operators, computing distribution for: Test statistics
• operators, computing distribution for: Special options
• operators, computing probabilities for: The formula generation algorithm
• operators, precedence in input files: Special options
• operators, precedence in output messages: Test round messages
• operators, priorities for: LTL formula options
• operators, priorities for: FormulaOptions section
• operators, priorities for: The formula generation algorithm
• operators, priorities for: Random LTL formulas
• parameters for random LTL formula generation algorithm: LTL formula options
• parameters for random LTL formula generation algorithm: FormulaOptions section
• parameters for random LTL formula generation algorithm: Random LTL formulas
• parameters for random state space generation algorithm: State space options
• parameters for random state space generation algorithm: StateSpaceOptions section
• parameters for random state space generation algorithm: Random state spaces
• priorities for formula constants, atomic propositions and operators: LTL formula options
• priorities for formula constants, atomic propositions and operators: FormulaOptions section
• priorities for formula constants, atomic propositions and operators: The formula generation algorithm
• priorities for formula constants, atomic propositions and operators: Random LTL formulas
• probabilities for formula constants and atomic propositions: The formula generation algorithm
• probabilities for formula operators: The formula generation algorithm
• proof for an LTL formula: Failure analysis commands
• quitting lbtt: Test control commands
• quitting lbtt: Invocation
• random connected graph: State space options
• random connected graph: StateSpaceOptions section
• random connected graph: Random state spaces
• random connected graph, generation algorithm: Algorithm for generating connected graphs
• random graph: State space options
• random graph: StateSpaceOptions section
• random graph: Random state spaces
• random LTL formula: Random LTL formulas
• random LTL formula, computing operator distribution: Special options
• random LTL formula, generation algorithm: The formula generation algorithm
• random LTL formula, generation modes: LTL formula options
• random LTL formula, generation modes: FormulaOptions section
• random LTL formula, output modes: LTL formula options
• random LTL formula, output modes: FormulaOptions section
• random LTL formula, parameters for generation algorithm: LTL formula options
• random LTL formula, parameters for generation algorithm: FormulaOptions section
• random LTL formula, parameters for generation algorithm: Random LTL formulas
• random LTL formula, random seed for generation algorithm: FormulaOptions section
• random LTL formula, size: Random LTL formulas
• random path: State space options
• random path: StateSpaceOptions section
• random path: Random state spaces
• random seed, LTL formula generation algorithm: LTL formula options
• random seed, LTL formula generation algorithm: FormulaOptions section
• random seed, state space generation algorithm: StateSpaceOptions section
• random state space: Random state spaces
• random state space, algorithm for generating random connected graphs: Algorithm for generating connected graphs
• random state space, density: StateSpaceOptions section
• random state space, density: Random state spaces
• random state space, generation parameters: State space options
• random state space, generation parameters: StateSpaceOptions section
• random state space, generation parameters: Random state spaces
• random state space, random seed for generation algorithm: State space options
• random state space, random seed for generation algorithm: StateSpaceOptions section
• redirecting command output: Command conventions
• refutation for an LTL formula: Failure analysis commands
• release (LTL formula operator): Random LTL formulas
• release (operator semantics in LTL): LTL formulas
• skipping test rounds: Test control commands
• skipping test rounds: Special options
• SPIN: The lbtt-translate utility
• Spot: The lbtt-translate utility
• starting lbtt: Invocation
• state space: Random state spaces
• state space: Random input generation
• state space, algorithm for generating random connected graphs: Algorithm for generating connected graphs
• state space, density: StateSpaceOptions section
• state space, density: Random state spaces
• state space, displaying with an user command: Data display commands
• state space, formal definition: State spaces
• state space, generation modes: State space options
• state space, generation modes: StateSpaceOptions section
• state space, generation modes: Random state spaces
• state space, generation parameters: State space options
• state space, generation parameters: StateSpaceOptions section
• state space, generation parameters: Random state spaces
• state space, random: Random state spaces
• `StateSpaceOptions' section (configuration file): StateSpaceOptions section
• string values in configuration file: Configuration file
• strong release (LTL formula operator): Random LTL formulas
• strong release (operator semantics in LTL): LTL formulas
• strong until (LTL formula operator): Random LTL formulas
• strong until (operator semantics in LTL): LTL formulas
• supported LTL formula operators: Random LTL formulas
• suppressing output: Special options
• `t' (Boolean constant semantics in LTL): LTL formulas
• testing procedure: Testing procedure
• tests, aborting: Invocation
• tests, against internal model checking algorithm: Test round messages
• tests, against internal model checking algorithm: StateSpaceOptions section
• tests, against internal model checking algorithm: Model checking result cross-comparison test
• tests, Büchi automata intersection emptiness check: Automata intersection emptiness check
• tests, controlling with user commands: Test control commands
• tests, enabling and disabling: Global options
• tests, enabling and disabling: Special options
• tests, enabling and disabling: GlobalOptions section
• tests, failure analysis: Failure analysis commands
• tests, failure report format: Test round messages
• tests, model checking result consistency check: Model checking result consistency check
• tests, model checking result cross-comparison test: Model checking result cross-comparison test
• tests, output example: Test round messages
• tests, profiling LTL-to-Büchi translators: Special options
• tests, skipping test rounds: Test control commands
• tests, skipping test rounds: Special options
• tests, starting: Invocation
• tests, statistics: Test statistics
• timeouts for translators: GlobalOptions section
• `Translator' section (configuration file): Translator section
• true (Boolean constant semantics in LTL): LTL formulas
• truth values in configuration file: Configuration file
• `U' (LTL formula operator): Random LTL formulas
• `U' (operator semantics in LTL): LTL formulas
• unless (LTL formula operator): Random LTL formulas
• unless (operator semantics in LTL): LTL formulas
• until (LTL formula operator): Random LTL formulas
• until (operator semantics in LTL): LTL formulas
• using a test failure log file: Special options
• using the internal model checking algorithm: StateSpaceOptions section
• using the internal model checking algorithm: Model checking result cross-comparison test
• `V' (LTL formula operator): Random LTL formulas
• `V' (operator semantics in LTL): LTL formulas
• verbosity, changing: Test control commands
• verbosity, changing: Global options
• verbosity, changing: GlobalOptions section
• `W' (LTL formula operator): Random LTL formulas
• `W' (operator semantics in LTL): LTL formulas
• weak release (LTL formula operator): Random LTL formulas
• weak release (operator semantics in LTL): LTL formulas
• weak until (LTL formula operator): Random LTL formulas
• weak until (operator semantics in LTL): LTL formulas
• witness: Failure analysis commands
• `X' (LTL formula operator): Random LTL formulas
• `X' (operator semantics in LTL): LTL formulas
• `xor' (LTL formula operator): Random LTL formulas
• `xor' (operator semantics in LTL): LTL formulas