diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst
index 2726653..9094432 100644
--- a/doc/source/doc/gspns.rst
+++ b/doc/source/doc/gspns.rst
@@ -1,9 +1,88 @@
-*******************
+**********************************
Generalized Stochastic Petri Nets
-*******************
+**********************************
+Loading GSPNs
+==============
+
+..
+ .. seealso:: `01-gspn.py `_
+..
+
+
+Generalized stochastic Petri nets can be given in 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
-=============
-TODO
+=============================
+..
+ todo .. seealso:: `02-gspn.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("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)
+
+Add 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 output, inhibition or input arcs::
+
+ >>> 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 can 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)
diff --git a/examples/gspns/01-gspns.py b/examples/gspns/01-gspns.py
index 2b2f273..9fcb32a 100644
--- a/examples/gspns/01-gspns.py
+++ b/examples/gspns/01-gspns.py
@@ -6,50 +6,15 @@ import stormpy.examples.files
def example_gspns_01():
- # construct gspn with gspn builder
- builder = stormpy.gspn.GSPNBuilder()
- builder.set_name("gspn")
-
- it_0 = builder.add_immediate_transition(1, 0.0, "it_0")
- it_layout = stormpy.gspn.LayoutInfo(1.5, 1.5)
- builder.set_transition_layout_info(it_0, it_layout)
-
- tt_0 = builder.add_timed_transition(0, 0.4, "tt_0")
- tt_layout = stormpy.gspn.LayoutInfo(12.5, 1.5)
- builder.set_transition_layout_info(tt_0, tt_layout)
-
- place_0 = builder.add_place(1, 1, "place_0")
- p0_layout = stormpy.gspn.LayoutInfo(6.5, 1.5)
- builder.set_place_layout_info(place_0, p0_layout)
-
- place_1 = builder.add_place(1, 0, "place_1")
- p1_layout = stormpy.gspn.LayoutInfo(18.5, 1.5)
- builder.set_place_layout_info(place_1, p1_layout)
-
- # arcs
- builder.add_output_arc(it_0, place_0)
- builder.add_inhibition_arc(place_0, it_0)
- builder.add_input_arc(place_0, tt_0)
- builder.add_output_arc(tt_0, place_1)
-
- # build gspn
- gspn = builder.build_gspn()
- print("GSPN with {} places, {} immediate transitions and {} timed transitions.".format(gspn.get_number_of_places(),
- gspn.get_number_of_immediate_transitions(),
- gspn.get_number_of_timed_transitions()))
-
- path = stormpy.examples.files.gspn_pnpro_simple
-
- # export gspn to pnpro format
- gspn.export_gspn_pnpro_file(path)
-
- # import gspn
+ # Load a GSPN from file (PNML format)
+ import_path = stormpy.examples.files.gspn_pnml_simple
gspn_parser = stormpy.gspn.GSPNParser()
- gspn_import = gspn_parser.parse(path)
+ gspn = gspn_parser.parse(import_path)
- print("GSPN with {} places, {} immediate transitions and {} timed transitions.".format(
- gspn_import.get_number_of_places(), gspn.get_number_of_immediate_transitions(),
- gspn.get_number_of_timed_transitions()))
+ print("Name of GSPN: {}.".format(gspn.get_name()))
+ print("Number of places: {}.".format(gspn.get_number_of_places()))
+ print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))
+ print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))
if __name__ == '__main__':
diff --git a/examples/gspns/02-gspns.py b/examples/gspns/02-gspns.py
new file mode 100644
index 0000000..f9a49ad
--- /dev/null
+++ b/examples/gspns/02-gspns.py
@@ -0,0 +1,53 @@
+import stormpy
+import stormpy.gspn
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+def example_gspns_02():
+ # Use GSPNBuilder to construct a GSPN
+ builder = stormpy.gspn.GSPNBuilder()
+ builder.set_name("my_gspn")
+
+ # Add immediate transition
+ 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)
+
+ # Add timed transition
+ 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)
+
+ # Add places
+ 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)
+
+ # Link places and transitions by arcs
+ 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)
+
+ # Build GSPN
+ gspn = builder.build_gspn()
+
+ print("Name of GSPN: {}.".format(gspn.get_name()))
+ print("Number of places: {}.".format(gspn.get_number_of_places()))
+ print("Number of immediate transitions: {}.".format(gspn.get_number_of_immediate_transitions()))
+ print("Number of timed transitions: {}.".format(gspn.get_number_of_timed_transitions()))
+
+ # Export to file (PNPRO format)
+ export_path = stormpy.examples.files.gspn_pnpro_simple
+ gspn.export_gspn_pnpro_file(export_path)
+
+
+if __name__ == '__main__':
+ example_gspns_02()
+
diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py
index 6fead05..59e1f00 100644
--- a/lib/stormpy/examples/files.py
+++ b/lib/stormpy/examples/files.py
@@ -43,3 +43,5 @@ dft_json_and = _path("dft", "and.json")
"""DFT example for AND gate (JSON format)"""
gspn_pnpro_simple = _path("gspn", "gspn_simple.pnpro")
"""GSPN example (PNPRO format)"""
+gspn_pnml_simple = _path("gspn", "gspn_simple.pnml")
+"""GSPN example (PNML format)"""
diff --git a/lib/stormpy/examples/files/gspn/gspn_simple.pnml b/lib/stormpy/examples/files/gspn/gspn_simple.pnml
new file mode 100644
index 0000000..cc79377
--- /dev/null
+++ b/lib/stormpy/examples/files/gspn/gspn_simple.pnml
@@ -0,0 +1,130 @@
+
+
+
+
+ Default,1
+
+
+ Default,1
+
+
+
+
+ Default,0
+
+
+ Default,1
+
+
+
+
+ Default,0
+
+
+ Default,1
+
+
+
+
+ Default,0
+
+
+ Default,1
+
+
+
+
+ 1
+
+
+ false
+
+
+
+
+ 1
+
+
+ false
+
+
+
+
+ 1
+
+
+ false
+
+
+
+
+ 0.4
+
+
+ true
+
+
+
+
+ 0.4
+
+
+ true
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
+ Default,1
+
+
+
+
+
diff --git a/lib/stormpy/examples/files/gspn/gspn_simple.pnpro b/lib/stormpy/examples/files/gspn/gspn_simple.pnpro
index 6f5008e..5c7140e 100644
--- a/lib/stormpy/examples/files/gspn/gspn_simple.pnpro
+++ b/lib/stormpy/examples/files/gspn/gspn_simple.pnpro
@@ -1,16 +1,16 @@
-
+
-
-
-
-
+
+
+
+
-
-
-
-
+
+
+
+
diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp
index 5e5c36e..176ca22 100644
--- a/src/gspn/gspn.cpp
+++ b/src/gspn/gspn.cpp
@@ -91,16 +91,19 @@ void define_gspn(py::module& m) {
.def("get_immediate_transitions", &GSPN::getImmediateTransitions, "Get the immediate transitions of this GSPN")
.def("get_initial_marking", &GSPN::getInitialMarking, "Computes the initial marking of this GSPN")
- .def_static("timed_transition_id_to_transition_id", &GSPN::timedTransitionIdToTransitionId)
- .def_static("immediate_transition_id_to_transition_id", &GSPN::immediateTransitionIdToTransitionId)
- .def_static("transition_id_to_timed_transition_id", &GSPN::transitionIdToTimedTransitionId)
- .def_static("transition_id_to_immediate_transition_id", &GSPN::transitionIdToImmediateTransitionId)
+ .def("is_valid", &GSPN::isValid, "Perform some checks")
// GSPN export
.def("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnpro"); }, "filepath"_a, "Export GSPN to PNPRO file")
.def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnml"); }, "filepath"_a, "Export GSPN to PNML file")
+
+ .def_static("timed_transition_id_to_transition_id", &GSPN::timedTransitionIdToTransitionId)
+ .def_static("immediate_transition_id_to_transition_id", &GSPN::immediateTransitionIdToTransitionId)
+ .def_static("transition_id_to_timed_transition_id", &GSPN::transitionIdToTimedTransitionId)
+ .def_static("transition_id_to_immediate_transition_id", &GSPN::transitionIdToImmediateTransitionId)
;
+
// LayoutInfo class
py::class_(m, "LayoutInfo")
.def(py::init<>())
diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py
index d94f005..c18a9a1 100644
--- a/tests/gspn/test_gspn.py
+++ b/tests/gspn/test_gspn.py
@@ -123,6 +123,7 @@ class TestGSPNBuilder:
gspn = builder.build_gspn()
assert gspn.get_name() == gspn_name
+ assert gspn.is_valid()
assert gspn.get_number_of_immediate_transitions() == 2
assert gspn.get_number_of_timed_transitions() == 2
assert gspn.get_number_of_places() == 4