Added structure for GSPN module

CMakeLists.txt

@@ -35,14 +35,17 @@ stormpy_module(logic)
 stormpy_module(storage)
 stormpy_module(utility)
 
-if(HAVE_STORM_PARS)
-    stormpy_module(pars storm-pars "${storm-pars_INCLUDE_DIR}")
-endif()
-
+# Optional modules
 if(HAVE_STORM_DFT)
     stormpy_module(dft storm-dft "${storm-dft_INCLUDE_DIR}")
 endif()
-
+if(HAVE_STORM_GSPN)
+    stormpy_module(gspn storm-gspn "${storm-gspn_INCLUDE_DIR}")
+endif()
+if(HAVE_STORM_PARS)
+    stormpy_module(pars storm-pars "${storm-pars_INCLUDE_DIR}")
+endif()
 if(HAVE_STORM_POMDP)
     stormpy_module(pomdp storm-pomdp "${storm-pomdp_INCLUDE_DIR}")
 endif()
+

cmake/CMakeLists.txt

@@ -8,13 +8,6 @@ set(STORM_DIR ${storm_DIR})
 set(STORM_VERSION ${storm_VERSION})
 set(STORM_LIBS ${storm_LIBRARIES})
 
-# Check for storm-pars
-find_library(STORM_PARS NAMES storm-pars HINTS "${storm_DIR}/lib/")
-if(STORM_PARS)
-    set(HAVE_STORM_PARS TRUE)
-else()
-    set(HAVE_STORM_PARS FALSE)
-endif()
 
 # Check for storm-dft
 find_library(STORM_DFT NAMES storm-dft HINTS "${storm_DIR}/lib/")
@@ -24,6 +17,23 @@ else()
     set(HAVE_STORM_DFT FALSE)
 endif()
 
+# Check for storm-gspn
+find_library(STORM_GSPN NAMES storm-gspn HINTS "${storm_DIR}/lib/")
+if(STORM_GSPN)
+    set(HAVE_STORM_GSPN TRUE)
+else()
+    set(HAVE_STORM_GSPN FALSE)
+endif()
+
+# Check for storm-pars
+find_library(STORM_PARS NAMES storm-pars HINTS "${storm_DIR}/lib/")
+if(STORM_PARS)
+    set(HAVE_STORM_PARS TRUE)
+else()
+    set(HAVE_STORM_PARS FALSE)
+endif()
+
+# Check for storm-pompd
 find_library(STORM_POMDP NAMES storm-pomdp HINTS "${storm_DIR}/lib/")
 if(STORM_POMDP)
     set(HAVE_STORM_POMDP TRUE)
@@ -31,10 +41,18 @@ else()
     set(HAVE_STORM_POMDP FALSE)
 endif()
 
-if(HAVE_STORM_PARS)
-    set(HAVE_STORM_PARS_BOOL "True")
+
+# Set variables
+if(STORM_USE_CLN_EA)
+    set(STORM_CLN_EA_BOOL "True")
 else()
-    set(HAVE_STORM_PARS_BOOL "False")
+    set(STORM_CLN_EA_BOOL "False")
+endif()
+
+if(STORM_USE_CLN_RF)
+    set(STORM_CLN_RF_BOOL "True")
+else()
+    set(STORM_CLN_RF_BOOL "False")
 endif()
 
 if(HAVE_STORM_DFT)
@@ -43,22 +61,22 @@ else()
     set(HAVE_STORM_DFT_BOOL "False")
 endif()
 
-if(HAVE_STORM_POMDP)
-    set(HAVE_STORM_POMDP_BOOL "True")
+if(HAVE_STORM_GSPN)
+    set(HAVE_STORM_GSPN_BOOL "True")
 else()
-    set(HAVE_STORM_POMDP_BOOL "False")
+    set(HAVE_STORM_GSPN_BOOL "False")
 endif()
 
-if(STORM_USE_CLN_EA)
-    set(STORM_CLN_EA_BOOL "True")
+if(HAVE_STORM_PARS)
+    set(HAVE_STORM_PARS_BOOL "True")
 else()
-    set(STORM_CLN_EA_BOOL "False")
+    set(HAVE_STORM_PARS_BOOL "False")
 endif()
 
-if(STORM_USE_CLN_RF)
-    set(STORM_CLN_RF_BOOL "True")
+if(HAVE_STORM_POMDP)
+    set(HAVE_STORM_POMDP_BOOL "True")
 else()
-    set(STORM_CLN_RF_BOOL "False")
+    set(HAVE_STORM_POMDP_BOOL "False")
 endif()
 
 configure_file(${CMAKE_CURRENT_SOURCE_DIR}/config.py.in ${CMAKE_CURRENT_BINARY_DIR}/generated/config.py @ONLY)

cmake/config.py.in

@@ -4,6 +4,7 @@ STORM_DIR = "@STORM_DIR@"
 STORM_VERSION = "@STORM_VERSION@"
 STORM_CLN_EA = @STORM_CLN_EA_BOOL@
 STORM_CLN_RF = @STORM_CLN_RF_BOOL@
-HAVE_STORM_PARS = @HAVE_STORM_PARS_BOOL@
 HAVE_STORM_DFT = @HAVE_STORM_DFT_BOOL@
+HAVE_STORM_GSPN = @HAVE_STORM_GSPN_BOOL@
+HAVE_STORM_PARS = @HAVE_STORM_PARS_BOOL@
 HAVE_STORM_POMDP = @HAVE_STORM_POMDP_BOOL@

lib/stormpy/gspn/__init__.py

@@ -0,0 +1,7 @@
+from . import _config
+
+if not _config.storm_with_gspn:
+    raise ImportError("No support for GSPNs was built in Storm.")
+
+from . import gspn
+from .gspn import *

setup.py

@@ -32,6 +32,7 @@ class CMakeBuild(build_ext):
     user_options = build_ext.user_options + [
         ('storm-dir=', None, 'Path to storm root (binary) location'),
         ('disable-dft', None, 'Disable support for DFTs'),
+        ('disable-gspn', None, 'Disable support for GSPNs'),
         ('disable-pars', None, 'Disable support for parametric models'),
         ('disable-pomdp', None, 'Disable support for POMDP analysis'),
         ('debug', None, 'Build in Debug mode'),
@@ -84,6 +85,7 @@ class CMakeBuild(build_ext):
 
         # Check additional support
         use_dft = cmake_conf.HAVE_STORM_DFT and not self.config.get_as_bool("disable_dft")
+        use_gspn = cmake_conf.HAVE_STORM_GSPN and not self.config.get_as_bool("disable_gspn")
         use_pars = cmake_conf.HAVE_STORM_PARS and not self.config.get_as_bool("disable_pars")
         use_pomdp = cmake_conf.HAVE_STORM_POMDP #and not self.config.get_as_bool("disable_pomdp")
 
@@ -93,6 +95,10 @@ class CMakeBuild(build_ext):
             print("Stormpy - Support for DFTs found and included.")
         else:
             print("Stormpy - Warning: No support for DFTs!")
+        if use_gspn:
+            print("Stormpy - Support for GSPNs found and included.")
+        else:
+            print("Stormpy - Warning: No support for GSPNs!")
         if use_pars:
             print("Stormpy - Support for parametric models found and included.")
         else:
@@ -110,6 +116,8 @@ class CMakeBuild(build_ext):
             cmake_args += ['-Dstorm_DIR=' + storm_dir]
         if use_dft:
             cmake_args += ['-DHAVE_STORM_DFT=ON']
+        if use_gspn:
+            cmake_args += ['-DHAVE_STORM_GSPN=ON']
         if use_pars:
             cmake_args += ['-DHAVE_STORM_PARS=ON']
         if use_pomdp:
@@ -146,6 +154,7 @@ class CMakeBuild(build_ext):
                     f.write("FactorizedRationalFunction = pycarl.{}.FactorizedRationalFunction\n".format(rfpackage))
                     f.write("\n")
                     f.write("storm_with_dft = {}\n".format(use_dft))
+                    f.write("storm_with_gspn = {}\n".format(use_gspn))
                     f.write("storm_with_pars = {}\n".format(use_pars))
 
             elif ext.name == "info":
@@ -161,6 +170,13 @@ class CMakeBuild(build_ext):
                 if not use_dft:
                     print("Stormpy - DFT bindings skipped")
                     continue
+            elif ext.name == "gspn":
+                with open(os.path.join(self._extdir(ext.name), ext.subdir, "_config.py"), "w") as f:
+                    f.write("# Generated from setup.py at {}\n".format(datetime.datetime.now()))
+                    f.write("storm_with_gspn = {}".format(use_gspn))
+                if not use_gspn:
+                    print("Stormpy - GSPN bindings skipped")
+                    continue
             elif ext.name == "pars":
                 with open(os.path.join(self._extdir(ext.name), ext.subdir, "_config.py"), "w") as f:
                     f.write("# Generated from setup.py at {}\n".format(datetime.datetime.now()))
@@ -182,6 +198,7 @@ class CMakeBuild(build_ext):
         # Set default values for custom cmdline flags
         self.storm_dir = None
         self.disable_dft = None
+        self.disable_gspn = None
         self.disable_pars = None
         self.disable_pomdp = None
         self.debug = None
@@ -195,6 +212,7 @@ class CMakeBuild(build_ext):
         # Update setup config
         self.config.update("storm_dir", self.storm_dir)
         self.config.update("disable_dft", self.disable_dft)
+        self.config.update("disable_gspn", self.disable_gspn)
         self.config.update("disable_pars", self.disable_pars)
         self.config.update("disable_pomdp", self.disable_pomdp)
         self.config.update("debug", self.debug)
@@ -248,6 +266,7 @@ setup(
                  CMakeExtension('storage', subdir='storage'),
                  CMakeExtension('utility', subdir='utility'),
                  CMakeExtension('dft', subdir='dft'),
+                 CMakeExtension('gspn', subdir='gspn'),
                  CMakeExtension('pars', subdir='pars'),
                  CMakeExtension('pomdp', subdir='pomdp')],
 

setup/config.py

@@ -29,6 +29,7 @@ class SetupConfig:
         return {
             "storm_dir": "",
             "disable_dft": False,
+            "disable_gspn": False,
             "disable_pars": False,
             "debug": False,
             "jobs": str(no_jobs),

src/gspn/common.h

@@ -0,0 +1,2 @@
+#include "src/common.h"
+#include "storm-gspn/api/storm-gspn.h"

src/gspn/gspn.cpp

@@ -0,0 +1,18 @@
+#include "gspn.h"
+#include "src/helpers.h"
+#include "storm-gspn/storage/gspn/GSPN.h"
+#include "storm-gspn/storage/gspn/GspnBuilder.h"
+#include "storm/settings/SettingsManager.h"
+
+
+typedef storm::gspn::GSPN GSPN;
+
+
+void define_gspn(py::module& m) {
+
+    // GSPN class
+    py::class_<GSPN, std::shared_ptr<GSPN>>(m, "GSPN", "Generalized Stochastic Petri Net")
+        .def("name", &GSPN::getName, "Name of GSPN")
+    ;
+
+}

src/gspn/gspn.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "common.h"
+
+void define_gspn(py::module& m);

src/mod_gspn.cpp

@@ -0,0 +1,14 @@
+#include "common.h"
+
+#include "gspn/gspn.h"
+
+PYBIND11_MODULE(gspn, m) {
+    m.doc() = "Support for GSPNs";
+
+#ifdef STORMPY_DISABLE_SIGNATURE_DOC
+    py::options options;
+    options.disable_function_signatures();
+#endif
+
+    define_gspn(m);
+}

tests/configurations.py

@@ -4,7 +4,9 @@ import stormpy._config as config
 
 # Skip not supported functionality
 has_dft = config.storm_with_dft
+has_gspn = config.storm_with_gspn
 has_pars = config.storm_with_pars
 
 dft = pytest.mark.skipif(not has_dft, reason="No support for DFTs")
+gspn = pytest.mark.skipif(not has_gspn, reason="No support for GSPNs")
 pars = pytest.mark.skipif(not has_pars, reason="No support for parametric model checking")

tests/gspn/conftest.py

@@ -0,0 +1,4 @@
+from configurations import has_gspn
+
+if has_gspn:
+    import stormpy.gspn

tests/gspn/test_gspn.py

@@ -0,0 +1,12 @@
+import os
+
+import stormpy
+from helpers.helper import get_example_path
+
+from configurations import gspn
+
+
+@gspn
+class TestGSPNBuilder:
+    def test_build_gspn(self):
+        assert True