API

Class Hierarchy

• • Namespace smc_storm
    • Namespace smc_storm::model_checker
      • Struct ModelAndProperties
      • Class SmcPluginInstance
      • Class StatisticalModelChecker
      • Template Class StatisticalModelCheckingEngine
    • Namespace smc_storm::parser
      • Class JaniParserExtended
    • Namespace smc_storm::samples
      • Struct BatchResults
      • Struct BatchStatistics
      • Struct TraceInformation
      • Class BatchBuffer
      • Class CompressedStateTraceExporter
      • Class SamplingResults
      • Class TracesExporter
      • Class UncompressedStateTraceExporter
      • Enum TraceResult
    • Namespace smc_storm::settings
      • Struct SmcSettings
      • Struct UserSettings
      • Class CmdSettings
    • Namespace smc_storm::state_generation
      • Template Class ActionScheduler
      • Template Class ExplorationInformation
      • Template Class JaniSmcStatesExpansion
        • Struct JaniSmcStatesExpansion::ActionDescription
        • Struct JaniSmcStatesExpansion::ComputedDestinations
        • Struct JaniSmcStatesExpansion::PairHash
      • Template Class StateExpansionHandler
      • Template Class StateExpansionHandler< storm::generator::CompressedState, ValueType >
      • Template Class StateExpansionHandler< uint32_t, ValueType >
      • Template Class StateGeneration
      • Template Class StateGenerationBase
      • Template Class StateGenerationCacheless
    • Namespace smc_storm::state_properties
      • Template Struct VariableInformation
      • Class PropertyDescription
      • Template Class StateDescription
      • Template Class StateVariableData
      • Template Class StateVariableInformation
      • Enum PropertyType
  • Namespace storm
    • Namespace storm::expressions
      • Template Class ExpressionEvaluator

File Hierarchy

• • Directory include
    • Directory model_checker
      • File model_and_properties.hpp
      • File model_and_settings_validation.hpp
      • File smc_plugin_instance.hpp
      • File statistical_model_checker.hpp
      • File statistical_model_checking_engine.hpp
    • Directory parser
      • File jani_parser_extended.hpp
      • File parsers.hpp
    • Directory samples
      • File batch_buffer.hpp
      • File batch_results.hpp
      • File batch_statistics.hpp
      • File sampling_results.hpp
      • File trace_information.hpp
      • File trace_result.hpp
      • File traces_exporter.hpp
    • Directory settings
      • File cmd_settings.hpp
      • File smc_settings.hpp
      • File user_settings.hpp
    • Directory state_generation
      • File action_scheduler.hpp
      • File available_actions.hpp
      • File exploration_information.hpp
      • File jani_smc_states_expansion.hpp
      • File state_expansion_handler.hpp
      • File state_generation.hpp
      • File state_generation_base.hpp
      • File state_generation_cacheless.hpp
    • Directory state_properties
      • File property_description.hpp
      • File property_type.hpp
      • File state_description.hpp
      • File state_info.hpp
      • File state_variable_information.hpp
    • Directory utils
      • File storm_utilities.hpp

Full API

Namespaces

• Namespace smc_storm
  • Namespaces

• Namespace smc_storm::model_checker
  • Classes
  • Functions

• Namespace smc_storm::parser
  • Classes
  • Functions
  • Typedefs

• Namespace smc_storm::samples
  • Classes
  • Enums
  • Functions

• Namespace smc_storm::settings
  • Classes
  • Variables

• Namespace smc_storm::state_generation
  • Classes
  • Typedefs

• Namespace smc_storm::state_properties
  • Namespaces
  • Classes
  • Enums
  • Functions
  • Typedefs

• Namespace smc_storm::state_properties::state_info
  • Functions
  • Variables

• Namespace smc_storm::utils
  • Functions

• Namespace storm
  • Namespaces

• Namespace storm::expressions
  • Classes

• Namespace storm::modelchecker

• Namespace storm::parser

Classes and Structs

• Struct ModelAndProperties
  • Struct Documentation
    • smc_storm::model_checker::ModelAndProperties
      • model
      • properties
      • plugins

• Struct BatchResults
  • Struct Documentation
    • smc_storm::samples::BatchResults
      • BatchResults()
      • BatchResults()
      • batchIncomplete()
      • addResult()
      • getBatchStatistics()
      • getCount()
      • reset()
      • batch_size
      • property_type
      • n_verified
      • n_not_verified
      • n_no_info
      • count
      • rewards
      • min_trace_length
      • max_trace_length
      • min_reward
      • max_reward

• Struct BatchStatistics
  • Struct Documentation
    • smc_storm::samples::BatchStatistics
      • BatchStatistics()
      • BatchStatistics()
      • BatchStatistics()
      • updateStats()
      • mean
      • variance
      • dim

• Struct TraceInformation
  • Struct Documentation
    • smc_storm::samples::TraceInformation
      • trace_length
      • outcome
      • reward

• Struct SmcSettings
  • Struct Documentation
    • smc_storm::settings::SmcSettings
      • SmcSettings()
      • stat_method
      • traces_file
      • confidence
      • epsilon
      • max_trace_length
      • max_n_traces
      • n_threads
      • batch_size
      • plugins_loaded
      • stop_after_failure
      • store_only_not_verified
      • cache_explored_states
      • show_statistics

• Struct UserSettings
  • Struct Documentation
    • smc_storm::settings::UserSettings
      • validModel()
      • validProperties()
      • model_file
      • properties_file
      • properties_names
      • custom_property
      • constants
      • stat_method
      • traces_file
      • plugin_paths
      • confidence
      • epsilon
      • max_trace_length
      • max_n_traces
      • n_threads
      • batch_size
      • stop_after_failure
      • store_only_not_verified
      • cache_explored_states
      • show_statistics

• Struct JaniSmcStatesExpansion::ActionDescription
  • Nested Relationships
  • Struct Documentation
    • smc_storm::state_generation::JaniSmcStatesExpansion::ActionDescription
      • ActionDescription()
      • action_reward
      • action_edges

• Struct JaniSmcStatesExpansion::ComputedDestinations
  • Nested Relationships
  • Struct Documentation
    • smc_storm::state_generation::JaniSmcStatesExpansion::ComputedDestinations
      • clear()
      • related_action
      • destinations

• Struct JaniSmcStatesExpansion::PairHash
  • Nested Relationships
  • Struct Documentation
    • smc_storm::state_generation::JaniSmcStatesExpansion::PairHash
      • operator()()

• Template Struct VariableInformation
  • Struct Documentation
    • smc_storm::state_properties::VariableInformation
      • value_type
      • VariableInformation()
      • variable
      • lower_bound
      • upper_bound
      • global

• Class SmcPluginInstance
  • Class Documentation
    • smc_storm::model_checker::SmcPluginInstance
      • PluginAndModelVariable
      • PluginAndModelVariableVector
      • PluginToModelExpressionMap
      • SmcPluginInstance()
      • SmcPluginInstance()
      • getAutomatonName()
      • getActionId()
      • getActionName()
      • appendInitData()
      • getInitData()
      • getInputVariablesMap()
      • getOutputVariablesMap()
      • appendInputData()
      • appendOutputData()
      • sortOutputData()
      • generatePluginInstance()

• Class StatisticalModelChecker
  • Class Documentation
    • smc_storm::model_checker::StatisticalModelChecker
      • StatisticalModelChecker()
      • StatisticalModelChecker()
      • ~StatisticalModelChecker()
      • printProperty()
      • check()
      • getResult()

• Template Class StatisticalModelCheckingEngine
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::model_checker::StatisticalModelCheckingEngine
      • ValueType
      • StateType
      • StateGeneratorType
      • TraceExportType
      • StatisticalModelCheckingEngine()
      • canHandle()
      • computeProbabilities()
      • computeReachabilityRewards()
      • canHandleStatic()

• Class JaniParserExtended
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::parser::JaniParserExtended
      • JaniParserExtended()
      • ~JaniParserExtended()
      • parseModelPropertiesAndPlugins()
      • parseModelPropertiesAndPlugins()
      • loadPlugins()
      • generateGlobalScope()
      • extractVariablesAutomatonScope()
      • _jani_json
      • _plugin_paths
      • _constants_map
      • _global_vars_map

• Class BatchBuffer
  • Class Documentation
    • smc_storm::samples::BatchBuffer
      • BatchBuffer()
      • ~BatchBuffer()
      • cancel()
      • addResults()
      • getResults()
      • waitForSlotAvailable()

• Class CompressedStateTraceExporter
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::samples::CompressedStateTraceExporter
      • CompressedStateTraceExporter()
      • addNextState()

• Class SamplingResults
  • Class Documentation
    • smc_storm::samples::SamplingResults
      • SamplingResults()
      • SamplingResults()
      • getBatchSize()
      • getBatchResultInstance()
      • addBatchResults()
      • getResultCount()
      • getEstimatedReward()
      • getProbabilityVerifiedProperty()
      • newBatchNeeded()
      • printResults()

• Class TracesExporter
  • Inheritance Relationships
    • Derived Types
  • Class Documentation
    • smc_storm::samples::TracesExporter
      • TracesExporter()
      • ~TracesExporter()
      • setExportOnlyFailures()
      • addCurrentTraceResult()
      • writeCachedStates()
      • clearTraces()
      • _file
      • _export_only_failures
      • _trace_counter
      • _n_variables

• Class UncompressedStateTraceExporter
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::samples::UncompressedStateTraceExporter
      • UncompressedStateTraceExporter()
      • addNextState()

• Class CmdSettings
  • Class Documentation
    • smc_storm::settings::CmdSettings
      • CmdSettings()
      • parse()
      • getSettings()

• Template Class ActionScheduler
  • Class Documentation
    • smc_storm::state_generation::ActionScheduler
      • ActionId
      • ActionScheduler()
      • sampleAction()

• Template Class ExplorationInformation
  • Class Documentation
    • smc_storm::state_generation::ExplorationInformation
      • IdToStateMap
      • const_iterator
      • ExplorationInformation()
      • getStateDescription()
      • addStateDescription()
      • findUnexploredState()
      • unexploredStatesEnd()
      • removeUnexploredState()
      • addUnexploredState()
      • isUnexplored()

• Template Class JaniSmcStatesExpansion
  • Nested Relationships
    • Nested Types
  • Class Documentation
    • smc_storm::state_generation::JaniSmcStatesExpansion
      • JaniSmcStatesExpansion()
      • ~JaniSmcStatesExpansion()
      • getVariableInformation()
      • getCurrentState()
      • setInitialState()
      • setNextState()
      • satisfies()
      • getStateReward()
      • getActionReward()
      • getTransitionReward()
      • getAvailableActions()
      • getDestinationsFromAction()
      • automaton_and_action_to_plugin_ids
      • parallel_automata
      • composite_edges
      • information
      • expression
      • current_state_reward

• Template Class StateExpansionHandler
  • Class Documentation
    • smc_storm::state_generation::StateExpansionHandler
      • StateExpansionHandler()
      • init()
      • stateExpansionCallback()

• Template Class StateExpansionHandler< storm::generator::CompressedState, ValueType >
  • Class Documentation
    • smc_storm::state_generation::StateExpansionHandler< storm::generator::CompressedState, ValueType >
      • StateExpansionHandler()
      • init()
      • stateExpansionCallback()
      • getNextStates()
      • clearNextStates()
      • getHashValue()

• Template Class StateExpansionHandler< uint32_t, ValueType >
  • Class Documentation
    • smc_storm::state_generation::StateExpansionHandler< uint32_t, ValueType >
      • StateExpansionHandler()
      • init()
      • stateExpansionCallback()
      • getExplorationInformation()

• Template Class StateGeneration
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::state_generation::StateGeneration
      • StateDescription
      • StateGeneration()
      • getVariableInformation()
      • resetModel()
      • getAvailableActions()
      • runAction()
      • getStateReward()
      • getStateInfo()
      • getCurrentState()

• Template Class StateGenerationBase
  • Inheritance Relationships
    • Derived Types
  • Class Documentation
    • smc_storm::state_generation::StateGenerationBase
      • ~StateGenerationBase()
      • getPropertyDescription()
      • resetModel()
      • getAvailableActions()
      • runAction()
      • getStateReward()
      • getStateInfo()
      • StateGenerationBase()
      • _property_description
      • _random_generator
      • _store_compressed_states

• Template Class StateGenerationCacheless
  • Inheritance Relationships
    • Base Type
  • Class Documentation
    • smc_storm::state_generation::StateGenerationCacheless
      • StateGenerationCacheless()
      • getVariableInformation()
      • resetModel()
      • getAvailableActions()
      • runAction()
      • getStateReward()
      • getStateInfo()
      • getCurrentState()

• Class PropertyDescription
  • Class Documentation
    • smc_storm::state_properties::PropertyDescription
      • LabelsMap
      • PropertyDescription()
      • PropertyDescription()
      • generateExpressions()
      • getConditionExpression()
      • getTargetExpression()
      • getIsTerminalVerified()
      • getLowerBound()
      • getUpperBound()

• Template Class StateDescription
  • Class Documentation
    • smc_storm::state_properties::StateDescription
      • StateDescription()
      • setStateInfo()
      • setReward()
      • setCompressedState()
      • addAction()
      • getStateInfo()
      • getReward()
      • getActions()
      • getCompressedState()
      • ActionTransitions
      • _compressed_state
      • _state_info
      • _reward
      • _actions

• Template Class StateVariableData
  • Class Documentation
    • smc_storm::state_properties::StateVariableData
      • StateVariableData()
      • StateVariableData()
      • StateVariableData()
      • empty()
      • operator=()
      • operator==()
      • setBool()
      • setInt()
      • setReal()
      • setLocation()
      • getBoolData()
      • getIntData()
      • getRealData()
      • getLocationData()

• Template Class StateVariableInformation
  • Class Documentation
    • smc_storm::state_properties::StateVariableInformation
      • StateVariableInformation()
      • StateVariableInformation()
      • checkVariableBounds()
      • generateVariableData()
      • booleanVariables()
      • integerVariables()
      • realVariables()
      • locationVariables()
      • setInEvaluator()

• Template Class ExpressionEvaluator
  • Class Documentation
    • storm::expressions::ExpressionEvaluator

Enums

• Enum TraceResult
  • Enum Documentation
    • TraceResult
      • VERIFIED
      • NOT_VERIFIED
      • NO_INFO

• Enum PropertyType
  • Enum Documentation
    • PropertyType
      • P
      • R

Functions

• Function smc_storm::model_checker::areModelAndSettingsValid
  • Function Documentation
    • areModelAndSettingsValid()

• Function smc_storm::parser::filterProperties
  • Function Documentation
    • filterProperties()

• Function smc_storm::parser::getRequestedProperties
  • Function Documentation
    • getRequestedProperties()

• Function smc_storm::parser::loadJaniModel
  • Function Documentation
    • loadJaniModel()

• Function smc_storm::parser::parseJaniModelAndProperties
  • Function Documentation
    • parseJaniModelAndProperties()

• Function smc_storm::parser::parseModelAndProperties
  • Function Documentation
    • parseModelAndProperties()

• Function smc_storm::parser::parsePrismModelAndProperties
  • Function Documentation
    • parsePrismModelAndProperties()

• Function smc_storm::parser::substituteConstants
  • Function Documentation
    • substituteConstants()

• Function smc_storm::samples::toString
  • Function Documentation
    • toString()

• Template Function smc_storm::state_properties::evaluateExpression
  • Function Documentation
    • evaluateExpression()

• Function smc_storm::state_properties::state_info::checkBreakCondition
  • Function Documentation
    • checkBreakCondition()

• Function smc_storm::state_properties::state_info::checkIsTerminal
  • Function Documentation
    • checkIsTerminal()

• Function smc_storm::state_properties::state_info::checkNoInfo
  • Function Documentation
    • checkNoInfo()

• Function smc_storm::state_properties::state_info::checkSatisfyTarget
  • Function Documentation
    • checkSatisfyTarget()

• Function smc_storm::utils::stormSetUp
  • Function Documentation
    • stormSetUp()

Variables

• Variable smc_storm::settings::VERSION
  • Variable Documentation
    • VERSION

• Variable smc_storm::state_properties::state_info::BREAK_CONDITION
  • Variable Documentation
    • BREAK_CONDITION

• Variable smc_storm::state_properties::state_info::IS_TERMINAL
  • Variable Documentation
    • IS_TERMINAL

• Variable smc_storm::state_properties::state_info::NO_INFO
  • Variable Documentation
    • NO_INFO

• Variable smc_storm::state_properties::state_info::SATISFY_TARGET
  • Variable Documentation
    • SATISFY_TARGET

Typedefs

• Typedef smc_storm::parser::JaniModelPropertiesPlugins
  • Typedef Documentation
    • JaniModelPropertiesPlugins

• Typedef smc_storm::state_generation::ActionIdAndReward
  • Typedef Documentation
    • ActionIdAndReward

• Typedef smc_storm::state_generation::AvailableActions
  • Typedef Documentation
    • AvailableActions

• Typedef smc_storm::state_properties::StateInfoType
  • Typedef Documentation
    • StateInfoType