Stormpy.gspn

class GSPN

Generalized Stochastic Petri Net

export_gspn_pnml_file(self: stormpy.gspn.gspn.GSPN, filepath: str) → None

Export GSPN to PNML file

export_gspn_pnpro_file(self: stormpy.gspn.gspn.GSPN, filepath: str) → None

Export GSPN to PNPRO file

get_immediate_transition(self: stormpy.gspn.gspn.GSPN, name: str) → storm::gspn::ImmediateTransition<double>

Returns the immediate transition with the corresponding name

get_immediate_transitions(self: stormpy.gspn.gspn.GSPN) → List[storm::gspn::ImmediateTransition<double>]

Returns the immediate transitions of this GSPN.

Return type

list[stormpy.ImmediateTransition]

get_initial_marking(self: stormpy.gspn.gspn.GSPN, arg0: Dict[int, int], arg1: int) → storm::gspn::Marking

Computes the initial marking of this GSPN

get_name(self: stormpy.gspn.gspn.GSPN) → str

Get name of GSPN

get_number_of_immediate_transitions(self: stormpy.gspn.gspn.GSPN) → int

Get the number of immediate transitions in this GSPN

get_number_of_places(self: stormpy.gspn.gspn.GSPN) → int

Get the number of places in this GSPN

get_number_of_timed_transitions(self: stormpy.gspn.gspn.GSPN) → int

Get the number of timed transitions in this GSPN

get_partitions(self: stormpy.gspn.gspn.GSPN) → List[storm::gspn::TransitionPartition]

Get the partitions of this GSPN

get_place(*args, **kwargs)

Overloaded function.

1. get_place(self: stormpy.gspn.gspn.GSPN, id: int) -> storm::gspn::Place

   Returns the place with the corresponding id.

   param uint64_t id

   The ID of the place.

   rtype

   stormpy.Place

2. get_place(self: stormpy.gspn.gspn.GSPN, name: str) -> storm::gspn::Place

get_places(self: stormpy.gspn.gspn.GSPN) → List[storm::gspn::Place]

Returns a vector of the places of this GSPN.

Return type

list[stormpy.Place]

get_timed_transition(self: stormpy.gspn.gspn.GSPN, name: str) → storm::gspn::TimedTransition<double>

Returns the timed transition with the corresponding name

get_timed_transitions(self: stormpy.gspn.gspn.GSPN) → List[storm::gspn::TimedTransition<double>]

Returns a vector of the timed transitions of this GSPN.

Return type

list[stormpy.TimedTransition]

get_transition(self: stormpy.gspn.gspn.GSPN, name: str) → storm::gspn::Transition

Returns the transition with the corresponding name

static immediate_transition_id_to_transition_id(arg0: int) → int

is_valid(self: stormpy.gspn.gspn.GSPN) → bool

Perform some checks

set_name(self: stormpy.gspn.gspn.GSPN, arg0: str) → None

Set name of GSPN

static timed_transition_id_to_transition_id(arg0: int) → int

static transition_id_to_immediate_transition_id(arg0: int) → int

static transition_id_to_timed_transition_id(arg0: int) → int

class GSPNBuilder

Generalized Stochastic Petri Net Builder

add_immediate_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int = 0, weight: float = 0, name: str = '') → int

Add an immediate transition to the GSPN

add_inhibition_arc(*args, **kwargs)

Overloaded function.

1. add_inhibition_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int = 1) -> None

   Add an new inhibition arc from a place to a transition.

   param from

   The ID or name of the place from which the arc is originating.

   type from

   uint_64_t or str

   param to

   The ID or name of the transition to which the arc goes to.

   type to

   uint_64_t or str

   param uint64_t multiplicity

   The multiplicity of the arc, default = 1.

2. add_inhibition_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int = 1) -> None

add_input_arc(*args, **kwargs)

Overloaded function.

1. add_input_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int = 1) -> None

   Add a new input arc from a place to a transition

   param from

   The ID or name of the place from which the arc is originating.

   type from

   uint_64_t or str

   param uint_64_t to

   The ID or name of the transition to which the arc goes to.

   type from

   uint_64_t or str

   param uint64_t multiplicity

   The multiplicity of the arc, default = 1.

2. add_input_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int = 1) -> None

add_normal_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int = 1) → None

Add an arc from a named element to a named element. Can be both input or output arc, but not an inhibition arc. Convenience function for textual format parsers.

Parameters

• from (str) – Source element in the GSPN from where this arc starts.

• to (str) – Target element in the GSPN where this arc ends.

• multiplicity (uint64_t) – Multiplicity of the arc, default = 1.

add_output_arc(*args, **kwargs)

Overloaded function.

1. add_output_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: int, to: int, multiplicity: int = 1) -> None

   Add an new output arc from a transition to a place.

   param from

   The ID or name of the transition from which the arc is originating.

   type from

   uint_64_t or str

   param to

   The ID or name of the place to which the arc goes to.

   type to

   uint_64_t or str

   param uint64_t multiplicity

   The multiplicity of the arc, default = 1.

2. add_output_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int) -> None

add_place(self: stormpy.gspn.gspn.GSPNBuilder, capacity: Optional[int] = 1, initial_tokens: int = 0, name: str = '') → int

Add a place to the GSPN

add_timed_transition(*args, **kwargs)

Overloaded function.

1. add_timed_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int, rate: float, name: str = ‘’) -> int

Add a timed transition to the GSPN

2. add_timed_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int, rate: float, num_servers: Optional[int], name: str = ‘’) -> int

build_gspn(self: stormpy.gspn.gspn.GSPNBuilder, expression_manager: stormpy.storage.storage.ExpressionManager = None, constants_substitution: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression] = {}) → storm::gspn::GSPN

Construct GSPN

set_name(self: stormpy.gspn.gspn.GSPNBuilder, name: str) → None

Set name of GSPN

set_place_layout_info(self: stormpy.gspn.gspn.GSPNBuilder, place_id: int, layout_info: storm::gspn::LayoutInfo) → None

Set place layout information.

Parameters

• id (uint64_t) – The ID of the place.

• layout_info (stormpy.LayoutInfo) – The layout information.

set_transition_layout_info(self: stormpy.gspn.gspn.GSPNBuilder, transition_id: int, layout_info: storm::gspn::LayoutInfo) → None

Set transition layout information.

Parameters

• id (uint64_t) – The ID of the transition.

• layout_info (stormpy.LayoutInfo) – The layout information.

class GSPNParser

parse(self: stormpy.gspn.gspn.GSPNParser, filename: str, constant_definitions: str = '') → stormpy.gspn.gspn.GSPN

class GSPNToJaniBuilder

build(self: stormpy.gspn.gspn.GSPNToJaniBuilder, automaton_name: str = 'gspn_automaton') → stormpy.storage.storage.JaniModel

Build Jani model from GSPN

create_deadlock_properties(self: stormpy.gspn.gspn.GSPNToJaniBuilder, jani_model: stormpy.storage.storage.JaniModel) → List[stormpy.core.Property]

Create standard properties for deadlocks

class ImmediateTransition

ImmediateTransition in a GSPN

get_weight(self: stormpy.gspn.gspn.ImmediateTransition) → float

Get weight of this transition

no_weight_attached(self: stormpy.gspn.gspn.ImmediateTransition) → bool

True iff no weight is attached

set_weight(self: stormpy.gspn.gspn.ImmediateTransition, weight: float) → None

Set weight of this transition

class LayoutInfo

property rotation

property x

property y

class Place

Place in a GSPN

get_capacity(self: stormpy.gspn.gspn.Place) → int

Get the capacity of tokens of this place

get_id(self: stormpy.gspn.gspn.Place) → int

Get the id of this place

get_name(self: stormpy.gspn.gspn.Place) → str

Get name of this place

get_number_of_initial_tokens(self: stormpy.gspn.gspn.Place) → int

Get the number of initial tokens of this place

has_restricted_capacity(self: stormpy.gspn.gspn.Place) → bool

Is capacity of this place restricted

set_capacity(self: stormpy.gspn.gspn.Place, cap: Optional[int]) → None

Set the capacity of tokens of this place

set_name(self: stormpy.gspn.gspn.Place, name: str) → None

Set name of this place

set_number_of_initial_tokens(self: stormpy.gspn.gspn.Place, tokens: int) → None

Set the number of initial tokens of this place

class TimedTransition

TimedTransition in a GSPN

get_number_of_servers(self: stormpy.gspn.gspn.TimedTransition) → int

Get number of servers

get_rate(self: stormpy.gspn.gspn.TimedTransition) → float

Get rate of this transition

has_infinite_server_semantics(self: stormpy.gspn.gspn.TimedTransition) → bool

Get semantics of this transition

has_k_server_semantics(self: stormpy.gspn.gspn.TimedTransition) → bool

Get semantics of this transition

has_single_server_semantics(self: stormpy.gspn.gspn.TimedTransition) → bool

Get semantics of this transition

set_infinite_server_semantics(self: stormpy.gspn.gspn.TimedTransition) → None

Set semantics of this transition

set_k_server_semantics(self: stormpy.gspn.gspn.TimedTransition, k: int) → None

Set semantics of this transition

set_rate(self: stormpy.gspn.gspn.TimedTransition, rate: float) → None

Set rate of this transition

set_single_server_semantics(self: stormpy.gspn.gspn.TimedTransition) → None

Set semantics of this transition

class Transition

Transition in a GSPN

exists_inhibition_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Check whether the given place is connected to this transition via an inhibition arc.

exists_input_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Check whether the given place is connected to this transition via an input arc.

exists_output_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Check whether the given place is connected to this transition via an output arc.

fire(self: stormpy.gspn.gspn.Transition, marking: storm::gspn::Marking) → storm::gspn::Marking

Fire the transition if possible.

get_id(self: stormpy.gspn.gspn.Transition) → int

Get id of this transition

get_inhibition_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → int

Returns the corresponding multiplicity.

get_inhibition_places(self: stormpy.gspn.gspn.Transition) → Dict[int, int]

get_input_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → int

Returns the corresponding multiplicity.

get_input_places(self: stormpy.gspn.gspn.Transition) → Dict[int, int]

get_name(self: stormpy.gspn.gspn.Transition) → str

Get name of this transition

get_output_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → int

Returns the corresponding multiplicity.

get_output_places(self: stormpy.gspn.gspn.Transition) → Dict[int, int]

get_priority(self: stormpy.gspn.gspn.Transition) → int

Get priority of this transition

is_enabled(self: stormpy.gspn.gspn.Transition, marking: storm::gspn::Marking) → bool

Check if the given marking enables the transition.

remove_inhibition_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Remove an inhibition arc connected to a given place.

remove_input_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Remove an input arc connected to a given place.

remove_output_arc(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place) → bool

Remove an output arc connected to a given place.

set_inhibition_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place, multiplicity: int) → None

Set the multiplicity of the inhibition arc originating from the place.

set_input_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place, multiplicity: int) → None

Set the multiplicity of the input arc originating from the place.

set_name(self: stormpy.gspn.gspn.Transition, name: str) → None

Set name of this transition

set_output_arc_multiplicity(self: stormpy.gspn.gspn.Transition, place: stormpy.gspn.gspn.Place, multiplicity: int) → None

Set the multiplicity of the output arc going to the place.

set_priority(self: stormpy.gspn.gspn.Transition, priority: int) → None

Set priority of this transition

class TransitionPartition

nr_transitions(self: stormpy.gspn.gspn.TransitionPartition) → int

Get number of transitions

property priority

property transitions