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 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 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 Prism_Boolean_Variable

A program boolean variable in a Prism program

class Prism_Integer_Variable

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 Prism_Variable

A program variable in a Prism program

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 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 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 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 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