From 47fbb98ed53be61cb5a0ff052c9764b2bd53f778 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 4 Mar 2020 16:55:34 +0100 Subject: [PATCH] Added structure for GSPN module --- CMakeLists.txt | 15 ++++++---- cmake/CMakeLists.txt | 56 ++++++++++++++++++++++++------------ cmake/config.py.in | 3 +- lib/stormpy/gspn/__init__.py | 7 +++++ setup.py | 19 ++++++++++++ setup/config.py | 1 + src/gspn/common.h | 2 ++ src/gspn/gspn.cpp | 18 ++++++++++++ src/gspn/gspn.h | 5 ++++ src/mod_gspn.cpp | 14 +++++++++ tests/configurations.py | 2 ++ tests/gspn/conftest.py | 4 +++ tests/gspn/test_gspn.py | 12 ++++++++ 13 files changed, 132 insertions(+), 26 deletions(-) create mode 100644 lib/stormpy/gspn/__init__.py create mode 100644 src/gspn/common.h create mode 100644 src/gspn/gspn.cpp create mode 100644 src/gspn/gspn.h create mode 100644 src/mod_gspn.cpp create mode 100644 tests/gspn/conftest.py create mode 100644 tests/gspn/test_gspn.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 7311ece..2e0e78b 100644 --- a/CMakeLists.txt +++ b/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() \ No newline at end of file +endif() + diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt index 04a44ab..0d90e2e 100644 --- a/cmake/CMakeLists.txt +++ b/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) diff --git a/cmake/config.py.in b/cmake/config.py.in index 0260476..905b57b 100644 --- a/cmake/config.py.in +++ b/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@ diff --git a/lib/stormpy/gspn/__init__.py b/lib/stormpy/gspn/__init__.py new file mode 100644 index 0000000..97c003a --- /dev/null +++ b/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 * diff --git a/setup.py b/setup.py index 388ee73..0f7b0dc 100755 --- a/setup.py +++ b/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')], diff --git a/setup/config.py b/setup/config.py index eef40ca..0bf9722 100644 --- a/setup/config.py +++ b/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), diff --git a/src/gspn/common.h b/src/gspn/common.h new file mode 100644 index 0000000..5d461f0 --- /dev/null +++ b/src/gspn/common.h @@ -0,0 +1,2 @@ +#include "src/common.h" +#include "storm-gspn/api/storm-gspn.h" \ No newline at end of file diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp new file mode 100644 index 0000000..b17ac26 --- /dev/null +++ b/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_>(m, "GSPN", "Generalized Stochastic Petri Net") + .def("name", &GSPN::getName, "Name of GSPN") + ; + +} diff --git a/src/gspn/gspn.h b/src/gspn/gspn.h new file mode 100644 index 0000000..17d58ea --- /dev/null +++ b/src/gspn/gspn.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_gspn(py::module& m); diff --git a/src/mod_gspn.cpp b/src/mod_gspn.cpp new file mode 100644 index 0000000..19adacd --- /dev/null +++ b/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); +} diff --git a/tests/configurations.py b/tests/configurations.py index 6dc681f..c57d259 100644 --- a/tests/configurations.py +++ b/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") diff --git a/tests/gspn/conftest.py b/tests/gspn/conftest.py new file mode 100644 index 0000000..323cb82 --- /dev/null +++ b/tests/gspn/conftest.py @@ -0,0 +1,4 @@ +from configurations import has_gspn + +if has_gspn: + import stormpy.gspn diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py new file mode 100644 index 0000000..fa368c2 --- /dev/null +++ b/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