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