Stormpy.core

class AtomicExpressionFormula

Formula with an atomic expression

class AtomicLabelFormula

Formula with an atomic label

class BinaryPathFormula

Path formula with two operands

left_subformula
right_subformula
class BinaryStateFormula

State formula with two operands

class BisimulationType

Types of bisimulation

STRONG = BisimulationType.STRONG
WEAK = BisimulationType.WEAK
class BitVector
get()
number_of_set_bits()
set()

Set

size()
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.

class BuilderOptions

Options for building process

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

class ChoiceOrigins

This class represents the origin of choices of a model in terms of the input model spec.

get_choice_info()

human readable string

get_identifier_info()

human readable string

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

A constant in a Prism program

defined

Is the constant defined?

expression_variable

Expression variable

name

Constant name

type

The type of the constant

class ConstraintCollector

Collector for constraints on parametric Markov chains

graph_preserving_constraints

Get the constraints ensuring the graph is preserved

wellformed_constraints

Get the constraints ensuring a wellformed model

class CumulativeRewardFormula

Summed rewards over a the paths

class DistributionDouble

Finite Support Distribution

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

scheduler

get scheduler

class Expression

Holds an expression

And()
Eq()
Geq()
Greater()
Iff()
Implies()
Leq()
Less()
Minus()
Multiply()
Neq()
Or()
Plus()
contains_variable()

Check if the expression contains any of the given variables.

contains_variables()

Check if the expression contains variables.

get_variables()

Get the variables

has_boolean_type()

Check if the expression is a boolean

has_integer_type()

Check if the expression is an integer

has_rational_type()

Check if the expression is a rational

is_literal()

Check if the expression is a literal

manager

Get the manager

substitute()
type

Get the Type

class ExpressionManager

Manages variables for expressions

create_boolean()

Create expression from boolean

create_boolean_variable()

create Boolean variable

create_integer()

Create expression from integer number

create_integer_variable()

create Integer variable

create_rational()

Create expression from rational number

create_rational_variable()

create Rational variable

class ExpressionParser

Parser for storm-expressions

parse()
set_identifier_mapping()

sets identifiers

class ExpressionType

The type of an expression

is_boolean
is_integer
is_rational
class FactorizedPolynomial

Represent a polynomial with its factorization

cache(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln._FactorizationCache
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
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
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()
is_probability_operator

is it a probability operator

is_reward_operator

is it a reward operator

substitute()

Substitute variables

substitute_labels_by_labels()

substitute label occurences

class GloballyFormula

Formula for globally

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

Add label

contains_label()

Check if the given label is contained in the labeling

get_labels()

Get all labels

class JaniAssignment

Jani Assignment

expression
class JaniAutomaton

A Jani Automation

add_edge()
add_initial_location()
add_location()

adds a new location, returns the index

edges

get edges

initial_location_indices
initial_states_restriction

initial state restriction

location_variable
locations
name
variables
class JaniBoundedIntegerVariable

A Bounded Integer

class JaniChoiceOrigins

This class represents for each choice the origin in the jani spec.

get_edge_index_set()

returns the set of edges that induced the choice

model

retrieves the associated JANI model

class JaniConstant

A Constant in JANI

defined

is constant defined by some expression

expression_variable

expression variable for this constant

name

name of constant

type

type of constant

class JaniEdge

A Jani Edge

action_index

action index

color

color for the edge

destinations

edge destinations

guard

edge guard

has_silent_action()

Is the edge labelled with the silent action

nr_destinations

nr edge destinations

rate

edge rate

source_location_index

index for source location

substitute()
template_edge

template edge

class JaniEdgeDestination

Destination in Jani

assignments
probability
target_location_index
class JaniLocation

A Location in JANI

assignments

location assignments

name

name of the location

class JaniModel

A Jani Model

add_automaton()

add an automaton (with a unique name)

automata

get automata

check_valid()

Some basic checks to ensure validity

constants

get constants

decode_automaton_and_edge_index()

get edge and automaton from edge/automaton index

define_constants()

define constants with a mapping from the corresponding expression variables to expressions

encode_automaton_and_edge_index()

get edge/automaton-index

expression_manager

get expression manager

finalize()

finalizes the model. After this action, be careful changing the data structure.

get_automaton_index()

get index for automaton name

get_constant()

get constant by name

global_variables
has_standard_composition()

is the composition the standard composition

has_undefined_constants

Flag if program has undefined constants

initial_states_restriction

initial states restriction

make_standard_compliant()

make standard JANI compliant

model_type

Model type

name

model name

remove_constant()

remove a constant. Make sure the constant does not appear in the model.

replace_automaton()

replace automaton at index

restrict_edges()

restrict model to edges given by set

set_model_type()

Sets (only) the model type

set_standard_system_composition()

sets the composition to the standard composition

substitute_constants()

substitute constants

substitute_functions()

substitute functions

to_dot()
undefined_constants_are_graph_preserving

Flag if the undefined constants do not change the graph structure

class 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()
clone()

clone assignments (performs a deep copy)

substitute()

substitute in rhs according to given substitution map

class JaniTemplateEdge

Template edge, internal data structure for edges

add_destination()
assignments
destinations
guard
class JaniTemplateEdgeDestination

Template edge destination, internal data structure for edge destinations

assignments
class JaniVariable

A Variable in JANI

expression_variable

expression variable for this variable

name

name of constant

class JaniVariableSet

Jani Set of Variables

add_bounded_integer_variable()
add_variable()
empty()

is there a variable in the set?

get_variable_by_expr_variable()
get_variable_by_name()
class 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
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

method
precision
class ModelFormulasPair

Pair of model and formulas

formulas

The formulas

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 OperatorFormula

Operator formula

comparison_type

Comparison type of bound

has_bound

Flag if formula is bounded

has_optimality_type

Flag if an optimality type is present

optimality_type

Flag for the optimality type

remove_bound()
remove_optimality_type()

remove the optimality type

set_bound()

Set bound

set_optimality_type()

set the optimality type (use remove optimiality type for clearing)

threshold

Threshold of bound (currently only applicable to rational expressions)

threshold_expr
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()

Get row

get_row_group_end()
get_row_group_start()
get_rows()

Get rows from start to end

has_trivial_row_grouping

Trivial row grouping

nr_columns

Number of columns

nr_entries

Number of non-zero entries

nr_rows

Number of rows

print_row()

Print row

row_iter()

Get iterator from start to end

submatrix()

Get submatrix

class ParametricSparseMatrixEntry

Entry of parametric sparse matrix

column

Column

set_value()

Set value

value()

Value

class ParametricSparseMatrixRows

Set of rows in a parametric sparse matrix

class PathFormula

Formula about the probability of a set of paths in an automaton

class Polynomial

Represent a multivariate polynomial

constant_part
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
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
total_degree
class PrismAssignment

An assignment in prism

expression

Expression for the update

variable

Variable that is updated

class PrismCommand

A command in a Prism program

global_index

Get global index

guard_expression

Get guard expression

updates

Updates in the command

class PrismModelType

Type of the prism model

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

A module in a Prism program

commands

Commands in the module

name

Name of the module

class PrismProgram

A Prism Program

constants

Get Program Constants

define_constants()

Define constants

expression_manager

Get the expression manager for expressions in this program

has_undefined_constants

Flag if program has undefined constants

model_type

Model type

modules

Modules in the program

nr_modules

Number of modules

restrict_commands()

Restrict commands

simplify()

Simplify

substitute_constants()

Substitute constants within program

to_jani()

Transform to Jani program

undefined_constants_are_graph_preserving

Flag if the undefined constants do not change the graph structure

used_constants()

Compute Used Constants

class PrismUpdate

An update in a Prism command

assignments

Assignments in the update

class ProbabilityOperator

Probability operator

class Property
name

Obtain the name of the property

raw_formula

Obtain the formula directly

class Rational

Class wrapping gmp-rational numbers

denominator
nominator
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
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
nominator
numerator
to_smt2(self: pycarl.cln.cln.RationalFunction) → str
RationalRF

alias of pycarl.cln.cln.Rational

class RewardOperator

Reward operator

has_reward_name()
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

add_backward_implication_cuts
check_threshold_feasible
continue_after_first_counterexample
encode_reachability
maximum_counterexamples
maximum_iterations_after_counterexample
silent
use_dynamic_constraints
class SMTCounterExampleGeneratorStats

Stats for highlevel counterexample generation

analysis_time
cut_time
iterations
model_checking_time
setup_time
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

defined

Is the choice defined by the scheduler?

deterministic

Is the choice deterministic (given by a Dirac distribution)?

get_choice()

Get the distribution over the actions

get_deterministic_choice()

Get the deterministic choice

class SchedulerDouble

A Finite Memory Scheduler

compute_action_support()
deterministic

Is the scheduler deterministic?

get_choice()
memory_size

How much memory does the scheduler take?

memoryless

Is the scheduler memoryless?

class SolverEnvironment

Environment for solvers

minmax_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

class SparseDtmc

DTMC in sparse representation

class SparseMA

MA in sparse representation

class SparseMatrix

Sparse matrix

get_row()

Get row

get_row_group_end()
get_row_group_start()
get_rows()

Get rows from start to end

has_trivial_row_grouping

Trivial row grouping

nr_columns

Number of columns

nr_entries

Number of non-zero entries

nr_rows

Number of rows

print_row()

Print rows from start to end

row_iter()

Get iterator from start to end

submatrix()

Get submatrix

class SparseMatrixEntry

Entry of sparse matrix

column

Column

set_value()

Set value

value()

Value

class SparseMatrixRows

Set of rows in a sparse matrix

class SparseMdp

MDP in sparse representation

apply_scheduler()

apply scheduler

nondeterministic_choice_indices
class SparseModelAction

Action for state in sparse model

id

Id

transitions

Get transitions

class SparseModelActions

Actions for state in sparse model

class SparseModelState

State in sparse model

actions

Get actions

id

Id

labels

Labels

class SparseModelStates

States in sparse model

class SparseParametricCtmc

pCTMC in sparse representation

class SparseParametricDtmc

pDTMC in sparse representation

class SparseParametricMA

pMA in sparse representation

class SparseParametricMdp

pMDP in sparse representation

apply_scheduler()

apply scheduler

nondeterministic_choice_indices
class SparseParametricModelAction

Action for state in sparse parametric model

id

Id

transitions

Get transitions

class SparseParametricModelActions

Actions for state in sparse parametric model

class SparseParametricModelState

State in sparse parametric model

actions

Get actions

id

Id

labels

Labels

class SparseParametricModelStates

States in sparse parametric model

class SparseParametricRewardModel

Reward structure for parametric sparse models

get_state_action_reward()
get_state_reward()
has_state_action_rewards
has_state_rewards
has_transition_rewards
reduce_to_state_based_rewards()

Reduce to state-based rewards

state_action_rewards
state_rewards
transition_rewards
class SparsePomdp

POMDP in sparse representation

nr_observations
observations
class SparseRewardModel

Reward structure for sparse models

get_state_action_reward()
get_state_reward()
get_zero_reward_states()

get states where all rewards are zero

has_state_action_rewards
has_state_rewards
has_transition_rewards
reduce_to_state_based_rewards()

Reduce to state-based rewards

state_action_rewards
state_rewards
transition_rewards
class StateFormula

Formula about a state of an automaton

class StateLabeling

Labeling for states

add_label_to_state()

Add label to state

get_labels_of_state()

Get labels of given state

get_states()

Get all states which have the given label

has_state_label()

Check if the given state has the given label

set_states()

Set all states which have the given label

exception StormError(message)

Base class for exceptions in Storm.

class SubsystemBuilderOptions

Options for constructing the subsystem

build_action_mapping
build_kept_actions
build_state_mapping
check_transitions_outside
class SubsystemBuilderReturnTypeDouble

Result of the construction of a subsystem

kept_actions

Actions of the subsystem available in the original system

model

the submodel

new_to_old_action_mapping

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

new_to_old_state_mapping

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

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

is_jani_model

Flag if program is in Jani format

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

class SymbolicQualitativeCheckResult

Symbolic qualitative model checking result

class SymbolicQuantitativeCheckResult

Symbolic quantitative model checking result

class SymbolicSylvanCtmc

CTMC in symbolic representation

class SymbolicSylvanDtmc

DTMC in symbolic representation

class SymbolicSylvanMA

MA in symbolic representation

class SymbolicSylvanMdp

MDP in symbolic representation

class SymbolicSylvanParametricCtmc

pCTMC in symbolic representation

class SymbolicSylvanParametricDtmc

pDTMC in symbolic representation

class SymbolicSylvanParametricMA

pMA in symbolic representation

class SymbolicSylvanParametricMdp

pMDP in symbolic representation

class SymbolicSylvanParametricRewardModel

Reward structure for parametric symbolic models

has_state_action_rewards
has_state_rewards
has_transition_rewards
class SymbolicSylvanRewardModel

Reward structure for symbolic models

has_state_action_rewards
has_state_rewards
has_transition_rewards
class TimeOperator

The time operator

class UnaryBooleanStateFormula

Unary boolean state formula

class UnaryPathFormula

Path formula with one operand

subformula

the subformula

class UnaryStateFormula

State formula with one operand

subformula

the subformula

class UntilFormula

Path Formula for unbounded until

class Variable
id
is_no_variable
name
rank
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)

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

Parameters:file (String) – DRN file containing the model.
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)

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

Parameters:file (String) – DRN file containing the model.
Returns:Parametric model in sparse representation.
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_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

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

eliminate_reward_accumulations()

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

Export parametric model in DRN format

export_to_drn(model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<double> >, file: str) → None

Export model in DRN format

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

parse_jani_model(path: str) → Tuple[storm::jani::Model, Dict[str, 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(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

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

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.

prob01max_states(model, eventually_formula)
prob01min_states(model, eventually_formula)
topological_sort(model, forward=True, initial=[])
Parameters:
  • model
  • forward
Returns:

transform_to_sparse_model(model)

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