Stormpy.storage¶

class BitVector¶

get()¶

number_of_set_bits()¶

set()¶: Set

size()¶

class ChoiceLabeling¶: Labeling for choices

class ChoiceOrigins¶

This class represents the origin of choices of a model in terms of the input model spec.

get_choice_info()¶: human readable string

get_identifier_info()¶: human readable string

class Constant¶

A constant in a Prism program

property defined¶: Is the constant defined?

property expression_variable¶: Expression variable

property name¶: Constant name

property type¶: The type of the constant

class DistributionDouble¶: Finite Support Distribution

class Expression¶

Holds an expression

And()¶

Eq()¶

Geq()¶

Greater()¶

Iff()¶

Implies()¶

Leq()¶

Less()¶

Minus()¶

Multiply()¶

Neq()¶

Or()¶

Plus()¶

property arity¶: The arity of the expression

contains_variable()¶: Check if the expression contains any of the given variables.

contains_variables()¶: Check if the expression contains variables.

evaluate_as_bool()¶: Get the boolean value this expression evaluates to

evaluate_as_double()¶: Get the double value this expression evaluates to

evaluate_as_int()¶: Get the integer value this expression evaluates to

evaluate_as_rational()¶: Get the rational number this expression evaluates to

get_operand()¶: Get the operand at the given index

get_variables()¶: Get the variables

has_boolean_type()¶: Check if the expression is a boolean

has_integer_type()¶: Check if the expression is an integer

has_rational_type()¶: Check if the expression is a rational

identifier()¶: Retrieves the identifier associated with this expression if this expression is a variable

property is_function_application¶: True iff the expression is a function application (of any sort

is_literal()¶: Check if the expression is a literal

is_variable()¶: Check if the expression is a variable

property manager¶: Get the manager

property operator¶: The operator of the expression (if it is a function application)

substitute()¶

property type¶: Get the Type

class ExpressionManager¶

Manages variables for expressions

create_boolean()¶: Create expression from boolean

create_boolean_variable()¶: create Boolean variable

create_integer()¶: Create expression from integer number

create_integer_variable()¶: create Integer variable

create_rational()¶: Create expression from rational number

create_rational_variable()¶: create Rational variable

class ExpressionParser¶

Parser for storm-expressions

parse()¶

set_identifier_mapping()¶: sets identifiers

class ExpressionType¶

The type of an expression

property is_boolean¶

property is_integer¶

property is_rational¶

class ItemLabeling¶

Labeling

add_label()¶: Add label

contains_label()¶: Check if the given label is contained in the labeling

get_labels()¶: Get all labels

class JaniAssignment¶

Jani Assignment

property expression¶

class JaniAutomaton¶

A Jani Automation

add_edge()¶

add_initial_location()¶

add_location()¶: adds a new location, returns the index

property edges¶: get edges

property initial_location_indices¶

property initial_states_restriction¶: initial state restriction

property location_variable¶

property locations¶

property name¶

property variables¶

class JaniBoundedIntegerVariable¶: A Bounded Integer

class JaniChoiceOrigins¶

This class represents for each choice the origin in the jani spec.

get_edge_index_set()¶: returns the set of edges that induced the choice

property model¶: retrieves the associated JANI model

class JaniConstant¶

A Constant in JANI

property defined¶: is constant defined by some expression

property expression_variable¶: expression variable for this constant

property name¶: name of constant

property type¶: type of constant

class JaniEdge¶

A Jani Edge

property action_index¶: action index

property color¶: color for the edge

property destinations¶: edge destinations

property guard¶: edge guard

has_silent_action()¶: Is the edge labelled with the silent action

property nr_destinations¶: nr edge destinations

property rate¶: edge rate

property source_location_index¶: index for source location

substitute()¶

property template_edge¶: template edge

class JaniEdgeDestination¶

Destination in Jani

property assignments¶

property probability¶

property target_location_index¶

class JaniLocation¶

A Location in JANI

property assignments¶: location assignments

property name¶: name of the location

class JaniModel¶

A Jani Model

add_automaton()¶: add an automaton (with a unique name)

property automata¶: get automata

check_valid()¶: Some basic checks to ensure validity

property constants¶: get constants

decode_automaton_and_edge_index()¶: get edge and automaton from edge/automaton index

define_constants()¶: define constants with a mapping from the corresponding expression variables to expressions

encode_automaton_and_edge_index()¶: get edge/automaton-index

property expression_manager¶: get expression manager

finalize()¶: finalizes the model. After this action, be careful changing the data structure.

get_automaton_index()¶: get index for automaton name

get_constant()¶: get constant by name

property global_variables¶

has_standard_composition()¶: is the composition the standard composition

property has_undefined_constants¶: Flag if program has undefined constants

property initial_states_restriction¶: initial states restriction

make_standard_compliant()¶: make standard JANI compliant

property model_type¶: Model type

property name¶: model name

remove_constant()¶: remove a constant. Make sure the constant does not appear in the model.

replace_automaton()¶: replace automaton at index

restrict_edges()¶: restrict model to edges given by set

set_model_type()¶: Sets (only) the model type

set_standard_system_composition()¶: sets the composition to the standard composition

substitute_constants()¶: substitute constants

substitute_functions()¶: substitute functions

to_dot()¶

property undefined_constants_are_graph_preserving¶: Flag if the undefined constants do not change the graph structure

class JaniOrderedAssignments¶

Set of assignments

add()¶

clone()¶: clone assignments (performs a deep copy)

substitute()¶: substitute in rhs according to given substitution map

class JaniTemplateEdge¶

Template edge, internal data structure for edges

add_destination()¶

property assignments¶

property destinations¶

property guard¶

class JaniTemplateEdgeDestination¶

Template edge destination, internal data structure for edge destinations

property assignments¶

class JaniVariable¶

A Variable in JANI

property expression_variable¶: expression variable for this variable

property name¶: name of constant

class JaniVariableSet¶

Jani Set of Variables

add_bounded_integer_variable()¶

add_variable()¶

empty()¶: is there a variable in the set?

get_variable_by_expr_variable()¶

get_variable_by_name()¶

class ModelType¶

Type of the model

CTMC = ModelType.CTMC¶

DTMC = ModelType.DTMC¶

MA = ModelType.MA¶

MDP = ModelType.MDP¶

POMDP = ModelType.POMDP¶

class OperatorType¶

Type of an operator (of any sort)

And = OperatorType.And¶

Ceil = OperatorType.Ceil¶

Divide = OperatorType.Divide¶

Equal = OperatorType.Equal¶

Floor = OperatorType.Floor¶

Greater = OperatorType.Greater¶

GreaterOrEqual = OperatorType.GreaterOrEqual¶

Iff = OperatorType.Iff¶

Implies = OperatorType.Implies¶

Ite = OperatorType.Ite¶

Less = OperatorType.Less¶

LessOrEqual = OperatorType.LessOrEqual¶

Max = OperatorType.Max¶

Min = OperatorType.Min¶

Minus = OperatorType.Minus¶

Modulo = OperatorType.Modulo¶

Not = OperatorType.Not¶

NotEqual = OperatorType.NotEqual¶

Or = OperatorType.Or¶

Plus = OperatorType.Plus¶

Power = OperatorType.Power¶

Times = OperatorType.Times¶

Xor = OperatorType.Xor¶

class ParametricSparseMatrix¶

Parametric sparse matrix

get_row()¶: Get row

get_row_group_end()¶

get_row_group_start()¶

get_rows()¶: Get rows from start to end

property has_trivial_row_grouping¶: Trivial row grouping

property nr_columns¶: Number of columns

property nr_entries¶: Number of non-zero entries

property nr_rows¶: Number of rows

print_row()¶: Print row

row_iter()¶: Get iterator from start to end

submatrix()¶: Get submatrix

class ParametricSparseMatrixEntry¶

Entry of parametric sparse matrix

property column¶: Column

set_value()¶: Set value

value()¶: Value

class ParametricSparseMatrixRows¶: Set of rows in a parametric sparse matrix

class PrismAssignment¶

An assignment in prism

property expression¶: Expression for the update

property variable¶: Variable that is updated

class PrismBooleanVariable¶: A program boolean variable in a Prism program

class PrismCommand¶

A command in a Prism program

property global_index¶: Get global index

property guard_expression¶: Get guard expression

property updates¶: Updates in the command

class PrismIntegerVariable¶

A program integer variable in a Prism program

property lower_bound_expression¶: The the lower bound expression of this integer variable

property upper_bound_expression¶: The the upper bound expression of this integer variable

class PrismModelType¶

Type of the prism model

CTMC = PrismModelType.CTMC¶

CTMDP = PrismModelType.CTMDP¶

DTMC = PrismModelType.DTMC¶

MA = PrismModelType.MA¶

MDP = PrismModelType.MDP¶

UNDEFINED = PrismModelType.UNDEFINED¶

class PrismModule¶

A module in a Prism program

property boolean_variables¶: All boolean Variables of this module

property commands¶: Commands in the module

property integer_variables¶: All integer Variables of this module

property name¶: Name of the module

class PrismProgram¶

A Prism Program

property constants¶: Get Program Constants

define_constants()¶: Define constants

property expression_manager¶: Get the expression manager for expressions in this program

get_label_expression()¶: Get the expression of the given label.

property hasUndefinedConstants¶: Does the program have undefined constants?

property has_undefined_constants¶: Flag if program has undefined constants

property isDeterministicModel¶: Does the program describe a deterministic model?

property model_type¶: Model type

property modules¶: Modules in the program

property nr_modules¶: Number of modules

restrict_commands()¶: Restrict commands

simplify()¶: Simplify

substitute_constants()¶: Substitute constants within program

to_jani()¶: Transform to Jani program

property undefined_constants_are_graph_preserving¶: Flag if the undefined constants do not change the graph structure

used_constants()¶: Compute Used Constants

property variables¶: Get all Expression Variables used by the program

class PrismUpdate¶

An update in a Prism command

property assignments¶: Assignments in the update

property probability_expression¶: The probability expression for this update

class PrismVariable¶

A program variable in a Prism program

property expression_variable¶: The expression variable corresponding to the variable

property initial_value_expression¶: The expression represented the initial value of the variable

property name¶: Variable name

class SchedulerChoiceDouble¶

A choice of a finite memory scheduler

property defined¶: Is the choice defined by the scheduler?

property deterministic¶: Is the choice deterministic (given by a Dirac distribution)?

get_choice()¶: Get the distribution over the actions

get_deterministic_choice()¶: Get the deterministic choice

class SchedulerDouble¶

A Finite Memory Scheduler

compute_action_support()¶

property deterministic¶: Is the scheduler deterministic?

get_choice()¶

property memory_size¶: How much memory does the scheduler take?

property memoryless¶: Is the scheduler memoryless?

class SimpleValuation¶

Valuations for storm variables

get_boolean_value()¶

get_integer_value()¶

class SparseCtmc¶: CTMC in sparse representation

class SparseDtmc¶: DTMC in sparse representation

class SparseMA¶: MA in sparse representation

class SparseMatrix¶

Sparse matrix

get_row()¶: Get row

get_row_group_end()¶

get_row_group_start()¶

get_rows()¶: Get rows from start to end

property has_trivial_row_grouping¶: Trivial row grouping

property nr_columns¶: Number of columns

property nr_entries¶: Number of non-zero entries

property nr_rows¶: Number of rows

print_row()¶: Print rows from start to end

row_iter()¶: Get iterator from start to end

submatrix()¶: Get submatrix

class SparseMatrixEntry¶

Entry of sparse matrix

property column¶: Column

set_value()¶: Set value

value()¶: Value

class SparseMatrixRows¶: Set of rows in a sparse matrix

class SparseMdp¶

MDP in sparse representation

apply_scheduler()¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseModelAction¶

Action for state in sparse model

property id¶: Id

property transitions¶: Get transitions

class SparseModelActions¶: Actions for state in sparse model

class SparseModelState¶

State in sparse model

property actions¶: Get actions

property id¶: Id

property labels¶: Labels

class SparseModelStates¶: States in sparse model

class SparseParametricCtmc¶: pCTMC in sparse representation

class SparseParametricDtmc¶: pDTMC in sparse representation

class SparseParametricMA¶: pMA in sparse representation

class SparseParametricMdp¶

pMDP in sparse representation

apply_scheduler()¶: apply scheduler

property nondeterministic_choice_indices¶

class SparseParametricModelAction¶

Action for state in sparse parametric model

property id¶: Id

property transitions¶: Get transitions

class SparseParametricModelActions¶: Actions for state in sparse parametric model

class SparseParametricModelState¶

State in sparse parametric model

property actions¶: Get actions

property id¶: Id

property labels¶: Labels

class SparseParametricModelStates¶: States in sparse parametric model

class SparseParametricRewardModel¶

Reward structure for parametric sparse models

get_state_action_reward()¶

get_state_reward()¶

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

reduce_to_state_based_rewards()¶: Reduce to state-based rewards

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class SparsePomdp¶

POMDP in sparse representation

property nr_observations¶

property observations¶

class SparseRewardModel¶

Reward structure for sparse models

get_state_action_reward()¶

get_state_reward()¶

get_zero_reward_states()¶: get states where all rewards are zero

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

reduce_to_state_based_rewards()¶: Reduce to state-based rewards

property state_action_rewards¶

property state_rewards¶

property transition_rewards¶

class StateGenerator¶

Interactively explore states using Storm’s PrismNextStateGenerator.

Variables: program – A PRISM program.

current_state_satisfies()¶

Check if the currently loaded state satisfies the given expression.

Parameters: expression (stormpy.Expression) – The expression to check against.
Return type: bool

current_state_to_valuation()¶

Return a valuation for the currently loaded state.

Return type: stormpy.ValuationMapping

expand()¶

Expand the currently loaded state and return its successors.

Return type: [[(state_id, probability)]]

load()¶

Parameters: state_id – The ID of the state to load.

load_initial_state()¶

Loads the (unique) initial state. Multiple initial states are not supported.

Return type: the ID of the initial state.

class StateLabeling¶

Labeling for states

add_label_to_state()¶: Add label to state

get_labels_of_state()¶: Get labels of given state

get_states()¶: Get all states which have the given label

has_state_label()¶: Check if the given state has the given label

set_states()¶: Set all states which have the given label

class StateValuation¶

Valuations for explicit states

get_state()¶

class SymbolicSylvanCtmc¶: CTMC in symbolic representation

class SymbolicSylvanDtmc¶: DTMC in symbolic representation

class SymbolicSylvanMA¶: MA in symbolic representation

class SymbolicSylvanMdp¶: MDP in symbolic representation

class SymbolicSylvanParametricCtmc¶: pCTMC in symbolic representation

class SymbolicSylvanParametricDtmc¶: pDTMC in symbolic representation

class SymbolicSylvanParametricMA¶: pMA in symbolic representation

class SymbolicSylvanParametricMdp¶: pMDP in symbolic representation

class SymbolicSylvanParametricRewardModel¶

Reward structure for parametric symbolic models

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

class SymbolicSylvanRewardModel¶

Reward structure for symbolic models

property has_state_action_rewards¶

property has_state_rewards¶

property has_transition_rewards¶

class ValuationMapping¶

A valuation mapping for a state consists of a mapping from variable to value for each of the three types.

property boolean_values¶

property integer_values¶

property rational_values¶

class Variable¶

Represents a variable

get_expression()¶: Get expression from variable

has_bitvector_type()¶: Check if the variable is of bitvector type

has_boolean_type()¶: Check if the variable is of boolean type

has_integer_type()¶: Check if the variable is of integer type

has_numerical_type()¶: Check if the variable is of numerical type

has_rational_type()¶: Check if the variable is of rational type

property name¶: Variable name

eliminate_reward_accumulations()¶: Eliminate reward accumulations