added content to the gspn documentation

6 years ago · c014234e77
8 changed files with 292 additions and 59 deletions
--- 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 <link to github: 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 <link to github: 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)

--- 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__':
--- a/examples/gspns/02-gspns.py
+++ 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()
+
--- 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)"""
--- a/lib/stormpy/examples/files/gspn/gspn_simple.pnml
+++ b/lib/stormpy/examples/files/gspn/gspn_simple.pnml
@ -0,0 +1,130 @@
+<pnml>
+  <net id="simple_gspn">
+    <place id="place_1">
+      <initialMarking>
+        <value>Default,1</value>
+      </initialMarking>
+      <capacity>
+        <value>Default,1</value>
+      </capacity>
+    </place>
+    <place id="place_2">
+      <initialMarking>
+        <value>Default,0</value>
+      </initialMarking>
+      <capacity>
+        <value>Default,1</value>
+      </capacity>
+    </place>
+    <place id="place_3">
+      <initialMarking>
+        <value>Default,0</value>
+      </initialMarking>
+      <capacity>
+        <value>Default,1</value>
+      </capacity>
+    </place>
+    <place id="place_4">
+      <initialMarking>
+        <value>Default,0</value>
+      </initialMarking>
+      <capacity>
+        <value>Default,1</value>
+      </capacity>
+    </place>
+    <transition id="it_1">
+      <rate>
+        <value>1</value>
+      </rate>
+      <timed>
+        <value>false</value>
+      </timed>
+    </transition>
+    <transition id="it_2">
+      <rate>
+        <value>1</value>
+      </rate>
+      <timed>
+        <value>false</value>
+      </timed>
+    </transition>
+    <transition id="it_3">
+      <rate>
+        <value>1</value>
+      </rate>
+      <timed>
+        <value>false</value>
+      </timed>
+    </transition>
+    <transition id="tt_1">
+      <rate>
+        <value>0.4</value>
+      </rate>
+      <timed>
+        <value>true</value>
+      </timed>
+    </transition>
+    <transition id="tt_2">
+      <rate>
+        <value>0.4</value>
+      </rate>
+      <timed>
+        <value>true</value>
+      </timed>
+    </transition>
+    <arc id="arc0" source="place_1" target="it_1" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="inhibition" />
+    </arc>
+    <arc id="arc1" source="it_1" target="place_1" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc2" source="place_2" target="it_2" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc3" source="it_2" target="place_3" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc4" source="place_4" target="it_3" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc5" source="place_1" target="tt_1" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc6" source="tt_1" target="place_2" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc7" source="place_3" target="tt_2" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+    <arc id="arc8" source="tt_2" target="place_4" >
+      <inscription>
+        <value>Default,1</value>
+      </inscription>
+      <type value="normal" />
+    </arc>
+  </net>
+</pnml>
--- a/lib/stormpy/examples/files/gspn/gspn_simple.pnpro
+++ b/lib/stormpy/examples/files/gspn/gspn_simple.pnpro
@ -1,16 +1,16 @@
 <project name="storm-export" version="121">
-  <gspn name="gspn" >
+  <gspn name="my_gspn" >
    <nodes>
-      <place marking="1" name ="place_0" x="6.5" y="1.5" />
-      <place marking="0" name ="place_1" x="18.5" y="1.5" />
-      <transition name="tt_0" type="EXP" nservers="1" delay="0.4000000000" x="12.50000000" y="1.500000000" />
-      <transition name="it_0" type="IMM" priority="1" weight="1.000000000" x="1.500000000" y="1.500000000" />
+      <place marking="1" name ="place_1" x="6.5" y="2" />
+      <place marking="0" name ="place_2" x="18.5" y="2" />
+      <transition name="tt_1" type="EXP" nservers="1" delay="0.4000000000" x="12.50000000" y="2.000000000" />
+      <transition name="it_1" type="IMM" priority="1" weight="1.000000000" x="1.500000000" y="2.000000000" />
    </nodes>
    <edges>
-      <arc head="tt_0" tail="place_0" kind="INPUT" mult="1" />
-      <arc head="place_1" tail="tt_0" kind="OUTPUT" mult="1" />
-      <arc head="it_0" tail="place_0" kind="INHIBITOR" mult="1" />
-      <arc head="place_0" tail="it_0" kind="OUTPUT" mult="1" />
+      <arc head="tt_1" tail="place_1" kind="INPUT" mult="1" />
+      <arc head="place_2" tail="tt_1" kind="OUTPUT" mult="1" />
+      <arc head="it_1" tail="place_1" kind="INHIBITOR" mult="1" />
+      <arc head="place_1" tail="it_1" kind="OUTPUT" mult="1" />
    </edges>
  </gspn>
 </project>
--- 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_<LayoutInfo>(m, "LayoutInfo")
        .def(py::init<>())
--- 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