Stormpy.core

class AtomicExpressionFormula

Formula with an atomic expression

class AtomicLabelFormula

Formula with an atomic label

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 BinaryPathFormula

Path formula with two operands

property left_subformula
property right_subformula
class BinaryStateFormula

State formula with two operands

class BisimulationType

Types of bisimulation

STRONG = BisimulationType.STRONG
WEAK = BisimulationType.WEAK
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 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_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

class CheckTask

Task for model checking

set_produce_schedulers(self: stormpy.core.CheckTask, produce_schedulers: bool = True) → None

Set whether schedulers should be produced (if possible)

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
GEQ = ComparisonType.GEQ
GREATER = ComparisonType.GREATER
LEQ = ComparisonType.LEQ
LESS = ComparisonType.LESS
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
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

class DirectEncodingOptions
property allow_placeholders
class DirectEncodingParserOptions

Options for the .drn parser

property build_choice_labels

Build with choice labels

class DistributionDouble

Finite Support Distribution

class EliminationLabelBehavior

Behavior of labels while eliminating non-Markovian chains

DELETE_LABELS = EliminationLabelBehavior.DELETE_LABELS
KEEP_LABELS = EliminationLabelBehavior.KEEP_LABELS
MERGE_LABELS = EliminationLabelBehavior.MERGE_LABELS
class Environment
property solver_environment

solver part of environment

class EquationSolverType

Solver type for equation systems

eigen = EquationSolverType.eigen
elimination = EquationSolverType.elimination
gmmxx = EquationSolverType.gmmxx
native = EquationSolverType.native
topological = EquationSolverType.topological
class EventuallyFormula

Formula for eventually

class ExplicitExactQuantitativeCheckResult

Explicit exact quantitative model checking result

at(self: stormpy.core.ExplicitExactQuantitativeCheckResult, state: int) → __gmp_expr<__mpq_struct [1], __mpq_struct [1]>

Get result for given state

get_values(self: stormpy.core.ExplicitExactQuantitativeCheckResult) → List[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]

Get model checking result values for all states

class ExplicitModelBuilder_Double

Model builder for sparse models

build(self: stormpy.core.ExplicitModelBuilder_Double) → storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >

Build the model

export_lookup(self: stormpy.core.ExplicitModelBuilder_Double) → storm::builder::ExplicitStateLookup<unsigned int>

Export a lookup model

class ExplicitModelBuilder_RF

Model builder for sparse models

build(self: stormpy.core.ExplicitModelBuilder_RF) → storm::models::sparse::Model<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> > >

Build the model

export_lookup(self: stormpy.core.ExplicitModelBuilder_RF) → storm::builder::ExplicitStateLookup<unsigned int>

Export a lookup model

class ExplicitParametricQuantitativeCheckResult

Explicit parametric quantitative model checking result

at(self: stormpy.core.ExplicitParametricQuantitativeCheckResult, state: int) → carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>

Get result for given state

get_values(self: stormpy.core.ExplicitParametricQuantitativeCheckResult) → List[carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>]

Get model checking result values for all states

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]) → int
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

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_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[__gmp_expr<__mpq_struct [1], __mpq_struct [1]>]

Get model checking result values for all states

class HybridParametricQuantitativeCheckResult

Symbolic parametric hybrid quantitative model checking result

get_values(self: stormpy.core.HybridParametricQuantitativeCheckResult) → List[carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>]

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

property initial_location_indices
property initial_states_restriction

initial state restriction

property location_variable
property locations
property name
property variables
class JaniBoundedIntegerVariable

A Bounded Integer

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]) → 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

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)

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 0x7f626df20e30>) → 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

CTMC = JaniModelType.CTMC
CTMDP = JaniModelType.CTMDP
DTMC = JaniModelType.DTMC
HA = JaniModelType.HA
LTS = JaniModelType.LTS
MA = JaniModelType.MA
MDP = JaniModelType.MDP
PHA = JaniModelType.PHA
PTA = JaniModelType.PTA
SHA = JaniModelType.SHA
STA = JaniModelType.STA
TA = JaniModelType.TA
UNDEFINED = JaniModelType.UNDEFINED
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
class JaniVariable

A Variable in JANI

property expression_variable

expression variable for this variable

property name

name of constant

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?

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 MinMaxMethod

Method for min-max equation systems

interval_iteration = MinMaxMethod.interval_iteration
linear_programming = MinMaxMethod.linear_programming
optimistic_value_iteration = MinMaxMethod.optimistic_value_iteration
policy_iteration = MinMaxMethod.policy_iteration
sound_value_iteration = MinMaxMethod.sound_value_iteration
topological = MinMaxMethod.topological
topological_cuda = MinMaxMethod.topological_cuda
value_iteration = MinMaxMethod.value_iteration
class MinMaxSolverEnvironment

Environment for Min-Max-Solvers

property method
property precision
class ModelFormulasPair

Pair of model and formulas

property formulas

The formulas

property model

The model

class ModelType

Type of the model

CTMC = ModelType.CTMC
DTMC = ModelType.DTMC
MA = ModelType.MA
MDP = ModelType.MDP
POMDP = ModelType.POMDP
class NativeLinearEquationSolverMethod

Method for linear equation systems with the native solver

SOR = NativeLinearEquationSolverMethod.SOR
gauss_seidel = NativeLinearEquationSolverMethod.gauss_seidel
interval_iteration = NativeLinearEquationSolverMethod.interval_iteration
jacobi = NativeLinearEquationSolverMethod.jacobi
optimistic_value_iteration = NativeLinearEquationSolverMethod.optimistic_value_iteration
power_iteration = NativeLinearEquationSolverMethod.power_iteration
sound_value_iteration = NativeLinearEquationSolverMethod.sound_value_iteration
walker_chae = NativeLinearEquationSolverMethod.walker_chae
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)

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 OptimizationDirection
Maximize = OptimizationDirection.Maximize
Minimize = OptimizationDirection.Minimize
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

Parametric 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 row

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 parametric 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 (RationalFunction) – 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 parametric 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

class ParametricSparseMatrixRows

Set of rows in a parametric sparse matrix

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 PrismAssignment

An assignment in prism

property expression

Expression for the update

property variable

Variable that is updated

class PrismBooleanVariable

A program boolean variable in a Prism program

class PrismChoiceOrigins

This class represents for each choice the set of prism commands that induced the choice.

get_command_set(self: stormpy.storage.storage.PrismChoiceOrigins, choice_index: int) → stormpy.core.FlatSet

Returns the set of prism commands that induced the choice

property program

retrieves the associated Prism program

class PrismCommand

A command in a Prism program

property action_index

What is the action index of the command

property global_index

Get global index

property guard_expression

Get guard expression

property labeled

Is the command labeled

property updates

Updates in the command

class PrismConstant

A constant in a Prism program

property defined

Is the constant defined?

property definition

Defining expression

property expression_variable

Expression variable

property name

Constant name

property type

The type of the constant

class PrismIntegerVariable

A program integer variable in a Prism program

property lower_bound_expression

The the lower bound expression of this integer variable

property upper_bound_expression

The the upper bound expression of this integer variable

class PrismLabel

A label in prism

property expression
property name
class PrismModelType

Type of the prism model

CTMC = PrismModelType.CTMC
CTMDP = PrismModelType.CTMDP
DTMC = PrismModelType.DTMC
MA = PrismModelType.MA
MDP = PrismModelType.MDP
UNDEFINED = PrismModelType.UNDEFINED
class PrismModule

A module in a Prism program

property boolean_variables

All boolean Variables of this module

property commands

Commands in the module

get_boolean_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) → storm::prism::BooleanVariable
get_command_indices_by_action_index(self: stormpy.storage.storage.PrismModule, action_index: int) → Set[int]
get_integer_variable(self: stormpy.storage.storage.PrismModule, variable_name: str) → storm::prism::IntegerVariable
property integer_variables

All integer Variables of this module

property name

Name of the module

class PrismProgram

A Prism Program

property constants

Get Program Constants

define_constants(self: stormpy.storage.storage.PrismProgram, arg0: Dict[storm::expressions::Variable, storm::expressions::Expression]) → stormpy.storage.storage.PrismProgram

Define constants

property expression_manager

Get the expression manager for expressions in this program

flatten(self: stormpy.storage.storage.PrismProgram, smt_factory: stormpy.utility.utility.SmtSolverFactory=<stormpy.utility.utility.SmtSolverFactory object at 0x7f626df1a370>) → 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 hasUndefinedConstants

Does the program have undefined constants?

property has_undefined_constants

Flag if program has undefined constants

property isDeterministicModel

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

class PrismRewardModel

Reward declaration in prism

property name

get name of the reward model

class PrismUpdate

An update in a Prism command

property assignments

Assignments in the update

property probability_expression

The probability expression for this update

class PrismVariable

A program variable in a Prism program

property expression_variable

The expression variable corresponding to the variable

property initial_value_expression

The expression represented the initial value of the variable

property name

Variable name

class ProbabilityOperator

Probability operator

class Property
property name

Obtain the name of the property

property raw_formula

Obtain the formula directly

class Rational

Class wrapping gmp-rational numbers

property denominator
property nominator
property numerator
class RationalFunction

Represent a rational function, that is the fraction of two multivariate polynomials

constant_part(self: pycarl.cln.cln.RationalFunction) → pycarl.cln.cln.Rational
property denominator
derive(self: pycarl.cln.cln.RationalFunction, variable: pycarl.core.Variable) → pycarl.cln.cln.RationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.RationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.RationalFunction) → Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.RationalFunction) → bool
property nominator
property numerator
to_smt2(self: pycarl.cln.cln.RationalFunction) → str
RationalRF

alias of pycarl.cln.cln.Rational

class RewardOperator

Reward operator

has_reward_name(self: stormpy.logic.logic.RewardOperator) → bool
property reward_name
class SMTCounterExampleGenerator

Highlevel Counterexample Generator with SMT as backend

build(env: stormpy.core.Environment, stats: stormpy.core.SMTCounterExampleGeneratorStats, symbolic_model: storm::storage::SymbolicModelDescription, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, cex_input: storm::counterexamples::SMTMinimalLabelSetGenerator<double>::CexInput, dontcare: stormpy.core.FlatSet, options: stormpy.core.SMTCounterExampleGeneratorOptions) → List[stormpy.core.FlatSet]

Compute counterexample

precompute(env: stormpy.core.Environment, symbolic_model: storm::storage::SymbolicModelDescription, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, formula: storm::logic::Formula) → storm::counterexamples::SMTMinimalLabelSetGenerator<double>::CexInput

Precompute input for counterexample generation

class SMTCounterExampleGeneratorOptions

Options for highlevel counterexample generation

property add_backward_implication_cuts
property check_threshold_feasible
property continue_after_first_counterexample
property encode_reachability
property maximum_counterexamples
property maximum_iterations_after_counterexample
property silent
property use_dynamic_constraints
class SMTCounterExampleGeneratorStats

Stats for highlevel counterexample generation

property analysis_time
property cut_time
property iterations
property model_checking_time
property setup_time
property solver_time
class SMTCounterExampleInput

Precomputed input for counterexample generation

add_reward_and_threshold(self: stormpy.core.SMTCounterExampleInput, reward_name: str, threshold: float) → None

add another reward structure and threshold

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

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 SolverEnvironment

Environment for solvers

property minmax_solver_environment
property native_solver_environment
set_force_sound(self: stormpy.core.SolverEnvironment, new_value: bool = True) → None

force soundness

set_linear_equation_solver_type(self: stormpy.core.SolverEnvironment, new_value: stormpy.core.EquationSolverType, set_from_default: bool = False) → None

set solver type to use

class SparseCtmc

CTMC in sparse representation

property exit_rates
class SparseDtmc

DTMC in sparse representation

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

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

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

class SparseModelState

State in sparse model

property actions

Get actions

property id

Id

property labels

Labels

class SparseModelStates

States in sparse model

class SparseParametricCtmc

pCTMC in sparse representation

class SparseParametricDtmc

pDTMC in sparse representation

class SparseParametricMA

pMA in sparse representation

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 parametric model

property id

Id

property transitions

Get transitions

class SparseParametricModelActions

Actions for state in sparse parametric model

class SparseParametricModelState

State in sparse parametric model

property actions

Get actions

property id

Id

property labels

Labels

class SparseParametricModelStates

States in sparse parametric 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
property nr_observations
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 StateFormula

Formula about a state of an automaton

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

exception StormError(message)

Base class for exceptions in Storm.

class SubsystemBuilderOptions

Options for constructing the subsystem

property build_action_mapping
property build_kept_actions
property build_state_mapping
property check_transitions_outside
class SubsystemBuilderReturnTypeDouble

Result of the construction of a subsystem

property kept_actions

Actions of the subsystem available in the original system

property model

the submodel

property new_to_old_action_mapping

for each action in result, the action index in the original model

property new_to_old_state_mapping

for each state in result, the state index in the original model

class SymbolicExactQuantitativeCheckResult

Symbolic exact quantitative model checking result

clone(self: stormpy.core.SymbolicExactQuantitativeCheckResult) → stormpy.core.SymbolicExactQuantitativeCheckResult
class SymbolicModelDescription

Symbolic description of model

as_jani_model(self: stormpy.core.SymbolicModelDescription) → storm::jani::Model

Return Jani model

as_prism_program(self: stormpy.core.SymbolicModelDescription) → storm::prism::Program

Return Prism program

instantiate_constants(self: stormpy.core.SymbolicModelDescription, constant_definitions: Dict[storm::expressions::Variable, storm::expressions::Expression]) → stormpy.core.SymbolicModelDescription

Instantiate constants in symbolic model description

property is_jani_model

Flag if program is in Jani format

property is_prism_program

Flag if program is in Prism format

parse_constant_definitions(self: stormpy.core.SymbolicModelDescription, String containing constants and their values: str) → Dict[storm::expressions::Variable, storm::expressions::Expression]

Parse given constant definitions

class SymbolicParametricQuantitativeCheckResult

Symbolic parametric quantitative model checking result

clone(self: stormpy.core.SymbolicParametricQuantitativeCheckResult) → stormpy.core.SymbolicParametricQuantitativeCheckResult
class SymbolicQualitativeCheckResult

Symbolic qualitative model checking result

get_truth_values(self: stormpy.core.SymbolicQualitativeCheckResult) → storm::dd::Bdd<(storm::dd::DdType)1>

Get Dd representing the truth values

class SymbolicQuantitativeCheckResult

Symbolic quantitative model checking result

clone(self: stormpy.core.SymbolicQuantitativeCheckResult) → stormpy.core.SymbolicQuantitativeCheckResult
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
class SymbolicSylvanRewardModel

Reward structure for symbolic models

property has_state_action_rewards
property has_state_rewards
property has_transition_rewards
class TimeOperator

The time operator

class UnaryBooleanStateFormula

Unary boolean state formula

class UnaryPathFormula

Path formula with one operand

property subformula

the subformula

class UnaryStateFormula

State formula with one operand

property subformula

the subformula

class UntilFormula

Path Formula for unbounded until

class Variable
property id
property is_no_variable
property name
property rank
property type
build_model(symbolic_description, properties=None)

Build a model in sparse representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Model in sparse representation.

build_model_from_drn(file, options=<stormpy.core.DirectEncodingParserOptions object>)

Build a model in sparse representation from the explicit DRN representation.

Parameters
  • file (String) – DRN file containing the model.

  • DirectEncodingParserOptions – Options for the parser.

Returns

Model in sparse representation.

build_parametric_model(symbolic_description, properties=None)

Build a parametric model in sparse representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Parametric model in sparse representation.

build_parametric_model_from_drn(file, options=<stormpy.core.DirectEncodingParserOptions object>)

Build a parametric model in sparse representation from the explicit DRN representation.

Parameters
  • file (String) – DRN file containing the model.

  • DirectEncodingParserOptions – Options for the parser.

Returns

Parametric model in sparse representation.

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.

build_sparse_model(symbolic_description, properties=None)

Build a model in sparse representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Model in sparse representation.

build_sparse_model_from_explicit(transition_file: str, labeling_file: str, state_reward_file: Optional[str] = '', transition_reward_file: Optional[str] = '', choice_labeling_file: Optional[str] = '') → storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >

Build the model model from explicit input

build_sparse_model_with_options(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions, use_jit: bool=False, doctor: bool=False) → storm::models::ModelBase

Build the model in sparse representation

build_sparse_parametric_model(symbolic_description, properties=None)

Build a parametric model in sparse representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Parametric model in sparse representation.

build_sparse_parametric_model_with_options(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions, use_jit: bool=False, doctor: bool=False) → storm::models::ModelBase

Build the model in sparse representation

build_symbolic_model(symbolic_description, properties=None)

Build a model in symbolic representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Model in symbolic representation.

build_symbolic_parametric_model(symbolic_description, properties=None)

Build a parametric model in symbolic representation from a symbolic description.

Parameters
  • symbolic_description – Symbolic model description to translate into a model.

  • properties (List[Property]) – List of properties that should be preserved during the translation. If None, then all properties are preserved.

Returns

Parametric model in symbolic representation.

check_model_dd(model, property, only_initial_states=False, environment=<stormpy.core.Environment object>)

Perform model checking using dd engine. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :return: Model checking result. :rtype: CheckResult

check_model_hybrid(model, property, only_initial_states=False, environment=<stormpy.core.Environment object>)

Perform model checking using hybrid engine. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :return: Model checking result. :rtype: CheckResult

check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=<stormpy.core.Environment object>)

Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler :return: Model checking result. :rtype: CheckResult

collect_information(arg0: stormpy.storage.storage.JaniModel) → stormpy.storage.storage.JaniInformationObject
compute_all_until_probabilities(arg0: stormpy.core.Environment, arg1: stormpy.core.CheckTask, arg2: storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >, arg3: storm::storage::BitVector, arg4: storm::storage::BitVector) → List[float]

Compute forward until probabilities

compute_prob01_states(model, phi_states, psi_states)

Compute prob01 states for properties of the form phi_states until psi_states

Parameters
  • model (SparseDTMC) –

  • phi_states (BitVector) –

  • psi_states (BitVector) – Target states

compute_prob01max_states(model, phi_states, psi_states)
compute_prob01min_states(model, phi_states, psi_states)
compute_transient_probabilities(arg0: stormpy.core.Environment, arg1: storm::models::sparse::Ctmc<double, storm::models::sparse::StandardRewardModel<double> >, arg2: storm::storage::BitVector, arg3: storm::storage::BitVector, arg4: float) → List[float]

Compute transient probabilities

construct_submodel(model, states, actions, keep_unreachable_states=True, options=<stormpy.core.SubsystemBuilderOptions object>)
Parameters
  • model – The model

  • states – Which states should be preserved

  • actions – Which actions should be preserved

  • keep_unreachable_states – If False, run a reachability analysis.

Returns

A model with fewer states/actions

create_filter_initial_states_sparse(model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >) → stormpy.core._QualitativeCheckResult

Create a filter for the initial states on a sparse model

create_filter_initial_states_symbolic(model: storm::models::symbolic::Model<(storm::dd::DdType)1, double>) → stormpy.core._QualitativeCheckResult

Create a filter for the initial states on a symbolic model

create_filter_symbolic(model: storm::models::symbolic::Model<(storm::dd::DdType)1, double>, states: storm::expressions::Expression) → stormpy.core._QualitativeCheckResult

Creates a filter for the given states and a symbolic model

eliminate_non_markovian_chains(ma, properties, label_behavior)

Eliminate chains of non-Markovian states if possible. :param ma: Markov automaton. :param properties: List of properties to transform as well. :param label_behavior: Behavior of labels while elimination. :return: Tuple (converted MA, converted properties).

eliminate_reward_accumulations(model: stormpy.storage.storage.JaniModel, properties: List[stormpy.core.Property]) → List[stormpy.core.Property]

Eliminate reward accumulations

export_parametric_to_drn(model: storm::models::sparse::Model<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true>, storm::models::sparse::StandardRewardModel<carl::RationalFunction<carl::FactorizedPolynomial<carl::MultivariatePolynomial<cln::cl_RA, carl::MonomialComparator<&carl::Monomial::compareGradedLexical, true>, carl::StdMultivariatePolynomialPolicies<carl::NoReasons, carl::NoAllocator> > >, true> > >, file: str, options: stormpy.core.DirectEncodingOptions=<stormpy.core.DirectEncodingOptions object at 0x7f626dfdbcf0>) → None

Export parametric model in DRN format

export_to_drn(model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, file: str, options: stormpy.core.DirectEncodingOptions=<stormpy.core.DirectEncodingOptions object at 0x7f626dfdb6f0>) → None

Export model in DRN format

make_sparse_model_builder(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions) → storm::builder::ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>

Construct a builder instance

make_sparse_model_builder_parametric(model_description: storm::storage::SymbolicModelDescription, options: storm::builder::BuilderOptions) → storm::builder::ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, unsigned int>

Construct a builder instance

model_checking(model, property, only_initial_states=False, extract_scheduler=False, environment=<stormpy.core.Environment object>)

Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler :return: Model checking result. :rtype: CheckResult

model_checking_fully_observable(model: storm::models::sparse::Pomdp<double, storm::models::sparse::StandardRewardModel<double> >, task: stormpy.core.CheckTask, environment: stormpy.core.Environment=<stormpy.core.Environment object at 0x7f626dfe1770>) → stormpy.core._CheckResult
parse_jani_model(path: str) → Tuple[storm::jani::Model, List[stormpy.core.Property]]

Parse Jani model

parse_prism_program(path: str, prism_compat: bool = False, simplify: bool = True) → storm::prism::Program

Parse Prism program

parse_properties(properties, context=None, filters=None)
Parameters
  • properties – A string with the pctl properties

  • context – A symbolic model that gives meaning to variables and constants.

  • filters – filters, if applicable.

Returns

A list of properties

parse_properties_for_jani_model(formula_string: str, jani_model: storm::jani::Model, property_filter: Optional[Set[str]]=None) → List[stormpy.core.Property]
parse_properties_for_prism_program(formula_string: str, prism_program: storm::prism::Program, property_filter: Optional[Set[str]]=None) → List[stormpy.core.Property]

Parses properties given in the prism format, allows references to variables in the prism program.

Parameters
  • formula_str (str) – A string of formulas

  • prism_program (PrismProgram) – A prism program

  • property_filter (str) – A filter

Returns

A list of properties

parse_properties_without_context(formula_string: str, property_filter: Optional[Set[str]] = None) → List[stormpy.core.Property]

Parse properties given in the prism format.

Parameters
  • formula_str (str) – A string of formulas

  • property_filter (str) – A filter

Returns

A list of properties

perform_bisimulation(model, properties, bisimulation_type)

Perform bisimulation on model. :param model: Model. :param properties: Properties to preserve during bisimulation. :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation.

perform_sparse_bisimulation(model, properties, bisimulation_type)

Perform bisimulation on model in sparse representation. :param model: Model. :param properties: Properties to preserve during bisimulation. :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation.

perform_symbolic_bisimulation(model, properties)

Perform bisimulation on model in symbolic representation. :param model: Model. :param properties: Properties to preserve during bisimulation. :return: Model after bisimulation.

preprocess_symbolic_input(symbolic_model_description: storm::storage::SymbolicModelDescription, properties: List[stormpy.core.Property], constant_definition_string: str) → Tuple[storm::storage::SymbolicModelDescription, List[stormpy.core.Property]]

Preprocess symoblic input

prob01max_states(model, eventually_formula)
prob01min_states(model, eventually_formula)
set_settings(arguments: List[str]) → None

Set settings

topological_sort(model, forward=True, initial=[])
Parameters
  • model

  • forward

Returns

transform_to_discrete_time_model(model, properties)

Transform continuous-time model to discrete time model. :param model: Continuous-time model. :param properties: List of properties to transform as well. :return: Tuple (Discrete-time model, converted properties).

transform_to_sparse_model(model)

Transform model in symbolic representation into model in sparse representation. :param model: Symbolic model. :return: Sparse model.