Stormpy.storage¶
-
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
¶ -
get
(self: stormpy.storage.storage.BitVector, index: int) → bool¶
-
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
¶ -
Bitvector
= DdMetaVariableType.Bitvector¶
-
Bool
= DdMetaVariableType.Bool¶
-
Int
= DdMetaVariableType.Int¶
-
-
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
-
property
-
class
DistributionDouble
¶ 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
(self: stormpy.storage.storage.ExactSparseMatrix, row_start: int, row_end: int) → storm::storage::SparseMatrix<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >::rows¶ Get rows from start to end
-
property
has_trivial_row_grouping
¶ Trivial row grouping
-
property
nr_columns
¶ Number of columns
-
property
nr_entries
¶ Number of non-zero entries
-
property
nr_rows
¶ Number of rows
-
print_row
(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: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) → 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
const& replacements (std::vector<double>) – 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: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) → None¶ Set value
-
value
(self: stormpy.storage.storage.ExactSparseMatrixEntry) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶ Value
-
property
-
class
ExactSparseMatrixRows
¶ Set of rows in a sparse matrix
-
class
Expression
¶ Holds an expression
-
And
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Conjunction
(arg0: List[stormpy.storage.storage.Expression]) → stormpy.storage.storage.Expression¶
-
Disjunction
(arg0: List[stormpy.storage.storage.Expression]) → stormpy.storage.storage.Expression¶
-
Divide
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Eq
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Geq
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Greater
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Iff
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Implies
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Leq
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Less
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Minus
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Modulo
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Multiply
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Neq
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
Or
(arg0: stormpy.storage.storage.Expression, arg1: stormpy.storage.storage.Expression) → stormpy.storage.storage.Expression¶
-
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) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶ 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: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) → 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
¶
-
property
-
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
-
property
-
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
-
property
-
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]) → None¶
-
property
template_edge
¶ template edge
-
property
-
class
JaniEdgeDestination
¶ Destination in Jani
-
property
assignments
¶
-
property
probability
¶
-
property
target_location_index
¶
-
property
-
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
¶
-
property
-
class
JaniLocation
¶ A Location in JANI
-
property
assignments
¶ location assignments
-
property
name
¶ name of the location
-
property
-
class
JaniLocationExpander
¶ A transformer for Jani expanding variables into locations
-
get_result
(self: stormpy.storage.storage.JaniLocationExpander) → stormpy.storage.storage.JaniModel¶
-
transform
(self: stormpy.storage.storage.JaniLocationExpander, automaton_name: str, variable_name: str) → None¶
-
-
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
-
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
-
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 0x7f0a9f2afc70>) → 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]) → 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
¶
-
property
-
class
JaniVariable
¶ A Variable in JANI
-
property
expression_variable
¶ expression variable for this variable
-
property
init_expression
¶
-
property
name
¶ name of constant
-
property
-
class
JaniVariableSet
¶ Jani Set of Variables
-
add_bounded_integer_variable
(self: stormpy.storage.storage.JaniVariableSet, variable: storm::jani::BoundedIntegerVariable) → storm::jani::BoundedIntegerVariable¶
-
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
ModelType
¶ Type of the model
-
CTMC
= ModelType.CTMC¶
-
DTMC
= ModelType.DTMC¶
-
MA
= ModelType.MA¶
-
MDP
= ModelType.MDP¶
-
POMDP
= ModelType.POMDP¶
-
-
class
OperatorType
¶ Type of an operator (of any sort)
-
And
= OperatorType.And¶
-
Ceil
= OperatorType.Ceil¶
-
Divide
= OperatorType.Divide¶
-
Equal
= OperatorType.Equal¶
-
Floor
= OperatorType.Floor¶
-
Greater
= OperatorType.Greater¶
-
GreaterOrEqual
= OperatorType.GreaterOrEqual¶
-
Iff
= OperatorType.Iff¶
-
Implies
= OperatorType.Implies¶
-
Ite
= OperatorType.Ite¶
-
Less
= OperatorType.Less¶
-
LessOrEqual
= OperatorType.LessOrEqual¶
-
Max
= OperatorType.Max¶
-
Min
= OperatorType.Min¶
-
Minus
= OperatorType.Minus¶
-
Modulo
= OperatorType.Modulo¶
-
Not
= OperatorType.Not¶
-
NotEqual
= OperatorType.NotEqual¶
-
Or
= OperatorType.Or¶
-
Plus
= OperatorType.Plus¶
-
Power
= OperatorType.Power¶
-
Times
= OperatorType.Times¶
-
Xor
= OperatorType.Xor¶
-
-
class
ParametricSparseMatrix
¶ Sparse matrix
-
get_row
(self: stormpy.storage.storage.ParametricSparseMatrix, row: int) → storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, 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
(self: stormpy.storage.storage.ParametricSparseMatrix, row_start: int, row_end: int) → storm::storage::SparseMatrix<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >::rows¶ Get rows from start to end
-
property
has_trivial_row_grouping
¶ Trivial row grouping
-
property
nr_columns
¶ Number of columns
-
property
nr_entries
¶ Number of non-zero entries
-
property
nr_rows
¶ Number of rows
-
print_row
(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: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>) → 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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, 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
const& replacements (std::vector<double>) – 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: carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>) → None¶ Set value
-
value
(self: stormpy.storage.storage.ParametricSparseMatrixEntry) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶ Value
-
property
-
class
ParametricSparseMatrixRows
¶ Set of rows in a sparse matrix
-
class
PrismAssignment
¶ An assignment in prism
-
property
expression
¶ Expression for the update
-
property
variable
¶ Variable that is updated
-
property
-
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
-
property
-
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
-
property
-
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
-
property
-
class
PrismModelType
¶ Type of the prism model
-
CTMC
= PrismModelType.CTMC¶
-
CTMDP
= PrismModelType.CTMDP¶
-
DTMC
= PrismModelType.DTMC¶
-
MA
= PrismModelType.MA¶
-
MDP
= PrismModelType.MDP¶
-
POMDP
= PrismModelType.POMDP¶
-
UNDEFINED
= PrismModelType.UNDEFINED¶
-
-
class
PrismModule
¶ A module in a Prism program
-
property
boolean_variables
¶ All boolean Variables of this module
-
property
commands
¶ Commands in the module
-
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
-
property
-
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 0x7f0a9f1e0370>) → 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¶
-
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
-
property
global_boolean_variables
¶ Retrieves the global boolean variables of the program
-
property
global_integer_variables
¶ Retrieves the global integer variables of the program
-
property
hasUndefinedConstants
¶ Does the program have undefined constants?
-
property
has_undefined_constants
¶ Flag if program has undefined constants
-
property
is_deterministic_model
¶ Does the program describe a deterministic model?
-
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
-
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
-
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
-
used_constants
(self: stormpy.storage.storage.PrismProgram) → List[storm::prism::Constant]¶ Compute Used Constants
-
property
variables
¶ Get all Expression Variables used by the program
-
property
-
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
-
property
-
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
-
property
-
class
SchedulerChoiceDouble
¶ A choice of a finite memory scheduler
-
property
defined
¶ Is the choice defined by the scheduler?
-
property
deterministic
¶ Is the choice deterministic (given by a Dirac distribution)?
-
get_choice
(self: stormpy.storage.storage.SchedulerChoiceDouble) → storm::storage::Distribution<double, unsigned long>¶ Get the distribution over the actions
-
get_deterministic_choice
(self: stormpy.storage.storage.SchedulerChoiceDouble) → int¶ Get the deterministic choice
-
property
-
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
-
property
-
class
SchedulerDouble
¶ A Finite Memory Scheduler
-
compute_action_support
(self: stormpy.storage.storage.SchedulerDouble, nondeterministic_choice_indices: List[int]) → stormpy.storage.storage.BitVector¶
-
property
deterministic
¶ Is the scheduler deterministic?
-
get_choice
(self: stormpy.storage.storage.SchedulerDouble, 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?
-
-
class
SchedulerExact
¶ A Finite Memory Scheduler
-
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?
-
-
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
transitions
¶ Get transitions
-
property
-
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_valuations
¶ A list that stores for each state to which variable valuation it belongs
-
property
transition_matrix
¶ The transition matrix
-
property
-
class
SparseExactModelState
¶ State in sparse model
-
property
actions
¶ Get actions
-
property
id
¶ Id
-
property
labels
¶ Labels
-
property
-
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) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶
-
get_state_reward
(self: stormpy.storage.storage.SparseExactRewardModel, arg0: int) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶
-
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
-
property
state_action_rewards
¶
-
property
state_rewards
¶
-
property
transition_rewards
¶
-
-
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
(self: stormpy.storage.storage.SparseMatrix, row_start: int, row_end: int) → storm::storage::SparseMatrix<double>::rows¶ Get rows from start to end
-
property
has_trivial_row_grouping
¶ Trivial row grouping
-
property
nr_columns
¶ Number of columns
-
property
nr_entries
¶ Number of non-zero entries
-
property
nr_rows
¶ Number of rows
-
print_row
(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
const& replacements (std::vector<double>) – 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
-
property
-
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
transitions
¶ Get transitions
-
property
-
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_valuations
¶ A list that stores for each state to which variable valuation it belongs
-
property
transition_matrix
¶ The transition matrix
-
property
-
class
SparseModelState
¶ State in sparse model
-
property
actions
¶ Get actions
-
property
id
¶ Id
-
property
labels
¶ Labels
-
property
-
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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, 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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> >, drop_unreachable_states: bool=True) → stormpy.storage.storage._SparseParametricModel¶ apply scheduler
-
property
nondeterministic_choice_indices
¶
-
-
class
SparseParametricModelAction
¶ Action for state in sparse model
-
property
id
¶ Id
-
property
transitions
¶ Get transitions
-
property
-
class
SparseParametricModelActions
¶ Actions for state in sparse model
-
class
SparseParametricModelState
¶ State in sparse model
-
property
actions
¶ Get actions
-
property
id
¶ Id
-
property
labels
¶ Labels
-
property
-
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) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶
-
get_state_reward
(self: stormpy.storage.storage.SparseParametricRewardModel, arg0: int) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>¶
-
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::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, 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
-
property
state_action_rewards
¶
-
property
state_rewards
¶
-
property
transition_rewards
¶
-
-
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) → str¶
-
get_nr_of_states
(self: stormpy.storage.storage.StateValuation) → int¶
-
get_rational_value
(self: stormpy.storage.storage.StateValuation, state: int, variable: storm::expressions::Variable) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>¶
-
get_string
(self: stormpy.storage.storage.StateValuation, state: int, pretty: bool=True, selected_variables: Optional[Set[storm::expressions::Variable]]=None) → str¶
-
-
class
StateValuationsBuilder
¶ -
add_state
(self: stormpy.storage.storage.StateValuationsBuilder, state: int, boolean_values: List[bool]=[], integer_values: List[int]=[], rational_values: List[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]=[]) → None¶ Adds a new state, no more variables should be added afterwards
-
add_variable
(self: stormpy.storage.storage.StateValuationsBuilder, variable: storm::expressions::Variable) → None¶ Adds a new variable
-
build
(self: stormpy.storage.storage.StateValuationsBuilder, arg0: int) → stormpy.storage.storage.StateValuation¶ Creates the finalized state valuations object
-
-
class
SymbolicSylvanCtmc
¶ CTMC in symbolic representation
-
class
SymbolicSylvanDtmc
¶ DTMC in symbolic representation
-
class
SymbolicSylvanMA
¶ MA in symbolic representation
-
class
SymbolicSylvanMdp
¶ MDP in symbolic representation
-
class
SymbolicSylvanParametricCtmc
¶ pCTMC in symbolic representation
-
class
SymbolicSylvanParametricDtmc
¶ pDTMC in symbolic representation
-
class
SymbolicSylvanParametricMA
¶ pMA in symbolic representation
-
class
SymbolicSylvanParametricMdp
¶ pMDP in symbolic representation
-
class
SymbolicSylvanParametricRewardModel
¶ Reward structure for parametric symbolic models
-
property
has_state_action_rewards
¶
-
property
has_state_rewards
¶
-
property
has_transition_rewards
¶
-
property
-
class
SymbolicSylvanRewardModel
¶ Reward structure for symbolic models
-
property
has_state_action_rewards
¶
-
property
has_state_rewards
¶
-
property
has_transition_rewards
¶
-
property
-
class
Variable
¶ Represents a variable
-
get_expression
(self: stormpy.storage.storage.Variable) → storm::expressions::Expression¶ Get expression from variable
-
has_bitvector_type
(self: stormpy.storage.storage.Variable) → bool¶ Check if the variable is of bitvector type
-
has_boolean_type
(self: stormpy.storage.storage.Variable) → bool¶ Check if the variable is of boolean type
-
has_integer_type
(self: stormpy.storage.storage.Variable) → bool¶ Check if the variable is of integer type
-
has_numerical_type
(self: stormpy.storage.storage.Variable) → bool¶ Check if the variable is of numerical type
-
has_rational_type
(self: stormpy.storage.storage.Variable) → bool¶ Check if the variable is of rational type
-
property
manager
¶ Variable manager
-
property
name
¶ Variable name
-
-
build_parametric_sparse_matrix
(array, row_group_indices=[])¶ Build a sparse matrix from numpy array.
- Parameters
array (numpy) – The array.
row_group_indices (List[double]) – List containing the starting row of each row group in ascending order.
- Returns
Parametric sparse matrix.
-
build_sparse_matrix
(array, row_group_indices=[])¶ Build a sparse matrix from numpy array.
- Parameters
array (numpy) – The array.
row_group_indices (List[double]) – List containing the starting row of each row group in ascending order.
- Returns
Sparse matrix.
-
collect_information
(arg0: stormpy.storage.storage.JaniModel) → stormpy.storage.storage.JaniInformationObject¶
-
eliminate_reward_accumulations
(model: stormpy.storage.storage.JaniModel, properties: List[stormpy.core.Property]) → List[stormpy.core.Property]¶ Eliminate reward accumulations