JaniModel¶

class JaniModel(self: stormpy.io.JaniModel, other_model: stormpy.io.JaniModel)¶

Bases: pybind11_object

A Jani Model

add_automaton(self: stormpy.io.JaniModel, automaton) → int¶: add an automaton (with a unique name)

add_constant(self: stormpy.io.JaniModel, constant) → None¶: adds constant to model

property automata¶: get automata

check_valid(self: stormpy.io.JaniModel) → None¶: Some basic checks to ensure validity

property constants¶: get constants

static decode_automaton_and_edge_index( arg0: SupportsInt | SupportsIndex, ) → tuple[int, int]¶: get edge and automaton from edge/automaton index

define_undefined_constants( self: stormpy.io.JaniModel, constant_definitions, ) → stormpy.io.JaniModel¶: define constants with a mapping from the corresponding expression variables to expressions

static encode_automaton_and_edge_index( arg0: SupportsInt | SupportsIndex, arg1: SupportsInt | SupportsIndex, ) → int¶: get edge/automaton-index

property expression_manager¶: get expression manager

finalize(self: stormpy.io.JaniModel) → None¶: finalizes the model. After this action, be careful changing the data structure.

flatten_composition( self: stormpy.io.JaniModel, smt_solver_factory=None, ) → stormpy.io.JaniModel¶

get_automaton(self: stormpy.io.JaniModel, name: str)¶

get_automaton_index(self: stormpy.io.JaniModel, name: str) → int¶: get index for automaton name

get_constant(self: stormpy.io.JaniModel, name: str)¶: get constant by name

property global_variables¶: get global variables

has_standard_composition(self: stormpy.io.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_jani_compliant(self: stormpy.io.JaniModel) → None¶: make standard JANI compliant

property model_type¶: Model type

property name¶: model name

remove_constant(self: stormpy.io.JaniModel, constant_name: str) → None¶: remove a constant. Make sure the constant does not appear in the model.

replace_automaton( self: stormpy.io.JaniModel, index: SupportsInt | SupportsIndex, new_automaton, ) → None¶: replace automaton at index

restrict_edges(self: stormpy.io.JaniModel, edge_set) → stormpy.io.JaniModel¶: restrict model to edges given by set

set_model_type(self: stormpy.io.JaniModel, arg0) → None¶: Sets (only) the model type

set_standard_system_composition(self: stormpy.io.JaniModel) → None¶: sets the composition to the standard composition

substitute_constants(self: stormpy.io.JaniModel) → stormpy.io.JaniModel¶: substitute constants

substitute_functions(self: stormpy.io.JaniModel) → None¶: substitute functions

to_dot(self: stormpy.io.JaniModel) → str¶

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