Interactive version: .

Generalized Stochastic Petri Nets

Loading GSPNs

01-gspns.py

Generalized stochastic Petri nets can be given either in the PNPRO format or in the PNML format. We start by loading a GSPN stored in the PNML format:

import stormpy
import stormpy.gspn
import stormpy.examples
import stormpy.examples.files

import_path = stormpy.examples.files.gspn_pnml_simple
gspn_parser = stormpy.gspn.GSPNParser()
gspn = gspn_parser.parse(import_path)

After loading, we can display some properties of the GSPN:

print("Name of GSPN: {}.".format(gspn.get_name()))

Name of GSPN: simple_gspn.

print("Number of places: {}.".format(gspn.get_number_of_places()))

Number of places: 4.

print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))

Number of immediate transitions: 3.

print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))

Number of timed transitions: 2.

Building GSPNs

02-gspns.py

In the following, we describe how to construct GSPNs via the GSPNBuilder. First, we create an instance of the GSPNBuilder and set the name of the GSPN:

builder = stormpy.gspn.GSPNBuilder()
builder.set_name("my_gspn")

In the next step, we add an immediate transition to the GSPN. Additionally, we define the position of the transition by setting its layout information:

it_1 = builder.add_immediate_transition(1, 0.0, "it_1")
it_layout = stormpy.gspn.LayoutInfo(1.5, 2.0)
builder.set_transition_layout_info(it_1, it_layout)

We add a timed transition and set its layout information:

tt_1 = builder.add_timed_transition(0, 0.4, "tt_1")
tt_layout = stormpy.gspn.LayoutInfo(12.5, 2.0)
builder.set_transition_layout_info(tt_1, tt_layout)

Next, we add two places to the GSPN and set their layouts:

place_1 = builder.add_place(1, 1, "place_1")
p1_layout = stormpy.gspn.LayoutInfo(6.5, 2.0)
builder.set_place_layout_info(place_1, p1_layout)

place_2 = builder.add_place(1, 0, "place_2")
p2_layout = stormpy.gspn.LayoutInfo(18.5, 2.0)
builder.set_place_layout_info(place_2, p2_layout)

Places and transitions can be linked by input, output and inhibition arcs. We add the arcs of our GSPN as follows:

builder.add_output_arc(it_1, place_1)
builder.add_inhibition_arc(place_1, it_1)
builder.add_input_arc(place_1, tt_1)
builder.add_output_arc(tt_1, place_2)

We can now build the GSPN:

gspn = builder.build_gspn()

After building, we export the GSPN. GSPNs can be saved in the PNPRO format via export_gspn_pnpro_file(path) and in the PNML format via export_gspn_pnml_file(path). We export the GSPN into the PNPRO format:

export_path = stormpy.examples.files.gspn_pnpro_simple
gspn.export_gspn_pnpro_file(export_path)

Write to file /opt/stormpy/lib/stormpy/examples/files/gspn/gspn_simple.pnpro.