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

defined¶

Is the constant defined?

expression_variable¶

Expression variable

name¶

Constant name

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()¶

contains_variable()¶

Check if the expression contains any of the given variables.

contains_variables()¶

Check if the expression contains variables.

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

is_literal()¶

Check if the expression is a literal

manager¶

Get the manager

substitute()¶

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

is_boolean¶

is_integer¶

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

expression¶

class JaniAutomaton¶

A Jani Automation

add_edge()¶

add_initial_location()¶

add_location()¶

adds a new location, returns the index

edges¶

get edges

initial_location_indices¶

initial_states_restriction¶

initial state restriction

location_variable¶

locations¶

name¶

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

model¶

retrieves the associated JANI model

class JaniConstant¶

A Constant in JANI

defined¶

is constant defined by some expression

expression_variable¶

expression variable for this constant

name¶

name of constant

type¶

type of constant

class JaniEdge¶

A Jani Edge

action_index¶

action index

color¶

color for the edge

destinations¶

edge destinations

guard¶

edge guard

has_silent_action()¶

Is the edge labelled with the silent action

nr_destinations¶

nr edge destinations

rate¶

edge rate

source_location_index¶

index for source location

substitute()¶

template_edge¶

template edge

class JaniEdgeDestination¶

Destination in Jani

assignments¶

probability¶

target_location_index¶

class JaniLocation¶

A Location in JANI

assignments¶

location assignments

name¶

name of the location

class JaniModel¶

A Jani Model

add_automaton()¶

add an automaton (with a unique name)

automata¶

get automata

check_valid()¶

Some basic checks to ensure validity

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

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

global_variables¶

has_standard_composition()¶

is the composition the standard composition

has_undefined_constants¶

Flag if program has undefined constants

initial_states_restriction¶

initial states restriction

make_standard_compliant()¶

make standard JANI compliant

model_type¶

Model type

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()¶

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()¶

assignments¶

destinations¶

guard¶

class JaniTemplateEdgeDestination¶

Template edge destination, internal data structure for edge destinations

assignments¶

class JaniVariable¶

A Variable in JANI

expression_variable¶

expression variable for this variable

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

Parametric sparse matrix

get_row()¶

Get row

get_row_group_end()¶

get_row_group_start()¶

get_rows()¶

Get rows from start to end

has_trivial_row_grouping¶

Trivial row grouping

nr_columns¶

Number of columns

nr_entries¶

Number of non-zero entries

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

column¶

Column

set_value()¶

Set value

value()¶

Value

class ParametricSparseMatrixRows¶

Set of rows in a parametric sparse matrix

class PrismAssignment¶

An assignment in prism

expression¶

Expression for the update

variable¶

Variable that is updated

class PrismCommand¶

A command in a Prism program

global_index¶

Get global index

guard_expression¶

Get guard expression

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

commands¶

Commands in the module

name¶

Name of the module

class PrismProgram¶

A Prism Program

constants¶

Get Program Constants

define_constants()¶

Define constants

expression_manager¶

Get the expression manager for expressions in this program

has_undefined_constants¶

Flag if program has undefined constants

model_type¶

Model type

modules¶

Modules in the program

nr_modules¶

Number of modules

restrict_commands()¶

Restrict commands

simplify()¶

Simplify

substitute_constants()¶

Substitute constants within program

to_jani()¶

Transform to Jani program

undefined_constants_are_graph_preserving¶

Flag if the undefined constants do not change the graph structure

used_constants()¶

Compute Used Constants

class PrismUpdate¶

An update in a Prism command

assignments¶

Assignments in the update

class SchedulerChoiceDouble¶

A choice of a finite memory scheduler

defined¶

Is the choice defined by the scheduler?

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()¶

deterministic¶

Is the scheduler deterministic?

get_choice()¶

memory_size¶

How much memory does the scheduler take?

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

has_trivial_row_grouping¶

Trivial row grouping

nr_columns¶

Number of columns

nr_entries¶

Number of non-zero entries

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

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

nondeterministic_choice_indices¶

class SparseModelAction¶

Action for state in sparse model

id¶

Id

transitions¶

Get transitions

class SparseModelActions¶

Actions for state in sparse model

class SparseModelState¶

State in sparse model

actions¶

Get actions

id¶

Id

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

nondeterministic_choice_indices¶

class SparseParametricModelAction¶

Action for state in sparse parametric model

id¶

Id

transitions¶

Get transitions

class SparseParametricModelActions¶

Actions for state in sparse parametric model

class SparseParametricModelState¶

State in sparse parametric model

actions¶

Get actions

id¶

Id

labels¶

Labels

class SparseParametricModelStates¶

States in sparse parametric model

class SparseParametricRewardModel¶

Reward structure for parametric sparse models

get_state_action_reward()¶

get_state_reward()¶

has_state_action_rewards¶

has_state_rewards¶

has_transition_rewards¶

reduce_to_state_based_rewards()¶

Reduce to state-based rewards

state_action_rewards¶

state_rewards¶

transition_rewards¶

class SparsePomdp¶

POMDP in sparse representation

nr_observations¶

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

has_state_action_rewards¶

has_state_rewards¶

has_transition_rewards¶

reduce_to_state_based_rewards()¶

Reduce to state-based rewards

state_action_rewards¶

state_rewards¶

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

has_state_action_rewards¶

has_state_rewards¶

has_transition_rewards¶

class SymbolicSylvanRewardModel¶

Reward structure for symbolic models

has_state_action_rewards¶

has_state_rewards¶

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

name¶

Variable name

eliminate_reward_accumulations()¶

Eliminate reward accumulations