Index

_

__add__() (pyfcstm.model.expr.Expr method) __all__ (in module pyfcstm.bmc) (in module pyfcstm.bmc.ast) (in module pyfcstm.bmc.binding) (in module pyfcstm.bmc.domain) (in module pyfcstm.bmc.engine) (in module pyfcstm.bmc.errors) (in module pyfcstm.bmc.expand) (in module pyfcstm.bmc.listener) (in module pyfcstm.bmc.macro) (in module pyfcstm.bmc.parse) (in module pyfcstm.bmc.pipeline) (in module pyfcstm.bmc.properties) (in module pyfcstm.bmc.query) (in module pyfcstm.bmc.relation) (in module pyfcstm.bmc.source) (in module pyfcstm.bmc.witness) (in module pyfcstm.diagnostics) (in module pyfcstm.diagnostics.analyzers) (in module pyfcstm.dsl.grammar.GrammarListener) (in module pyfcstm.dsl.node) (in module pyfcstm.entry) (in module pyfcstm.entry.bmc) (in module pyfcstm.highlight) (in module pyfcstm.highlight.bmc_query_lexer) (in module pyfcstm.highlight.pygments_lexer) (in module pyfcstm.llm) (in module pyfcstm.model) (in module pyfcstm.model.expr) (in module pyfcstm.model.imports) (in module pyfcstm.model.load) (in module pyfcstm.model.model) (in module pyfcstm.model.plantuml) (in module pyfcstm.simulate) (in module pyfcstm.solver) (in module pyfcstm.solver.domain) (in module pyfcstm.solver.operation) (in module pyfcstm.template) (in module pyfcstm.utils.fixed) (in module pyfcstm.utils.parse) (in module pyfcstm.verify) (in module pyfcstm.verify.algorithms) (in module pyfcstm.verify.algorithms.effect) (in module pyfcstm.verify.algorithms.guard) (in module pyfcstm.verify.algorithms.lifecycle) (in module pyfcstm.verify.algorithms.transition) (in module pyfcstm.verify.encoding) (in module pyfcstm.verify.encoding.expr) (in module pyfcstm.verify.encoding.guard) (in module pyfcstm.verify.encoding.initial) (in module pyfcstm.verify.encoding.lifecycle) (in module pyfcstm.verify.encoding.operation) (in module pyfcstm.verify.encoding.trigger) (in module pyfcstm.verify.inspect_adapter) (in module pyfcstm.verify.registry) (in module pyfcstm.verify.result) (in module pyfcstm.verify.taxonomy) (in module pyfcstm.verify.topology) __and__() (pyfcstm.model.expr.Expr method) __AUTHOR__ (in module pyfcstm.config.meta) __AUTHOR_EMAIL__ (in module pyfcstm.config.meta) __call__() (pyfcstm.model.expr.Expr method) __DESCRIPTION__ (in module pyfcstm.config.meta) __dir__() (in module pyfcstm.bmc) __ge__() (pyfcstm.model.expr.Expr method) __getattr__() (in module pyfcstm.bmc) __gt__() (pyfcstm.model.expr.Expr method) __init__() (pyfcstm.bmc.engine.BmcEngine method) (pyfcstm.bmc.grammar.BmcQueryLexer.BmcQueryLexer method) (pyfcstm.bmc.grammar.BmcQueryParser.BmcQueryParser method) (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.diagnostics.sink.DiagnosticSink method) (pyfcstm.dsl.error.AmbiguityError method) (pyfcstm.dsl.error.CollectingErrorListener method) (pyfcstm.dsl.error.ContextSensitivityError method) (pyfcstm.dsl.error.FullContextAttemptError method) (pyfcstm.dsl.error.GrammarParseError method) (pyfcstm.dsl.error.SyntaxFailError method) (pyfcstm.dsl.error.UnfinishedParsingError method) (pyfcstm.dsl.grammar.GrammarLexer.GrammarLexer method) (pyfcstm.dsl.grammar.GrammarParser.GrammarParser method) (pyfcstm.dsl.listener.GrammarParseListener method) (pyfcstm.entry.base.KeyboardInterrupted method) (pyfcstm.entry.simulate.batch.BatchProcessor method) (pyfcstm.entry.simulate.commands.CommandProcessor method) (pyfcstm.entry.simulate.commands.Settings method) (pyfcstm.entry.simulate.completer.SimulationCompleter method) (pyfcstm.entry.simulate.display.StateDisplay method) (pyfcstm.entry.simulate.logging.SimulateCliFormatter method) (pyfcstm.entry.simulate.logging.SimulateLogHighlighter method) (pyfcstm.entry.simulate.logging.SimulatePlainLogHandler method) (pyfcstm.entry.simulate.logging.SimulateRichLogHandler method) (pyfcstm.entry.simulate.repl.AutoSuggestFromCompleter method) (pyfcstm.entry.simulate.repl.SimulationREPL method) (pyfcstm.render.render.StateMachineCodeRenderer method) (pyfcstm.simulate.runtime.SimulationRuntime method) (pyfcstm.utils.validate.ModelValidationError method) __le__() (pyfcstm.model.expr.Expr method) __lshift__() (pyfcstm.model.expr.Expr method) __lt__() (pyfcstm.model.expr.Expr method) __mod__() (pyfcstm.model.expr.Expr method) __mul__() (pyfcstm.model.expr.Expr method) __neg__() (pyfcstm.model.expr.Expr method)

__or__() (pyfcstm.model.expr.Expr method) __pos__() (pyfcstm.model.expr.Expr method) __post_init__() (pyfcstm.dsl.node.BinaryOp method) (pyfcstm.dsl.node.Boolean method) (pyfcstm.dsl.node.ImportStatement method) (pyfcstm.dsl.node.StateDefinition method) (pyfcstm.dsl.node.UnaryOp method) (pyfcstm.model.expr.BinaryOp method) (pyfcstm.model.expr.Boolean method) (pyfcstm.model.expr.UnaryOp method) (pyfcstm.model.model.State method) (pyfcstm.model.plantuml.PlantUMLOptions method) (pyfcstm.simulate.context.ReadOnlyExecutionContext method) (pyfcstm.solver.operation.OperationBranch method) (pyfcstm.verify.topology.LeafLevelGraph method) __pow__() (pyfcstm.model.expr.Expr method) __radd__() (pyfcstm.model.expr.Expr method) __rand__() (pyfcstm.model.expr.Expr method) __repr__() (pyfcstm.solver.solve.SolveResult method) __rlshift__() (pyfcstm.model.expr.Expr method) __rmod__() (pyfcstm.model.expr.Expr method) __rmul__() (pyfcstm.model.expr.Expr method) __ror__() (pyfcstm.model.expr.Expr method) __rpow__() (pyfcstm.model.expr.Expr method) __rrshift__() (pyfcstm.model.expr.Expr method) __rshift__() (pyfcstm.model.expr.Expr method) __rsub__() (pyfcstm.model.expr.Expr method) __rtruediv__() (pyfcstm.model.expr.Expr method) __rxor__() (pyfcstm.model.expr.Expr method) __str__() (pyfcstm.bmc.ast.BmcExpr method) (pyfcstm.bmc.ast.CallFilter method) (pyfcstm.bmc.ast.CallStepPoint method) (pyfcstm.bmc.ast.CallStepSelector method) (pyfcstm.bmc.binding.BmcBindingDiagnostic method) (pyfcstm.bmc.domain.FrameRef method) (pyfcstm.bmc.domain.StepRef method) (pyfcstm.bmc.query.BmcAssumption method) (pyfcstm.bmc.query.BmcProperty method) (pyfcstm.bmc.query.BmcQuery method) (pyfcstm.bmc.query.InitialSpec method) (pyfcstm.bmc.query.InitialVariablePolicy method) (pyfcstm.bmc.witness.BmcEventDecodePolicy method) (pyfcstm.bmc.witness.BmcReplayMismatch method) (pyfcstm.bmc.witness.BmcReplayResult method) (pyfcstm.bmc.witness.BmcRuntimeFrame method) (pyfcstm.bmc.witness.BmcRuntimeStep method) (pyfcstm.bmc.witness.BmcRuntimeTrace method) (pyfcstm.bmc.witness.BmcSolveResult method) (pyfcstm.bmc.witness.BmcWitnessCallRecord method) (pyfcstm.bmc.witness.BmcWitnessEvent method) (pyfcstm.bmc.witness.BmcWitnessFrame method) (pyfcstm.bmc.witness.BmcWitnessStep method) (pyfcstm.bmc.witness.BmcWitnessTrace method) (pyfcstm.dsl.node.BinaryOp method) (pyfcstm.dsl.node.ChainID method) (pyfcstm.dsl.node.Condition method) (pyfcstm.dsl.node.ConditionalOp method) (pyfcstm.dsl.node.Constant method) (pyfcstm.dsl.node.ConstantDefinition method) (pyfcstm.dsl.node.DefAssignment method) (pyfcstm.dsl.node.DuringAbstractFunction method) (pyfcstm.dsl.node.DuringAspectAbstractFunction method) (pyfcstm.dsl.node.DuringAspectOperations method) (pyfcstm.dsl.node.DuringAspectRefFunction method) (pyfcstm.dsl.node.DuringOperations method) (pyfcstm.dsl.node.DuringRefFunction method) (pyfcstm.dsl.node.EnterAbstractFunction method) (pyfcstm.dsl.node.EnterOperations method) (pyfcstm.dsl.node.EnterRefFunction method) (pyfcstm.dsl.node.EventDefinition method) (pyfcstm.dsl.node.ExitAbstractFunction method) (pyfcstm.dsl.node.ExitOperations method) (pyfcstm.dsl.node.ExitRefFunction method) (pyfcstm.dsl.node.Float method) (pyfcstm.dsl.node.ForceTransitionDefinition method) (pyfcstm.dsl.node.HexInt method) (pyfcstm.dsl.node.ImportDefExactSelector method) (pyfcstm.dsl.node.ImportDefFallbackSelector method) (pyfcstm.dsl.node.ImportDefMapping method) (pyfcstm.dsl.node.ImportDefPatternSelector method) (pyfcstm.dsl.node.ImportDefSetSelector method) (pyfcstm.dsl.node.ImportDefTargetTemplate method) (pyfcstm.dsl.node.ImportEventMapping method) (pyfcstm.dsl.node.ImportStatement method) (pyfcstm.dsl.node.InitialAssignment method) (pyfcstm.dsl.node.Literal method) (pyfcstm.dsl.node.Name method) (pyfcstm.dsl.node.Operation method) (pyfcstm.dsl.node.OperationalDeprecatedAssignment method) (pyfcstm.dsl.node.OperationAssignment method) (pyfcstm.dsl.node.OperationIf method) (pyfcstm.dsl.node.Paren method) (pyfcstm.dsl.node.Preamble method) (pyfcstm.dsl.node.StateDefinition method) (pyfcstm.dsl.node.StateMachineDSLProgram method) (pyfcstm.dsl.node.TransitionDefinition method) (pyfcstm.dsl.node.UFunc method) (pyfcstm.dsl.node.UnaryOp method) (pyfcstm.model.expr.Expr method) __sub__() (pyfcstm.model.expr.Expr method) __TITLE__ (in module pyfcstm.config.meta) __truediv__() (pyfcstm.model.expr.Expr method) __VERSION__ (in module pyfcstm.config.meta) __xor__() (pyfcstm.model.expr.Expr method)

A

absolute() (pyfcstm.bmc.ast.CallStepPoint class method) abstract_error_mode (pyfcstm.simulate.runtime.SimulationRuntime property) abstract_handler() (in module pyfcstm.simulate.decorators) abstract_handler_errors (pyfcstm.simulate.runtime.SimulationRuntime property) abstract_on_during_aspects (pyfcstm.model.model.State property) abstract_on_durings (pyfcstm.model.model.State property) abstract_on_enters (pyfcstm.model.model.State property) abstract_on_exits (pyfcstm.model.model.State property) ActionBlock (class in pyfcstm.bmc.macro) ActionInfo (class in pyfcstm.diagnostics.inspect) Active (class in pyfcstm.bmc.ast) active_state() (pyfcstm.bmc.relation.BmcTraceSymbols method) add_builtins_to_env() (in module pyfcstm.utils.jinja2) add_settings_for_env() (in module pyfcstm.utils.jinja2) affecting_variables() (pyfcstm.diagnostics.analyzers.use_def.UseDefGraph method) AlgorithmResult (class in pyfcstm.verify.result) aliases (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer attribute) (pyfcstm.highlight.pygments_lexer.FcstmLexer attribute)

ALL (in module pyfcstm.dsl.node) all() (pyfcstm.bmc.ast.CallStepSelector class method) allocate() (pyfcstm.bmc.relation.BmcTraceSymbols class method) allows_semantic_delta (pyfcstm.bmc.source.MacroStepSource property) AmbiguityError (class in pyfcstm.dsl.error) analyse_text() (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer static method) (pyfcstm.highlight.pygments_lexer.FcstmLexer static method) and_() (pyfcstm.bmc.macro.BoolTemplate class method) (pyfcstm.model.expr.Expr method) assemble_state_machine_imports() (in module pyfcstm.model.imports) assign_event_colors() (in module pyfcstm.model.plantuml) AstExportable (class in pyfcstm.model.base) ASTNode (class in pyfcstm.dsl.node) atom() (pyfcstm.bmc.macro.BoolTemplate class method) atom_name (pyfcstm.bmc.macro.GuardRequirement property) auto_decode() (in module pyfcstm.utils.decode) AutoSuggestFromCompleter (class in pyfcstm.entry.simulate.repl)

B

BatchProcessor (class in pyfcstm.entry.simulate.batch) BinaryOp (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) bind_bmc_query() (in module pyfcstm.bmc.binding) bind_bmc_query_structure() (in module pyfcstm.bmc.binding) BmcAbstractCallRecord (class in pyfcstm.bmc.relation) BmcAssumption (class in pyfcstm.bmc.query) BmcBindingDiagnostic (class in pyfcstm.bmc.binding) BmcBuildError (class in pyfcstm.bmc.errors) BmcCaseRelation (class in pyfcstm.bmc.relation) BmcCondExpr (class in pyfcstm.bmc.ast) BmcCoreFormula (class in pyfcstm.bmc.relation) BmcDomain (class in pyfcstm.bmc.domain) BmcEngine (class in pyfcstm.bmc.engine) BmcError (class in pyfcstm.bmc.errors) BmcEventDecodePolicy (class in pyfcstm.bmc.witness) BmcExpr (class in pyfcstm.bmc.ast) BmcNumExpr (class in pyfcstm.bmc.ast) BmcOptions (class in pyfcstm.bmc.engine) BmcPreparedContext (class in pyfcstm.bmc.engine) BmcProperty (class in pyfcstm.bmc.query) BmcPropertyFormula (class in pyfcstm.bmc.properties) BmcQuery (class in pyfcstm.bmc.query) BmcQueryLexer (class in pyfcstm.bmc.grammar.BmcQueryLexer) BmcQueryParseError (class in pyfcstm.bmc.errors) BmcQueryParseListener (class in pyfcstm.bmc.listener) BmcQueryParser (class in pyfcstm.bmc.grammar.BmcQueryParser) BmcQueryParserListener (class in pyfcstm.bmc.grammar.BmcQueryParserListener) BmcReplayMismatch (class in pyfcstm.bmc.witness) BmcReplayResult (class in pyfcstm.bmc.witness) BmcRuntimeFrame (class in pyfcstm.bmc.witness) BmcRuntimeStep (class in pyfcstm.bmc.witness) BmcRuntimeTrace (class in pyfcstm.bmc.witness)

BmcSolveResult (class in pyfcstm.bmc.witness) BmcSolveStatus (in module pyfcstm.bmc.witness) BmcStepRelation (class in pyfcstm.bmc.relation) BmcTraceSymbols (class in pyfcstm.bmc.relation) BmcWitnessCallRecord (class in pyfcstm.bmc.witness) BmcWitnessEvent (class in pyfcstm.bmc.witness) BmcWitnessFrame (class in pyfcstm.bmc.witness) BmcWitnessStep (class in pyfcstm.bmc.witness) BmcWitnessTrace (class in pyfcstm.bmc.witness) Boolean (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) BoolLiteral (class in pyfcstm.bmc.ast) BoolTemplate (class in pyfcstm.bmc.macro) bound (pyfcstm.bmc.binding.BoundProperty property) (pyfcstm.bmc.engine.BmcPreparedContext property) (pyfcstm.bmc.properties.BmcPropertyFormula property) BoundAssumption (class in pyfcstm.bmc.binding) BoundBmcQuery (class in pyfcstm.bmc.binding) BoundInitialSpec (class in pyfcstm.bmc.binding) BoundProperty (class in pyfcstm.bmc.binding) BoundReference (class in pyfcstm.bmc.binding) BranchFeasibility (class in pyfcstm.solver.domain) brief_stack (pyfcstm.simulate.runtime.SimulationRuntime property) build_bmc_ast_from_parse_tree() (in module pyfcstm.bmc.parse) build_bmc_core_formula() (in module pyfcstm.bmc.relation) build_bmc_domain() (in module pyfcstm.bmc.domain) build_bmc_output() (in module pyfcstm.entry.bmc) build_fallback_case() (in module pyfcstm.bmc.macro) build_inspect_json() (in module pyfcstm.entry.inspect) build_inspect_output() (in module pyfcstm.entry.inspect) build_leaf_level_macro_graph() (in module pyfcstm.verify.topology) build_plantuml_output() (in module pyfcstm.entry.plantuml) build_semantic_delta_case() (in module pyfcstm.bmc.macro) build_use_def_graph() (in module pyfcstm.diagnostics.analyzers.use_def)

C

CALL_COUNT_SCALING_ORDER (in module pyfcstm.verify.taxonomy) call_filter (pyfcstm.bmc.ast.Called property) CallCount (class in pyfcstm.bmc.ast) CallCountScaling (in module pyfcstm.verify.taxonomy) Called (class in pyfcstm.bmc.ast) CallFilter (class in pyfcstm.bmc.ast) CallStepPoint (class in pyfcstm.bmc.ast) CallStepSelector (class in pyfcstm.bmc.ast) canonical_text (pyfcstm.dsl.node.ComboEventTerm property) (pyfcstm.dsl.node.ComboGuardTerm property) (pyfcstm.dsl.node.ComboTransitionTrigger property) (pyfcstm.dsl.node.ComboTriggerTerm property) Case (class in pyfcstm.bmc.ast) case_path_condition() (in module pyfcstm.bmc.macro) case_registry (pyfcstm.bmc.relation.BmcStepRelation property) case_selector() (pyfcstm.bmc.relation.BmcTraceSymbols method) cases (pyfcstm.bmc.macro.MacroStepFormal property) ChainID (class in pyfcstm.dsl.node) check_errors() (pyfcstm.dsl.error.CollectingErrorListener method) check_expr_safety() (in module pyfcstm.solver.safety) check_expr_safety_for_effect() (in module pyfcstm.solver.safety) check_unfinished_parsing_error() (pyfcstm.dsl.error.CollectingErrorListener method) clear_abstract_handler_session() (pyfcstm.simulate.runtime.SimulationRuntime method) clear_all_abstract_handlers() (pyfcstm.simulate.runtime.SimulationRuntime method) cli (in module pyfcstm.entry.cli), [1] ClickErrorException (class in pyfcstm.entry.base) ClickWarningException (class in pyfcstm.entry.base) Closedness (in module pyfcstm.verify.taxonomy) CODE_REGISTRY (in module pyfcstm.diagnostics.codes) CodeFieldSpec (class in pyfcstm.diagnostics.codes) CodeSpec (class in pyfcstm.diagnostics.codes) CodesSchemaError (class in pyfcstm.diagnostics.codes) collect (pyfcstm.diagnostics.sink.DiagnosticSink property) collect_combo_warnings() (in module pyfcstm.diagnostics.analyzers.combo) collect_const_fold_warnings() (in module pyfcstm.diagnostics.analyzers.const_fold) collect_data_flow_warnings() (in module pyfcstm.diagnostics.analyzers.data_flow) collect_design_health_warnings() (in module pyfcstm.diagnostics.analyzers.design_health) collect_event_transitions() (in module pyfcstm.model.plantuml) collect_expr_variables() (in module pyfcstm.diagnostics.analyzers.use_def) collect_naming_warnings() (in module pyfcstm.diagnostics.analyzers.naming) collect_numeric_warnings() (in module pyfcstm.diagnostics.analyzers.numeric) collect_redundancy_warnings() (in module pyfcstm.diagnostics.analyzers.redundancy) collect_structural_warnings() (in module pyfcstm.diagnostics.analyzers.structural) collect_threshold_warnings() (in module pyfcstm.diagnostics.analyzers.thresholds) collect_transition_infos() (in module pyfcstm.diagnostics.analyzers.transition_info) collect_type_warnings() (in module pyfcstm.diagnostics.analyzers.type_shape)

CollectingErrorListener (class in pyfcstm.dsl.error) COMBO_GUARD_VERIFY_REPLACEMENT_CODES (in module pyfcstm.diagnostics.inspect) ComboEventTerm (class in pyfcstm.dsl.node) ComboGuardTerm (class in pyfcstm.dsl.node) ComboOriginInfo (class in pyfcstm.diagnostics.inspect) ComboOriginRef (class in pyfcstm.model.model) ComboOriginRefInfo (class in pyfcstm.diagnostics.inspect) ComboOriginTermInfo (class in pyfcstm.diagnostics.inspect) ComboTransitionTrigger (class in pyfcstm.dsl.node) ComboTriggerTerm (class in pyfcstm.dsl.node) command_wrap() (in module pyfcstm.entry.base) CommandProcessor (class in pyfcstm.entry.simulate.commands) CommandResult (class in pyfcstm.entry.simulate.commands) compile_bmc_property() (in module pyfcstm.bmc.properties) compile_bmc_query() (in module pyfcstm.bmc.pipeline) COMPLEXITY_TIER_ORDER (in module pyfcstm.verify.taxonomy) ComplexityTier (in module pyfcstm.verify.taxonomy) composite_init_guards_incomplete() (in module pyfcstm.verify.algorithms.transition) CondBinaryOp (class in pyfcstm.bmc.ast) CondConditionalOp (class in pyfcstm.bmc.ast) Condition (class in pyfcstm.dsl.node) ConditionalOp (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) CondUnaryOp (class in pyfcstm.bmc.ast) configure_simulate_cli_logger() (in module pyfcstm.entry.simulate.logging) Constant (class in pyfcstm.dsl.node) ConstantDefinition (class in pyfcstm.dsl.node) ConstValue (in module pyfcstm.diagnostics.analyzers.const_fold) CONTEXT_SETTINGS (in module pyfcstm.entry.base) ContextSensitivityError (class in pyfcstm.dsl.error) copy_one_file() (pyfcstm.render.render.StateMachineCodeRenderer method) copy_session_configuration_to() (pyfcstm.simulate.runtime.SimulationRuntime method) counterexample_found (pyfcstm.bmc.witness.BmcSolveResult property) create_completer() (pyfcstm.entry.simulate.commands.CommandProcessor method) create_cross_platform_output_func() (in module pyfcstm.entry.simulate.batch) create_env() (in module pyfcstm.render.env) create_expr_render_template() (in module pyfcstm.render.expr) create_local_plantuml_backend() (in module pyfcstm.entry.visualize) create_remote_plantuml_backend() (in module pyfcstm.entry.visualize) create_simulate_log_handler() (in module pyfcstm.entry.simulate.logging) create_stmt_render_template() (in module pyfcstm.render.statement) create_z3_vars_from_models() (in module pyfcstm.solver.expr) current_state (pyfcstm.simulate.runtime.SimulationRuntime property) Cycle (class in pyfcstm.bmc.ast) cycle() (pyfcstm.simulate.runtime.SimulationRuntime method) CycleCase (class in pyfcstm.bmc.macro) CycleResult (class in pyfcstm.simulate.runtime)

D

dead_guard() (in module pyfcstm.verify.algorithms.guard) decode_bmc_witness() (in module pyfcstm.bmc.witness) DefAssignment (class in pyfcstm.dsl.node) DEFAULT_DEEP_HIERARCHY_THRESHOLD (in module pyfcstm.diagnostics.inspect) DEFAULT_LARGE_COMPOSITE_THRESHOLD (in module pyfcstm.diagnostics.inspect) DEFAULT_VAR_TO_LEAF_RATIO_THRESHOLD (in module pyfcstm.diagnostics.inspect) delta_flag() (pyfcstm.bmc.relation.BmcTraceSymbols method) dependencies_of() (pyfcstm.diagnostics.analyzers.use_def.UseDefGraph method) DetailLevelLiteral (in module pyfcstm.model.plantuml) detect_headless_environment() (in module pyfcstm.entry.visualize) diagnostics (pyfcstm.diagnostics.sink.DiagnosticSink property)

DiagnosticSink (class in pyfcstm.diagnostics.sink) DomainConstraint (class in pyfcstm.solver.domain) DomainSource (class in pyfcstm.solver.domain) DuringAbstractFunction (class in pyfcstm.dsl.node) DuringAspectAbstractFunction (class in pyfcstm.dsl.node) DuringAspectOperations (class in pyfcstm.dsl.node) DuringAspectRefFunction (class in pyfcstm.dsl.node) DuringAspectStatement (class in pyfcstm.dsl.node) DuringOperations (class in pyfcstm.dsl.node) DuringRefFunction (class in pyfcstm.dsl.node) DuringStatement (class in pyfcstm.dsl.node)

E

effect_contradicts_guard() (in module pyfcstm.verify.algorithms.effect) effect_no_op_under_guard() (in module pyfcstm.verify.algorithms.effect) effective_step (pyfcstm.bmc.ast.CallFilter property) eligible_for_inspect() (in module pyfcstm.verify.inspect_adapter) emit() (pyfcstm.diagnostics.sink.DiagnosticSink method) enter_postcondition_implies_during_precondition() (in module pyfcstm.verify.algorithms.lifecycle) EnterAbstractFunction (class in pyfcstm.dsl.node) EnterOperations (class in pyfcstm.dsl.node) EnterRefFunction (class in pyfcstm.dsl.node) EnterStatement (class in pyfcstm.dsl.node) entry_source() (in module pyfcstm.bmc.source) eq() (pyfcstm.model.expr.Expr method) error_info (pyfcstm.simulate.runtime.SimulationRuntime property) escape_plantuml_table_cell() (in module pyfcstm.model.plantuml) evaluate() (pyfcstm.bmc.macro.BoolTemplate method) Event (class in pyfcstm.bmc.ast) (class in pyfcstm.model.model) event_by_id() (pyfcstm.bmc.domain.BmcDomain method) event_by_path() (pyfcstm.bmc.domain.BmcDomain method) event_emission_to_consumer_reachable() (in module pyfcstm.verify.topology) event_id_to_path() (pyfcstm.bmc.domain.BmcDomain method) event_input() (pyfcstm.bmc.domain.BmcDomain method) (pyfcstm.bmc.relation.BmcTraceSymbols method) event_path_to_id() (pyfcstm.bmc.domain.BmcDomain method) EventAssumption (class in pyfcstm.bmc.query) EventCardinalityAssumption (class in pyfcstm.bmc.query) EventDefinition (class in pyfcstm.dsl.node) EventDomainEntry (class in pyfcstm.bmc.domain) EventInfo (class in pyfcstm.diagnostics.inspect) EventInputRef (class in pyfcstm.bmc.domain) EventUse (class in pyfcstm.bmc.macro) execute_commands() (pyfcstm.entry.simulate.batch.BatchProcessor method) execute_operations() (in module pyfcstm.solver.operation) execute_operations_domain() (in module pyfcstm.solver.operation) exit_code (pyfcstm.entry.base.KeyboardInterrupted attribute) EXIT_ROOT_SINK (in module pyfcstm.verify.topology) EXIT_STATE (in module pyfcstm.dsl.node) ExitAbstractFunction (class in pyfcstm.dsl.node) exitAssume_clause() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitAtomExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitBinaryExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitBinaryExprFromCondCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitBinaryExprFromNumCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitBinaryExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitBinaryExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitBmc_boolean_atom() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitBmc_cond_expression_entry() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitBmc_num_expression_entry() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitBool_cmp_op() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitBool_literal() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitCall_argument() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCall_argument_value() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCall_arguments() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCall_step_point() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCall_step_selector() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCallCountExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCardinality_assume() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitChain_combo_guard_alias() (pyfcstm.dsl.listener.GrammarParseListener method) exitChain_combo_trigger() (pyfcstm.dsl.listener.GrammarParseListener method) exitChain_id() (pyfcstm.dsl.listener.GrammarParseListener method) exitCheck_clause() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitCombo_event_term() (pyfcstm.dsl.listener.GrammarParseListener method) exitCombo_guard_term() (pyfcstm.dsl.listener.GrammarParseListener method) exitCombo_transition_trigger() (pyfcstm.dsl.listener.GrammarParseListener method) exitCombo_trigger_term() (pyfcstm.dsl.listener.GrammarParseListener method) exitCompositeStateDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitCondition() (pyfcstm.dsl.listener.GrammarParseListener method) exitConditionalCStyleCondNum() (pyfcstm.dsl.listener.GrammarParseListener method) exitConditionalCStyleExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitConditionalCStyleExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitConstant_definition() (pyfcstm.dsl.listener.GrammarParseListener method) exitCycleExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitDef_assignment() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringAbstractFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringAspectAbstractFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringAspectOperations() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringAspectRefFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringOperations() (pyfcstm.dsl.listener.GrammarParseListener method) exitDuringRefFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitEnterAbstractFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitEnterOperations() (pyfcstm.dsl.listener.GrammarParseListener method) exitEnterRefFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitEntry_chain_combo_leading_guard() (pyfcstm.dsl.listener.GrammarParseListener method) exitEntry_chain_combo_trigger() (pyfcstm.dsl.listener.GrammarParseListener method) exitEntry_chain_combo_trigger_term() (pyfcstm.dsl.listener.GrammarParseListener method)

exitEntry_combo_transition_trigger() (pyfcstm.dsl.listener.GrammarParseListener method) exitEntryTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitEvent_assume() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitEvent_cycle_selector() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitEvent_definition() (pyfcstm.dsl.listener.GrammarParseListener method) exitEvent_range_selector() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitExitAbstractFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitExitAllForceTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitExitForceTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitExitOperations() (pyfcstm.dsl.listener.GrammarParseListener method) exitExitRefFunc() (pyfcstm.dsl.listener.GrammarParseListener method) exitExitTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitFrame_assume() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitFrame_selector() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitFrameVarExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitFuncExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitFuncExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitGeneric_expression() (pyfcstm.dsl.listener.GrammarParseListener method) exitIdExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitIf_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitImport_def_mapping() (pyfcstm.dsl.listener.GrammarParseListener method) exitImport_event_mapping() (pyfcstm.dsl.listener.GrammarParseListener method) exitImport_mapping_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitImport_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitImportDefExactSelector() (pyfcstm.dsl.listener.GrammarParseListener method) exitImportDefFallbackSelector() (pyfcstm.dsl.listener.GrammarParseListener method) exitImportDefPatternSelector() (pyfcstm.dsl.listener.GrammarParseListener method) exitImportDefSetSelector() (pyfcstm.dsl.listener.GrammarParseListener method) exitInit_clause() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitInit_havoc_clause() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitInit_target() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitInit_var_ref() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitInitial_assignment() (pyfcstm.dsl.listener.GrammarParseListener method) exitInteger_literal() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitLeafStateDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitLiteralExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitLiteralExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitLiteralExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitLocal_combo_event_term() (pyfcstm.dsl.listener.GrammarParseListener method) exitLocal_combo_leading_guard() (pyfcstm.dsl.listener.GrammarParseListener method) exitLocal_combo_trigger() (pyfcstm.dsl.listener.GrammarParseListener method) exitLocal_combo_trigger_term() (pyfcstm.dsl.listener.GrammarParseListener method) exitMath_const() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitMathConstExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitMathConstExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitNormalAllForceTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitNormalForceTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitNormalTransitionDefinition() (pyfcstm.dsl.listener.GrammarParseListener method) exitNum_literal() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitOperation_assignment() (pyfcstm.dsl.listener.GrammarParseListener method) exitOperation_block() (pyfcstm.dsl.listener.GrammarParseListener method) exitOperation_program() (pyfcstm.dsl.listener.GrammarParseListener method) exitOperational_assignment() (pyfcstm.dsl.listener.GrammarParseListener method) exitOperational_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitOperational_statement_set() (pyfcstm.dsl.listener.GrammarParseListener method) ExitOperations (class in pyfcstm.dsl.node) exitParenExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitParenExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitParenExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitPreamble_program() (pyfcstm.dsl.listener.GrammarParseListener method) exitPreamble_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitProperty_body() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitProperty_kind() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitQuery() (pyfcstm.bmc.listener.BmcQueryParseListener method) ExitRefFunction (class in pyfcstm.dsl.node) exitResponse_property_body() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitState_inner_statement() (pyfcstm.dsl.listener.GrammarParseListener method) exitState_machine_dsl() (pyfcstm.dsl.listener.GrammarParseListener method) ExitStatement (class in pyfcstm.dsl.node) exitString_list() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitString_literal() (pyfcstm.bmc.listener.BmcQueryParseListener method) exitUnaryExprCond() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) exitUnaryExprInit() (pyfcstm.dsl.listener.GrammarParseListener method) exitUnaryExprNum() (pyfcstm.bmc.listener.BmcQueryParseListener method) (pyfcstm.dsl.listener.GrammarParseListener method) expand_macro_step_cases() (in module pyfcstm.bmc.expand) Expr (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) expr_to_z3() (in module pyfcstm.solver.expr) ExprDomain (class in pyfcstm.solver.domain) extract_template() (in module pyfcstm.template)

F

FallbackUnknownRisk (in module pyfcstm.verify.taxonomy) false() (pyfcstm.bmc.macro.BoolTemplate class method) FcstmBmcQueryLexer (class in pyfcstm.highlight.bmc_query_lexer) FcstmLexer (class in pyfcstm.highlight.pygments_lexer) filenames (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer attribute) (pyfcstm.highlight.pygments_lexer.FcstmLexer attribute) finalize_or_raise() (pyfcstm.diagnostics.sink.DiagnosticSink method) FinitenessReport (class in pyfcstm.verify.topology) Float (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) FloatLiteral (class in pyfcstm.bmc.ast) fn_expr_render() (in module pyfcstm.render.expr) fn_stmt_render() (in module pyfcstm.render.statement) fn_stmts_render() (in module pyfcstm.render.statement) fold_condition_expression() (in module pyfcstm.diagnostics.analyzers.const_fold) fold_numeric_expression() (in module pyfcstm.diagnostics.analyzers.const_fold) forced_guard_unsat_under_init() (in module pyfcstm.verify.algorithms.guard) ForcedTransitionInfo (class in pyfcstm.diagnostics.inspect) ForceTransitionDefinition (class in pyfcstm.dsl.node) ForLlmSpec (class in pyfcstm.diagnostics.codes)

format_action_text() (in module pyfcstm.model.plantuml) format_current_state() (pyfcstm.entry.simulate.display.StateDisplay method) format_event_name() (in module pyfcstm.model.plantuml) format_events() (pyfcstm.entry.simulate.display.StateDisplay method) format_line() (pyfcstm.utils.validate.ModelDiagnostic method) format_multiline_comment() (in module pyfcstm.utils.doc) format_state_name() (in module pyfcstm.model.plantuml) format_table() (pyfcstm.entry.simulate.display.StateDisplay method) formula (pyfcstm.bmc.relation.BmcCaseRelation property) FormulaSizeScaling (in module pyfcstm.verify.taxonomy) frame0_state_ids (pyfcstm.bmc.domain.BmcDomain property) frame_state() (pyfcstm.bmc.relation.BmcTraceSymbols method) frame_var() (pyfcstm.bmc.relation.BmcTraceSymbols method) FrameAssumption (class in pyfcstm.bmc.query) FrameRef (class in pyfcstm.bmc.domain) FrameVar (class in pyfcstm.bmc.ast) from_json() (pyfcstm.utils.json.IJsonOp class method) from_value() (pyfcstm.model.plantuml.PlantUMLOptions class method) FullContextAttemptError (class in pyfcstm.dsl.error) func_name (pyfcstm.model.model.OnAspect property) (pyfcstm.model.model.OnStage property)

G

gamma_flag() (pyfcstm.bmc.relation.BmcTraceSymbols method) get() (pyfcstm.entry.simulate.commands.Settings method) get_abstract_handlers() (pyfcstm.simulate.runtime.SimulationRuntime method) get_completions() (pyfcstm.entry.simulate.completer.SimulationCompleter method) get_current_event_completion_items() (in module pyfcstm.entry.simulate.events) get_current_event_display_items() (in module pyfcstm.entry.simulate.events) get_fbmcq_language_guide_prompt_for_llm() (in module pyfcstm.llm.fbmcq) get_fbmcq_language_guide_prompt_metadata_for_llm() (in module pyfcstm.llm.fbmcq) get_fbmcq_language_guide_prompt_path_for_llm() (in module pyfcstm.llm.fbmcq) get_full_state_path() (pyfcstm.simulate.context.ReadOnlyExecutionContext method) get_grammar_guide_prompt_for_llm() (in module pyfcstm.llm.fcstm) get_grammar_guide_prompt_metadata_for_llm() (in module pyfcstm.llm.fcstm) get_grammar_guide_prompt_path_for_llm() (in module pyfcstm.llm.fcstm) get_guide_prompt() (in module pyfcstm.llm._resources) get_guide_prompt_metadata() (in module pyfcstm.llm._resources) get_guide_prompt_path() (in module pyfcstm.llm._resources)

get_handler_metadata() (in module pyfcstm.simulate.decorators) get_logger() (in module pyfcstm.utils.logging) get_state_name() (pyfcstm.simulate.context.ReadOnlyExecutionContext method) get_suggestion() (pyfcstm.entry.simulate.repl.AutoSuggestFromCompleter method) get_template_info() (in module pyfcstm.template) get_var() (pyfcstm.simulate.context.ReadOnlyExecutionContext method) get_visualize_cache_dir() (in module pyfcstm.entry.visualize) GrammarGuidePromptIntegrityError (class in pyfcstm.llm.error) GrammarGuidePromptPathUnavailableError (class in pyfcstm.llm.error) GrammarItemError (class in pyfcstm.dsl.error) GrammarLexer (class in pyfcstm.dsl.grammar.GrammarLexer) GrammarParseError (class in pyfcstm.dsl.error) GrammarParseListener (class in pyfcstm.dsl.listener) GrammarParser (class in pyfcstm.dsl.grammar.GrammarParser) GrammarParserListener (class in pyfcstm.dsl.grammar.GrammarParserListener) guard_tautology() (in module pyfcstm.verify.algorithms.guard) GuardRequirement (class in pyfcstm.bmc.macro)

H

has_abstract_handlers() (pyfcstm.simulate.runtime.SimulationRuntime method) has_errors() (pyfcstm.diagnostics.sink.DiagnosticSink method) has_template() (in module pyfcstm.template) has_var() (pyfcstm.simulate.context.ReadOnlyExecutionContext method)

havoc_names() (pyfcstm.bmc.binding.BoundInitialSpec method) (pyfcstm.bmc.query.InitialVariablePolicy method) HexInt (class in pyfcstm.dsl.node) highlight() (pyfcstm.entry.simulate.logging.SimulateLogHighlighter method) HumanRenderOptions (class in pyfcstm.diagnostics.inspect_render)

I

Identifier (class in pyfcstm.dsl.node) IdentifierKeywordLanguage (in module pyfcstm.utils.text) if_then_else() (pyfcstm.model.expr.Expr method) IfBlock (class in pyfcstm.model.model) IfBlockBranch (class in pyfcstm.model.model) IJsonOp (class in pyfcstm.utils.json) ImportDefExactSelector (class in pyfcstm.dsl.node) ImportDefFallbackSelector (class in pyfcstm.dsl.node) ImportDefMapping (class in pyfcstm.dsl.node) ImportDefPatternSelector (class in pyfcstm.dsl.node) ImportDefSelector (class in pyfcstm.dsl.node) ImportDefSetSelector (class in pyfcstm.dsl.node) ImportDefTargetTemplate (class in pyfcstm.dsl.node) ImportEventMapping (class in pyfcstm.dsl.node) ImportMappingStatement (class in pyfcstm.dsl.node) ImportStatement (class in pyfcstm.dsl.node) incomplete (pyfcstm.bmc.witness.BmcSolveResult property) InevitabilityReport (class in pyfcstm.verify.topology) INIT_CASE_PATH (in module pyfcstm.bmc.source) init_source() (in module pyfcstm.bmc.source) INIT_STATE (in module pyfcstm.dsl.node) init_transitions (pyfcstm.model.model.State property) InitialAssignment (class in pyfcstm.dsl.node) InitialSpec (class in pyfcstm.bmc.query) InitialVariablePolicy (class in pyfcstm.bmc.query) input_event_paths (pyfcstm.bmc.witness.BmcWitnessStep property) INSPECT_LLM_SCHEMA_VERSION (in module pyfcstm.diagnostics.inspect_render) inspect_model() (in module pyfcstm.diagnostics.inspect) inspect_output_suffix_warning() (in module pyfcstm.diagnostics.inspect_render) InspectAccessForbiddenError (class in pyfcstm.verify.inspect_adapter) InspectRunResult (class in pyfcstm.verify.inspect_adapter) Int16 (class in pyfcstm.utils.fixed) Int32 (class in pyfcstm.utils.fixed)

Int64 (class in pyfcstm.utils.fixed) Int8 (class in pyfcstm.utils.fixed) Integer (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) IntLiteral (class in pyfcstm.bmc.ast) InvalidBmcDomain (class in pyfcstm.bmc.errors) InvalidBmcEncoding (class in pyfcstm.bmc.errors) InvalidBmcQuery (class in pyfcstm.bmc.errors) is_abstract_handler() (in module pyfcstm.simulate.decorators) is_aspect (pyfcstm.model.model.OnAspect property) (pyfcstm.model.model.OnStage property) is_binary_file() (in module pyfcstm.utils.binary) is_c_public_identifier_reserved() (in module pyfcstm.utils.jinja2) is_combo (pyfcstm.dsl.node.ComboTransitionTrigger property) is_empty (pyfcstm.bmc.query.InitialVariablePolicy property) is_ended (pyfcstm.simulate.runtime.SimulationRuntime property) is_error() (pyfcstm.utils.validate.ModelDiagnostic method) is_error_state (pyfcstm.simulate.runtime.SimulationRuntime property) is_leaf_state (pyfcstm.model.model.State property) is_overlap() (in module pyfcstm.solver.logical) is_ref (pyfcstm.model.model.OnAspect property) (pyfcstm.model.model.OnStage property) is_root_state (pyfcstm.model.model.State property) is_sat (in module pyfcstm.verify.encoding._core) is_sat() (in module pyfcstm.solver.logical) is_state_resolve_event_path() (in module pyfcstm.simulate.utils) is_stoppable (pyfcstm.model.model.State property) is_valid() (in module pyfcstm.solver.logical) iter_inspect_eligible() (in module pyfcstm.verify.inspect_adapter) iter_on_during_after_aspect_recursively() (pyfcstm.model.model.State method) iter_on_during_aspect_recursively() (pyfcstm.model.model.State method) iter_on_during_before_aspect_recursively() (pyfcstm.model.model.State method) IValidatable (class in pyfcstm.utils.validate)

J

json (pyfcstm.utils.json.IJsonOp property)

K

KeyboardInterrupted (class in pyfcstm.entry.base) kind (pyfcstm.bmc.binding.BoundProperty property) (pyfcstm.bmc.witness.BmcSolveResult property)

KNOWN_SPANLESS_CODES (in module pyfcstm.diagnostics.inspect)

L

LeafLevelGraph (class in pyfcstm.verify.topology) list_all() (pyfcstm.entry.simulate.commands.Settings method) list_on_during_aspect_recursively() (pyfcstm.model.model.State method) list_on_during_aspects() (pyfcstm.model.model.State method) list_on_durings() (pyfcstm.model.model.State method) list_on_enters() (pyfcstm.model.model.State method) list_on_exits() (pyfcstm.model.model.State method) list_templates() (in module pyfcstm.template)

list_variables() (pyfcstm.model.expr.Expr method) Literal (class in pyfcstm.dsl.node) load_codes() (in module pyfcstm.diagnostics.codes) load_plantumlcli_classes() (in module pyfcstm.entry.visualize) load_state_machine_from_file() (in module pyfcstm.model.load) load_state_machine_from_text() (in module pyfcstm.model.load) log() (pyfcstm.entry.simulate.display.StateDisplay method) LogLevel (class in pyfcstm.entry.simulate.commands)

M

MacroExpansionOptions (class in pyfcstm.bmc.expand) MacroStepFormal (class in pyfcstm.bmc.macro) MacroStepSource (class in pyfcstm.bmc.source) make_diag() (in module pyfcstm.verify.result) MathConst (class in pyfcstm.bmc.ast) merge_definedness_constraints() (in module pyfcstm.solver.domain) merge_operation_definedness() (in module pyfcstm.solver.operation) mimetypes (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer attribute) (pyfcstm.highlight.pygments_lexer.FcstmLexer attribute) mode (pyfcstm.bmc.binding.BoundInitialSpec property) model (pyfcstm.bmc.engine.BmcEngine property) ModelDiagnostic (class in pyfcstm.utils.validate) ModelInspect (class in pyfcstm.diagnostics.inspect) ModelLookupError (class in pyfcstm.utils.validate) ModelMetrics (class in pyfcstm.diagnostics.inspect) ModelValidationError (class in pyfcstm.utils.validate) ModelValueError (class in pyfcstm.utils.validate) module pyfcstm pyfcstm.bmc pyfcstm.bmc.ast pyfcstm.bmc.binding pyfcstm.bmc.domain pyfcstm.bmc.engine pyfcstm.bmc.errors pyfcstm.bmc.expand pyfcstm.bmc.grammar pyfcstm.bmc.grammar.BmcQueryLexer pyfcstm.bmc.grammar.BmcQueryParser pyfcstm.bmc.grammar.BmcQueryParserListener pyfcstm.bmc.listener pyfcstm.bmc.macro pyfcstm.bmc.parse pyfcstm.bmc.pipeline pyfcstm.bmc.properties pyfcstm.bmc.query pyfcstm.bmc.relation pyfcstm.bmc.source pyfcstm.bmc.witness pyfcstm.config pyfcstm.config.meta pyfcstm.diagnostics pyfcstm.diagnostics.analyzers pyfcstm.diagnostics.analyzers.combo pyfcstm.diagnostics.analyzers.const_fold pyfcstm.diagnostics.analyzers.data_flow pyfcstm.diagnostics.analyzers.design_health pyfcstm.diagnostics.analyzers.naming pyfcstm.diagnostics.analyzers.numeric pyfcstm.diagnostics.analyzers.redundancy pyfcstm.diagnostics.analyzers.structural pyfcstm.diagnostics.analyzers.thresholds pyfcstm.diagnostics.analyzers.transition_info pyfcstm.diagnostics.analyzers.type_shape pyfcstm.diagnostics.analyzers.use_def pyfcstm.diagnostics.codes pyfcstm.diagnostics.inspect pyfcstm.diagnostics.inspect_render pyfcstm.diagnostics.sink pyfcstm.diagnostics.suggested_fix pyfcstm.dsl pyfcstm.dsl.error pyfcstm.dsl.grammar pyfcstm.dsl.grammar.GrammarLexer pyfcstm.dsl.grammar.GrammarListener pyfcstm.dsl.grammar.GrammarParser pyfcstm.dsl.grammar.GrammarParserListener pyfcstm.dsl.listener pyfcstm.dsl.node pyfcstm.dsl.parse pyfcstm.entry pyfcstm.entry.base pyfcstm.entry.bmc pyfcstm.entry.cli pyfcstm.entry.dispatch pyfcstm.entry.generate pyfcstm.entry.inspect pyfcstm.entry.plantuml pyfcstm.entry.simulate pyfcstm.entry.simulate.batch pyfcstm.entry.simulate.commands pyfcstm.entry.simulate.completer pyfcstm.entry.simulate.display pyfcstm.entry.simulate.events pyfcstm.entry.simulate.logging pyfcstm.entry.simulate.repl pyfcstm.entry.visualize pyfcstm.highlight pyfcstm.highlight.bmc_query_lexer pyfcstm.highlight.pygments_lexer pyfcstm.llm pyfcstm.llm._resources pyfcstm.llm.error pyfcstm.llm.fbmcq pyfcstm.llm.fcstm pyfcstm.model pyfcstm.model.base pyfcstm.model.expr pyfcstm.model.imports pyfcstm.model.load pyfcstm.model.model pyfcstm.model.plantuml pyfcstm.render pyfcstm.render.c_runtime pyfcstm.render.env pyfcstm.render.expr pyfcstm.render.func pyfcstm.render.render pyfcstm.render.statement pyfcstm.simulate pyfcstm.simulate.context pyfcstm.simulate.decorators pyfcstm.simulate.runtime pyfcstm.simulate.utils pyfcstm.solver pyfcstm.solver.domain pyfcstm.solver.expr pyfcstm.solver.logical pyfcstm.solver.operation pyfcstm.solver.safety pyfcstm.solver.solve pyfcstm.template pyfcstm.utils pyfcstm.utils.binary pyfcstm.utils.decode pyfcstm.utils.doc pyfcstm.utils.fixed pyfcstm.utils.jinja2 pyfcstm.utils.json pyfcstm.utils.logging pyfcstm.utils.parse pyfcstm.utils.safe pyfcstm.utils.text pyfcstm.utils.validate pyfcstm.verify pyfcstm.verify.algorithms pyfcstm.verify.algorithms.effect pyfcstm.verify.algorithms.guard pyfcstm.verify.algorithms.lifecycle pyfcstm.verify.algorithms.transition pyfcstm.verify.encoding pyfcstm.verify.encoding._core pyfcstm.verify.encoding.expr pyfcstm.verify.encoding.guard pyfcstm.verify.encoding.initial pyfcstm.verify.encoding.lifecycle pyfcstm.verify.encoding.operation pyfcstm.verify.encoding.trigger pyfcstm.verify.inspect_adapter pyfcstm.verify.registry pyfcstm.verify.result pyfcstm.verify.taxonomy pyfcstm.verify.topology

N

Name (class in pyfcstm.dsl.node) name (pyfcstm.bmc.domain.EventInputRef property) (pyfcstm.bmc.domain.FrameRef property) (pyfcstm.bmc.domain.StepRef property) (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer attribute) (pyfcstm.highlight.pygments_lexer.FcstmLexer attribute) name_ast_node() (pyfcstm.model.model.VarDefine method) NameRef (class in pyfcstm.bmc.ast) ne() (pyfcstm.model.expr.Expr method) non_abstract_on_during_aspects (pyfcstm.model.model.State property)

non_abstract_on_durings (pyfcstm.model.model.State property) non_abstract_on_enters (pyfcstm.model.model.State property) non_abstract_on_exits (pyfcstm.model.model.State property) normalize() (in module pyfcstm.utils.text) not_() (pyfcstm.bmc.macro.BoolTemplate class method) (pyfcstm.model.expr.Expr method) NumBinaryOp (class in pyfcstm.bmc.ast) NumConditionalOp (class in pyfcstm.bmc.ast) NumericComparison (class in pyfcstm.bmc.ast) NumUnaryOp (class in pyfcstm.bmc.ast)

O

ok (pyfcstm.bmc.witness.BmcReplayResult property) omitted() (pyfcstm.bmc.ast.CallStepSelector class method) OnAspect (class in pyfcstm.model.model) OnStage (class in pyfcstm.model.model) Op (class in pyfcstm.model.expr) op_mark (pyfcstm.model.expr.BinaryOp property) (pyfcstm.model.expr.ConditionalOp property) (pyfcstm.model.expr.Op property) (pyfcstm.model.expr.UnaryOp property) open_diagram_with_default_app() (in module pyfcstm.entry.visualize) Operation (class in pyfcstm.dsl.node) (class in pyfcstm.model.model) OperationalDeprecatedAssignment (class in pyfcstm.dsl.node) OperationalNode (in module pyfcstm.render.c_runtime)

OperationalStatement (class in pyfcstm.dsl.node) OperationAssignment (class in pyfcstm.dsl.node) OperationBranch (class in pyfcstm.solver.operation) OperationExecution (class in pyfcstm.solver.operation) OperationFailure (class in pyfcstm.solver.operation) OperationIf (class in pyfcstm.dsl.node) OperationIfBranch (class in pyfcstm.dsl.node) OperationSource (in module pyfcstm.solver.operation) OperationStatement (class in pyfcstm.model.model) OperationStep (class in pyfcstm.solver.operation) options (pyfcstm.bmc.engine.BmcEngine property) or_() (pyfcstm.bmc.macro.BoolTemplate class method) (pyfcstm.model.expr.Expr method) outcome (pyfcstm.bmc.witness.BmcSolveResult property)

P

P (in module pyfcstm.entry.base) Paren (class in pyfcstm.dsl.node) parent (pyfcstm.model.model.OnAspect property), [1] (pyfcstm.model.model.OnStage property), [1] (pyfcstm.model.model.State property), [1] (pyfcstm.model.model.Transition property), [1] parse_bmc_cond_expression() (in module pyfcstm.bmc.parse) parse_bmc_num_expression() (in module pyfcstm.bmc.parse) parse_bmc_query() (in module pyfcstm.bmc.parse) parse_condition() (in module pyfcstm.dsl.parse) parse_dsl_node_to_state_machine() (in module pyfcstm.model.model) parse_expr() (in module pyfcstm.model.expr) parse_expr_from_string() (in module pyfcstm.model.expr) parse_expr_node_to_expr() (in module pyfcstm.model.expr) parse_key_value_pairs() (in module pyfcstm.utils.parse) parse_operation() (in module pyfcstm.dsl.parse) parse_operations() (in module pyfcstm.solver.operation) parse_preamble() (in module pyfcstm.dsl.parse) parse_state_machine_dsl() (in module pyfcstm.dsl.parse) parse_value() (in module pyfcstm.utils.parse) parse_with_bmc_grammar_entry() (in module pyfcstm.bmc.parse) parse_with_grammar_entry() (in module pyfcstm.dsl.parse) PartitionCheckResult (class in pyfcstm.bmc.macro) path (pyfcstm.model.model.Event property) path_name (pyfcstm.model.model.Event property) PLANTUML_OPTION_TYPES (in module pyfcstm.entry.plantuml) PlantUMLExportable (class in pyfcstm.model.base) PlantUMLOptions (class in pyfcstm.model.plantuml) PlantUMLOptionsInput (in module pyfcstm.model.plantuml) point() (pyfcstm.bmc.ast.CallStepSelector class method) polarity (pyfcstm.bmc.witness.BmcSolveResult property) POST_EXIT_CONTINUATION_LABEL (in module pyfcstm.entry.simulate.events) Preamble (class in pyfcstm.dsl.node) predicate (pyfcstm.bmc.binding.BoundInitialSpec property) prepare() (pyfcstm.bmc.engine.BmcEngine method) prepare_bmc_query() (in module pyfcstm.bmc.engine) pretty_print() (pyfcstm.bmc.witness.BmcEventDecodePolicy method) (pyfcstm.bmc.witness.BmcReplayMismatch method) (pyfcstm.bmc.witness.BmcReplayResult method) (pyfcstm.bmc.witness.BmcRuntimeFrame method) (pyfcstm.bmc.witness.BmcRuntimeStep method) (pyfcstm.bmc.witness.BmcRuntimeTrace method) (pyfcstm.bmc.witness.BmcSolveResult method) (pyfcstm.bmc.witness.BmcWitnessCallRecord method) (pyfcstm.bmc.witness.BmcWitnessEvent method) (pyfcstm.bmc.witness.BmcWitnessFrame method) (pyfcstm.bmc.witness.BmcWitnessStep method) (pyfcstm.bmc.witness.BmcWitnessTrace method) print_exception() (in module pyfcstm.entry.base) print_version() (in module pyfcstm.entry.dispatch) PriorityExclusion (class in pyfcstm.bmc.macro) process() (pyfcstm.entry.simulate.commands.CommandProcessor method) process_item_to_object() (in module pyfcstm.render.func) property_satisfied (pyfcstm.bmc.witness.BmcSolveResult property) pyfcstm module pyfcstm.bmc module pyfcstm.bmc.ast module pyfcstm.bmc.binding module pyfcstm.bmc.domain module pyfcstm.bmc.engine module pyfcstm.bmc.errors module pyfcstm.bmc.expand module pyfcstm.bmc.grammar module pyfcstm.bmc.grammar.BmcQueryLexer module pyfcstm.bmc.grammar.BmcQueryParser module pyfcstm.bmc.grammar.BmcQueryParserListener module pyfcstm.bmc.listener module pyfcstm.bmc.macro module pyfcstm.bmc.parse module pyfcstm.bmc.pipeline module pyfcstm.bmc.properties module pyfcstm.bmc.query module pyfcstm.bmc.relation module pyfcstm.bmc.source module pyfcstm.bmc.witness module pyfcstm.config module pyfcstm.config.meta module pyfcstm.diagnostics module pyfcstm.diagnostics.analyzers module pyfcstm.diagnostics.analyzers.combo module pyfcstm.diagnostics.analyzers.const_fold module pyfcstm.diagnostics.analyzers.data_flow module pyfcstm.diagnostics.analyzers.design_health module pyfcstm.diagnostics.analyzers.naming module pyfcstm.diagnostics.analyzers.numeric module pyfcstm.diagnostics.analyzers.redundancy module pyfcstm.diagnostics.analyzers.structural module pyfcstm.diagnostics.analyzers.thresholds module pyfcstm.diagnostics.analyzers.transition_info module pyfcstm.diagnostics.analyzers.type_shape module pyfcstm.diagnostics.analyzers.use_def module pyfcstm.diagnostics.codes module pyfcstm.diagnostics.inspect module pyfcstm.diagnostics.inspect_render module pyfcstm.diagnostics.sink module pyfcstm.diagnostics.suggested_fix module pyfcstm.dsl module pyfcstm.dsl.error module pyfcstm.dsl.grammar module pyfcstm.dsl.grammar.GrammarLexer module pyfcstm.dsl.grammar.GrammarListener module pyfcstm.dsl.grammar.GrammarParser module pyfcstm.dsl.grammar.GrammarParserListener module pyfcstm.dsl.listener module pyfcstm.dsl.node module pyfcstm.dsl.parse module pyfcstm.entry module pyfcstm.entry.base module pyfcstm.entry.bmc module

pyfcstm.entry.cli module pyfcstm.entry.dispatch module pyfcstm.entry.generate module pyfcstm.entry.inspect module pyfcstm.entry.plantuml module pyfcstm.entry.simulate module pyfcstm.entry.simulate.batch module pyfcstm.entry.simulate.commands module pyfcstm.entry.simulate.completer module pyfcstm.entry.simulate.display module pyfcstm.entry.simulate.events module pyfcstm.entry.simulate.logging module pyfcstm.entry.simulate.repl module pyfcstm.entry.visualize module pyfcstm.highlight module pyfcstm.highlight.bmc_query_lexer module pyfcstm.highlight.pygments_lexer module pyfcstm.llm module pyfcstm.llm._resources module pyfcstm.llm.error module pyfcstm.llm.fbmcq module pyfcstm.llm.fcstm module pyfcstm.model module pyfcstm.model.base module pyfcstm.model.expr module pyfcstm.model.imports module pyfcstm.model.load module pyfcstm.model.model module pyfcstm.model.plantuml module pyfcstm.render module pyfcstm.render.c_runtime module pyfcstm.render.env module pyfcstm.render.expr module pyfcstm.render.func module pyfcstm.render.render module pyfcstm.render.statement module pyfcstm.simulate module pyfcstm.simulate.context module pyfcstm.simulate.decorators module pyfcstm.simulate.runtime module pyfcstm.simulate.utils module pyfcstm.solver module pyfcstm.solver.domain module pyfcstm.solver.expr module pyfcstm.solver.logical module pyfcstm.solver.operation module pyfcstm.solver.safety module pyfcstm.solver.solve module pyfcstm.template module pyfcstm.utils module pyfcstm.utils.binary module pyfcstm.utils.decode module pyfcstm.utils.doc module pyfcstm.utils.fixed module pyfcstm.utils.jinja2 module pyfcstm.utils.json module pyfcstm.utils.logging module pyfcstm.utils.parse module pyfcstm.utils.safe module pyfcstm.utils.text module pyfcstm.utils.validate module pyfcstm.verify module pyfcstm.verify.algorithms module pyfcstm.verify.algorithms.effect module pyfcstm.verify.algorithms.guard module pyfcstm.verify.algorithms.lifecycle module pyfcstm.verify.algorithms.transition module pyfcstm.verify.encoding module pyfcstm.verify.encoding._core module pyfcstm.verify.encoding.expr module pyfcstm.verify.encoding.guard module pyfcstm.verify.encoding.initial module pyfcstm.verify.encoding.lifecycle module pyfcstm.verify.encoding.operation module pyfcstm.verify.encoding.trigger module pyfcstm.verify.inspect_adapter module pyfcstm.verify.registry module pyfcstm.verify.result module pyfcstm.verify.taxonomy module pyfcstm.verify.topology module pyfcstmcli() (in module pyfcstm.entry.dispatch) python_round_to_z3() (in module pyfcstm.solver.expr)

R

R (in module pyfcstm.entry.base) range() (pyfcstm.bmc.ast.CallStepSelector class method) read_json() (pyfcstm.utils.json.IJsonOp class method) read_yaml() (pyfcstm.utils.json.IJsonOp class method) ReadOnlyExecutionContext (class in pyfcstm.simulate.context) recurrence_state_ids (pyfcstm.bmc.domain.BmcDomain property) references (pyfcstm.bmc.engine.BmcPreparedContext property) refs_with_suggested_fix() (in module pyfcstm.diagnostics.suggested_fix) register_abstract_handler() (pyfcstm.simulate.runtime.SimulationRuntime method) register_handlers_from_object() (pyfcstm.simulate.runtime.SimulationRuntime method) REGISTRY (in module pyfcstm.verify.registry) relative() (pyfcstm.bmc.ast.CallStepPoint class method) render() (pyfcstm.render.render.StateMachineCodeRenderer method) render_c_action_body() (in module pyfcstm.render.c_runtime) render_c_condition_body() (in module pyfcstm.render.c_runtime) render_c_reset_vars_body() (in module pyfcstm.render.c_runtime) render_expr_node() (in module pyfcstm.render.expr) render_inspect_human() (in module pyfcstm.diagnostics.inspect_render) render_inspect_llm_json() (in module pyfcstm.diagnostics.inspect_render) render_inspect_llm_markdown() (in module pyfcstm.diagnostics.inspect_render)

render_one_file() (pyfcstm.render.render.StateMachineCodeRenderer method) render_plantuml_diagram() (in module pyfcstm.entry.visualize) render_stmt_node() (in module pyfcstm.render.statement) render_stmt_nodes() (in module pyfcstm.render.statement) render_suggested_fix() (in module pyfcstm.diagnostics.suggested_fix) replay_bmc_witness() (in module pyfcstm.bmc.witness) reportAmbiguity() (pyfcstm.dsl.error.CollectingErrorListener method) reportAttemptingFullContext() (pyfcstm.dsl.error.CollectingErrorListener method) reportContextSensitivity() (pyfcstm.dsl.error.CollectingErrorListener method) required_fields() (pyfcstm.diagnostics.codes.CodeSpec method) resolve_event() (pyfcstm.model.model.State method) (pyfcstm.model.model.StateMachine method) resolve_inspect_color_enabled() (in module pyfcstm.entry.inspect) resolve_renderer_backend() (in module pyfcstm.entry.visualize) resolve_visualize_output_path() (in module pyfcstm.entry.visualize) ResultKind (in module pyfcstm.verify.result) role (pyfcstm.bmc.domain.FrameRef property) run() (pyfcstm.entry.simulate.repl.SimulationREPL method) run_inspect_algorithms() (in module pyfcstm.verify.inspect_adapter) run_plantumlcli_builtin_check() (in module pyfcstm.entry.visualize)

S

SafetyCheck (class in pyfcstm.solver.safety) SafetyReason (in module pyfcstm.solver.safety) SatResult (class in pyfcstm.solver.logical) select() (pyfcstm.model.expr.Expr method) sequence_safe() (in module pyfcstm.utils.safe) serializedATN() (in module pyfcstm.bmc.grammar.BmcQueryLexer) (in module pyfcstm.bmc.grammar.BmcQueryParser) (in module pyfcstm.dsl.grammar.GrammarLexer) (in module pyfcstm.dsl.grammar.GrammarParser) set() (pyfcstm.entry.simulate.commands.Settings method) Settings (class in pyfcstm.entry.simulate.commands) should_show_action() (in module pyfcstm.model.plantuml) show() (pyfcstm.entry.base.ClickErrorException method) (pyfcstm.entry.base.ClickWarningException method) SimulateCliFormatter (class in pyfcstm.entry.simulate.logging) SimulateLogHighlighter (class in pyfcstm.entry.simulate.logging) SimulatePlainLogHandler (class in pyfcstm.entry.simulate.logging) SimulateRichLogHandler (class in pyfcstm.entry.simulate.logging) SimulationCompleter (class in pyfcstm.entry.simulate.completer) SimulationREPL (class in pyfcstm.entry.simulate.repl) SimulationRuntime (class in pyfcstm.simulate.runtime) SimulationRuntimeActionReferenceError (class in pyfcstm.simulate.runtime) SimulationRuntimeDfsError (class in pyfcstm.simulate.runtime) SimulationRuntimeEventError (class in pyfcstm.simulate.runtime) SimulationRuntimeExpressionError (class in pyfcstm.simulate.runtime) SimulationRuntimeTerminalStateError (class in pyfcstm.simulate.runtime) skip_result() (in module pyfcstm.verify.result) SMTLogic (in module pyfcstm.verify.taxonomy)

solve() (in module pyfcstm.solver.solve) solve_bmc_property() (in module pyfcstm.bmc.witness) SolveResult (class in pyfcstm.solver.solve) source_from_initial_spec() (in module pyfcstm.bmc.source) SourceExcerpt (class in pyfcstm.diagnostics.inspect_render) SourceExcerptLine (class in pyfcstm.diagnostics.inspect_render) Span (class in pyfcstm.utils.validate) stable_leaf_source() (in module pyfcstm.bmc.source) State (class in pyfcstm.model.model) state_by_id() (pyfcstm.bmc.domain.BmcDomain method) state_by_path() (pyfcstm.bmc.domain.BmcDomain method) state_id_to_path() (pyfcstm.bmc.domain.BmcDomain method) STATE_INIT_ID (in module pyfcstm.bmc.domain) state_path_to_id() (pyfcstm.bmc.domain.BmcDomain method) STATE_TERMINATE_ID (in module pyfcstm.bmc.domain) StateDefinition (class in pyfcstm.dsl.node) StateDisplay (class in pyfcstm.entry.simulate.display) StateDomainEntry (class in pyfcstm.bmc.domain) StateInfo (class in pyfcstm.diagnostics.inspect) StateMachine (class in pyfcstm.model.model) StateMachineCodeRenderer (class in pyfcstm.render.render) StateMachineDSLProgram (class in pyfcstm.dsl.node) Statement (class in pyfcstm.dsl.node) StepRef (class in pyfcstm.bmc.domain) strongly_connected_components() (in module pyfcstm.verify.topology) SuggestedFixSpec (class in pyfcstm.diagnostics.codes) syntaxError() (pyfcstm.dsl.error.CollectingErrorListener method) SyntaxFailError (class in pyfcstm.dsl.error)

T

T (in module pyfcstm.utils.json) TERMINATE_CASE_PATH (in module pyfcstm.bmc.source) Terminated (class in pyfcstm.bmc.ast) terminated_absorb_case() (in module pyfcstm.bmc.macro) terminated_source() (in module pyfcstm.bmc.source) to_ast_node() (pyfcstm.bmc.binding.BoundBmcQuery method) (pyfcstm.model.base.AstExportable method) (pyfcstm.model.expr.BinaryOp method) (pyfcstm.model.expr.Boolean method) (pyfcstm.model.expr.ConditionalOp method) (pyfcstm.model.expr.Expr method) (pyfcstm.model.expr.Float method) (pyfcstm.model.expr.Integer method) (pyfcstm.model.expr.UFunc method) (pyfcstm.model.expr.UnaryOp method) (pyfcstm.model.expr.Variable method) (pyfcstm.model.model.Event method) (pyfcstm.model.model.IfBlock method) (pyfcstm.model.model.IfBlockBranch method) (pyfcstm.model.model.OnAspect method) (pyfcstm.model.model.OnStage method) (pyfcstm.model.model.Operation method) (pyfcstm.model.model.State method) (pyfcstm.model.model.StateMachine method) (pyfcstm.model.model.Transition method) (pyfcstm.model.model.VarDefine method) to_c_identifier() (in module pyfcstm.utils.text) to_c_path_identifier() (in module pyfcstm.utils.jinja2) to_c_public_identifier() (in module pyfcstm.utils.jinja2) to_c_public_macro_identifier() (in module pyfcstm.utils.jinja2) to_canonical() (pyfcstm.bmc.ast.BmcExpr method) (pyfcstm.bmc.ast.CallFilter method) (pyfcstm.bmc.ast.CallStepPoint method) (pyfcstm.bmc.ast.CallStepSelector method) (pyfcstm.bmc.binding.BmcBindingDiagnostic method) (pyfcstm.bmc.binding.BoundAssumption method) (pyfcstm.bmc.binding.BoundBmcQuery method) (pyfcstm.bmc.binding.BoundInitialSpec method) (pyfcstm.bmc.binding.BoundProperty method) (pyfcstm.bmc.binding.BoundReference method) (pyfcstm.bmc.domain.BmcDomain method) (pyfcstm.bmc.domain.EventDomainEntry method) (pyfcstm.bmc.domain.EventInputRef method) (pyfcstm.bmc.domain.FrameRef method) (pyfcstm.bmc.domain.StateDomainEntry method) (pyfcstm.bmc.domain.StepRef method) (pyfcstm.bmc.domain.VarDomainEntry method) (pyfcstm.bmc.engine.BmcOptions method) (pyfcstm.bmc.engine.BmcPreparedContext method) (pyfcstm.bmc.macro.ActionBlock method) (pyfcstm.bmc.macro.BoolTemplate method) (pyfcstm.bmc.macro.CycleCase method) (pyfcstm.bmc.macro.EventUse method) (pyfcstm.bmc.macro.GuardRequirement method) (pyfcstm.bmc.macro.MacroStepFormal method) (pyfcstm.bmc.macro.PartitionCheckResult method) (pyfcstm.bmc.macro.PriorityExclusion method) (pyfcstm.bmc.properties.BmcPropertyFormula method) (pyfcstm.bmc.query.BmcAssumption method) (pyfcstm.bmc.query.BmcProperty method) (pyfcstm.bmc.query.BmcQuery method) (pyfcstm.bmc.query.InitialSpec method) (pyfcstm.bmc.query.InitialVariablePolicy method) (pyfcstm.bmc.relation.BmcAbstractCallRecord method) (pyfcstm.bmc.relation.BmcCaseRelation method) (pyfcstm.bmc.relation.BmcCoreFormula method) (pyfcstm.bmc.relation.BmcStepRelation method) (pyfcstm.bmc.relation.BmcTraceSymbols method) (pyfcstm.bmc.source.MacroStepSource method) (pyfcstm.bmc.witness.BmcEventDecodePolicy method) (pyfcstm.bmc.witness.BmcReplayMismatch method) (pyfcstm.bmc.witness.BmcReplayResult method) (pyfcstm.bmc.witness.BmcRuntimeFrame method) (pyfcstm.bmc.witness.BmcRuntimeStep method) (pyfcstm.bmc.witness.BmcRuntimeTrace method) (pyfcstm.bmc.witness.BmcSolveResult method) (pyfcstm.bmc.witness.BmcWitnessCallRecord method) (pyfcstm.bmc.witness.BmcWitnessEvent method) (pyfcstm.bmc.witness.BmcWitnessFrame method) (pyfcstm.bmc.witness.BmcWitnessStep method) (pyfcstm.bmc.witness.BmcWitnessTrace method)

to_config() (pyfcstm.model.plantuml.PlantUMLOptions method) to_cpp_identifier() (in module pyfcstm.utils.text) to_go_identifier() (in module pyfcstm.utils.text) to_identifier() (in module pyfcstm.utils.text) to_java_identifier() (in module pyfcstm.utils.text) to_js_identifier() (in module pyfcstm.utils.text) to_json() (pyfcstm.diagnostics.inspect.ModelInspect method) (pyfcstm.utils.json.IJsonOp method) to_plantuml() (pyfcstm.model.base.PlantUMLExportable method) (pyfcstm.model.model.State method) (pyfcstm.model.model.StateMachine method) to_python_identifier() (in module pyfcstm.utils.text) to_ruby_identifier() (in module pyfcstm.utils.text) to_rust_identifier() (in module pyfcstm.utils.text) to_semantic_canonical() (pyfcstm.bmc.source.MacroStepSource method) to_text() (pyfcstm.bmc.witness.BmcEventDecodePolicy method) (pyfcstm.bmc.witness.BmcReplayMismatch method) (pyfcstm.bmc.witness.BmcReplayResult method) (pyfcstm.bmc.witness.BmcRuntimeFrame method) (pyfcstm.bmc.witness.BmcRuntimeStep method) (pyfcstm.bmc.witness.BmcRuntimeTrace method) (pyfcstm.bmc.witness.BmcSolveResult method) (pyfcstm.bmc.witness.BmcWitnessCallRecord method) (pyfcstm.bmc.witness.BmcWitnessEvent method) (pyfcstm.bmc.witness.BmcWitnessFrame method) (pyfcstm.bmc.witness.BmcWitnessStep method) (pyfcstm.bmc.witness.BmcWitnessTrace method) to_transition_ast_node() (pyfcstm.model.model.State method) to_ts_identifier() (in module pyfcstm.utils.text) to_yaml() (pyfcstm.utils.json.IJsonOp method) tokens (pyfcstm.highlight.bmc_query_lexer.FcstmBmcQueryLexer attribute) (pyfcstm.highlight.pygments_lexer.FcstmLexer attribute) topological_finite() (in module pyfcstm.verify.topology) topological_inevitable_terminator() (in module pyfcstm.verify.topology) topological_reachable_set() (in module pyfcstm.verify.topology) Transition (class in pyfcstm.model.model) transition_shadowed_by_predecessor() (in module pyfcstm.verify.algorithms.transition) transition_to_ast_node() (pyfcstm.model.model.State class method) TransitionDefinition (class in pyfcstm.dsl.node) TransitionInfo (class in pyfcstm.diagnostics.inspect) transitions_entering_children (pyfcstm.model.model.State property) transitions_entering_children_simplified (pyfcstm.model.model.State property) transitions_from (pyfcstm.model.model.State property) transitions_to (pyfcstm.model.model.State property) translate_expr_domain() (in module pyfcstm.solver.domain) TranslationFailure (class in pyfcstm.solver.domain) true() (pyfcstm.bmc.macro.BoolTemplate class method)

U

UFunc (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) UFuncCall (class in pyfcstm.bmc.ast) UInt16 (class in pyfcstm.utils.fixed) UInt32 (class in pyfcstm.utils.fixed) UInt64 (class in pyfcstm.utils.fixed) UInt8 (class in pyfcstm.utils.fixed)

UnaryOp (class in pyfcstm.dsl.node) (class in pyfcstm.model.expr) UnfinishedParsingError (class in pyfcstm.dsl.error) unreachable_states() (in module pyfcstm.verify.topology) unregister_abstract_handler() (pyfcstm.simulate.runtime.SimulationRuntime method) UnsupportedBmcQuery (class in pyfcstm.bmc.errors) UseDefGraph (class in pyfcstm.diagnostics.analyzers.use_def) uses_stable_fallback (pyfcstm.bmc.source.MacroStepSource property)

V

validate() (pyfcstm.utils.validate.IValidatable method) ValidationError (class in pyfcstm.utils.validate) value (pyfcstm.bmc.ast.BoolLiteral property) (pyfcstm.bmc.ast.FloatLiteral property) (pyfcstm.bmc.ast.IntLiteral property) (pyfcstm.dsl.node.Literal property) var_name_to_ast_node() (pyfcstm.model.model.Operation method) VarDefine (class in pyfcstm.model.model) VarDomainEntry (class in pyfcstm.bmc.domain) Variable (class in pyfcstm.model.expr) variable_by_id() (pyfcstm.bmc.domain.BmcDomain method)

variable_by_name() (pyfcstm.bmc.domain.BmcDomain method) variable_id_to_name() (pyfcstm.bmc.domain.BmcDomain method) variable_name_to_id() (pyfcstm.bmc.domain.BmcDomain method) variable_policy (pyfcstm.bmc.binding.BoundInitialSpec property) VariableInfo (class in pyfcstm.diagnostics.inspect) variables (pyfcstm.bmc.macro.BoolTemplate property) VerificationScope (in module pyfcstm.verify.taxonomy) verify_boolean_partition() (in module pyfcstm.bmc.macro) verify_partition() (pyfcstm.bmc.macro.MacroStepFormal method) VERIFY_SHARED_STATIC_CODES (in module pyfcstm.diagnostics.inspect) verify_source_partition() (in module pyfcstm.bmc.macro) VerifyAlgorithmMeta (class in pyfcstm.verify.taxonomy)

W

walk_states() (pyfcstm.model.model.State method) (pyfcstm.model.model.StateMachine method)

windows_chinese_encodings (in module pyfcstm.utils.decode) witness_found (pyfcstm.bmc.witness.BmcSolveResult property) write_bmc_output() (in module pyfcstm.entry.bmc)