stormpy.developer

Warning

The stormpy developer API is internal and can be subject to change.

Raw pybind11 bindings for the core library of Storm.

This module is only meant for developers. Use stormpy for the public API.

The naming of functions and classes of the bindings mirrors the corresponding storm:: C++ functions and classes.

Functions

build_explicit_drn_model	Build sparse model from DRN file
build_explicit_model(transitions_file, ...)	Build sparse model from explicit input files
build_sparse_model	Build model in sparse representation
build_subsystem(...)	Build a subsystem of a sparse model
build_symbolic_model	Build model in symbolic representation
compute_all_transient_probabilities(env, ...)	Compute transient probabilities for all states of a CTMC
compute_all_until_probabilities(env, task, ...)	Compute until probabilities for all states of a CTMC
compute_expected_visiting_times_with_sparse_engine(...)	Compute expected visiting times of deterministic model
compute_steady_state_distribution_with_sparse_engine(...)	Compute steady-state distribution of deterministic model
create_weight_vector_checker(-> tuple[storm, ...)	Create checker for weighted sums of objectives.
eliminate_non_markovian_chains(...)	Eliminate chains of non-Markovian states in MA
export_sparse_model_as_drn(...)	Export sparse model in DRN format
get_exact_environment()	Create a new environment which enforces exact computations
get_log_level()	Get log level of Storm
get_reachable_states(...)	Get states reachable from the initial states
get_sound_environment()	Create a new environment which enforces sound computations
install_signal_handler(maximal_wait_time)	Install signal handler for timeouts and interrupts
make_explicit_model_builder	Construct an explicit model builder
parse_constant_definition_string(manager, ...)	Parse a string of constant definitions
parse_jani_model(filename[, property_filter])	Parse Jani model and its properties
parse_jani_model_from_string(jsonstring[, ...])	Parse Jani model and its properties from string
parse_program(filename[, ...])	Parse Prism program
parse_properties(input_string[, property_filter])	Parse properties (without model context)
parse_properties_for_jani_model(...[, ...])	Parse properties, allowing references to variables of the Jani model
parse_properties_for_prism_program(...[, ...])	Parse properties, allowing references to variables of the Prism program
parse_properties_for_symbolic_model_description(...)	Parse properties, allowing references to variables of the symbolic model description
perform_bisimulation_minimization(...)	Perform bisimulation minimization on sparse model
perform_multi_objective_model_checking(-> storm)	Perform multi-objective model checking on MDP
perform_prob01(...)	Compute states with probability 0 and 1 of satisfying phi until psi
perform_prob01_max(...)	Compute states with maximal probability 0 and 1 of satisfying phi until psi
perform_prob01_min(...)	Compute states with minimal probability 0 and 1 of satisfying phi until psi
reset_timeout_alarm()	Reset timeout
set_from_exploded_string(command_line_arguments)	Set Storm settings from command line arguments
set_log_level(level)	Set log level of Storm
set_timeout_alarm(timeout)	Set timeout in seconds
substitute_constants_in_properties(...)	Substitute constants in properties
transform_continuous_to_discrete_time_sparse_model(...)	Transform continuous-time model into discrete-time model
transform_symbolic_to_sparse_model(...)	Transform symbolic model into sparse model
verify_with_dd_engine(...)	Verify model with dd engine
verify_with_hybrid_engine(...)	Verify model with hybrid engine
verify_with_sparse_engine(...)	Verify MDP with sparse engine

Classes

ActionMask	Mask for actions during state space exploration
AddUncertainty	Transform model into interval model with specified uncertainty
BuilderOptions(BuilderOptions)	Options for building process
CheckTask	Task for model checking
Choice	Choice of a state during state space exploration
DdBisimulationOptions(self)	Options for bisimulation on symbolic models
DiscreteTimePrismProgramSimulator	Simulator for Prism programs
DiscreteTimeSparseModelSimulator	Simulator for sparse discrete-time models
EndComponentEliminator	Elimination of end components
EndComponentEliminatorReturnType	Result of end component elimination
EnvironmentBuilder	Builds an environment from the current Storm settings
EnvironmentFactory(self)	Factory creating environments with default values
ExactEnvironmentFactory(self)	Factory creating environments which enforce exact computations
ExplicitModelBuilder	Model builder for sparse models
ExplicitModelBuilderOptions	Options for the explicit model builder
ExplicitStateLookup	Lookup of state ids by their variable valuation
ExplorationOrder(*values)	Order in which states are explored
FlatSet(FlatSet)	Flat set of integers
InitialPartitionMode(*values)	Initial partition mode for symbolic bisimulation
LogLevel(*values)	Log level of Storm
ModelReference	Lightweight Wrapper around results
PcaaWeightVectorChecker	Checker for weighted sums of objectives
RefinementMode(*values)	Refinement mode for symbolic bisimulation
ReuseMode(*values)	Reuse mode for symbolic bisimulation
SchedulerClass(self)	Class of schedulers
SchedulerMemoryPattern(*values)	Memory pattern of a scheduler
SignatureMode(*values)	Signature mode for symbolic bisimulation
SmtCheckResult(*values)	Result type
SMTMinimalLabelSetGenerator	Highlevel Counterexample Generator with SMT as backend
SMTMinimalLabelSetGeneratorCexInput	Precomputed input for counterexample generation
SMTMinimalLabelSetGeneratorOptions	Options for highlevel counterexample generation
SMTMinimalLabelSetGeneratorStats	Stats for highlevel counterexample generation
SmtSolver	Generic Storm SmtSolver Wrapper
SmtSolverFactory	Factory for creating SMT Solvers
SoundEnvironmentFactory(self)	Factory creating environments which enforce sound computations
StateValuationFunctionMask	Action mask based on state valuations
Z3SmtSolver(self, manager)	z3 API for storm smtsolver wrapper
Z3SmtSolverFactory(self)	Factory for creating z3 based SMT solvers