Stormpy.storage¶
- class AddIterator_Sylvan_Double¶
AddIterator
- get(self: stormpy.storage.storage.AddIterator_Sylvan_Double) Tuple[storm::expressions::SimpleValuation, float] ¶
- class Add_Sylvan_Double¶
Add
- class Bdd_Sylvan¶
Bdd
- to_expression(self: stormpy.storage.storage.Bdd_Sylvan, expression_manager: storm::expressions::ExpressionManager) Tuple[List[storm::expressions::Expression], Dict[int, storm::expressions::Variable]] ¶
- class BitVector¶
- as_int(self: stormpy.storage.storage.BitVector, index: int, no_bits: int) int ¶
Get as unsigned int
- get(self: stormpy.storage.storage.BitVector, index: int) bool ¶
- static load_from_string(description: str) stormpy.storage.storage.BitVector ¶
- number_of_set_bits(self: stormpy.storage.storage.BitVector) int ¶
- set(self: stormpy.storage.storage.BitVector, index: int, value: bool = True) None ¶
Set
- size(self: stormpy.storage.storage.BitVector) int ¶
- store_as_string(self: stormpy.storage.storage.BitVector) str ¶
- class ChoiceLabeling¶
Labeling for choices
- add_label_to_choice(self: stormpy.storage.storage.ChoiceLabeling, label: str, state: int) None ¶
Adds a label to a given choice
- get_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str) stormpy.storage.storage.BitVector ¶
Get all choices which have the given label
- get_labels_of_choice(self: stormpy.storage.storage.ChoiceLabeling, choice: int) Set[str] ¶
Get labels of the given choice
- set_choices(self: stormpy.storage.storage.ChoiceLabeling, label: str, choices: stormpy.storage.storage.BitVector) None ¶
Add a label to a the given choices
- class ChoiceOrigins¶
This class represents the origin of choices of a model in terms of the input model spec.
- as_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) storm::storage::sparse::JaniChoiceOrigins ¶
- as_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) storm::storage::sparse::PrismChoiceOrigins ¶
- get_choice_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) str ¶
human readable string
- get_identifier_info(self: stormpy.storage.storage.ChoiceOrigins, identifier: int) str ¶
human readable string
- get_number_of_identifiers(self: stormpy.storage.storage.ChoiceOrigins) int ¶
the number of considered identifier
- is_jani_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) bool ¶
- is_prism_choice_origins(self: stormpy.storage.storage.ChoiceOrigins) bool ¶
- class DdManager_Sylvan¶
- get_meta_variable(self: stormpy.storage.storage.DdManager_Sylvan, expression_variable: storm::expressions::Variable) stormpy.storage.storage.DdMetaVariable_Sylvan ¶
- class DdMetaVariableType¶
Members:
Int
Bool
Bitvector
- Bitvector = <DdMetaVariableType.Bitvector: 2>¶
- Bool = <DdMetaVariableType.Bool: 0>¶
- Int = <DdMetaVariableType.Int: 1>¶
- property name¶
- property value¶
- class DdMetaVariable_Sylvan¶
- compute_indices(self: stormpy.storage.storage.DdMetaVariable_Sylvan, sorted: bool = True) List[int] ¶
- property lowest_value¶
- property name¶
- property type¶
- class Dd_Sylvan¶
Dd
- property dd_manager¶
get the manager
- property meta_variables¶
the contained meta variables
- property node_count¶
get node count
- class DiceStringVisitor¶
Translate expressions to dice
- to_string(self: stormpy.storage.storage.DiceStringVisitor, arg0: stormpy.storage.storage.Expression) str ¶
- class Distribution¶
Finite Support Distribution
- class DistributionExact¶
Finite Support Distribution
- class DistributionInterval¶
Finite Support Distribution
- class ExactSparseMatrix¶
Sparse matrix
- get_row(self: stormpy.storage.storage.ExactSparseMatrix, row: int) storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::rows ¶
Get row
- get_row_group_end(self: stormpy.storage.storage.ExactSparseMatrix, arg0: int) int ¶
- get_row_group_start(self: stormpy.storage.storage.ExactSparseMatrix, arg0: int) int ¶
- get_rows_for_group(self: stormpy.storage.storage.ExactSparseMatrix, row_group: int) List[int] ¶
Get rows within a row group
- property has_trivial_row_grouping¶
Trivial row grouping
- make_row_grouping_trivial(self: stormpy.storage.storage.ExactSparseMatrix) None ¶
Makes row groups trivial. Use with care.
- property nr_columns¶
Number of columns
- property nr_entries¶
Number of non-zero entries
- property nr_rows¶
Number of rows
- print_row(self: stormpy.storage.storage.ExactSparseMatrix, row: int) str ¶
Print rows from start to end
- row_iter(self: stormpy.storage.storage.ExactSparseMatrix, row_start: int, row_end: int) Iterator ¶
Get iterator from start to end
- submatrix(self: stormpy.storage.storage.ExactSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.ExactSparseMatrix ¶
Get submatrix
- class ExactSparseMatrixBuilder¶
Builder of sparse matrix
- add_next_value(self: stormpy.storage.storage.ExactSparseMatrixBuilder, row: int, column: int, value: pycarl.gmp.gmp.Rational) None ¶
Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.
Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are treated as empty. If these constraints are not met, an exception is thrown.
- Parameters:
row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column
- build(self: stormpy.storage.storage.ExactSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > ¶
Finalize the sparse matrix
- get_current_row_group_count(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int ¶
Get the current row group count
- get_last_column(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int ¶
the most recently used column
- get_last_row(self: stormpy.storage.storage.ExactSparseMatrixBuilder) int ¶
Get the most recently used row
- new_row_group(self: stormpy.storage.storage.ExactSparseMatrixBuilder, starting_row: int) None ¶
Start a new row group in the matrix
- replace_columns(self: stormpy.storage.storage.ExactSparseMatrixBuilder, replacements: List[int], offset: int) None ¶
Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.
- Parameters:
replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.
- class ExactSparseMatrixEntry¶
Entry of sparse matrix
- property column¶
Column
- set_value(self: stormpy.storage.storage.ExactSparseMatrixEntry, value: pycarl.gmp.gmp.Rational) None ¶
Set value
- value(self: stormpy.storage.storage.ExactSparseMatrixEntry) pycarl.gmp.gmp.Rational ¶
Value
- class ExactSparseMatrixRows¶
Set of rows in a sparse matrix
- class Expression¶
Holds an expression
- static And(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Conjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression ¶
- static Disjunction(arg0: List[stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression ¶
- static Divide(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Eq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Geq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Greater(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Iff(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Implies(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Leq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Less(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Minus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Modulo(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Multiply(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Neq(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Or(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- static Plus(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
- property arity¶
The arity of the expression
- contains_variable(self: stormpy.storage.storage.Expression, variables: Set[stormpy.storage.storage.Variable]) bool ¶
Check if the expression contains any of the given variables.
- contains_variables(self: stormpy.storage.storage.Expression) bool ¶
Check if the expression contains variables.
- evaluate_as_bool(self: stormpy.storage.storage.Expression) bool ¶
Get the boolean value this expression evaluates to
- evaluate_as_double(self: stormpy.storage.storage.Expression) float ¶
Get the double value this expression evaluates to
- evaluate_as_int(self: stormpy.storage.storage.Expression) int ¶
Get the integer value this expression evaluates to
- evaluate_as_rational(self: stormpy.storage.storage.Expression) pycarl.gmp.gmp.Rational ¶
Get the rational number this expression evaluates to
- get_operand(self: stormpy.storage.storage.Expression, operandIndex: int) stormpy.storage.storage.Expression ¶
Get the operand at the given index
- get_variables(self: stormpy.storage.storage.Expression) Set[stormpy.storage.storage.Variable] ¶
Get the variables
- has_boolean_type(self: stormpy.storage.storage.Expression) bool ¶
Check if the expression is a boolean
- has_integer_type(self: stormpy.storage.storage.Expression) bool ¶
Check if the expression is an integer
- has_rational_type(self: stormpy.storage.storage.Expression) bool ¶
Check if the expression is a rational
- identifier(self: stormpy.storage.storage.Expression) str ¶
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(self: stormpy.storage.storage.Expression) bool ¶
Check if the expression is a literal
- is_variable(self: stormpy.storage.storage.Expression) bool ¶
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)
- simplify(self: stormpy.storage.storage.Expression) stormpy.storage.storage.Expression ¶
Simplify expression
- substitute(self: stormpy.storage.storage.Expression, substitution_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) stormpy.storage.storage.Expression ¶
- property type¶
Get the Type
- class ExpressionManager¶
Manages variables for expressions
- create_boolean(self: stormpy.storage.storage.ExpressionManager, boolean: bool) storm::expressions::Expression ¶
Create expression from boolean
- create_boolean_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable ¶
create Boolean variable
- create_integer(self: stormpy.storage.storage.ExpressionManager, integer: int) storm::expressions::Expression ¶
Create expression from integer number
- create_integer_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable ¶
create Integer variable
- create_rational(self: stormpy.storage.storage.ExpressionManager, rational: pycarl.gmp.gmp.Rational) storm::expressions::Expression ¶
Create expression from rational number
- create_rational_variable(self: stormpy.storage.storage.ExpressionManager, name: str, auxiliary: bool = False) storm::expressions::Variable ¶
create Rational variable
- get_variable(self: stormpy.storage.storage.ExpressionManager, name: str) storm::expressions::Variable ¶
get variably by name
- get_variables(self: stormpy.storage.storage.ExpressionManager) Set[storm::expressions::Variable] ¶
Retrieves the set of all variables known to this manager.
- class ExpressionParser¶
Parser for storm-expressions
- parse(self: stormpy.storage.storage.ExpressionParser, string: str, ignore_error: bool = False) stormpy.storage.storage.Expression ¶
parse
- set_identifier_mapping(self: stormpy.storage.storage.ExpressionParser, arg0: Dict[str, stormpy.storage.storage.Expression]) None ¶
sets identifiers
- class ExpressionType¶
The type of an expression
- property is_boolean¶
- property is_integer¶
- property is_rational¶
- class IntervalSparseMatrix¶
Sparse matrix
- get_row(self: stormpy.storage.storage.IntervalSparseMatrix, row: int) storm::storage::SparseMatrix<carl::Interval<double> >::rows ¶
Get row
- get_row_group_end(self: stormpy.storage.storage.IntervalSparseMatrix, arg0: int) int ¶
- get_row_group_start(self: stormpy.storage.storage.IntervalSparseMatrix, arg0: int) int ¶
- get_rows_for_group(self: stormpy.storage.storage.IntervalSparseMatrix, row_group: int) List[int] ¶
Get rows within a row group
- property has_trivial_row_grouping¶
Trivial row grouping
- make_row_grouping_trivial(self: stormpy.storage.storage.IntervalSparseMatrix) None ¶
Makes row groups trivial. Use with care.
- property nr_columns¶
Number of columns
- property nr_entries¶
Number of non-zero entries
- property nr_rows¶
Number of rows
- print_row(self: stormpy.storage.storage.IntervalSparseMatrix, row: int) str ¶
Print rows from start to end
- row_iter(self: stormpy.storage.storage.IntervalSparseMatrix, row_start: int, row_end: int) Iterator ¶
Get iterator from start to end
- submatrix(self: stormpy.storage.storage.IntervalSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.IntervalSparseMatrix ¶
Get submatrix
- class IntervalSparseMatrixBuilder¶
Builder of sparse matrix
- add_next_value(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, row: int, column: int, value: pycarl.core.Interval) None ¶
Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.
Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are treated as empty. If these constraints are not met, an exception is thrown.
- Parameters:
row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column
- build(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<carl::Interval<double> > ¶
Finalize the sparse matrix
- get_current_row_group_count(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int ¶
Get the current row group count
- get_last_column(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int ¶
the most recently used column
- get_last_row(self: stormpy.storage.storage.IntervalSparseMatrixBuilder) int ¶
Get the most recently used row
- new_row_group(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, starting_row: int) None ¶
Start a new row group in the matrix
- replace_columns(self: stormpy.storage.storage.IntervalSparseMatrixBuilder, replacements: List[int], offset: int) None ¶
Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.
- Parameters:
replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.
- class IntervalSparseMatrixEntry¶
Entry of sparse matrix
- property column¶
Column
- set_value(self: stormpy.storage.storage.IntervalSparseMatrixEntry, value: pycarl.core.Interval) None ¶
Set value
- value(self: stormpy.storage.storage.IntervalSparseMatrixEntry) pycarl.core.Interval ¶
Value
- class IntervalSparseMatrixRows¶
Set of rows in a sparse matrix
- class ItemLabeling¶
Labeling
- add_label(self: stormpy.storage.storage.ItemLabeling, label: str) None ¶
Add label
- contains_label(self: stormpy.storage.storage.ItemLabeling, label: str) bool ¶
Check if the given label is contained in the labeling
- get_labels(self: stormpy.storage.storage.ItemLabeling) Set[str] ¶
Get all labels
- class JaniAssignment¶
Jani Assignment
- property expression¶
- property variable¶
variable that is assigned to, if any
- class JaniAutomaton¶
A Jani Automation
- add_edge(self: stormpy.storage.storage.JaniAutomaton, edge: storm::jani::Edge) None ¶
- add_initial_location(self: stormpy.storage.storage.JaniAutomaton, index: int) None ¶
- add_location(self: stormpy.storage.storage.JaniAutomaton, location: storm::jani::Location) int ¶
adds a new location, returns the index
- property edges¶
get edges
- get_location_index(self: stormpy.storage.storage.JaniAutomaton, name: str) int ¶
- property initial_location_indices¶
- property initial_states_restriction¶
initial state restriction
- property location_variable¶
- property locations¶
- property name¶
- property variables¶
- class JaniChoiceOrigins¶
This class represents for each choice the origin in the jani spec.
- get_edge_index_set(self: stormpy.storage.storage.JaniChoiceOrigins, choice_index: int) stormpy.core.FlatSet ¶
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(self: stormpy.storage.storage.JaniEdge) bool ¶
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(self: stormpy.storage.storage.JaniEdge, mapping: Dict[storm::expressions::Variable, storm::expressions::Expression], substitute_transcendental_numbers: bool) None ¶
- property template_edge¶
template edge
- class JaniEdgeDestination¶
Destination in Jani
- property assignments¶
- property probability¶
- property target_location_index¶
- class JaniInformationObject¶
An object holding information about a JANI model
- property avg_var_domain_size¶
- property model_type¶
- property nr_automata¶
- property nr_edges¶
- property nr_variables¶
- property state_domain_size¶
- class JaniLocation¶
A Location in JANI
- property assignments¶
location assignments
- property name¶
name of the location
- class JaniLocationExpander¶
A transformer for Jani expanding variables into locations
- transform(self: stormpy.storage.storage.JaniLocationExpander, automaton_name: str, variable_name: str) storm::jani::JaniLocationExpander::ReturnType ¶
- class JaniModel¶
A Jani Model
- add_automaton(self: stormpy.storage.storage.JaniModel, automaton: storm::jani::Automaton) int ¶
add an automaton (with a unique name)
- add_constant(self: stormpy.storage.storage.JaniModel, constant: storm::jani::Constant) None ¶
adds constant to model
- property automata¶
get automata
- check_valid(self: stormpy.storage.storage.JaniModel) None ¶
Some basic checks to ensure validity
- property constants¶
get constants
- static decode_automaton_and_edge_index(arg0: int) Tuple[int, int] ¶
get edge and automaton from edge/automaton index
- define_constants(self: stormpy.storage.storage.JaniModel, map: Dict[storm::expressions::Variable, storm::expressions::Expression]) stormpy.storage.storage.JaniModel ¶
define constants with a mapping from the corresponding expression variables to expressions
- static encode_automaton_and_edge_index(arg0: int, arg1: int) int ¶
get edge/automaton-index
- property expression_manager¶
get expression manager
- finalize(self: stormpy.storage.storage.JaniModel) None ¶
finalizes the model. After this action, be careful changing the data structure.
- flatten_composition(self: stormpy.storage.storage.JaniModel, smt_solver_factory: stormpy.utility.utility.SmtSolverFactory = <stormpy.utility.utility.SmtSolverFactory object at 0x7f327f773370>) stormpy.storage.storage.JaniModel ¶
- get_automaton(self: stormpy.storage.storage.JaniModel, name: str) storm::jani::Automaton ¶
- get_automaton_index(self: stormpy.storage.storage.JaniModel, name: str) int ¶
get index for automaton name
- get_constant(self: stormpy.storage.storage.JaniModel, name: str) storm::jani::Constant ¶
get constant by name
- property global_variables¶
- has_standard_composition(self: stormpy.storage.storage.JaniModel) bool ¶
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(self: stormpy.storage.storage.JaniModel) None ¶
make standard JANI compliant
- property model_type¶
Model type
- property name¶
model name
- remove_constant(self: stormpy.storage.storage.JaniModel, constant_name: str) None ¶
remove a constant. Make sure the constant does not appear in the model.
- replace_automaton(self: stormpy.storage.storage.JaniModel, index: int, new_automaton: storm::jani::Automaton) None ¶
replace automaton at index
- restrict_edges(self: stormpy.storage.storage.JaniModel, edge_set: stormpy.core.FlatSet) stormpy.storage.storage.JaniModel ¶
restrict model to edges given by set
- set_model_type(self: stormpy.storage.storage.JaniModel, arg0: stormpy.core.JaniModelType) None ¶
Sets (only) the model type
- set_standard_system_composition(self: stormpy.storage.storage.JaniModel) None ¶
sets the composition to the standard composition
- substitute_constants(self: stormpy.storage.storage.JaniModel) stormpy.storage.storage.JaniModel ¶
substitute constants
- substitute_functions(self: stormpy.storage.storage.JaniModel) None ¶
substitute functions
- to_dot(self: stormpy.storage.storage.JaniModel) str ¶
- property undefined_constants_are_graph_preserving¶
Flag if the undefined constants do not change the graph structure
- class JaniOrderedAssignments¶
Set of assignments
- add(self: stormpy.storage.storage.JaniOrderedAssignments, new_assignment: storm::jani::Assignment, add_to_existing: bool = False) bool ¶
- clone(self: stormpy.storage.storage.JaniOrderedAssignments) stormpy.storage.storage.JaniOrderedAssignments ¶
clone assignments (performs a deep copy)
- substitute(self: stormpy.storage.storage.JaniOrderedAssignments, substitution_map: Dict[storm::expressions::Variable, storm::expressions::Expression], substitute_transcendental_numbers: bool) None ¶
substitute in rhs according to given substitution map
- class JaniScopeChanger¶
A transformer for Jani changing variables from local to global and vice versa
- make_variables_local(self: stormpy.storage.storage.JaniScopeChanger, model: stormpy.storage.storage.JaniModel, properties: List[stormpy.core.Property] = []) stormpy.storage.storage.JaniModel ¶
- class JaniTemplateEdge¶
Template edge, internal data structure for edges
- add_destination(self: stormpy.storage.storage.JaniTemplateEdge, arg0: storm::jani::TemplateEdgeDestination) None ¶
- 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 init_expression¶
- property name¶
name of constant
- class JaniVariableSet¶
Jani Set of Variables
- add_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::jani::Variable) None ¶
- empty(self: stormpy.storage.storage.JaniVariableSet) bool ¶
is there a variable in the set?
- erase_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::expressions::Variable) storm::jani::Variable ¶
variable
- get_variable_by_expr_variable(self: stormpy.storage.storage.JaniVariableSet, arg0: storm::expressions::Variable) storm::jani::Variable ¶
- get_variable_by_name(self: stormpy.storage.storage.JaniVariableSet, arg0: str) storm::jani::Variable ¶
- class MaximalEndComponentDecomposition_double¶
Decomposition of maximal end components
- property size¶
Number of MECs in the decomposition
- class MaximalEndComponentDecomposition_exact¶
Decomposition of maximal end components
- property size¶
Number of MECs in the decomposition
- class MaximalEndComponentDecomposition_interval¶
Decomposition of maximal end components
- property size¶
Number of MECs in the decomposition
- class MaximalEndComponentDecomposition_ratfunc¶
Decomposition of maximal end components
- property size¶
Number of MECs in the decomposition
- class ModelType¶
Type of the model
Members:
DTMC
MDP
POMDP
CTMC
MA
SMG
- CTMC = <ModelType.CTMC: 1>¶
- DTMC = <ModelType.DTMC: 0>¶
- MA = <ModelType.MA: 3>¶
- MDP = <ModelType.MDP: 2>¶
- POMDP = <ModelType.POMDP: 5>¶
- SMG = <ModelType.SMG: 6>¶
- property name¶
- property value¶
- class OperatorType¶
Type of an operator (of any sort)
Members:
And
Or
Xor
Implies
Iff
Plus
Minus
Times
Divide
Min
Max
Power
Modulo
Equal
NotEqual
Less
LessOrEqual
Greater
GreaterOrEqual
Not
Floor
Ceil
Ite
- And = <OperatorType.And: 0>¶
- Ceil = <OperatorType.Ceil: 24>¶
- Divide = <OperatorType.Divide: 8>¶
- Equal = <OperatorType.Equal: 16>¶
- Floor = <OperatorType.Floor: 23>¶
- Greater = <OperatorType.Greater: 20>¶
- GreaterOrEqual = <OperatorType.GreaterOrEqual: 21>¶
- Iff = <OperatorType.Iff: 4>¶
- Implies = <OperatorType.Implies: 3>¶
- Ite = <OperatorType.Ite: 25>¶
- Less = <OperatorType.Less: 18>¶
- LessOrEqual = <OperatorType.LessOrEqual: 19>¶
- Max = <OperatorType.Max: 10>¶
- Min = <OperatorType.Min: 9>¶
- Minus = <OperatorType.Minus: 6>¶
- Modulo = <OperatorType.Modulo: 12>¶
- Not = <OperatorType.Not: 22>¶
- NotEqual = <OperatorType.NotEqual: 17>¶
- Or = <OperatorType.Or: 1>¶
- Plus = <OperatorType.Plus: 5>¶
- Power = <OperatorType.Power: 11>¶
- Times = <OperatorType.Times: 7>¶
- Xor = <OperatorType.Xor: 2>¶
- property name¶
- property value¶
- class OverlappingGuardAnalyser¶
An SMT driven analysis for overlapping guards
- has_module_with_inner_action_overlapping_guard(self: stormpy.storage.storage.OverlappingGuardAnalyser) bool ¶
- class ParametricSparseMatrix¶
Sparse matrix
- get_row(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >::rows ¶
Get row
- get_row_group_end(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) int ¶
- get_row_group_start(self: stormpy.storage.storage.ParametricSparseMatrix, arg0: int) int ¶
- get_rows_for_group(self: stormpy.storage.storage.ParametricSparseMatrix, row_group: int) List[int] ¶
Get rows within a row group
- property has_trivial_row_grouping¶
Trivial row grouping
- make_row_grouping_trivial(self: stormpy.storage.storage.ParametricSparseMatrix) None ¶
Makes row groups trivial. Use with care.
- property nr_columns¶
Number of columns
- property nr_entries¶
Number of non-zero entries
- property nr_rows¶
Number of rows
- print_row(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) str ¶
Print rows from start to end
- row_iter(self: stormpy.storage.storage.ParametricSparseMatrix, row_start: int, row_end: int) Iterator ¶
Get iterator from start to end
- submatrix(self: stormpy.storage.storage.ParametricSparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.ParametricSparseMatrix ¶
Get submatrix
- class ParametricSparseMatrixBuilder¶
Builder of sparse matrix
- add_next_value(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, row: int, column: int, value: pycarl.cln.cln.FactorizedRationalFunction) None ¶
Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.
Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are treated as empty. If these constraints are not met, an exception is thrown.
- Parameters:
row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column
- build(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > ¶
Finalize the sparse matrix
- get_current_row_group_count(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) int ¶
Get the current row group count
- get_last_column(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) int ¶
the most recently used column
- get_last_row(self: stormpy.storage.storage.ParametricSparseMatrixBuilder) int ¶
Get the most recently used row
- new_row_group(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, starting_row: int) None ¶
Start a new row group in the matrix
- replace_columns(self: stormpy.storage.storage.ParametricSparseMatrixBuilder, replacements: List[int], offset: int) None ¶
Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.
- Parameters:
replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.
- class ParametricSparseMatrixEntry¶
Entry of sparse matrix
- property column¶
Column
- set_value(self: stormpy.storage.storage.ParametricSparseMatrixEntry, value: pycarl.cln.cln.FactorizedRationalFunction) None ¶
Set value
- class ParametricSparseMatrixRows¶
Set of rows in a sparse matrix
- class PolytopeDouble¶
- create_downward_closure(self: stormpy.storage.storage.PolytopeDouble) stormpy.storage.storage.PolytopeDouble ¶
- get_vertices_clockwise(self: stormpy.storage.storage.PolytopeDouble) List[List[float]] ¶
- property vertices¶
- class PolytopeExact¶
- create_downward_closure(self: stormpy.storage.storage.PolytopeExact) stormpy.storage.storage.PolytopeExact ¶
- get_vertices_clockwise(self: stormpy.storage.storage.PolytopeExact) List[List[pycarl.gmp.gmp.Rational]] ¶
- property vertices¶
- 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 PrismChoiceOrigins¶
This class represents for each choice the set of prism commands that induced the choice.
- get_command_set(self: stormpy.storage.storage.PrismChoiceOrigins, choice_index: int) stormpy.core.FlatSet ¶
Returns the set of prism commands that induced the choice
- property program¶
retrieves the associated Prism program
- class PrismCommand¶
A command in a Prism program
- property action_index¶
What is the action index of the command
- property action_name¶
Retrieves the action name of this command
- property global_index¶
Get global index
- property guard_expression¶
Get guard expression
- property is_labeled¶
Retrieves whether the command possesses a synchronization label
- property labeled¶
Is the command labeled
- property updates¶
Updates in the command
- class PrismConstant¶
A constant in a Prism program
- property defined¶
Is the constant defined?
- property definition¶
Defining expression
- property expression_variable¶
Expression variable
- property name¶
Constant name
- property type¶
The type of the constant
- 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
Members:
DTMC
CTMC
MDP
CTMDP
MA
POMDP
UNDEFINED
- CTMC = <PrismModelType.CTMC: 2>¶
- CTMDP = <PrismModelType.CTMDP: 4>¶
- DTMC = <PrismModelType.DTMC: 1>¶
- MA = <PrismModelType.MA: 5>¶
- MDP = <PrismModelType.MDP: 3>¶
- POMDP = <PrismModelType.POMDP: 6>¶
- UNDEFINED = <PrismModelType.UNDEFINED: 0>¶
- property name¶
- property value¶
- class PrismModule¶
A module in a Prism program
- property boolean_variables¶
All boolean Variables of this module
- property commands¶
Commands in the module
- get_boolean_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) storm::prism::BooleanVariable ¶
- get_command_indices_by_action_index(self: stormpy.storage.storage.PrismModule, action_index: int) Set[int] ¶
- get_integer_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) storm::prism::IntegerVariable ¶
- 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(self: stormpy.storage.storage.PrismProgram, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]) stormpy.storage.storage.PrismProgram ¶
Define constants
- property expression_manager¶
Get the expression manager for expressions in this program
- flatten(self: stormpy.storage.storage.PrismProgram, smt_factory: stormpy.utility.utility.SmtSolverFactory = <stormpy.utility.utility.SmtSolverFactory object at 0x7f327f74d6f0>) stormpy.storage.storage.PrismProgram ¶
Put program into a single module
- get_action_name(self: stormpy.storage.storage.PrismProgram, action_index: int) str ¶
Get the action name for a given action index
- get_constant(self: stormpy.storage.storage.PrismProgram, name: str) storm::prism::Constant ¶
Requires that the program has a constant with this name
- get_label_expression(self: stormpy.storage.storage.PrismProgram, label: str) storm::expressions::Expression ¶
Get the expression of the given label.
- get_module(self: stormpy.storage.storage.PrismProgram, module_name: str) storm::prism::Module ¶
- get_module_indices_by_action_index(self: stormpy.storage.storage.PrismProgram, action_index: int) Set[int] ¶
get all modules that have a particular action index
- get_synchronizing_action_indices(self: stormpy.storage.storage.PrismProgram) Set[int] ¶
Get the synchronizing action indices
- get_undefined_constants(self: stormpy.storage.storage.PrismProgram) List[storm::prism::Constant] ¶
Collect the undefined constants
- property global_boolean_variables¶
Retrieves the global boolean variables of the program
- property global_integer_variables¶
Retrieves the global integer variables of the program
- has_constant(self: stormpy.storage.storage.PrismProgram, name: str) bool ¶
- property has_initial_states_expression¶
Is an initial states expression given.
- has_label(self: stormpy.storage.storage.PrismProgram, name: str) bool ¶
- has_reward_model(self: stormpy.storage.storage.PrismProgram, name: str) bool ¶
Is a reward model with the specified name defined?
- property has_undefined_constants¶
Flag if program has undefined constants
- property initial_states_expression¶
Get the initial states expression, or none, if none exists
- property is_deterministic_model¶
Does the program describe a deterministic model?
- label_unlabelled_commands(self: stormpy.storage.storage.PrismProgram, name_suggestions: Dict[int, str]) stormpy.storage.storage.PrismProgram ¶
Label unlabelled commands
- property labels¶
Get all labels in the program
- property model_type¶
Model type
- property modules¶
Modules in the program
- property nr_modules¶
Number of modules
- property number_of_unlabeled_commands¶
Gets the number of commands that are not labelled
- replace_constant_by_variable(self: stormpy.storage.storage.PrismProgram, constant: storm::prism::Constant, lower_bound: storm::expressions::Expression, upper_bound: storm::expressions::Expression, observable: bool = True) stormpy.storage.storage.PrismProgram ¶
Operation to take a constant and make it into a global variable (ranging from lower to upper bound).
- replace_variable_initialization_by_init_expression(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram ¶
Replaces initializations from the individual variables to a init expression.
- restrict_commands(self: stormpy.storage.storage.PrismProgram, arg0: stormpy.core.FlatSet) stormpy.storage.storage.PrismProgram ¶
Restrict commands
- property reward_models¶
The defined reward models
- simplify(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram ¶
Simplify
- substitute_constants(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram ¶
Substitute constants within program
- substitute_formulas(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram ¶
Substitute formulas within program
- substitute_nonstandard_predicates(self: stormpy.storage.storage.PrismProgram) stormpy.storage.storage.PrismProgram ¶
Remove nonstandard predicates from the prism program
- to_jani(self: stormpy.storage.storage.PrismProgram, properties: List[stormpy.core.Property], all_variables_global: bool = True, suffix: str = '') Tuple[storm::jani::Model, List[stormpy.core.Property]] ¶
Transform to Jani program
- property undefined_constants_are_graph_preserving¶
Flag if the undefined constants do not change the graph structure
- update_initial_states_expression(self: stormpy.storage.storage.PrismProgram, new_expression: storm::expressions::Expression) None ¶
Replace initial expression. Can only be called if initial expression exists.
- used_constants(self: stormpy.storage.storage.PrismProgram) List[storm::prism::Constant] ¶
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
- get_as_variable_to_expression_map(self: stormpy.storage.storage.PrismUpdate) Dict[storm::expressions::Variable, storm::expressions::Expression] ¶
Creates a mapping representation of this update
- get_assignment(self: stormpy.storage.storage.PrismUpdate, variable_name: str) storm::prism::Assignment ¶
Retrieves a reference to the assignment for the variable with the given name
- property global_index¶
Retrieves the global index of the update, that is, a unique index over all modules
- property probability_expression¶
The probability expression for this update
- simplify(self: stormpy.storage.storage.PrismUpdate) stormpy.storage.storage.PrismUpdate ¶
Simplifies the update in various ways (also removes identity assignments)
- substitute(self: stormpy.storage.storage.PrismUpdate, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]) stormpy.storage.storage.PrismUpdate ¶
Substitutes all identifiers in the update according to the given map
- 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 Scheduler¶
A Finite Memory Scheduler
- cast_to_double_datatype(self: stormpy.storage.storage.Scheduler) stormpy.storage.storage.Scheduler ¶
Construct the scheduler with double value type
- cast_to_exact_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > ¶
Construct the scheduler with exact value type
- cast_to_interval_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<carl::Interval<double> > ¶
Construct the scheduler with interval value type
- cast_to_parametric_datatype(self: stormpy.storage.storage.Scheduler) storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > ¶
Construct the scheduler with parametric value type
- compute_action_support(self: stormpy.storage.storage.Scheduler, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector ¶
- property deterministic¶
Is the scheduler deterministic?
- get_choice(self: stormpy.storage.storage.Scheduler, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<double> ¶
- property memory_size¶
How much memory does the scheduler take?
- property memoryless¶
Is the scheduler memoryless?
- property partial¶
Is the scheduler partial?
- set_choice(self: stormpy.storage.storage.Scheduler, choice: storm::storage::SchedulerChoice<double>, state: int, memory_index: int = 0) None ¶
- to_json_str(self: stormpy.storage.storage.Scheduler, model: stormpy.storage.storage._SparseModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str ¶
- class SchedulerChoice¶
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(self: stormpy.storage.storage.SchedulerChoice) storm::storage::Distribution<double, unsigned long> ¶
Get the distribution over the actions
- get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoice) int ¶
Get the deterministic choice
- class SchedulerChoiceExact¶
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(self: stormpy.storage.storage.SchedulerChoiceExact) storm::storage::Distribution<__gmp_expr<__mpq_struct [1], __mpq_struct [1]>, unsigned long> ¶
Get the distribution over the actions
- get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceExact) int ¶
Get the deterministic choice
- class SchedulerChoiceInterval¶
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(self: stormpy.storage.storage.SchedulerChoiceInterval) storm::storage::Distribution<carl::Interval<double>, unsigned long> ¶
Get the distribution over the actions
- get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceInterval) int ¶
Get the deterministic choice
- class SchedulerChoiceParametric¶
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(self: stormpy.storage.storage.SchedulerChoiceParametric) storm::storage::Distribution<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, unsigned long> ¶
Get the distribution over the actions
- get_deterministic_choice(self: stormpy.storage.storage.SchedulerChoiceParametric) int ¶
Get the deterministic choice
- class SchedulerExact¶
A Finite Memory Scheduler
- cast_to_double_datatype(self: stormpy.storage.storage.SchedulerExact) stormpy.storage.storage.Scheduler ¶
Construct the scheduler with double value type
- cast_to_exact_datatype(self: stormpy.storage.storage.SchedulerExact) stormpy.storage.storage.SchedulerExact ¶
Construct the scheduler with exact value type
- cast_to_interval_datatype(self: stormpy.storage.storage.SchedulerExact) storm::storage::Scheduler<carl::Interval<double> > ¶
Construct the scheduler with interval value type
- cast_to_parametric_datatype(self: stormpy.storage.storage.SchedulerExact) storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > ¶
Construct the scheduler with parametric value type
- compute_action_support(self: stormpy.storage.storage.SchedulerExact, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector ¶
- property deterministic¶
Is the scheduler deterministic?
- get_choice(self: stormpy.storage.storage.SchedulerExact, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > ¶
- property memory_size¶
How much memory does the scheduler take?
- property memoryless¶
Is the scheduler memoryless?
- property partial¶
Is the scheduler partial?
- set_choice(self: stormpy.storage.storage.SchedulerExact, choice: storm::storage::SchedulerChoice<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, state: int, memory_index: int = 0) None ¶
- to_json_str(self: stormpy.storage.storage.SchedulerExact, model: stormpy.storage.storage._SparseExactModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str ¶
- class SchedulerInterval¶
A Finite Memory Scheduler
- compute_action_support(self: stormpy.storage.storage.SchedulerInterval, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector ¶
- property deterministic¶
Is the scheduler deterministic?
- get_choice(self: stormpy.storage.storage.SchedulerInterval, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<carl::Interval<double> > ¶
- property memory_size¶
How much memory does the scheduler take?
- property memoryless¶
Is the scheduler memoryless?
- property partial¶
Is the scheduler partial?
- set_choice(self: stormpy.storage.storage.SchedulerInterval, choice: storm::storage::SchedulerChoice<carl::Interval<double> >, state: int, memory_index: int = 0) None ¶
- to_json_str(self: stormpy.storage.storage.SchedulerInterval, model: stormpy.storage.storage._SparseIntervalModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str ¶
- class SchedulerParametric¶
A Finite Memory Scheduler
- cast_to_double_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.Scheduler ¶
Construct the scheduler with double value type
- cast_to_exact_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.SchedulerExact ¶
Construct the scheduler with exact value type
- cast_to_parametric_datatype(self: stormpy.storage.storage.SchedulerParametric) stormpy.storage.storage.SchedulerParametric ¶
Construct the scheduler with parametric value type
- compute_action_support(self: stormpy.storage.storage.SchedulerParametric, nondeterministic_choice_indices: List[int]) stormpy.storage.storage.BitVector ¶
- property deterministic¶
Is the scheduler deterministic?
- get_choice(self: stormpy.storage.storage.SchedulerParametric, state_index: int, memory_index: int = 0) storm::storage::SchedulerChoice<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > ¶
- property memory_size¶
How much memory does the scheduler take?
- property memoryless¶
Is the scheduler memoryless?
- property partial¶
Is the scheduler partial?
- set_choice(self: stormpy.storage.storage.SchedulerParametric, choice: storm::storage::SchedulerChoice<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, state: int, memory_index: int = 0) None ¶
- to_json_str(self: stormpy.storage.storage.SchedulerParametric, model: stormpy.storage.storage._SparseParametricModel, skip_unique_choices: bool = False, skip_dont_care_states: bool = False) str ¶
- class SimpleValuation¶
- get_boolean_value(self: stormpy.storage.storage.SimpleValuation, variable: storm::expressions::Variable) bool ¶
Get Boolean Value for expression variable
- get_integer_value(self: stormpy.storage.storage.SimpleValuation, variable: storm::expressions::Variable) int ¶
Get Integer Value for expression variable
- to_json(self: stormpy.storage.storage.SimpleValuation) stormpy.utility.utility.JsonContainerRational ¶
Convert to JSON
- to_string(self: stormpy.storage.storage.SimpleValuation, pretty: bool = True) str ¶
to string
- class SparseDtmc¶
DTMC in sparse representation
- class SparseExactDtmc¶
DTMC in sparse representation
- class SparseExactMA¶
MA in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseExactMA, scheduler: storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseExactModel ¶
apply scheduler
- convert_to_ctmc(self: stormpy.storage.storage.SparseExactMA) stormpy.storage.storage.SparseExactCtmc ¶
Convert the MA into a CTMC.
- property convertible_to_ctmc¶
Check whether the MA can be converted into a CTMC.
- property exit_rates¶
- property markovian_states¶
- property nondeterministic_choice_indices¶
- class SparseExactMdp¶
MDP in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseExactMdp, scheduler: storm::storage::Scheduler<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseExactModel ¶
apply scheduler
- get_choice_index(self: stormpy.storage.storage.SparseExactMdp, state: int, action_offset: int) int ¶
gets the choice index for the offset action from the given state.
- get_nr_available_actions(self: stormpy.storage.storage.SparseExactMdp, state: int) int ¶
- property nondeterministic_choice_indices¶
- class SparseExactModelAction¶
Action for state in sparse model
- property id¶
Id
- property labels¶
Get choice labels
- property origins¶
Get choice origins
- property transitions¶
Get transitions
- class SparseExactModelActions¶
Actions for state in sparse model
- class SparseExactModelComponents¶
Components required for building a sparse model
- property choice_labeling¶
A list that stores a labeling for each choice
- property choice_origins¶
Stores for each choice from which parts of the input model description it originates
- property exit_rates¶
The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.
- property markovian_states¶
A list that stores which states are Markovian (only for Markov Automata)
- property observability_classes¶
The POMDP observations
- property player1_matrix¶
Matrix of player 1 choices (needed for stochastic two player games
- property rate_transitions¶
True iff the transition values (for Markovian choices) are interpreted as rates
- property reward_models¶
Reward models associated with the model
- property state_labeling¶
The state labeling
- property state_player_indications¶
The vector mapping states to player indices
- property state_valuations¶
A list that stores for each state to which variable valuation it belongs
- property transition_matrix¶
The transition matrix
- class SparseExactModelState¶
State in sparse model
- property actions¶
Get actions
- property id¶
Id
- property labels¶
Get state labels
- property valuations¶
Get state valuations
- class SparseExactModelStates¶
States in sparse model
- class SparseExactPomdp¶
POMDP in sparse representation
- get_observation(self: stormpy.storage.storage.SparseExactPomdp, state: int) int ¶
- has_observation_valuations(self: stormpy.storage.storage.SparseExactPomdp) bool ¶
- property nr_observations¶
- property observation_valuations¶
- property observations¶
- class SparseExactRewardModel¶
Reward structure for sparse models
- get_state_action_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) pycarl.gmp.gmp.Rational ¶
- get_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) pycarl.gmp.gmp.Rational ¶
- get_zero_reward_states(self: stormpy.storage.storage.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >) stormpy.storage.storage.BitVector ¶
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(self: stormpy.storage.storage.SparseExactRewardModel, transition_matrix: storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >, only_state_rewards: bool) None ¶
Reduce to state-based rewards
- set_state_reward(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int, arg1: pycarl.gmp.gmp.Rational) None ¶
- property state_action_rewards¶
- property state_rewards¶
- property transition_rewards¶
- class SparseExactSmg¶
SMG in sparse representation
- get_player_of_state(self: stormpy.storage.storage.SparseExactSmg, state: int) int ¶
Get player for the given state
- get_state_player_indications(self: stormpy.storage.storage.SparseExactSmg) List[int] ¶
Get for each state its corresponding player
- class SparseIntervalDtmc¶
DTMC in sparse representation
- class SparseIntervalMA¶
MA in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseIntervalMA, scheduler: storm::storage::Scheduler<carl::Interval<double> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseIntervalModel ¶
apply scheduler
- convert_to_ctmc(self: stormpy.storage.storage.SparseIntervalMA) stormpy.storage.storage.SparseIntervalCtmc ¶
Convert the MA into a CTMC.
- property convertible_to_ctmc¶
Check whether the MA can be converted into a CTMC.
- property exit_rates¶
- property markovian_states¶
- property nondeterministic_choice_indices¶
- class SparseIntervalMdp¶
MDP in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseIntervalMdp, scheduler: storm::storage::Scheduler<carl::Interval<double> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseIntervalModel ¶
apply scheduler
- get_choice_index(self: stormpy.storage.storage.SparseIntervalMdp, state: int, action_offset: int) int ¶
gets the choice index for the offset action from the given state.
- get_nr_available_actions(self: stormpy.storage.storage.SparseIntervalMdp, state: int) int ¶
- property nondeterministic_choice_indices¶
- class SparseIntervalModelAction¶
Action for state in sparse model
- property id¶
Id
- property labels¶
Get choice labels
- property origins¶
Get choice origins
- property transitions¶
Get transitions
- class SparseIntervalModelActions¶
Actions for state in sparse model
- class SparseIntervalModelComponents¶
Components required for building a sparse model
- property choice_labeling¶
A list that stores a labeling for each choice
- property choice_origins¶
Stores for each choice from which parts of the input model description it originates
- property exit_rates¶
The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.
- property markovian_states¶
A list that stores which states are Markovian (only for Markov Automata)
- property observability_classes¶
The POMDP observations
- property player1_matrix¶
Matrix of player 1 choices (needed for stochastic two player games
- property rate_transitions¶
True iff the transition values (for Markovian choices) are interpreted as rates
- property reward_models¶
Reward models associated with the model
- property state_labeling¶
The state labeling
- property state_player_indications¶
The vector mapping states to player indices
- property state_valuations¶
A list that stores for each state to which variable valuation it belongs
- property transition_matrix¶
The transition matrix
- class SparseIntervalModelState¶
State in sparse model
- property actions¶
Get actions
- property id¶
Id
- property labels¶
Get state labels
- property valuations¶
Get state valuations
- class SparseIntervalModelStates¶
States in sparse model
- class SparseIntervalPomdp¶
POMDP in sparse representation
- get_observation(self: stormpy.storage.storage.SparseIntervalPomdp, state: int) int ¶
- has_observation_valuations(self: stormpy.storage.storage.SparseIntervalPomdp) bool ¶
- property nr_observations¶
- property observation_valuations¶
- property observations¶
- class SparseIntervalRewardModel¶
Reward structure for sparse models
- get_state_action_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) pycarl.core.Interval ¶
- get_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int) pycarl.core.Interval ¶
- get_zero_reward_states(self: stormpy.storage.storage.SparseIntervalRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::Interval<double> >) stormpy.storage.storage.BitVector ¶
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(self: stormpy.storage.storage.SparseIntervalRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::Interval<double> >, only_state_rewards: bool) None ¶
Reduce to state-based rewards
- set_state_reward(self: stormpy.storage.storage.SparseIntervalRewardModel, arg0: int, arg1: pycarl.core.Interval) None ¶
- property state_action_rewards¶
- property state_rewards¶
- property transition_rewards¶
- class SparseIntervalSmg¶
SMG in sparse representation
- get_player_of_state(self: stormpy.storage.storage.SparseIntervalSmg, state: int) int ¶
Get player for the given state
- get_state_player_indications(self: stormpy.storage.storage.SparseIntervalSmg) List[int] ¶
Get for each state its corresponding player
- class SparseMA¶
MA in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseMA, scheduler: storm::storage::Scheduler<double>, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseModel ¶
apply scheduler
- convert_to_ctmc(self: stormpy.storage.storage.SparseMA) stormpy.storage.storage.SparseCtmc ¶
Convert the MA into a CTMC.
- property convertible_to_ctmc¶
Check whether the MA can be converted into a CTMC.
- property exit_rates¶
- property markovian_states¶
- property nondeterministic_choice_indices¶
- class SparseMatrix¶
Sparse matrix
- get_row(self: stormpy.storage.storage.SparseMatrix, row: int) storm::storage::SparseMatrix<double>::rows ¶
Get row
- get_row_group_end(self: stormpy.storage.storage.SparseMatrix, arg0: int) int ¶
- get_row_group_start(self: stormpy.storage.storage.SparseMatrix, arg0: int) int ¶
- get_rows_for_group(self: stormpy.storage.storage.SparseMatrix, row_group: int) List[int] ¶
Get rows within a row group
- property has_trivial_row_grouping¶
Trivial row grouping
- make_row_grouping_trivial(self: stormpy.storage.storage.SparseMatrix) None ¶
Makes row groups trivial. Use with care.
- property nr_columns¶
Number of columns
- property nr_entries¶
Number of non-zero entries
- property nr_rows¶
Number of rows
- print_row(self: stormpy.storage.storage.SparseMatrix, row: int) str ¶
Print rows from start to end
- row_iter(self: stormpy.storage.storage.SparseMatrix, row_start: int, row_end: int) Iterator ¶
Get iterator from start to end
- submatrix(self: stormpy.storage.storage.SparseMatrix, row_constraint: stormpy.storage.storage.BitVector, column_constraint: stormpy.storage.storage.BitVector, insert_diagonal_entries: bool = False) stormpy.storage.storage.SparseMatrix ¶
Get submatrix
- class SparseMatrixBuilder¶
Builder of sparse matrix
- add_next_value(self: stormpy.storage.storage.SparseMatrixBuilder, row: int, column: int, value: float) None ¶
Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory.
Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are treated as empty. If these constraints are not met, an exception is thrown.
- Parameters:
row (double) – The row in which the matrix entry is to be set
column (double) – The column in which the matrix entry is to be set
value (double) – The value that is to be set at the specified row and column
- build(self: stormpy.storage.storage.SparseMatrixBuilder, overridden_row_count: int = 0, overridden_column_count: int = 0, overridden-row_group_count: int = 0) storm::storage::SparseMatrix<double> ¶
Finalize the sparse matrix
- get_current_row_group_count(self: stormpy.storage.storage.SparseMatrixBuilder) int ¶
Get the current row group count
- get_last_column(self: stormpy.storage.storage.SparseMatrixBuilder) int ¶
the most recently used column
- get_last_row(self: stormpy.storage.storage.SparseMatrixBuilder) int ¶
Get the most recently used row
- new_row_group(self: stormpy.storage.storage.SparseMatrixBuilder, starting_row: int) None ¶
Start a new row group in the matrix
- replace_columns(self: stormpy.storage.storage.SparseMatrixBuilder, replacements: List[int], offset: int) None ¶
Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted.
- Parameters:
replacements (std::vector<double> const&) – replacements Mapping indicating the replacements from offset+i -> value of i
offset (int) – Offset to add to each id in vector index.
- class SparseMatrixEntry¶
Entry of sparse matrix
- property column¶
Column
- set_value(self: stormpy.storage.storage.SparseMatrixEntry, value: float) None ¶
Set value
- value(self: stormpy.storage.storage.SparseMatrixEntry) float ¶
Value
- class SparseMatrixRows¶
Set of rows in a sparse matrix
- class SparseMdp¶
MDP in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseMdp, scheduler: storm::storage::Scheduler<double>, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseModel ¶
apply scheduler
- get_choice_index(self: stormpy.storage.storage.SparseMdp, state: int, action_offset: int) int ¶
gets the choice index for the offset action from the given state.
- get_nr_available_actions(self: stormpy.storage.storage.SparseMdp, state: int) int ¶
- property nondeterministic_choice_indices¶
- class SparseModelAction¶
Action for state in sparse model
- property id¶
Id
- property labels¶
Get choice labels
- property origins¶
Get choice origins
- property transitions¶
Get transitions
- class SparseModelActions¶
Actions for state in sparse model
- class SparseModelComponents¶
Components required for building a sparse model
- property choice_labeling¶
A list that stores a labeling for each choice
- property choice_origins¶
Stores for each choice from which parts of the input model description it originates
- property exit_rates¶
The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.
- property markovian_states¶
A list that stores which states are Markovian (only for Markov Automata)
- property observability_classes¶
The POMDP observations
- property player1_matrix¶
Matrix of player 1 choices (needed for stochastic two player games
- property rate_transitions¶
True iff the transition values (for Markovian choices) are interpreted as rates
- property reward_models¶
Reward models associated with the model
- property state_labeling¶
The state labeling
- property state_player_indications¶
The vector mapping states to player indices
- property state_valuations¶
A list that stores for each state to which variable valuation it belongs
- property transition_matrix¶
The transition matrix
- class SparseModelState¶
State in sparse model
- property actions¶
Get actions
- property id¶
Id
- property labels¶
Get state labels
- property valuations¶
Get state valuations
- class SparseModelStates¶
States in sparse model
- class SparseParametricCtmc¶
pCTMC in sparse representation
- class SparseParametricDtmc¶
pDTMC in sparse representation
- class SparseParametricMA¶
pMA in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseParametricMA, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseParametricModel ¶
apply scheduler
- property nondeterministic_choice_indices¶
- class SparseParametricMdp¶
pMDP in sparse representation
- apply_scheduler(self: stormpy.storage.storage.SparseParametricMdp, scheduler: storm::storage::Scheduler<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, drop_unreachable_states: bool = True) stormpy.storage.storage._SparseParametricModel ¶
apply scheduler
- get_nr_available_actions(self: stormpy.storage.storage.SparseParametricMdp, state: int) int ¶
- property nondeterministic_choice_indices¶
- class SparseParametricModelAction¶
Action for state in sparse model
- property id¶
Id
- property labels¶
Get choice labels
- property origins¶
Get choice origins
- property transitions¶
Get transitions
- class SparseParametricModelActions¶
Actions for state in sparse model
- class SparseParametricModelComponents¶
Components required for building a sparse model
- property choice_labeling¶
A list that stores a labeling for each choice
- property choice_origins¶
Stores for each choice from which parts of the input model description it originates
- property exit_rates¶
The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.
- property markovian_states¶
A list that stores which states are Markovian (only for Markov Automata)
- property observability_classes¶
The POMDP observations
- property player1_matrix¶
Matrix of player 1 choices (needed for stochastic two player games
- property rate_transitions¶
True iff the transition values (for Markovian choices) are interpreted as rates
- property reward_models¶
Reward models associated with the model
- property state_labeling¶
The state labeling
- property state_player_indications¶
The vector mapping states to player indices
- property state_valuations¶
A list that stores for each state to which variable valuation it belongs
- property transition_matrix¶
The transition matrix
- class SparseParametricModelState¶
State in sparse model
- property actions¶
Get actions
- property id¶
Id
- property labels¶
Get state labels
- property valuations¶
Get state valuations
- class SparseParametricModelStates¶
States in sparse model
- class SparseParametricPomdp¶
POMDP in sparse representation
- get_observation(self: stormpy.storage.storage.SparseParametricPomdp, state: int) int ¶
- property nr_observations¶
- property observations¶
- class SparseParametricRewardModel¶
Reward structure for parametric sparse models
- get_state_action_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) pycarl.cln.cln.FactorizedRationalFunction ¶
- get_state_reward(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) pycarl.cln.cln.FactorizedRationalFunction ¶
- property has_state_action_rewards¶
- property has_state_rewards¶
- property has_transition_rewards¶
- reduce_to_state_based_rewards(self: stormpy.storage.storage.SparseParametricRewardModel, transition_matrix: storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> >, only_state_rewards: bool) None ¶
Reduce to state-based rewards
- property state_action_rewards¶
- property state_rewards¶
- property transition_rewards¶
- class SparsePomdp¶
POMDP in sparse representation
- get_observation(self: stormpy.storage.storage.SparsePomdp, state: int) int ¶
- has_observation_valuations(self: stormpy.storage.storage.SparsePomdp) bool ¶
- property nr_observations¶
- property observation_valuations¶
- property observations¶
- class SparseRewardModel¶
Reward structure for sparse models
- get_state_action_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int) float ¶
- get_state_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int) float ¶
- get_zero_reward_states(self: stormpy.storage.storage.SparseRewardModel, transition_matrix: storm::storage::SparseMatrix<double>) stormpy.storage.storage.BitVector ¶
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(self: stormpy.storage.storage.SparseRewardModel, transition_matrix: storm::storage::SparseMatrix<double>, only_state_rewards: bool) None ¶
Reduce to state-based rewards
- set_state_reward(self: stormpy.storage.storage.SparseRewardModel, arg0: int, arg1: float) None ¶
- property state_action_rewards¶
- property state_rewards¶
- property transition_rewards¶
- class SparseSmg¶
SMG in sparse representation
- get_player_of_state(self: stormpy.storage.storage.SparseSmg, state: int) int ¶
Get player for the given state
- get_state_player_indications(self: stormpy.storage.storage.SparseSmg) List[int] ¶
Get for each state its corresponding player
- class StateLabeling¶
Labeling for states
- add_label_to_state(self: stormpy.storage.storage.StateLabeling, label: str, state: int) None ¶
Add label to state
- get_labels_of_state(self: stormpy.storage.storage.StateLabeling, state: int) Set[str] ¶
Get labels of given state
- get_states(self: stormpy.storage.storage.StateLabeling, label: str) stormpy.storage.storage.BitVector ¶
Get all states which have the given label
- has_state_label(self: stormpy.storage.storage.StateLabeling, label: str, state: int) bool ¶
Check if the given state has the given label
- set_states(self: stormpy.storage.storage.StateLabeling, label: str, states: stormpy.storage.storage.BitVector) None ¶
Add a label to the given states
- class StateValuation¶
Valuations for explicit states
- get_boolean_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) bool ¶
- get_integer_value(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) int ¶
- get_json(self: stormpy.storage.storage.StateValuation, state: int, selected_variables: Optional[Set[storm::expressions::Variable]] = None) stormpy.utility.utility.JsonContainerRational ¶
- get_nr_of_states(self: stormpy.storage.storage.StateValuation) int ¶