Stormpy.core¶
- class ActionMaskDouble¶
- class AddIterator_Sylvan_Double¶
AddIterator
- get(self: stormpy.storage.storage.AddIterator_Sylvan_Double) Tuple[storm::expressions::SimpleValuation, float] ¶
- class Add_Sylvan_Double¶
Add
- class AtomicExpressionFormula¶
Formula with an atomic expression
- get_expression(self: stormpy.logic.logic.AtomicExpressionFormula) stormpy.storage.storage.Expression ¶
- 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 BinaryBooleanOperatorType¶
Members:
AND
OR
- AND = <BinaryBooleanOperatorType.AND: 0>¶
- OR = <BinaryBooleanOperatorType.OR: 1>¶
- property name¶
- property value¶
- class BinaryPathFormula¶
Path formula with two operands
- property left_subformula¶
- property right_subformula¶
- class BinaryStateFormula¶
State formula with two operands
- class BisimulationType¶
Types of bisimulation
Members:
STRONG
WEAK
- STRONG = <BisimulationType.STRONG: 0>¶
- WEAK = <BisimulationType.WEAK: 1>¶
- property name¶
- property value¶
- 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 BooleanBinaryStateFormula¶
Boolean binary state formula
- class BooleanLiteralFormula¶
Formula with a boolean literal
- class BoundedUntilFormula¶
Until Formula with either a step or a time bound.
- property has_lower_bound¶
- property is_multidimensional¶
Is the bound multi-dimensional
- property left_subformula¶
- property right_subformula¶
- property upper_bound_expression¶
- class BuilderOptions¶
Options for building process
- property preserved_label_names¶
Labels preserved
- set_add_out_of_bounds_state(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build with out of bounds state
- set_add_overlapping_guards_label(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build with overlapping guards state labeled
- set_build_all_labels(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build with all state labels
- set_build_all_reward_models(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build with all reward models
- set_build_choice_labels(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build with choice labels
- set_build_observation_valuations(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build observation valuations
- set_build_state_valuations(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build state valuations
- set_build_with_choice_origins(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Build choice origins
- set_exploration_checks(self: stormpy.core.BuilderOptions, new_value: bool = True) stormpy.core.BuilderOptions ¶
Perform extra checks during exploration
- class CheckTask¶
Task for model checking
- set_hint(self: stormpy.core.CheckTask, arg0: storm::modelchecker::ModelCheckerHint) None ¶
Sets a hint that may speed up the solver
- set_produce_schedulers(self: stormpy.core.CheckTask, produce_schedulers: bool = True) None ¶
Set whether schedulers should be produced (if possible)
- set_robust_uncertainty(self: stormpy.core.CheckTask, arg0: bool) None ¶
Sets whether robust uncertainty should be considered
- 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 ComparisonType¶
Members:
LESS
LEQ
GREATER
GEQ
- GEQ = <ComparisonType.GEQ: 3>¶
- GREATER = <ComparisonType.GREATER: 2>¶
- LEQ = <ComparisonType.LEQ: 1>¶
- LESS = <ComparisonType.LESS: 0>¶
- property name¶
- property value¶
- class ConditionalFormula¶
Formula with the right hand side being a condition.
- class ConstraintCollector¶
Collector for constraints on parametric Markov chains
- property graph_preserving_constraints¶
Get the constraints ensuring the graph is preserved
- property wellformed_constraints¶
Get the constraints ensuring a wellformed model
- class CumulativeRewardFormula¶
Summed rewards over a the paths
- 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 DirectEncodingParserOptions¶
Options for the .drn parser
- property build_choice_labels¶
Build with choice labels
- class Distribution¶
Finite Support Distribution
- class DistributionExact¶
Finite Support Distribution
- class DistributionInterval¶
Finite Support Distribution
- class EliminationLabelBehavior¶
Behavior of labels while eliminating non-Markovian chains
Members:
KEEP_LABELS
MERGE_LABELS
DELETE_LABELS
- DELETE_LABELS = <EliminationLabelBehavior.DELETE_LABELS: 3>¶
- KEEP_LABELS = <EliminationLabelBehavior.KEEP_LABELS: 0>¶
- MERGE_LABELS = <EliminationLabelBehavior.MERGE_LABELS: 2>¶
- property name¶
- property value¶
- class EndComponentEliminatorReturnTypeDouble¶
Container for result of endcomponent elimination
- property matrix¶
The resulting matrix
- property new_to_old_row_mapping¶
Index mapping that gives for each row fo the new matrix the corresponding row in the original matrix
- property old_to_new_state_mapping¶
For each state of the original matrix (and subsystem) the corresponding state in the result. Removed states are mapped to the EC.
- property sink_rows¶
Rows that indicate staying in the EC forever
- class EquationSolverType¶
Solver type for equation systems
Members:
native
eigen
elimination
gmmxx
topological
- eigen = <EquationSolverType.eigen: 2>¶
- elimination = <EquationSolverType.elimination: 3>¶
- gmmxx = <EquationSolverType.gmmxx: 1>¶
- property name¶
- native = <EquationSolverType.native: 0>¶
- topological = <EquationSolverType.topological: 4>¶
- property value¶
- class EventuallyFormula¶
Formula for eventually
- class ExactCheckTask¶
Task for model checking with exact numbers
- set_produce_schedulers(self: stormpy.core.ExactCheckTask, produce_schedulers: bool = True) None ¶
Set whether schedulers should be produced (if possible)
- 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 ExplicitExactQuantitativeCheckResult¶
Explicit exact quantitative model checking result
- at(self: stormpy.core.ExplicitExactQuantitativeCheckResult, state: int) pycarl.gmp.gmp.Rational ¶
Get result for given state
- get_values(self: stormpy.core.ExplicitExactQuantitativeCheckResult) List[pycarl.gmp.gmp.Rational] ¶
Get model checking result values for all states
- property scheduler¶
get scheduler
- class ExplicitModelBuilder¶
Model builder for sparse models
- build(self: stormpy.core.ExplicitModelBuilder) storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> > ¶
Build the model
- export_lookup(self: stormpy.core.ExplicitModelBuilder) storm::builder::ExplicitStateLookup<unsigned int> ¶
Export a lookup model
- class ExplicitModelCheckerHintDouble¶
Information that may accelerate an explicit state model checker
- set_compute_only_maybe_states(self: stormpy.core.ExplicitModelCheckerHintDouble, arg0: bool) None ¶
value
- set_maybe_states(self: stormpy.core.ExplicitModelCheckerHintDouble, arg0: storm::storage::BitVector) None ¶
sets the maybe states. This is assumed to be correct.
- set_result_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, result_hint: List[float] | None) None ¶
- set_scheduler_hint(self: stormpy.core.ExplicitModelCheckerHintDouble, scheduler_hint: Optional[storm::storage::Scheduler<double>]) None ¶
Set a scheduler that is close to the optimal scheduler
- class ExplicitParametricModelBuilder¶
Model builder for sparse models
- build(self: stormpy.core.ExplicitParametricModelBuilder) storm::models::sparse::Model<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::NotRelevant, carl::StdMultivariatePolynomialPolicies<0> > >, true> > > ¶
Build the model
- export_lookup(self: stormpy.core.ExplicitParametricModelBuilder) storm::builder::ExplicitStateLookup<unsigned int> ¶
Export a lookup model
- class ExplicitParametricQuantitativeCheckResult¶
Explicit parametric quantitative model checking result
- at(self: stormpy.core.ExplicitParametricQuantitativeCheckResult, state: int) pycarl.cln.cln.FactorizedRationalFunction ¶
Get result for given state
- get_values(self: stormpy.core.ExplicitParametricQuantitativeCheckResult) List[pycarl.cln.cln.FactorizedRationalFunction] ¶
Get model checking result values for all states
- property scheduler¶
get scheduler
- class ExplicitParetoCurveCheckResultDouble¶
Result for explicit multiobjective model checking
- class ExplicitQualitativeCheckResult¶
Explicit qualitative model checking result
- at(self: stormpy.core.ExplicitQualitativeCheckResult, state: int) bool ¶
Get result for given state
- get_truth_values(self: stormpy.core.ExplicitQualitativeCheckResult) storm::storage::BitVector ¶
Get BitVector representing the truth values
- class ExplicitQuantitativeCheckResult¶
Explicit quantitative model checking result
- at(self: stormpy.core.ExplicitQuantitativeCheckResult, state: int) float ¶
Get result for given state
- get_values(self: stormpy.core.ExplicitQuantitativeCheckResult) List[float] ¶
Get model checking result values for all states
- property scheduler¶
get scheduler
- class ExplicitStateLookup¶
Lookup model for states
- lookup(self: stormpy.core.ExplicitStateLookup, state_description: Dict[storm::expressions::Variable, storm::expressions::Expression]) object ¶
- 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 FactorizedPolynomial¶
Represent a polynomial with its factorization
- cache(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln._FactorizationCache ¶
- property coefficient¶
- constant_part(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln.Rational ¶
- derive(self: pycarl.cln.cln.FactorizedPolynomial, variable: pycarl.core.Variable) pycarl.cln.cln.FactorizedPolynomial ¶
Compute the derivative
- evaluate(self: pycarl.cln.cln.FactorizedPolynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) pycarl.cln.cln.Rational ¶
- factorization(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln.Factorization ¶
Get factorization
- gather_variables(self: pycarl.cln.cln.FactorizedPolynomial) Set[pycarl.core.Variable] ¶
- is_constant(self: pycarl.cln.cln.FactorizedPolynomial) bool ¶
- is_one(self: pycarl.cln.cln.FactorizedPolynomial) bool ¶
- polynomial(self: pycarl.cln.cln.FactorizedPolynomial) pycarl.cln.cln.Polynomial ¶
Get underlying polynomial
- to_smt2(self: pycarl.cln.cln.FactorizedPolynomial) str ¶
- class FactorizedRationalFunction¶
Represent a rational function, that is the fraction of two factorized polynomials
- constant_part(self: pycarl.cln.cln.FactorizedRationalFunction) pycarl.cln.cln.Rational ¶
- property denominator¶
- derive(self: pycarl.cln.cln.FactorizedRationalFunction, variable: pycarl.core.Variable) pycarl.cln.cln.FactorizedRationalFunction ¶
Compute the derivative
- evaluate(self: pycarl.cln.cln.FactorizedRationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) pycarl.cln.cln.Rational ¶
- gather_variables(self: pycarl.cln.cln.FactorizedRationalFunction) Set[pycarl.core.Variable] ¶
- is_constant(self: pycarl.cln.cln.FactorizedRationalFunction) bool ¶
- property numerator¶
- rational_function(self: pycarl.cln.cln.FactorizedRationalFunction) pycarl.cln.cln.RationalFunction ¶
- to_smt2(self: pycarl.cln.cln.FactorizedRationalFunction) str ¶
- class FlatSet¶
Container to pass to program
- insert(self: stormpy.core.FlatSet, arg0: int) None ¶
- insert_set(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) None ¶
- is_subset_of(self: stormpy.core.FlatSet, arg0: stormpy.core.FlatSet) bool ¶
- class Formula¶
Generic Storm Formula
- clone(self: stormpy.logic.logic.Formula) stormpy.logic.logic.Formula ¶
- property is_bounded_until_formula¶
- property is_eventually_formula¶
- property is_multi_objective_formula¶
- property is_probability_operator¶
is it a probability operator
- property is_reward_operator¶
is it a reward operator
- property is_until_formula¶
- substitute(self: stormpy.logic.logic.Formula, constants_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) stormpy.logic.logic.Formula ¶
Substitute variables
- substitute_labels_by_labels(self: stormpy.logic.logic.Formula, replacements: Dict[str, str]) stormpy.logic.logic.Formula ¶
substitute label occurences
- class GloballyFormula¶
Formula for globally
- class HybridExactQuantitativeCheckResult¶
Symbolic exact hybrid quantitative model checking result
- get_values(self: stormpy.core.HybridExactQuantitativeCheckResult) List[pycarl.gmp.gmp.Rational] ¶
Get model checking result values for all states
- class HybridParametricQuantitativeCheckResult¶
Symbolic parametric hybrid quantitative model checking result
- get_values(self: stormpy.core.HybridParametricQuantitativeCheckResult) List[pycarl.cln.cln.FactorizedRationalFunction] ¶
Get model checking result values for all states
- class HybridQuantitativeCheckResult¶
Hybrid quantitative model checking result
- get_values(self: stormpy.core.HybridQuantitativeCheckResult) List[float] ¶
Get model checking result values for all states
- class InstantaneousRewardFormula¶
Instantaneous reward
- 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 0x7f04b7896870>) 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 JaniModelType¶
Type of the Jani model
Members:
DTMC
CTMC
MDP
CTMDP
MA
LTS
TA
PTA
STA
HA
PHA
SHA
UNDEFINED
- CTMC = <JaniModelType.CTMC: 3>¶
- CTMDP = <JaniModelType.CTMDP: 5>¶
- DTMC = <JaniModelType.DTMC: 2>¶
- HA = <JaniModelType.HA: 10>¶
- LTS = <JaniModelType.LTS: 1>¶
- MA = <JaniModelType.MA: 6>¶
- MDP = <JaniModelType.MDP: 4>¶
- PHA = <JaniModelType.PHA: 11>¶
- PTA = <JaniModelType.PTA: 8>¶
- SHA = <JaniModelType.SHA: 12>¶
- STA = <JaniModelType.STA: 9>¶
- TA = <JaniModelType.TA: 7>¶
- UNDEFINED = <JaniModelType.UNDEFINED: 0>¶
- property name¶
- property value¶
- 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 LongRunAvarageOperator¶
Long run average operator
- class LongRunAverageRewardFormula¶
Long run average reward
- 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 MinMaxMethod¶
Method for min-max equation systems
Members:
policy_iteration
value_iteration
linear_programming
topological
rational_search
interval_iteration
sound_value_iteration
optimistic_value_iteration
- interval_iteration = <MinMaxMethod.interval_iteration: 5>¶
- linear_programming = <MinMaxMethod.linear_programming: 2>¶
- property name¶
- optimistic_value_iteration = <MinMaxMethod.optimistic_value_iteration: 7>¶
- policy_iteration = <MinMaxMethod.policy_iteration: 1>¶
- rational_search = <MinMaxMethod.rational_search: 4>¶
- sound_value_iteration = <MinMaxMethod.sound_value_iteration: 6>¶
- topological = <MinMaxMethod.topological: 3>¶
- property value¶
- value_iteration = <MinMaxMethod.value_iteration: 0>¶
- class ModelCheckerHint¶
Information that may accelerate the model checking process
- class ModelFormulasPair¶
Pair of model and formulas
- property formulas¶
The formulas
- property model¶
The model
- 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 MultiObjectiveFormula¶
Multi objective formula
- property nr_subformulas¶
Get number of subformulas
- property subformulas¶
Get vector of subformulas
- class NativeLinearEquationSolverMethod¶
Method for linear equation systems with the native solver
Members:
power_iteration
sound_value_iteration
optimistic_value_iteration
interval_iteration
rational_search
jacobi
SOR
gauss_seidel
walker_chae
- SOR = <NativeLinearEquationSolverMethod.SOR: 2>¶
- gauss_seidel = <NativeLinearEquationSolverMethod.gauss_seidel: 1>¶
- interval_iteration = <NativeLinearEquationSolverMethod.interval_iteration: 7>¶
- jacobi = <NativeLinearEquationSolverMethod.jacobi: 0>¶
- property name¶
- optimistic_value_iteration = <NativeLinearEquationSolverMethod.optimistic_value_iteration: 6>¶
- power_iteration = <NativeLinearEquationSolverMethod.power_iteration: 4>¶
- rational_search = <NativeLinearEquationSolverMethod.rational_search: 8>¶
- sound_value_iteration = <NativeLinearEquationSolverMethod.sound_value_iteration: 5>¶
- property value¶
- walker_chae = <NativeLinearEquationSolverMethod.walker_chae: 3>¶
- class NativeSolverEnvironment¶
Environment for Native solvers
- property maximum_iterations¶
- property method¶
- property precision¶
- class OperatorFormula¶
Operator formula
- property comparison_type¶
Comparison type of bound
- property has_bound¶
Flag if formula is bounded
- property has_optimality_type¶
Flag if an optimality type is present
- property optimality_type¶
Flag for the optimality type
- remove_bound(self: stormpy.logic.logic.OperatorFormula) None ¶
- remove_optimality_type(self: stormpy.logic.logic.OperatorFormula) None ¶
remove the optimality type
- set_bound(self: stormpy.logic.logic.OperatorFormula, comparison_type: stormpy.logic.logic.ComparisonType, bound: stormpy.storage.storage.Expression) None ¶
Set bound
- set_optimality_type(self: stormpy.logic.logic.OperatorFormula, new_optimality_type: stormpy.core.OptimizationDirection) None ¶
set the optimality type (use remove optimiality type for clearing)
- property threshold¶
Threshold of bound (currently only applicable to rational expressions)
- property threshold_expr¶
- 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 OptimizationDirection¶
Members:
Minimize
Maximize
- Maximize = <OptimizationDirection.Maximize: 1>¶
- Minimize = <OptimizationDirection.Minimize: 0>¶
- 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 ParametricCheckTask¶
Task for parametric model checking
- set_produce_schedulers(self: stormpy.core.ParametricCheckTask, produce_schedulers: bool = True) None ¶
Set whether schedulers should be produced (if possible)
- 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 ParetoCurveCheckResultDouble¶
Result for multiobjective model checking
- get_overapproximation(self: stormpy.core.ParetoCurveCheckResultDouble) storm::storage::geometry::Polytope<double> ¶
- get_underapproximation(self: stormpy.core.ParetoCurveCheckResultDouble) storm::storage::geometry::Polytope<double> ¶
- class PathFormula¶
Formula about the probability of a set of paths in an automaton
- class Polynomial¶
Represent a multivariate polynomial
- constant_part(self: pycarl.cln.cln.Polynomial) pycarl.cln.cln.Rational ¶
- degree(self: pycarl.cln.cln.Polynomial, arg0: pycarl.core.Variable) int ¶
- derive(self: pycarl.cln.cln.Polynomial, variable: pycarl.core.Variable) pycarl.cln.cln.Polynomial ¶
Compute the derivative
- evaluate(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) pycarl.cln.cln.Rational ¶
- gather_variables(self: pycarl.cln.cln.Polynomial) Set[pycarl.core.Variable] ¶
- is_constant(self: pycarl.cln.cln.Polynomial) bool ¶
- property nr_terms¶
- substitute(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Polynomial]) pycarl.cln.cln.Polynomial ¶
- to_smt2(self: pycarl.cln.cln.Polynomial) str ¶
- property total_degree¶
- 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<