PrismProgram¶

class PrismProgram¶

Bases: pybind11_object

A Prism Program

property constants¶: Get Program Constants

define_undefined_constants( self: stormpy.io.PrismProgram, constant_definitions, ) → stormpy.io.PrismProgram¶: Define constants

property expression_manager¶: Get the expression manager for expressions in this program

flatten_modules( self: stormpy.io.PrismProgram, smt_factory=None, ) → stormpy.io.PrismProgram¶: Put program into a single module

get_action_name( self: stormpy.io.PrismProgram, action_index: SupportsInt | SupportsIndex, ) → str¶: Get the action name for a given action index

get_all_expression_variables( self: stormpy.io.PrismProgram, include_constants: bool = True, )¶: Get all expression variables (and constants) used by the program

get_constant(self: stormpy.io.PrismProgram, name: str)¶: Requires that the program has a constant with this name

get_label_expression(self: stormpy.io.PrismProgram, label: str)¶: Get the expression of the given label.

get_module(self: stormpy.io.PrismProgram, module_name: str)¶

get_module_indices_by_action_index( self: stormpy.io.PrismProgram, action_index: SupportsInt | SupportsIndex, ) → set[int]¶: get all modules that have a particular action index

get_synchronizing_action_indices(self: stormpy.io.PrismProgram) → set[int]¶: Get the synchronizing action indices

get_undefined_constants(self: stormpy.io.PrismProgram)¶: Collect the undefined constants

property global_boolean_variables¶: Retrieves the global boolean variables of the program

property global_integer_variables¶: Retrieves the global integer variables of the program

has_constant(self: stormpy.io.PrismProgram, name: str) → bool¶

property has_initial_states_expression¶: Is an initial states expression given.

has_label(self: stormpy.io.PrismProgram, name: str) → bool¶

has_reward_model(self: stormpy.io.PrismProgram, name: str) → bool¶: Is a reward model with the specified name defined?

property has_undefined_constants¶: Flag if program has undefined constants

property initial_states_expression¶: Get the initial states expression, or none, if none exists

property is_deterministic_model¶: Does the program describe a deterministic model?

label_unlabelled_commands( self: stormpy.io.PrismProgram, name_suggestions: collections.abc.Mapping[SupportsInt | SupportsIndex, str], ) → stormpy.io.PrismProgram¶: Label unlabelled commands

property labels¶: Get all labels in the program

property model_type¶: Model type

property modules¶: Modules in the program

property nr_modules¶: Number of modules

property number_of_unlabeled_commands¶: Gets the number of commands that are not labelled

replace_constant_by_variable( self: stormpy.io.PrismProgram, constant, lower_bound, upper_bound, observable: bool = True, ) → stormpy.io.PrismProgram¶: Operation to take a constant and make it into a global variable (ranging from lower to upper bound).

replace_variable_initialization_by_init_expression( self: stormpy.io.PrismProgram, ) → stormpy.io.PrismProgram¶: Replaces initializations from the individual variables to a init expression.

restrict_commands(self: stormpy.io.PrismProgram, arg0) → stormpy.io.PrismProgram¶: Restrict commands

property reward_models¶: The defined reward models

simplify(self: stormpy.io.PrismProgram) → stormpy.io.PrismProgram¶: Simplify

substitute_constants(self: stormpy.io.PrismProgram) → stormpy.io.PrismProgram¶: Substitute constants within program

substitute_formulas(self: stormpy.io.PrismProgram) → stormpy.io.PrismProgram¶: Substitute formulas within program

substitute_non_standard_predicates( self: stormpy.io.PrismProgram, ) → stormpy.io.PrismProgram¶: Remove nonstandard predicates from the prism program

to_jani(properties, all_variables_global: bool = True, suffix: str = '')¶

to_jani(all_variables_global: bool = True, suffix: str = '')

Transform to Jani program

Convert the program to a JANI model

property undefined_constants_are_graph_preserving¶: Flag if the undefined constants do not change the graph structure

update_initial_states_expression(self: stormpy.io.PrismProgram, new_expression) → None¶: Replace initial expression. Can only be called if initial expression exists.

used_constants(self: stormpy.io.PrismProgram)¶: Compute Used Constants

property variables¶: Retrieves all expression variables (including constants) of the program