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.
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
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
-
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
-
timed_transition_id_to_transition_id
(arg0: int) → int¶
-
transition_id_to_immediate_transition_id
(arg0: int) → int¶
-
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.
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.
add_inhibition_arc(self: stormpy.gspn.gspn.GSPNBuilder, from: str, to: str, multiplicity: int=1) -> None
-
add_input_arc
(*args, **kwargs)¶ Overloaded function.
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.
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.
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.
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.
add_timed_transition(self: stormpy.gspn.gspn.GSPNBuilder, priority: int, rate: float, name: str=’’) -> int
Add a timed transition to the GSPN
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
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
-