From d060658bee4a3a47d37109632eb4dfde03c35ef7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 20 May 2020 10:11:28 +0200 Subject: [PATCH 01/36] Adaption to changes in storm-dft --- setup.py | 2 +- src/dft/dft.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/setup.py b/setup.py index 6c30f46..172ee03 100755 --- a/setup.py +++ b/setup.py @@ -14,7 +14,7 @@ if sys.version_info[0] == 2: sys.exit('Sorry, Python 2.x is not supported') # Minimal storm version required -storm_min_version = "1.4.2" +storm_min_version = "1.5.1" # Get the long description from the README file with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f: diff --git a/src/dft/dft.cpp b/src/dft/dft.cpp index 3b720ed..758eee0 100644 --- a/src/dft/dft.cpp +++ b/src/dft/dft.cpp @@ -3,6 +3,7 @@ #include "storm-dft/storage/dft/DFT.h" #include "storm/settings/SettingsManager.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/settings/modules/DftIOSettings.h" template using DFT = storm::storage::DFT; @@ -12,6 +13,7 @@ void define_dft(py::module& m) { m.def("_set_up", []() { storm::settings::addModule(); + storm::settings::addModule(); }, "Initialize Storm-dft"); From 5eda9b6ae2d51c8c6a6b1d10d1fc1fe0e7ec5145 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 20 May 2020 10:12:51 +0200 Subject: [PATCH 02/36] Travis: use latest Storm release --- .travis.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index 9ac38ba..ecb3144 100644 --- a/.travis.yml +++ b/.travis.yml @@ -48,13 +48,13 @@ jobs: # Docker Storm stable - os: linux compiler: gcc - env: TASK=Test CONFIG=Release DOCKER=storm:1.4.1 PYTHON=python3 + env: TASK=Test CONFIG=Release DOCKER=storm:1.5.1 PYTHON=python3 script: travis/build.sh # Docker Storm stable in debug mode - os: linux compiler: gcc - env: TASK=Test CONFIG=Debug DOCKER=storm:1.4.1-debug PYTHON=python3 + env: TASK=Test CONFIG=Debug DOCKER=storm:1.5.1-debug PYTHON=python3 script: travis/build.sh # Documentation @@ -76,6 +76,6 @@ jobs: # Allow failures of stable versions as new features might have been added allow_failures: - os: linux - env: TASK=Test CONFIG=Release DOCKER=storm:1.4.1 PYTHON=python3 + env: TASK=Test CONFIG=Release DOCKER=storm:1.5.1 PYTHON=python3 - os: linux - env: TASK=Test CONFIG=Debug DOCKER=storm:1.4.1-debug PYTHON=python3 + env: TASK=Test CONFIG=Debug DOCKER=storm:1.5.1-debug PYTHON=python3 From 320fe5eb5dd068ac39c1e71a45068f4999d166a1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 20 May 2020 13:36:55 +0200 Subject: [PATCH 03/36] Updated required Storm version --- setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/setup.py b/setup.py index 172ee03..388ee73 100755 --- a/setup.py +++ b/setup.py @@ -14,7 +14,7 @@ if sys.version_info[0] == 2: sys.exit('Sorry, Python 2.x is not supported') # Minimal storm version required -storm_min_version = "1.5.1" +storm_min_version = "1.5.2" # Get the long description from the README file with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f: From 7ea0055c11906c5fdac9f573ccdae58c47578ba7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 22 May 2020 14:41:20 +0200 Subject: [PATCH 04/36] added an example that prints the model checking result for all states --- examples/analysis/04-analysis.py | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 examples/analysis/04-analysis.py diff --git a/examples/analysis/04-analysis.py b/examples/analysis/04-analysis.py new file mode 100644 index 0000000..2dd5a26 --- /dev/null +++ b/examples/analysis/04-analysis.py @@ -0,0 +1,28 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_analysis_04(): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + + result = stormpy.model_checking(model, properties[0]) + + # Print the model checking result for all states + + print("Model checking results:") + for i in range(len(model.states)): + print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_state(i),result.at(i))) + +if __name__ == '__main__': + example_analysis_04() \ No newline at end of file From 7318abdd64d962d460fd9ba99dce79bdbec7dfdc Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 22 May 2020 15:53:52 +0200 Subject: [PATCH 05/36] Travis: fixed failure not being an error --- travis/build-helper.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/travis/build-helper.sh b/travis/build-helper.sh index a566447..ea04b46 100755 --- a/travis/build-helper.sh +++ b/travis/build-helper.sh @@ -65,7 +65,6 @@ run() { if [[ "$TASK" == *Test* ]] then # Run tests - set +e python setup.py test fi From 47fbb98ed53be61cb5a0ff052c9764b2bd53f778 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 4 Mar 2020 16:55:34 +0100 Subject: [PATCH 06/36] 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 From 00569096f95666504c321fca1e2dbcb044d5c7fb Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 10 Mar 2020 14:50:24 +0100 Subject: [PATCH 07/36] added gspn_builder class --- src/gspn/gspn.cpp | 27 ++++++++++++++++++++++++--- src/gspn/gspn.h | 2 ++ tests/gspn/test_gspn.py | 10 +++++++++- 3 files changed, 35 insertions(+), 4 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index b17ac26..2049d0f 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -5,14 +5,35 @@ #include "storm/settings/SettingsManager.h" -typedef storm::gspn::GSPN GSPN; +using GSPN = storm::gspn::GSPN; +using GSPNBuilder = storm::gspn::GspnBuilder; void define_gspn(py::module& m) { - // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") .def("name", &GSPN::getName, "Name of GSPN") + // todo getter ; - +//} +// todo ? void define_gspn_builder(py::module& m) { + // GSPN_Builder class + py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") + .def(py::init(), "Constructor") + .def("set_name", &GSPNBuilder::setGspnName, "Name of GSPN", py::arg("name")) + //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the gspn", py::arg("todo")) + //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Layout"py::arg("todo")) + //addImmediateTransition + //addTimedTransition + //addTimedTransition + //setTransitionLayoutInfo + //addInputArc todo overloaded fcts + //addInhibitionArc //todo overloaded fcts + //addOutputArc //todo overloaded fcts + //addNormalArc + .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) + // todo py::arg(... + // , py::arg("constantsSubstitution") = std::map() + // todo: argument ExpressionManager, map constantsSubstitution (aufrufe auch ohne args) + ; } diff --git a/src/gspn/gspn.h b/src/gspn/gspn.h index 17d58ea..ff36197 100644 --- a/src/gspn/gspn.h +++ b/src/gspn/gspn.h @@ -3,3 +3,5 @@ #include "common.h" void define_gspn(py::module& m); +// todo ? void define_gspn_builder(py::module& m); + diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index fa368c2..4948f27 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -9,4 +9,12 @@ from configurations import gspn @gspn class TestGSPNBuilder: def test_build_gspn(self): - assert True + # assert True + # builder: ~/storm/src/storm-dft/transformations/DFTToGSPNTransformator.cpp + name = "gspn_test" + builder = stormpy.gspn.GSPNBuilder() + builder.set_name(name) + gspn = builder.build_gspn() + assert gspn.name() == name + + From 279c24d6bd1d6d7fa1297ba63935ed14df2b018b Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 10 Mar 2020 20:11:16 +0100 Subject: [PATCH 08/36] added functions to gspn_builder --- src/gspn/gspn.cpp | 45 ++++++++++++++++++++++++++++------------- tests/gspn/test_gspn.py | 24 +++++++++++++++++++--- 2 files changed, 52 insertions(+), 17 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 2049d0f..b1c00b4 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -20,20 +20,37 @@ void define_gspn(py::module& m) { // GSPN_Builder class py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") .def(py::init(), "Constructor") - .def("set_name", &GSPNBuilder::setGspnName, "Name of GSPN", py::arg("name")) - //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the gspn", py::arg("todo")) - //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Layout"py::arg("todo")) - //addImmediateTransition - //addTimedTransition - //addTimedTransition - //setTransitionLayoutInfo - //addInputArc todo overloaded fcts - //addInhibitionArc //todo overloaded fcts - //addOutputArc //todo overloaded fcts - //addNormalArc + .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) + + // todo: boost::optional + //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = std::string("")) + //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) + + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = uint_fast64_t(0), py::arg("weight") = double(0), py::arg("name") = std::string("")) + + // todo: boost::optional + .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = std::string("")) + .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") + + // todo descriptions + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + + // todo LayoutInfo + //.def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) + + .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = uint64_t(1)) + .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) - // todo py::arg(... - // , py::arg("constantsSubstitution") = std::map() - // todo: argument ExpressionManager, map constantsSubstitution (aufrufe auch ohne args) + + // todo prvate? + // .def("is_timed_transition_id", &GSPNBuilder::isTimedTransitionId, py::arg("tid")) + // .def("is_immediate_transition_id", &GSPNBuilder::isImmediateTransitionId, py::arg("tid")) + // getTransition + ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index 4948f27..d7a3b33 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -11,10 +11,28 @@ class TestGSPNBuilder: def test_build_gspn(self): # assert True # builder: ~/storm/src/storm-dft/transformations/DFTToGSPNTransformator.cpp - name = "gspn_test" + gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() - builder.set_name(name) + builder.set_name(gspn_name) + # todo place tests, set_place_layout_info (boost) + # p_id_0 = builder.add_place(capacity = 1, initialTokens=0, name="place_test") + + ti_id_0 = builder.add_immediate_transition() + ti_id_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") + + tt_id_0 = builder.add_timed_transition(priority=0, rate=0.5, name="tt_0") + # todo problems with sumServers (boost) + # tt_id_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") + + # todo tests for add_ (add_place needed) + # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) + # todo test addNormalArc + # todo test setTransitionLayoutInfo ... + + gspn = builder.build_gspn() - assert gspn.name() == name + assert gspn.name() == gspn_name + + From 90c33339c00138cceed19b9b1d435133f9584740 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Mar 2020 12:42:21 +0100 Subject: [PATCH 09/36] added fcts to GSPN class --- src/gspn/gspn.cpp | 27 ++++++++++++++++++++------- src/gspn/gspn.h | 2 +- tests/gspn/test_gspn.py | 9 ++++++--- 3 files changed, 27 insertions(+), 11 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index b1c00b4..acef32f 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -13,26 +13,39 @@ void define_gspn(py::module& m) { // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") .def("name", &GSPN::getName, "Name of GSPN") - // todo getter + .def("set_name", &GSPN::setName, "Set name of GSPN") + + //todo constructor + // .def(py::init, ... >()) + + // todo write tests: + .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) + + // getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... + + //todo private? ; -//} -// todo ? void define_gspn_builder(py::module& m) { + // GSPN_Builder class py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") .def(py::init(), "Constructor") .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) - // todo: boost::optional - //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = std::string("")) + // todo: boost::optional capacity + //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = boost::optional(1), py::arg("initialTokens") = uint_fast64_t(0), py::arg("name") = std::string("")) //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) + // todo GSPNBuilder::RateType(0) ? .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = uint_fast64_t(0), py::arg("weight") = double(0), py::arg("name") = std::string("")) // todo: boost::optional .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = std::string("")) .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") - // todo descriptions + // todo add descriptions .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) @@ -47,7 +60,7 @@ void define_gspn(py::module& m) { .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) - // todo prvate? + // todo private fcts and attributes? // .def("is_timed_transition_id", &GSPNBuilder::isTimedTransitionId, py::arg("tid")) // .def("is_immediate_transition_id", &GSPNBuilder::isImmediateTransitionId, py::arg("tid")) // getTransition diff --git a/src/gspn/gspn.h b/src/gspn/gspn.h index ff36197..cc43acd 100644 --- a/src/gspn/gspn.h +++ b/src/gspn/gspn.h @@ -3,5 +3,5 @@ #include "common.h" void define_gspn(py::module& m); -// todo ? void define_gspn_builder(py::module& m); + diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index d7a3b33..ab379d3 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -1,7 +1,6 @@ import os import stormpy -from helpers.helper import get_example_path from configurations import gspn @@ -9,13 +8,13 @@ from configurations import gspn @gspn class TestGSPNBuilder: def test_build_gspn(self): - # assert True - # builder: ~/storm/src/storm-dft/transformations/DFTToGSPNTransformator.cpp + gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() builder.set_name(gspn_name) # todo place tests, set_place_layout_info (boost) # p_id_0 = builder.add_place(capacity = 1, initialTokens=0, name="place_test") + # p_id_0 = builder.add_place(1, 0, "place_test") ti_id_0 = builder.add_immediate_transition() ti_id_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") @@ -33,6 +32,10 @@ class TestGSPNBuilder: gspn = builder.build_gspn() assert gspn.name() == gspn_name + gspn_new_name = "new_name" + gspn.set_name(gspn_new_name) + assert gspn.name() == gspn_new_name + From 74a69e3dd2335bdbeeccab40a2b800d9c0334698 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Mar 2020 17:14:03 +0100 Subject: [PATCH 10/36] added LayoutInfo class --- src/gspn/gspn.cpp | 27 +++++++++++++++++---------- tests/gspn/test_gspn.py | 23 ++++++++++++++++++++++- 2 files changed, 39 insertions(+), 11 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index acef32f..a0c3394 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -7,9 +7,19 @@ using GSPN = storm::gspn::GSPN; using GSPNBuilder = storm::gspn::GspnBuilder; +using LayoutInfo = storm::gspn::LayoutInfo; void define_gspn(py::module& m) { + // LayoutInfo class + py::class_(m, "LayoutInfo") + .def(py::init<>()) + .def(py::init(), py::arg("x"), py::arg("y"), py::arg("rotation") = 0.0) //todo add rotation predefined + .def_readwrite("x", &LayoutInfo::x) + .def_readwrite("y", &LayoutInfo::y) + .def_readwrite("rotation", &LayoutInfo::rotation) + ; + // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") .def("name", &GSPN::getName, "Name of GSPN") @@ -35,14 +45,14 @@ void define_gspn(py::module& m) { .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) // todo: boost::optional capacity - //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = boost::optional(1), py::arg("initialTokens") = uint_fast64_t(0), py::arg("name") = std::string("")) + //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") + //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) - // todo GSPNBuilder::RateType(0) ? - .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = uint_fast64_t(0), py::arg("weight") = double(0), py::arg("name") = std::string("")) + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") // todo: boost::optional - .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = std::string("")) + .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") // todo add descriptions @@ -56,14 +66,11 @@ void define_gspn(py::module& m) { // todo LayoutInfo //.def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) - .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = uint64_t(1)) + .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) - // todo private fcts and attributes? - // .def("is_timed_transition_id", &GSPNBuilder::isTimedTransitionId, py::arg("tid")) - // .def("is_immediate_transition_id", &GSPNBuilder::isImmediateTransitionId, py::arg("tid")) - // getTransition - ; + + ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index ab379d3..0b8078e 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -7,13 +7,31 @@ from configurations import gspn @gspn class TestGSPNBuilder: + def test_layout_info(self): + layout = stormpy.gspn.LayoutInfo() + assert layout.x == 0 + assert layout.y == 0 + assert layout.rotation == 0 + layout.x = 1 + assert layout.x == 1 + + layout_xy = stormpy.gspn.LayoutInfo(2, 3) + assert layout_xy.x == 2 + assert layout_xy.rotation == 0 + + layout_xyr = stormpy.gspn.LayoutInfo(2, 3, 4) + assert layout_xyr.rotation == 4 + + def test_build_gspn(self): + + gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() builder.set_name(gspn_name) # todo place tests, set_place_layout_info (boost) - # p_id_0 = builder.add_place(capacity = 1, initialTokens=0, name="place_test") + # p_id_0 = builder.add_place() # p_id_0 = builder.add_place(1, 0, "place_test") ti_id_0 = builder.add_immediate_transition() @@ -29,6 +47,9 @@ class TestGSPNBuilder: # todo test setTransitionLayoutInfo ... + #builder.setTransitionLayoutInfo(tPropagationDontCare,layout); + + gspn = builder.build_gspn() assert gspn.name() == gspn_name From c8a9230e6e6ab77c756372fe481885ed37368ce2 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Mar 2020 19:58:49 +0100 Subject: [PATCH 11/36] added Place class --- src/gspn/gspn.cpp | 25 +++++++++++++++++++++---- tests/gspn/test_gspn.py | 27 +++++++++++++++++++++++---- 2 files changed, 44 insertions(+), 8 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index a0c3394..012970b 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -8,18 +8,36 @@ using GSPN = storm::gspn::GSPN; using GSPNBuilder = storm::gspn::GspnBuilder; using LayoutInfo = storm::gspn::LayoutInfo; +using Place = storm::gspn::Place; void define_gspn(py::module& m) { + // LayoutInfo class py::class_(m, "LayoutInfo") .def(py::init<>()) - .def(py::init(), py::arg("x"), py::arg("y"), py::arg("rotation") = 0.0) //todo add rotation predefined + .def(py::init(), "x"_a, "y"_a, "rotation"_a = 0.0) //todo add rotation predefined .def_readwrite("x", &LayoutInfo::x) .def_readwrite("y", &LayoutInfo::y) .def_readwrite("rotation", &LayoutInfo::rotation) ; + py::class_>(m, "Place", "Place in a GSPN") + .def(py::init(), "id"_a) + .def("get_name", &Place::getName, "Get name of this place") + .def("set_name", &Place::setName, "name"_a, "Set name of this place") + .def("get_id", &Place::getID, "Get the id of this place") + .def("set_number_of_initial_tokens", &Place::setNumberOfInitialTokens, "tokens"_a, "Set the number of initial tokens of this place") + .def("get_number_of_initial_tokens", &Place::getNumberOfInitialTokens, "Get the number of initial tokens of this place") + .def("set_capacity", &Place::setCapacity, "cap"_a, "Set the capacity of tokens of this place") + .def("get_capacity", &Place::getCapacity, "Get the capacity of tokens of this place") + .def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") + ; + + // TimedTransition class + // ImmediateTransition + + // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") .def("name", &GSPN::getName, "Name of GSPN") @@ -46,7 +64,6 @@ void define_gspn(py::module& m) { // todo: boost::optional capacity //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") - //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") @@ -63,8 +80,8 @@ void define_gspn(py::module& m) { .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - // todo LayoutInfo - //.def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) + + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index 0b8078e..ae54da1 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -22,10 +22,28 @@ class TestGSPNBuilder: layout_xyr = stormpy.gspn.LayoutInfo(2, 3, 4) assert layout_xyr.rotation == 4 + def test_place(self): + p_id = 4 + place = stormpy.gspn.Place(id = p_id) + assert p_id == place.get_id() + + assert place.has_restricted_capacity() == False + # todo this does not work (boost::optional ?): + place.set_capacity(cap = 5) + #assert place.has_restricted_capacity() == True + #assert place.get_capacity() == 5 + + p_name = "P_0" + place.set_name(name = p_name) + assert place.get_name() == p_name + + p_tokens = 2 + place.set_number_of_initial_tokens(p_tokens) + assert place.get_number_of_initial_tokens() == p_tokens - def test_build_gspn(self): + def test_build_gspn(self): gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() @@ -46,15 +64,16 @@ class TestGSPNBuilder: # todo test addNormalArc # todo test setTransitionLayoutInfo ... - - #builder.setTransitionLayoutInfo(tPropagationDontCare,layout); - + # todo test setLayout info + layout = stormpy.gspn.LayoutInfo(1,2) + builder.set_transition_layout_info(ti_id_0, layout) gspn = builder.build_gspn() assert gspn.name() == gspn_name gspn_new_name = "new_name" gspn.set_name(gspn_new_name) + assert gspn.name() == gspn_new_name From e69c1814622a9364f467aee73cb670053c1c2d1c Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 11 Mar 2020 21:17:13 +0100 Subject: [PATCH 12/36] added Transition classes --- src/gspn/gspn.cpp | 52 ++++++++++++++++++++++++++++++----------- tests/gspn/test_gspn.py | 24 +++++++++++++++++-- 2 files changed, 60 insertions(+), 16 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 012970b..4bf14f8 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -9,6 +9,9 @@ using GSPN = storm::gspn::GSPN; using GSPNBuilder = storm::gspn::GspnBuilder; using LayoutInfo = storm::gspn::LayoutInfo; using Place = storm::gspn::Place; +using TimedTransition = storm::gspn::TimedTransition; +using ImmediateTransition = storm::gspn::ImmediateTransition; +using Transition = storm::gspn::Transition; void define_gspn(py::module& m) { @@ -16,12 +19,13 @@ void define_gspn(py::module& m) { // LayoutInfo class py::class_(m, "LayoutInfo") .def(py::init<>()) - .def(py::init(), "x"_a, "y"_a, "rotation"_a = 0.0) //todo add rotation predefined + .def(py::init(), "x"_a, "y"_a, "rotation"_a = 0.0) .def_readwrite("x", &LayoutInfo::x) .def_readwrite("y", &LayoutInfo::y) .def_readwrite("rotation", &LayoutInfo::rotation) ; + // Place class py::class_>(m, "Place", "Place in a GSPN") .def(py::init(), "id"_a) .def("get_name", &Place::getName, "Get name of this place") @@ -34,17 +38,43 @@ void define_gspn(py::module& m) { .def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") ; + // Transition class + py::class_>(m, "Transition", "Transition in a GSPN") + .def(py::init<>()) + .def("get_name", &Transition::getName, "Get name of this transition") + .def("set_name", &Transition::setName, "name"_a, "Set name of this transition") + // todo add missing + ; + // TimedTransition class - // ImmediateTransition + py::class_>(m, "TimedTransition", "TimedTransition in a GSPN") + .def(py::init<>()) + .def("get_rate", &TimedTransition::getRate, "Get rate of this transition") + .def("set_rate", &TimedTransition::setRate, "rate"_a, "Set rate of this transition") + .def("set_k_server_semantics", &TimedTransition::setKServerSemantics, "k"_a, "Set semantics of this transition") + .def("set_single_server_semantics", &TimedTransition::setSingleServerSemantics, "Set semantics of this transition") + .def("set_infinite_server_semantics", &TimedTransition::setInfiniteServerSemantics, "Set semantics of this transition") + .def("has_k_server_semantics", &TimedTransition::hasKServerSemantics, "Get semantics of this transition") + .def("has_single_server_semantics", &TimedTransition::hasSingleServerSemantics, "Get semantics of this transition") + .def("has_infinite_server_semantics", &TimedTransition::hasInfiniteServerSemantics, "Get semantics of this transition") + .def("get_number_of_servers", &TimedTransition::getNumberOfServers, "Get number of servers") + ; + // ImmediateTransition class + py::class_>(m, "ImmediateTransition", "ImmediateTransition in a GSPN") + .def(py::init<>()) + .def("get_weight", &ImmediateTransition::getWeight, "Get weight of this transition") + .def("set_weight", &ImmediateTransition::setWeight, "weight"_a, "Set weight of this transition") + .def("no_weight_attached", &ImmediateTransition::noWeightAttached, "True iff no weight is attached") + ; // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") .def("name", &GSPN::getName, "Name of GSPN") .def("set_name", &GSPN::setName, "Set name of GSPN") - //todo constructor - // .def(py::init, ... >()) + // todo constructor: + // .def(py::init, ... >()) // todo write tests: .def_static("timed_transition_id_to_transition_id", &GSPN::timedTransitionIdToTransitionId) @@ -52,9 +82,9 @@ void define_gspn(py::module& m) { .def_static("transition_id_to_timed_transition_id", &GSPN::transitionIdToTimedTransitionId) .def_static("transition_id_to_immediate_transition_id", &GSPN::transitionIdToImmediateTransitionId) - // getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... + // todo: getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... + // todo export (see JaniToString) toPnpro, toPnml - //todo private? ; // GSPN_Builder class @@ -68,26 +98,20 @@ void define_gspn(py::module& m) { .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") - // todo: boost::optional + // todo: boost::optional + write tests: .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) - // todo add descriptions .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - - - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) - .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) - - ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index ae54da1..b62e8cc 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -30,8 +30,8 @@ class TestGSPNBuilder: assert place.has_restricted_capacity() == False # todo this does not work (boost::optional ?): place.set_capacity(cap = 5) - #assert place.has_restricted_capacity() == True - #assert place.get_capacity() == 5 + # assert place.has_restricted_capacity() == True + # assert place.get_capacity() == 5 p_name = "P_0" place.set_name(name = p_name) @@ -41,6 +41,26 @@ class TestGSPNBuilder: place.set_number_of_initial_tokens(p_tokens) assert place.get_number_of_initial_tokens() == p_tokens + def test_transition(self): + # test TimedTrasnition + tt = stormpy.gspn.TimedTransition() + tt_name = " tt" + tt.set_name(tt_name) + assert tt_name == tt.get_name() + tt_rate = 0.2 + tt.set_rate(tt_rate) + assert tt_rate == tt.get_rate() + + # test ImmediateTransition + ti = stormpy.gspn.ImmediateTransition() + ti_name = " ti" + ti.set_name(ti_name) + assert ti_name == ti.get_name() + assert ti.no_weight_attached() == True + ti_weight = 0.2 + ti.set_weight(ti_weight) + assert ti_weight == ti.get_weight() + assert ti.no_weight_attached() == False def test_build_gspn(self): From 4d357a7409600032861b2cd846cea87cee5f4ef3 Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 13 Mar 2020 11:28:38 +0100 Subject: [PATCH 13/36] write gspn to Pnpro --- src/gspn/gspn.cpp | 135 +++++++++++++++++++++++++--------------- tests/gspn/test_gspn.py | 37 ++++++++--- 2 files changed, 116 insertions(+), 56 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 4bf14f8..d0afd99 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -4,6 +4,7 @@ #include "storm-gspn/storage/gspn/GspnBuilder.h" #include "storm/settings/SettingsManager.h" +#include "storm/utility/file.h" using GSPN = storm::gspn::GSPN; using GSPNBuilder = storm::gspn::GspnBuilder; @@ -12,17 +13,87 @@ using Place = storm::gspn::Place; using TimedTransition = storm::gspn::TimedTransition; using ImmediateTransition = storm::gspn::ImmediateTransition; using Transition = storm::gspn::Transition; - +using TransitionPartition = storm::gspn::TransitionPartition; + +// todo to toPnproFile, totoPnmlFile (switch? to_pnpro) +void gspnToFile(GSPN const& gspn, std::string const& filepath) { + std::ofstream fs; + storm::utility::openFile(filepath, fs); + gspn.toPnpro(fs); //gspn.toPnml(fs); + storm::utility::closeFile(fs); +} void define_gspn(py::module& m) { + // GSPN_Builder class + py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") + .def(py::init(), "Constructor") + .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) + + // todo: boost::optional capacity + //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") + //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) + + // does not work either: + //.def("add_place", [](GSPNBuilder& b, boost::optional capacity = boost::optional(1), uint_fast64_t const& initialTokens = 0, std::string const& name = "") { + // b.addPlace(capacity, initialTokens, name); } , py::arg("capacity") = boost::optional(1), py::arg("initialTokens") = 0, py::arg("name") = "") + + + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") + + + // todo: boost::optional + write tests: + .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") + .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) + + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) + .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) + + .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) + ; + + // GSPN class + py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") + // Constructor + .def(py::init const& , std::vector const& , + std::vector const& , std::vector const& , + std::shared_ptr const& , std::map const& > (), + "name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map()) + + .def("name", &GSPN::getName, "Name of GSPN") + .def("set_name", &GSPN::setName, "Set name of GSPN") + .def("get_number_of_places", &GSPN::getNumberOfPlaces, "Get the number of places in this GSPN") + .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") + .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the timed transitions in this GSPN") + + // todo write tests: + .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) + + // todo: getPartitions, getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... and test (returns vector) + // todo getPlace getTra... + tests (returns pointer to place/..) + + // todo export (see JaniToString) toPnpro, toPnml + .def("export_gspn_pnpro_file", &gspnToFile, "filepath"_a) + .def("export_gspn_pnml_file", &gspnToFile, "filepath"_a) + ; + // LayoutInfo class py::class_(m, "LayoutInfo") - .def(py::init<>()) - .def(py::init(), "x"_a, "y"_a, "rotation"_a = 0.0) - .def_readwrite("x", &LayoutInfo::x) - .def_readwrite("y", &LayoutInfo::y) - .def_readwrite("rotation", &LayoutInfo::rotation) + .def(py::init<>()) + .def(py::init(), "x"_a, "y"_a, "rotation"_a = 0.0) + .def_readwrite("x", &LayoutInfo::x) + .def_readwrite("y", &LayoutInfo::y) + .def_readwrite("rotation", &LayoutInfo::rotation) ; // Place class @@ -33,11 +104,19 @@ void define_gspn(py::module& m) { .def("get_id", &Place::getID, "Get the id of this place") .def("set_number_of_initial_tokens", &Place::setNumberOfInitialTokens, "tokens"_a, "Set the number of initial tokens of this place") .def("get_number_of_initial_tokens", &Place::getNumberOfInitialTokens, "Get the number of initial tokens of this place") - .def("set_capacity", &Place::setCapacity, "cap"_a, "Set the capacity of tokens of this place") + .def("set_capacity", &Place::setCapacity, "cap"_a, "Set the capacity of tokens of this place") // problem: boost or lambda [](.. .def("get_capacity", &Place::getCapacity, "Get the capacity of tokens of this place") .def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") ; + // TransitionPartition class + py::class_(m, "TransitionPartition") + .def(py::init<>()) + .def_readwrite("priority", &TransitionPartition::priority) + .def_readwrite("transitions", &TransitionPartition::transitions) + .def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") + ; + // Transition class py::class_>(m, "Transition", "Transition in a GSPN") .def(py::init<>()) @@ -68,50 +147,8 @@ void define_gspn(py::module& m) { .def("no_weight_attached", &ImmediateTransition::noWeightAttached, "True iff no weight is attached") ; - // GSPN class - py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") - .def("name", &GSPN::getName, "Name of GSPN") - .def("set_name", &GSPN::setName, "Set name of GSPN") - // todo constructor: - // .def(py::init, ... >()) - // todo write tests: - .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) - - // todo: getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... - // todo export (see JaniToString) toPnpro, toPnml - - ; - - // GSPN_Builder class - py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") - .def(py::init(), "Constructor") - .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) - - // todo: boost::optional capacity - //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") - //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) - - .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") - // todo: boost::optional + write tests: - .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") - .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) - - .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) - - ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index b62e8cc..92af3c0 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -4,6 +4,8 @@ import stormpy from configurations import gspn +from helpers.helper import get_example_path + @gspn class TestGSPNBuilder: @@ -62,6 +64,10 @@ class TestGSPNBuilder: assert ti_weight == ti.get_weight() assert ti.no_weight_attached() == False + #def test_gspn(self): + # todo + #immediateTransitions = + #gspn = stormpy.gspn.GSPN("gspn", places, immediateTransitions, timedTransitions, orderedPartitions, actualExprManager, constantsSubstitution) def test_build_gspn(self): @@ -69,8 +75,10 @@ class TestGSPNBuilder: builder = stormpy.gspn.GSPNBuilder() builder.set_name(gspn_name) # todo place tests, set_place_layout_info (boost) - # p_id_0 = builder.add_place() - # p_id_0 = builder.add_place(1, 0, "place_test") + #p_id_0 = builder.add_place() + # p_id_0 = builder.add_place(capacity = 1, initialTokens = 0, name = "place_test") + # p_layout = stormpy.gspn.LayoutInfo(1, 2) + # builder.set_place_layout_info(p_id_0, t_layout) ti_id_0 = builder.add_immediate_transition() ti_id_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") @@ -82,20 +90,35 @@ class TestGSPNBuilder: # todo tests for add_ (add_place needed) # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) # todo test addNormalArc - # todo test setTransitionLayoutInfo ... - # todo test setLayout info - layout = stormpy.gspn.LayoutInfo(1,2) - builder.set_transition_layout_info(ti_id_0, layout) + t_layout = stormpy.gspn.LayoutInfo(1, 2) + builder.set_transition_layout_info(ti_id_0, t_layout) gspn = builder.build_gspn() assert gspn.name() == gspn_name gspn_new_name = "new_name" gspn.set_name(gspn_new_name) - assert gspn.name() == gspn_new_name + def test_export_to_pnpro(self, tmpdir): + gspn_name = "gspn_test" + builder = stormpy.gspn.GSPNBuilder() + builder.set_name(gspn_name) + gspn = builder.build_gspn() + # todo add trans and places (layout?) + assert gspn.name() == gspn_name + #todo assert gspn.nr trans etc + export_file = os.path.join(str(tmpdir), "gspn.pnpro") + gspn.export_gspn_pnpro_file(export_file) + + + #todo: load and assert gspn.nr trans etc + # gspn_from_file = stormpy.gspn.load_gspn_file(export_file) + # assert gspn_from_file.nr ==... + + #def test_export_to_pnml(self, tmpdir): + From 7fee180e4010dfcbdcec8c58cf320d33f53910d0 Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 13 Mar 2020 20:52:24 +0100 Subject: [PATCH 14/36] export gspn to pnml --- src/gspn/gspn.cpp | 45 +++++++++++++++++++++++++++++---------------- 1 file changed, 29 insertions(+), 16 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index d0afd99..ac8f4e5 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -4,6 +4,7 @@ #include "storm-gspn/storage/gspn/GspnBuilder.h" #include "storm/settings/SettingsManager.h" +#include "storm-gspn/parser/GspnParser.h" #include "storm/utility/file.h" using GSPN = storm::gspn::GSPN; @@ -14,12 +15,19 @@ using TimedTransition = storm::gspn::TimedTransition; using ImmediateTransition = storm::gspn::ImmediateTransition; using Transition = storm::gspn::Transition; using TransitionPartition = storm::gspn::TransitionPartition; +using GSPNParser = storm::parser::GspnParser; -// todo to toPnproFile, totoPnmlFile (switch? to_pnpro) -void gspnToFile(GSPN const& gspn, std::string const& filepath) { + +void gspnToFile(GSPN const& gspn, std::string const& filepath, std::string const& option) { std::ofstream fs; storm::utility::openFile(filepath, fs); - gspn.toPnpro(fs); //gspn.toPnml(fs); + + if(option == "to-pnpro") { + gspn.toPnpro(fs); + } + else if (option == "to-pnml"){ + gspn.toPnml(fs); + } storm::utility::closeFile(fs); } @@ -42,7 +50,7 @@ void define_gspn(py::module& m) { .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") - // todo: boost::optional + write tests: + // todo: problem with boost::optional + write tests: .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) @@ -62,10 +70,8 @@ void define_gspn(py::module& m) { py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") // Constructor .def(py::init const& , std::vector const& , - std::vector const& , std::vector const& , - std::shared_ptr const& , std::map const& > (), - "name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map()) + std::vector const& , std::vector const& , std::shared_ptr const& , std::map const& > (), "name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map()) .def("name", &GSPN::getName, "Name of GSPN") .def("set_name", &GSPN::setName, "Set name of GSPN") @@ -73,20 +79,29 @@ void define_gspn(py::module& m) { .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the timed transitions in this GSPN") - // todo write tests: + // todo write tests: .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) - // todo: getPartitions, getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... and test (returns vector) - // todo getPlace getTra... + tests (returns pointer to place/..) + // todo: getPartitions, getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... and test (returns vector) + // todo getPlace getTra... + tests (returns pointer to place/..) + + // GSPN export + .def("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnpro"); }, "filepath"_a) + .def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnml"); }, "filepath"_a) + + ; - // todo export (see JaniToString) toPnpro, toPnml - .def("export_gspn_pnpro_file", &gspnToFile, "filepath"_a) - .def("export_gspn_pnml_file", &gspnToFile, "filepath"_a) + // GspnParser class + py::class_>(m, "GSPNParser") + .def(py::init<>()) + //todo .def("parse", ) ; + + // LayoutInfo class py::class_(m, "LayoutInfo") .def(py::init<>()) @@ -149,6 +164,4 @@ void define_gspn(py::module& m) { - - } From b5cb9d71ee7ee88785cc2bb78e96a37a8dd86036 Mon Sep 17 00:00:00 2001 From: hannah Date: Sat, 14 Mar 2020 13:58:58 +0100 Subject: [PATCH 15/36] added GSPNParser class for gspn import and missing GSPN class methods --- src/gspn/gspn.cpp | 88 ++++++++++++++++++++++------------------- tests/gspn/test_gspn.py | 42 ++++++++++++-------- 2 files changed, 74 insertions(+), 56 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index ac8f4e5..589f4b7 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -31,12 +31,13 @@ void gspnToFile(GSPN const& gspn, std::string const& filepath, std::string const storm::utility::closeFile(fs); } + void define_gspn(py::module& m) { // GSPN_Builder class py::class_>(m, "GSPNBuilder", "Generalized Stochastic Petri Net Builder") .def(py::init(), "Constructor") - .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", py::arg("name")) + .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) // todo: boost::optional capacity //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") @@ -46,24 +47,29 @@ void define_gspn(py::module& m) { //.def("add_place", [](GSPNBuilder& b, boost::optional capacity = boost::optional(1), uint_fast64_t const& initialTokens = 0, std::string const& name = "") { // b.addPlace(capacity, initialTokens, name); } , py::arg("capacity") = boost::optional(1), py::arg("initialTokens") = 0, py::arg("name") = "") - - .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", py::arg("priority") = 0, py::arg("weight") = 0, py::arg("name") = "") - + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") // todo: problem with boost::optional + write tests: - .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("name") = "") - .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", py::arg("priority"), py::arg("rate"), py::arg("numServers"), py::arg("name") = "") - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", py::arg("transitionId"), py::arg("layoutInfo")) - - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity")) - .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", py::arg("from"), py::arg("to"), py::arg("multiplicity") = 1) - - .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", py::arg("exprManager") = nullptr, py::arg("constantsSubstitution") = std::map()) + .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") + .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", "transitionId"_a, "layoutInfo"_a) + + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a) + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", "from"_a, "to"_a, "multiplicity"_a = 1) + + .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", "exprManager"_a = nullptr, "constantsSubstitution"_a = std::map()) + ; + + // GspnParser class + py::class_>(m, "GSPNParser") + .def(py::init<>()) + .def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& { + return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constantDefinitions"_a = "") ; // GSPN class @@ -73,11 +79,27 @@ void define_gspn(py::module& m) { std::vector const& , std::vector const& , std::shared_ptr const& , std::map const& > (), "name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map()) - .def("name", &GSPN::getName, "Name of GSPN") + .def("get_name", &GSPN::getName, "Get name of GSPN") .def("set_name", &GSPN::setName, "Set name of GSPN") + // todo write tests: .def("get_number_of_places", &GSPN::getNumberOfPlaces, "Get the number of places in this GSPN") .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") - .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the timed transitions in this GSPN") + .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the number of timed transitions in this GSPN") + + // todo write tests: + .def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") + .def("get_places", &GSPN::getPlaces, "Get the places of this GSPN") + .def("get_timed_transitions", &GSPN::getTimedTransitions, "Get the timed transitions of this GSPN") + .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") + + // todo tests (special case: getTimedTransition/... returns nullptr + // dereferencing a null pointer is undefined behavior, getTimedTransition returns nullptr (if transition naem does not exist -> test) + // test if get_place by id and name correct (overloaded) + .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a) + .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) + .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a) + .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a) // todo write tests: .def_static("timed_transition_id_to_transition_id", &GSPN::timedTransitionIdToTransitionId) @@ -85,23 +107,11 @@ void define_gspn(py::module& m) { .def_static("transition_id_to_timed_transition_id", &GSPN::transitionIdToTimedTransitionId) .def_static("transition_id_to_immediate_transition_id", &GSPN::transitionIdToImmediateTransitionId) - // todo: getPartitions, getNumberOfPlaces, getNumberOfImmediateTransitions, getNumberOfTimedTransitions, ... and test (returns vector) - // todo getPlace getTra... + tests (returns pointer to place/..) - // GSPN export .def("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnpro"); }, "filepath"_a) .def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnml"); }, "filepath"_a) - ; - // GspnParser class - py::class_>(m, "GSPNParser") - .def(py::init<>()) - //todo .def("parse", ) - ; - - - // LayoutInfo class py::class_(m, "LayoutInfo") .def(py::init<>()) @@ -124,14 +134,6 @@ void define_gspn(py::module& m) { .def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") ; - // TransitionPartition class - py::class_(m, "TransitionPartition") - .def(py::init<>()) - .def_readwrite("priority", &TransitionPartition::priority) - .def_readwrite("transitions", &TransitionPartition::transitions) - .def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") - ; - // Transition class py::class_>(m, "Transition", "Transition in a GSPN") .def(py::init<>()) @@ -162,6 +164,12 @@ void define_gspn(py::module& m) { .def("no_weight_attached", &ImmediateTransition::noWeightAttached, "True iff no weight is attached") ; - + // TransitionPartition class + py::class_(m, "TransitionPartition") + .def(py::init<>()) + .def_readwrite("priority", &TransitionPartition::priority) + .def_readwrite("transitions", &TransitionPartition::transitions) + .def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") + ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index 92af3c0..cfe9094 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -80,43 +80,53 @@ class TestGSPNBuilder: # p_layout = stormpy.gspn.LayoutInfo(1, 2) # builder.set_place_layout_info(p_id_0, t_layout) - ti_id_0 = builder.add_immediate_transition() - ti_id_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") + ti_0 = builder.add_immediate_transition() + ti_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") - tt_id_0 = builder.add_timed_transition(priority=0, rate=0.5, name="tt_0") + tt_0 = builder.add_timed_transition(priority=0, rate=0.5, name="tt_0") # todo problems with sumServers (boost) - # tt_id_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") + # tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") # todo tests for add_ (add_place needed) # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) - # todo test addNormalArc + # builder.add_normal_arc + # builder.add_output_arc t_layout = stormpy.gspn.LayoutInfo(1, 2) - builder.set_transition_layout_info(ti_id_0, t_layout) + builder.set_transition_layout_info(ti_0, t_layout) gspn = builder.build_gspn() - assert gspn.name() == gspn_name + assert gspn.get_name() == gspn_name gspn_new_name = "new_name" gspn.set_name(gspn_new_name) - assert gspn.name() == gspn_new_name + assert gspn.get_name() == gspn_new_name def test_export_to_pnpro(self, tmpdir): - gspn_name = "gspn_test" + builder = stormpy.gspn.GSPNBuilder() - builder.set_name(gspn_name) + builder.set_name("gspn_test") + ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") gspn = builder.build_gspn() - # todo add trans and places (layout?) - assert gspn.name() == gspn_name - #todo assert gspn.nr trans etc + # todo add trans and places (place layout after import?) + export_file = os.path.join(str(tmpdir), "gspn.pnpro") + # export gspn to pnpro gspn.export_gspn_pnpro_file(export_file) + # import gspn + gspn_parser = stormpy.gspn.GSPNParser() + gspn_import = gspn_parser.parse(export_file) + assert gspn_import.get_name() == gspn.get_name() + assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() + assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() + assert gspn_import.get_number_of_places() == gspn.get_number_of_places() + # tets transition name + # ti_0_import = gspn_import. - - #todo: load and assert gspn.nr trans etc - # gspn_from_file = stormpy.gspn.load_gspn_file(export_file) # assert gspn_from_file.nr ==... + #asser name of ti + # todo test to_pnml (cp test to pnpro) #def test_export_to_pnml(self, tmpdir): From 3c71a4b04a3fb1346efce3fabc15b96c966102db Mon Sep 17 00:00:00 2001 From: hannah Date: Sat, 14 Mar 2020 23:47:35 +0100 Subject: [PATCH 16/36] added some tests --- src/gspn/gspn.cpp | 36 ++++++++++---------- tests/gspn/test_gspn.py | 75 ++++++++++++++++++++++++++++++----------- 2 files changed, 72 insertions(+), 39 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 589f4b7..99e0a0b 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -54,6 +54,7 @@ void define_gspn(py::module& m) { .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", "transitionId"_a, "layoutInfo"_a) + // todo write tests .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a) .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a) .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) @@ -67,9 +68,8 @@ void define_gspn(py::module& m) { // GspnParser class py::class_>(m, "GSPNParser") - .def(py::init<>()) - .def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& { - return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constantDefinitions"_a = "") + .def(py::init<>()) + .def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& {return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constantDefinitions"_a = "") ; // GSPN class @@ -81,27 +81,22 @@ void define_gspn(py::module& m) { .def("get_name", &GSPN::getName, "Get name of GSPN") .def("set_name", &GSPN::setName, "Set name of GSPN") - // todo write tests: + .def("get_number_of_places", &GSPN::getNumberOfPlaces, "Get the number of places in this GSPN") .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the number of timed transitions in this GSPN") - // todo write tests: + .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a) + .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) + .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a) + .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a) .def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") .def("get_places", &GSPN::getPlaces, "Get the places of this GSPN") .def("get_timed_transitions", &GSPN::getTimedTransitions, "Get the timed transitions of this GSPN") .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") - // todo tests (special case: getTimedTransition/... returns nullptr - // dereferencing a null pointer is undefined behavior, getTimedTransition returns nullptr (if transition naem does not exist -> test) - // test if get_place by id and name correct (overloaded) - .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a) - .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) - .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a) - .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a) - - // todo write tests: + //todo tests: .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) @@ -137,8 +132,11 @@ void define_gspn(py::module& m) { // Transition class py::class_>(m, "Transition", "Transition in a GSPN") .def(py::init<>()) - .def("get_name", &Transition::getName, "Get name of this transition") + .def("get_id", &Transition::getID, "Get id of this transition") .def("set_name", &Transition::setName, "name"_a, "Set name of this transition") + .def("get_name", &Transition::getName, "Get name of this transition") + .def("set_priority", &Transition::getID, "Get priority of this transition") + .def("get_priority", &Transition::getPriority, "Get priority of this transition") // todo add missing ; @@ -166,10 +164,10 @@ void define_gspn(py::module& m) { // TransitionPartition class py::class_(m, "TransitionPartition") - .def(py::init<>()) - .def_readwrite("priority", &TransitionPartition::priority) - .def_readwrite("transitions", &TransitionPartition::transitions) - .def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") + .def(py::init<>()) + .def_readwrite("priority", &TransitionPartition::priority) + .def_readwrite("transitions", &TransitionPartition::transitions) + .def("nr_transitions", &TransitionPartition::nrTransitions, "Get number of transitions") ; } diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index cfe9094..7da5ecd 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -30,7 +30,7 @@ class TestGSPNBuilder: assert p_id == place.get_id() assert place.has_restricted_capacity() == False - # todo this does not work (boost::optional ?): + # todo this does not work (boost::optional problem?): place.set_capacity(cap = 5) # assert place.has_restricted_capacity() == True # assert place.get_capacity() == 5 @@ -64,26 +64,23 @@ class TestGSPNBuilder: assert ti_weight == ti.get_weight() assert ti.no_weight_attached() == False - #def test_gspn(self): - # todo - #immediateTransitions = - #gspn = stormpy.gspn.GSPN("gspn", places, immediateTransitions, timedTransitions, orderedPartitions, actualExprManager, constantsSubstitution) def test_build_gspn(self): - gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() + builder.set_name(gspn_name) + # todo place tests, set_place_layout_info (boost) - #p_id_0 = builder.add_place() - # p_id_0 = builder.add_place(capacity = 1, initialTokens = 0, name = "place_test") + # p_0 = builder.add_place() + # p_1 = builder.add_place(capacity = 2, initialTokens = 0, name = "place_test") # p_layout = stormpy.gspn.LayoutInfo(1, 2) - # builder.set_place_layout_info(p_id_0, t_layout) + # builder.set_place_layout_info(p_0, t_layout) - ti_0 = builder.add_immediate_transition() - ti_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") + ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0") + ti_1 = builder.add_immediate_transition() - tt_0 = builder.add_timed_transition(priority=0, rate=0.5, name="tt_0") + tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") # todo problems with sumServers (boost) # tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") @@ -96,38 +93,76 @@ class TestGSPNBuilder: builder.set_transition_layout_info(ti_0, t_layout) gspn = builder.build_gspn() + assert gspn.get_name() == gspn_name + assert gspn.get_number_of_immediate_transitions() == 2 + # assert gspn.get_number_of_timed_transitions() == 2 + # assert gspn.get_number_of_places() == 2 + cp_ti_0 = gspn.get_immediate_transition("ti_0") + assert cp_ti_0.get_id() == ti_0 + assert cp_ti_0.get_weight() == 0.5 + assert cp_ti_0.get_priority() == 1 + cp_tt_0 = gspn.get_timed_transition("tt_0") + assert cp_tt_0.get_id() == tt_0 + assert cp_tt_0.get_rate() == 0.4 + assert cp_tt_0.get_priority() == 2 + # cp_p_0 = gspn.get_immediate_transition("p_0") + # assert cp_p_0.get_id() == p_0 + # assert cp_p_0.get_capacity() == 2 gspn_new_name = "new_name" gspn.set_name(gspn_new_name) assert gspn.get_name() == gspn_new_name def test_export_to_pnpro(self, tmpdir): - builder = stormpy.gspn.GSPNBuilder() builder.set_name("gspn_test") ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") gspn = builder.build_gspn() - # todo add trans and places (place layout after import?) + # todo add some trans and places (place layout after import?) + # add arcs export_file = os.path.join(str(tmpdir), "gspn.pnpro") + # export gspn to pnpro gspn.export_gspn_pnpro_file(export_file) + # import gspn gspn_parser = stormpy.gspn.GSPNParser() gspn_import = gspn_parser.parse(export_file) + assert gspn_import.get_name() == gspn.get_name() assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() assert gspn_import.get_number_of_places() == gspn.get_number_of_places() - # tets transition name - # ti_0_import = gspn_import. + cp_ti_0 = gspn_import.get_immediate_transition("ti_0") + assert cp_ti_0.get_id() == ti_0 + + + def test_export_to_pnml(self, tmpdir): + builder = stormpy.gspn.GSPNBuilder() + builder.set_name("gspn_test") + ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") + gspn = builder.build_gspn() + # todo add some trans and places (place layout after import?) + # add arcs (cp from above) + + export_file = os.path.join(str(tmpdir), "gspn.pnml") + + # export gspn to pnml + gspn.export_gspn_pnml_file(export_file) + + # import gspn + gspn_parser = stormpy.gspn.GSPNParser() + gspn_import = gspn_parser.parse(export_file) - # assert gspn_from_file.nr ==... - #asser name of ti + assert gspn_import.get_name() == gspn.get_name() + assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() + assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() + assert gspn_import.get_number_of_places() == gspn.get_number_of_places() + cp_ti_0 = gspn_import.get_immediate_transition("ti_0") + assert cp_ti_0.get_id() == ti_0 - # todo test to_pnml (cp test to pnpro) - #def test_export_to_pnml(self, tmpdir): From 2eec1828c186374177314a023e4ebd4f29da9b98 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 30 Mar 2020 18:51:06 +0200 Subject: [PATCH 17/36] GSPNs methods using boost::optional are working after fix in Storm --- src/gspn/gspn.cpp | 6 +++--- tests/gspn/test_gspn.py | 30 +++++++++++++----------------- 2 files changed, 16 insertions(+), 20 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 99e0a0b..c6dba99 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -40,8 +40,8 @@ void define_gspn(py::module& m) { .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) // todo: boost::optional capacity - //.def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") - //.def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) + .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") + .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) // does not work either: //.def("add_place", [](GSPNBuilder& b, boost::optional capacity = boost::optional(1), uint_fast64_t const& initialTokens = 0, std::string const& name = "") { @@ -51,7 +51,7 @@ void define_gspn(py::module& m) { // todo: problem with boost::optional + write tests: .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") - .def("add_timed_transition", py::overload_cast, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") + .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", "transitionId"_a, "layoutInfo"_a) // todo write tests diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index 7da5ecd..c1ebcd1 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -32,8 +32,8 @@ class TestGSPNBuilder: assert place.has_restricted_capacity() == False # todo this does not work (boost::optional problem?): place.set_capacity(cap = 5) - # assert place.has_restricted_capacity() == True - # assert place.get_capacity() == 5 + assert place.has_restricted_capacity() == True + assert place.get_capacity() == 5 p_name = "P_0" place.set_name(name = p_name) @@ -44,7 +44,7 @@ class TestGSPNBuilder: assert place.get_number_of_initial_tokens() == p_tokens def test_transition(self): - # test TimedTrasnition + # test TimedTransition tt = stormpy.gspn.TimedTransition() tt_name = " tt" tt.set_name(tt_name) @@ -72,17 +72,17 @@ class TestGSPNBuilder: builder.set_name(gspn_name) # todo place tests, set_place_layout_info (boost) - # p_0 = builder.add_place() - # p_1 = builder.add_place(capacity = 2, initialTokens = 0, name = "place_test") - # p_layout = stormpy.gspn.LayoutInfo(1, 2) - # builder.set_place_layout_info(p_0, t_layout) + p_0 = builder.add_place() + p_1 = builder.add_place(capacity = 2, initialTokens = 0, name = "place_test") + p_layout = stormpy.gspn.LayoutInfo(1, 2) + builder.set_place_layout_info(p_0, p_layout) ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0") ti_1 = builder.add_immediate_transition() tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") # todo problems with sumServers (boost) - # tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") + tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") # todo tests for add_ (add_place needed) # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) @@ -96,8 +96,8 @@ class TestGSPNBuilder: assert gspn.get_name() == gspn_name assert gspn.get_number_of_immediate_transitions() == 2 - # assert gspn.get_number_of_timed_transitions() == 2 - # assert gspn.get_number_of_places() == 2 + assert gspn.get_number_of_timed_transitions() == 2 + assert gspn.get_number_of_places() == 2 cp_ti_0 = gspn.get_immediate_transition("ti_0") assert cp_ti_0.get_id() == ti_0 assert cp_ti_0.get_weight() == 0.5 @@ -106,9 +106,9 @@ class TestGSPNBuilder: assert cp_tt_0.get_id() == tt_0 assert cp_tt_0.get_rate() == 0.4 assert cp_tt_0.get_priority() == 2 - # cp_p_0 = gspn.get_immediate_transition("p_0") - # assert cp_p_0.get_id() == p_0 - # assert cp_p_0.get_capacity() == 2 + cp_p_1 = gspn.get_place("place_test") + assert cp_p_1.get_id() == p_1 + assert cp_p_1.get_capacity() == 2 gspn_new_name = "new_name" gspn.set_name(gspn_new_name) @@ -163,7 +163,3 @@ class TestGSPNBuilder: cp_ti_0 = gspn_import.get_immediate_transition("ti_0") assert cp_ti_0.get_id() == ti_0 - - - - From 9a74d83079f4b5d6b71462a59f237997af8c5c93 Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 31 Mar 2020 20:27:38 +0200 Subject: [PATCH 18/36] added remaining tests --- src/gspn/gspn.cpp | 11 +-- tests/gspn/test_gspn.py | 150 ++++++++++++++++++++++++++++------------ 2 files changed, 110 insertions(+), 51 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index c6dba99..8c90b81 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -39,22 +39,15 @@ void define_gspn(py::module& m) { .def(py::init(), "Constructor") .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) - // todo: boost::optional capacity .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") - .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("placeId"), py::arg("layoutInfo")) - - // does not work either: - //.def("add_place", [](GSPNBuilder& b, boost::optional capacity = boost::optional(1), uint_fast64_t const& initialTokens = 0, std::string const& name = "") { - // b.addPlace(capacity, initialTokens, name); } , py::arg("capacity") = boost::optional(1), py::arg("initialTokens") = 0, py::arg("name") = "") + .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("place_id"), py::arg("layout_info")) .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") - // todo: problem with boost::optional + write tests: .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", "transitionId"_a, "layoutInfo"_a) - // todo write tests .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a) .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a) .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) @@ -90,6 +83,8 @@ void define_gspn(py::module& m) { .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a) .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a) + .def("get_transition",[](GSPN const& g, std::string const& name) -> const Transition& {return *(g.getTransition(name)); }, "name"_a) + .def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") .def("get_places", &GSPN::getPlaces, "Get the places of this GSPN") .def("get_timed_transitions", &GSPN::getTimedTransitions, "Get the timed transitions of this GSPN") diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index c1ebcd1..b840327 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -4,7 +4,6 @@ import stormpy from configurations import gspn -from helpers.helper import get_example_path @gspn @@ -30,7 +29,6 @@ class TestGSPNBuilder: assert p_id == place.get_id() assert place.has_restricted_capacity() == False - # todo this does not work (boost::optional problem?): place.set_capacity(cap = 5) assert place.has_restricted_capacity() == True assert place.get_capacity() == 5 @@ -69,47 +67,78 @@ class TestGSPNBuilder: gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() - builder.set_name(gspn_name) - - # todo place tests, set_place_layout_info (boost) - p_0 = builder.add_place() - p_1 = builder.add_place(capacity = 2, initialTokens = 0, name = "place_test") + id_p_0 = builder.add_place() + id_p_1 = builder.add_place(initialTokens = 1) + id_p_2 = builder.add_place(initialTokens = 0, name = "place_2") + id_p_3 = builder.add_place(capacity = 2, initialTokens = 3, name = "place_3") p_layout = stormpy.gspn.LayoutInfo(1, 2) - builder.set_place_layout_info(p_0, p_layout) - - ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0") - ti_1 = builder.add_immediate_transition() + builder.set_place_layout_info(id_p_0, p_layout) - tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") - # todo problems with sumServers (boost) - tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") + id_ti_0 = builder.add_immediate_transition(priority=1, weight=0.5, name="ti_0") + id_ti_1 = builder.add_immediate_transition() - # todo tests for add_ (add_place needed) - # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) - # builder.add_normal_arc - # builder.add_output_arc + id_tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") + id_tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") t_layout = stormpy.gspn.LayoutInfo(1, 2) - builder.set_transition_layout_info(ti_0, t_layout) + builder.set_transition_layout_info(id_ti_0, t_layout) + + # add arcs + builder.add_input_arc(id_p_0, id_ti_1, multiplicity = 2) + builder.add_input_arc("place_2", "ti_0", multiplicity = 2) + + builder.add_output_arc(id_ti_1, id_p_2, multiplicity = 2) + builder.add_output_arc("tt_0", "place_3", multiplicity = 2) + builder.add_inhibition_arc(id_p_2, id_tt_0, multiplicity = 2) + builder.add_inhibition_arc("place_3", "tt_0", multiplicity = 2) + + builder.add_normal_arc("place_3", "tt_0", multiplicity = 2) + builder.add_normal_arc("tt_0", "place_3", multiplicity = 2) + + # test gspn composition + builder.set_name(gspn_name) gspn = builder.build_gspn() assert gspn.get_name() == gspn_name assert gspn.get_number_of_immediate_transitions() == 2 assert gspn.get_number_of_timed_transitions() == 2 - assert gspn.get_number_of_places() == 2 - cp_ti_0 = gspn.get_immediate_transition("ti_0") - assert cp_ti_0.get_id() == ti_0 - assert cp_ti_0.get_weight() == 0.5 - assert cp_ti_0.get_priority() == 1 - cp_tt_0 = gspn.get_timed_transition("tt_0") - assert cp_tt_0.get_id() == tt_0 - assert cp_tt_0.get_rate() == 0.4 - assert cp_tt_0.get_priority() == 2 - cp_p_1 = gspn.get_place("place_test") - assert cp_p_1.get_id() == p_1 - assert cp_p_1.get_capacity() == 2 - + assert gspn.get_number_of_places() == 4 + + # test places + p_0 = gspn.get_place(id_p_0) + assert p_0.get_id() == id_p_0 + + p_1 = gspn.get_place(id_p_1) + assert p_1.get_id() == id_p_1 + assert p_1.get_number_of_initial_tokens() == 1 + + p_2 = gspn.get_place(id_p_2) + assert p_2.get_id() == id_p_2 + assert p_2.get_name() == "place_2" + + p_3 = gspn.get_place(id_p_3) + assert p_3.get_name() == "place_3" + assert p_3.get_capacity() == 2 + assert p_3.get_number_of_initial_tokens() == 3 + assert p_3.has_restricted_capacity() == True + + # test transitions + ti_0 = gspn.get_immediate_transition("ti_0") + assert ti_0.get_id() == id_ti_0 + assert ti_0.get_weight() == 0.5 + assert ti_0.get_priority() == 1 + + tt_0 = gspn.get_timed_transition("tt_0") + assert tt_0.get_id() == id_tt_0 + assert tt_0.get_rate() == 0.4 + assert tt_0.get_priority() == 2 + + tt_1 = gspn.get_timed_transition("tt_1") + assert tt_1.get_id() == id_tt_1 + assert tt_1.get_number_of_servers() == 2 + + # test new name gspn_new_name = "new_name" gspn.set_name(gspn_new_name) assert gspn.get_name() == gspn_new_name @@ -117,35 +146,57 @@ class TestGSPNBuilder: def test_export_to_pnpro(self, tmpdir): builder = stormpy.gspn.GSPNBuilder() builder.set_name("gspn_test") - ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") + + # add places and transitions + id_p_0 = builder.add_place() + id_p_1 = builder.add_place(initialTokens = 3, name = "place_1", capacity = 2) + id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") + id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") + gspn = builder.build_gspn() - # todo add some trans and places (place layout after import?) - # add arcs export_file = os.path.join(str(tmpdir), "gspn.pnpro") - # export gspn to pnpro + # export gspn to pnml gspn.export_gspn_pnpro_file(export_file) # import gspn gspn_parser = stormpy.gspn.GSPNParser() gspn_import = gspn_parser.parse(export_file) + # test imported gspn assert gspn_import.get_name() == gspn.get_name() assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() assert gspn_import.get_number_of_places() == gspn.get_number_of_places() - cp_ti_0 = gspn_import.get_immediate_transition("ti_0") - assert cp_ti_0.get_id() == ti_0 + + p_0 = gspn_import.get_place(id_p_0) + assert p_0.get_id() == id_p_0 + p_1 = gspn_import.get_place(id_p_1) + assert p_1.get_name() == "place_1" + # todo capacity info lost + #assert p_1.get_capacity() == 2 + #assert p_1.has_restricted_capacity() == True + assert p_1.get_number_of_initial_tokens() == 3 + + ti_0 = gspn_import.get_immediate_transition("ti_0") + assert ti_0.get_id() == id_ti_0 + tt_0 = gspn_import.get_timed_transition("tt_0") + assert tt_0.get_id() == id_tt_0 + def test_export_to_pnml(self, tmpdir): builder = stormpy.gspn.GSPNBuilder() builder.set_name("gspn_test") - ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") + + # add places and transitions + id_p_0 = builder.add_place() + id_p_1 = builder.add_place(initialTokens = 3, name = "place_1", capacity = 2) + id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") + id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") + gspn = builder.build_gspn() - # todo add some trans and places (place layout after import?) - # add arcs (cp from above) export_file = os.path.join(str(tmpdir), "gspn.pnml") @@ -156,10 +207,23 @@ class TestGSPNBuilder: gspn_parser = stormpy.gspn.GSPNParser() gspn_import = gspn_parser.parse(export_file) + # test imported gspn assert gspn_import.get_name() == gspn.get_name() assert gspn_import.get_number_of_timed_transitions() == gspn.get_number_of_timed_transitions() assert gspn_import.get_number_of_immediate_transitions() == gspn.get_number_of_immediate_transitions() assert gspn_import.get_number_of_places() == gspn.get_number_of_places() - cp_ti_0 = gspn_import.get_immediate_transition("ti_0") - assert cp_ti_0.get_id() == ti_0 + + p_0 = gspn_import.get_place(id_p_0) + assert p_0.get_id() == id_p_0 + p_1 = gspn_import.get_place(id_p_1) + assert p_1.get_name() == "place_1" + assert p_1.get_capacity() == 2 + assert p_1.get_number_of_initial_tokens() == 3 + assert p_1.has_restricted_capacity() == True + + ti_0 = gspn_import.get_immediate_transition("ti_0") + assert ti_0.get_id() == id_ti_0 + tt_0 = gspn_import.get_timed_transition("tt_0") + assert tt_0.get_id() == id_tt_0 + From 27546c7918cb7c3ad43e5467da43181c7a8a814b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 Apr 2020 17:50:20 +0200 Subject: [PATCH 19/36] Simplified some assertions --- tests/gspn/test_gspn.py | 50 ++++++++++++++++++----------------------- 1 file changed, 22 insertions(+), 28 deletions(-) diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index b840327..8de9073 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -5,7 +5,6 @@ import stormpy from configurations import gspn - @gspn class TestGSPNBuilder: def test_layout_info(self): @@ -25,16 +24,16 @@ class TestGSPNBuilder: def test_place(self): p_id = 4 - place = stormpy.gspn.Place(id = p_id) + place = stormpy.gspn.Place(id=p_id) assert p_id == place.get_id() assert place.has_restricted_capacity() == False - place.set_capacity(cap = 5) + place.set_capacity(cap=5) assert place.has_restricted_capacity() == True assert place.get_capacity() == 5 p_name = "P_0" - place.set_name(name = p_name) + place.set_name(name=p_name) assert place.get_name() == p_name p_tokens = 2 @@ -56,21 +55,20 @@ class TestGSPNBuilder: ti_name = " ti" ti.set_name(ti_name) assert ti_name == ti.get_name() - assert ti.no_weight_attached() == True + assert ti.no_weight_attached() ti_weight = 0.2 ti.set_weight(ti_weight) assert ti_weight == ti.get_weight() - assert ti.no_weight_attached() == False - + assert not ti.no_weight_attached() def test_build_gspn(self): gspn_name = "gspn_test" builder = stormpy.gspn.GSPNBuilder() id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens = 1) - id_p_2 = builder.add_place(initialTokens = 0, name = "place_2") - id_p_3 = builder.add_place(capacity = 2, initialTokens = 3, name = "place_3") + id_p_1 = builder.add_place(initialTokens=1) + id_p_2 = builder.add_place(initialTokens=0, name="place_2") + id_p_3 = builder.add_place(capacity=2, initialTokens=3, name="place_3") p_layout = stormpy.gspn.LayoutInfo(1, 2) builder.set_place_layout_info(id_p_0, p_layout) @@ -84,17 +82,17 @@ class TestGSPNBuilder: builder.set_transition_layout_info(id_ti_0, t_layout) # add arcs - builder.add_input_arc(id_p_0, id_ti_1, multiplicity = 2) - builder.add_input_arc("place_2", "ti_0", multiplicity = 2) + builder.add_input_arc(id_p_0, id_ti_1, multiplicity=2) + builder.add_input_arc("place_2", "ti_0", multiplicity=2) - builder.add_output_arc(id_ti_1, id_p_2, multiplicity = 2) - builder.add_output_arc("tt_0", "place_3", multiplicity = 2) + builder.add_output_arc(id_ti_1, id_p_2, multiplicity=2) + builder.add_output_arc("tt_0", "place_3", multiplicity=2) - builder.add_inhibition_arc(id_p_2, id_tt_0, multiplicity = 2) - builder.add_inhibition_arc("place_3", "tt_0", multiplicity = 2) + builder.add_inhibition_arc(id_p_2, id_tt_0, multiplicity=2) + builder.add_inhibition_arc("place_3", "tt_0", multiplicity=2) - builder.add_normal_arc("place_3", "tt_0", multiplicity = 2) - builder.add_normal_arc("tt_0", "place_3", multiplicity = 2) + builder.add_normal_arc("place_3", "tt_0", multiplicity=2) + builder.add_normal_arc("tt_0", "place_3", multiplicity=2) # test gspn composition builder.set_name(gspn_name) @@ -121,7 +119,7 @@ class TestGSPNBuilder: assert p_3.get_name() == "place_3" assert p_3.get_capacity() == 2 assert p_3.get_number_of_initial_tokens() == 3 - assert p_3.has_restricted_capacity() == True + assert p_3.has_restricted_capacity() # test transitions ti_0 = gspn.get_immediate_transition("ti_0") @@ -149,7 +147,7 @@ class TestGSPNBuilder: # add places and transitions id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens = 3, name = "place_1", capacity = 2) + id_p_1 = builder.add_place(initialTokens=3, name="place_1", capacity=2) id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") @@ -175,8 +173,8 @@ class TestGSPNBuilder: p_1 = gspn_import.get_place(id_p_1) assert p_1.get_name() == "place_1" # todo capacity info lost - #assert p_1.get_capacity() == 2 - #assert p_1.has_restricted_capacity() == True + # assert p_1.get_capacity() == 2 + # assert p_1.has_restricted_capacity() == True assert p_1.get_number_of_initial_tokens() == 3 ti_0 = gspn_import.get_immediate_transition("ti_0") @@ -184,15 +182,13 @@ class TestGSPNBuilder: tt_0 = gspn_import.get_timed_transition("tt_0") assert tt_0.get_id() == id_tt_0 - - def test_export_to_pnml(self, tmpdir): builder = stormpy.gspn.GSPNBuilder() builder.set_name("gspn_test") # add places and transitions id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens = 3, name = "place_1", capacity = 2) + id_p_1 = builder.add_place(initialTokens=3, name="place_1", capacity=2) id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") @@ -219,11 +215,9 @@ class TestGSPNBuilder: assert p_1.get_name() == "place_1" assert p_1.get_capacity() == 2 assert p_1.get_number_of_initial_tokens() == 3 - assert p_1.has_restricted_capacity() == True + assert p_1.has_restricted_capacity() ti_0 = gspn_import.get_immediate_transition("ti_0") assert ti_0.get_id() == id_ti_0 tt_0 = gspn_import.get_timed_transition("tt_0") assert tt_0.get_id() == id_tt_0 - - From 019c8ba91284619d45d0df0ea5cfc2d6c5e93a02 Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 19 Apr 2020 13:48:14 +0200 Subject: [PATCH 20/36] added missing Transition class methods --- src/gspn/gspn.cpp | 27 +++++++++++++++++++++++++-- tests/gspn/test_gspn.py | 28 ++++++++++++++++++++++++++-- 2 files changed, 51 insertions(+), 4 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 8c90b81..9eede02 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -130,9 +130,32 @@ void define_gspn(py::module& m) { .def("get_id", &Transition::getID, "Get id of this transition") .def("set_name", &Transition::setName, "name"_a, "Set name of this transition") .def("get_name", &Transition::getName, "Get name of this transition") - .def("set_priority", &Transition::getID, "Get priority of this transition") + .def("set_priority", &Transition::setPriority, "priority"_a, "Set priority of this transition") .def("get_priority", &Transition::getPriority, "Get priority of this transition") - // todo add missing + + .def("set_input_arc_multiplicity", &Transition::setInputArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the input arc originating from the place.") + .def("remove_input_arc", &Transition::removeInputArc, "place"_a, "Remove an input arc connected to a given place.") + .def("exists_input_arc", &Transition::existsInputArc, "place"_a, "Check whether the given place is connected to this transition via an input arc.") + + .def("set_output_arc_multiplicity", &Transition::setOutputArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the output arc going to the place.") + .def("remove_output_arc", &Transition::removeOutputArc, "place"_a, "Remove an output arc connected to a given place.") + .def("exists_output_arc", &Transition::existsOutputArc, "place"_a, "Check whether the given place is connected to this transition via an output arc.") + + .def("set_inhibition_arc_multiplicity", &Transition::setInhibitionArcMultiplicity, "place"_a, "multiplicity"_a, "Set the multiplicity of the inhibition arc originating from the place.") + .def("remove_inhibition_arc", &Transition::removeInhibitionArc, "place"_a, "Remove an inhibition arc connected to a given place.") + .def("exists_inhibition_arc", &Transition::existsInhibitionArc, "place"_a, "Check whether the given place is connected to this transition via an inhibition arc.") + + .def("get_input_places", &Transition::getInputPlaces) + .def("get_output_places", &Transition::getOutputPlaces) + .def("get_inhibition_places", &Transition::getInhibitionPlaces) + + .def("get_input_arc_multiplicity", &Transition::getInputArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") + .def("get_inhibition_arc_multiplicity", &Transition::getInhibitionArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") + .def("get_output_arc_multiplicity", &Transition::getOutputArcMultiplicity, "place"_a, "Returns the corresponding multiplicity.") + + .def("is_enabled", &Transition::isEnabled, "marking"_a, "Check if the given marking enables the transition.") + .def("fire", &Transition::fire, "marking"_a, "Fire the transition if possible.") + ; // TimedTransition class diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index 8de9073..d94f005 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -27,9 +27,9 @@ class TestGSPNBuilder: place = stormpy.gspn.Place(id=p_id) assert p_id == place.get_id() - assert place.has_restricted_capacity() == False + assert not place.has_restricted_capacity() place.set_capacity(cap=5) - assert place.has_restricted_capacity() == True + assert place.has_restricted_capacity() assert place.get_capacity() == 5 p_name = "P_0" @@ -50,6 +50,30 @@ class TestGSPNBuilder: tt.set_rate(tt_rate) assert tt_rate == tt.get_rate() + # connect a place to this transition and test arcs + place = stormpy.gspn.Place(0) + # test input arcs + assert not tt.exists_input_arc(place) + tt.set_input_arc_multiplicity(place, 2) + assert tt.exists_input_arc(place) + assert tt.get_input_arc_multiplicity(place) == 2 + tt.remove_input_arc(place) + assert not tt.exists_input_arc(place) + # test output arcs + assert not tt.exists_output_arc(place) + tt.set_output_arc_multiplicity(place, 3) + assert tt.exists_output_arc(place) + assert tt.get_output_arc_multiplicity(place) == 3 + tt.remove_output_arc(place) + assert not tt.exists_output_arc(place) + # test inhibition arcs + assert not tt.exists_inhibition_arc(place) + tt.set_inhibition_arc_multiplicity(place, 5) + assert tt.exists_inhibition_arc(place) + assert tt.get_inhibition_arc_multiplicity(place) == 5 + tt.remove_inhibition_arc(place) + assert not tt.exists_inhibition_arc(place) + # test ImmediateTransition ti = stormpy.gspn.ImmediateTransition() ti_name = " ti" From 42e0774d831bbce1fb4b41d8efd9ebf93b11e33b Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 19 Apr 2020 16:16:17 +0200 Subject: [PATCH 21/36] documentation for gspn bindings --- doc/source/advanced_topics.rst | 3 ++- doc/source/api.rst | 1 + doc/source/api/gspn.rst | 7 +++++++ doc/source/doc/gspns.rst | 9 +++++++++ src/gspn/gspn.cpp | 33 ++++++++++++++++----------------- 5 files changed, 35 insertions(+), 18 deletions(-) create mode 100644 doc/source/api/gspn.rst create mode 100644 doc/source/doc/gspns.rst diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 55de824..9d2d225 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -16,4 +16,5 @@ This guide is a collection of examples meant to bridge the gap between the getti doc/schedulers doc/shortest_paths doc/parametric_models - doc/dfts \ No newline at end of file + doc/dfts + doc/gspns diff --git a/doc/source/api.rst b/doc/source/api.rst index f9144c4..22e0df0 100644 --- a/doc/source/api.rst +++ b/doc/source/api.rst @@ -14,4 +14,5 @@ Work in progress! api/utility api/dft + api/gspn api/pars diff --git a/doc/source/api/gspn.rst b/doc/source/api/gspn.rst new file mode 100644 index 0000000..d752360 --- /dev/null +++ b/doc/source/api/gspn.rst @@ -0,0 +1,7 @@ +Stormpy.gspn +************************** + +.. automodule:: stormpy.gspn + :members: + :undoc-members: + :imported-members: diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst new file mode 100644 index 0000000..2726653 --- /dev/null +++ b/doc/source/doc/gspns.rst @@ -0,0 +1,9 @@ +******************* +Generalized Stochastic Petri Nets +******************* + + +Building GSPNs +============= +TODO + diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 9eede02..5e5c36e 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -42,17 +42,17 @@ void define_gspn(py::module& m) { .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("place_id"), py::arg("layout_info")) - .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Adds an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Add an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") - .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") - .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "Adds an timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "set transition layout information", "transitionId"_a, "layoutInfo"_a) + .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") + .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "Set transition layout information", "transitionId"_a, "layoutInfo"_a) - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a) - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a) - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add an new input arc from a place to an transition") + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new output arc from a place to an transition") .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", "from"_a, "to"_a, "multiplicity"_a = 1) @@ -79,11 +79,11 @@ void define_gspn(py::module& m) { .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the number of timed transitions in this GSPN") - .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a) - .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) - .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a) - .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a) - .def("get_transition",[](GSPN const& g, std::string const& name) -> const Transition& {return *(g.getTransition(name)); }, "name"_a) + .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a, "Returns the place with the corresponding id") + .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a, "Returns the place with the corresponding name") + .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a, "Returns the timed transition with the corresponding name") + .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a, "Returns the immediate transition with the corresponding name") + .def("get_transition",[](GSPN const& g, std::string const& name) -> const Transition& {return *(g.getTransition(name)); }, "name"_a, "Returns the transition with the corresponding name") .def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") .def("get_places", &GSPN::getPlaces, "Get the places of this GSPN") @@ -91,15 +91,14 @@ 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") - //todo tests: .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) // GSPN export - .def("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnpro"); }, "filepath"_a) - .def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, "to-pnml"); }, "filepath"_a) + .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") ; // LayoutInfo class From 339781db4a752715c57f648928e325bc464c9466 Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 21 Apr 2020 22:07:29 +0200 Subject: [PATCH 22/36] created gspn example --- examples/gspns/01-gspns.py | 56 +++++++++++++++++++ lib/stormpy/examples/files.py | 2 + .../examples/files/gspn/gspn_simple.pnpro | 16 ++++++ 3 files changed, 74 insertions(+) create mode 100644 examples/gspns/01-gspns.py create mode 100644 lib/stormpy/examples/files/gspn/gspn_simple.pnpro diff --git a/examples/gspns/01-gspns.py b/examples/gspns/01-gspns.py new file mode 100644 index 0000000..2b2f273 --- /dev/null +++ b/examples/gspns/01-gspns.py @@ -0,0 +1,56 @@ +import stormpy +import stormpy.gspn + +import stormpy.examples +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 + gspn_parser = stormpy.gspn.GSPNParser() + gspn_import = gspn_parser.parse(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())) + + +if __name__ == '__main__': + example_gspns_01() diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 1a0c3b5..6fead05 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -41,3 +41,5 @@ dft_galileo_hecs = _path("dft", "hecs.dft") """DFT example for HECS (Galileo format)""" 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)""" diff --git a/lib/stormpy/examples/files/gspn/gspn_simple.pnpro b/lib/stormpy/examples/files/gspn/gspn_simple.pnpro new file mode 100644 index 0000000..6f5008e --- /dev/null +++ b/lib/stormpy/examples/files/gspn/gspn_simple.pnpro @@ -0,0 +1,16 @@ + + + + + + + + + + + + + + + + From c014234e7763cf949e1d81ff79aeea3812c877f7 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 23 Apr 2020 21:56:55 +0200 Subject: [PATCH 23/36] added content to the gspn documentation --- doc/source/doc/gspns.rst | 87 +++++++++++- examples/gspns/01-gspns.py | 49 +------ examples/gspns/02-gspns.py | 53 +++++++ lib/stormpy/examples/files.py | 2 + .../examples/files/gspn/gspn_simple.pnml | 130 ++++++++++++++++++ .../examples/files/gspn/gspn_simple.pnpro | 18 +-- src/gspn/gspn.cpp | 11 +- tests/gspn/test_gspn.py | 1 + 8 files changed, 292 insertions(+), 59 deletions(-) create mode 100644 examples/gspns/02-gspns.py create mode 100644 lib/stormpy/examples/files/gspn/gspn_simple.pnml 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 From c076609c34ec2608f396e2f5b53c10e371ad2a0d Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 24 Apr 2020 15:33:56 +0200 Subject: [PATCH 24/36] small correction in gspn doc --- doc/source/doc/gspns.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst index 9094432..740db79 100644 --- a/doc/source/doc/gspns.rst +++ b/doc/source/doc/gspns.rst @@ -43,9 +43,10 @@ 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") + >>> 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:: +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) @@ -79,8 +80,7 @@ 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)``. +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 From efabfd0cbef1aefe1ae0a08bad8420752369c174 Mon Sep 17 00:00:00 2001 From: hannah Date: Mon, 27 Apr 2020 15:07:53 +0200 Subject: [PATCH 25/36] completed documentation and added some testcases --- doc/source/doc/gspns.rst | 11 ++--- src/gspn/gspn.cpp | 90 +++++++++++++++++++++++++++++++++------- tests/gspn/test_gspn.py | 4 ++ 3 files changed, 84 insertions(+), 21 deletions(-) diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst index 740db79..e02769e 100644 --- a/doc/source/doc/gspns.rst +++ b/doc/source/doc/gspns.rst @@ -6,11 +6,11 @@ Loading GSPNs ============== .. - .. seealso:: `01-gspn.py `_ + .. seealso:: `01-gspn.py `_ .. -Generalized stochastic Petri nets can be given in either in the PNPRO format or in the PNML format. +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 @@ -36,7 +36,7 @@ After loading, we can display some properties of the GSPN:: Building GSPNs ============================= .. - todo .. seealso:: `02-gspn.py `_ + todo .. seealso:: `02-gspn.py `_ .. In the following, we describe how to construct GSPNs via the GSPNBuilder. @@ -52,7 +52,7 @@ Additionally, we define the position of the transition by setting its layout inf >>> 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:: +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) @@ -68,7 +68,8 @@ Next, we add two places to the GSPN and set their layouts:: >>> 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:: +Places and transitions can be linked by output, inhibition or input 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) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 176ca22..378a626 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -40,21 +40,62 @@ void define_gspn(py::module& m) { .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") - .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, "Set place layout information", py::arg("place_id"), py::arg("layout_info")) + .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, py::arg("place_id"), py::arg("layout_info"), R"doc( + Set place layout information. - .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Add an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") + :param uint64_t id: The ID of the place. + :param stormpy.LayoutInfo layout_info: The layout information. + )doc") + .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Add an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") - .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "Set transition layout information", "transitionId"_a, "layoutInfo"_a) - - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") - .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add an new input arc from a place to an transition") - .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new input arc from a place to an transition") - .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a = 1, "Add a new output arc from a place to an transition") + .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "transitionId"_a, "layoutInfo"_a, R"doc( + Set transition layout information. + + :param uint64_t id: The ID of the transition. + :param stormpy.LayoutInfo layout_info: The layout information. + )doc") + + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a , "to"_a, "multiplicity"_a = 1, R"doc( + Add a new input arc from a place to a transition + + :param from: The ID or name of the place from which the arc is originating. + :type from: uint_64_t or str + :param uint_64_t to: The ID or name of the transition to which the arc goes to. + :type from: uint_64_t or str + :param uint64_t multiplicity: The multiplicity of the arc, default = 1. + )doc") + .def("add_input_arc", py::overload_cast(&GSPNBuilder::addInputArc), "from"_a, "to"_a, "multiplicity"_a = 1) + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( + Add an new inhibition arc from a place to a transition. + + :param from: The ID or name of the place from which the arc is originating. + :type from: uint_64_t or str + :param to: The ID or name of the transition to which the arc goes to. + :type to: uint_64_t or str + :param uint64_t multiplicity: The multiplicity of the arc, default = 1. + )doc") + .def("add_inhibition_arc", py::overload_cast(&GSPNBuilder::addInhibitionArc), "from"_a, "to"_a, "multiplicity"_a = 1) + .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( + Add an new output arc from a transition to a place. + + :param from: The ID or name of the transition from which the arc is originating. + :type from: uint_64_t or str + :param to: The ID or name of the place to which the arc goes to. + :type to: uint_64_t or str + :param uint64_t multiplicity: The multiplicity of the arc, default = 1. + )doc") .def("add_output_arc", py::overload_cast(&GSPNBuilder::addOutputArc), "from"_a, "to"_a, "multiplicity"_a) - .def("add_normal_arc", &GSPNBuilder::addNormalArc, "Add normal arc from a named element to a named element", "from"_a, "to"_a, "multiplicity"_a = 1) + .def("add_normal_arc", &GSPNBuilder::addNormalArc, "from"_a, "to"_a, "multiplicity"_a = 1, R"doc( + Add an arc from a named element to a named element. + Can be both input or output arc, but not an inhibition arc. + Convenience function for textual format parsers. + + :param str from: Source element in the GSPN from where this arc starts. + :param str to: Target element in the GSPN where this arc ends. + :param uint64_t multiplicity: Multiplicity of the arc, default = 1. + )doc") .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", "exprManager"_a = nullptr, "constantsSubstitution"_a = std::map()) ; @@ -79,16 +120,33 @@ void define_gspn(py::module& m) { .def("get_number_of_immediate_transitions", &GSPN::getNumberOfImmediateTransitions, "Get the number of immediate transitions in this GSPN") .def("get_number_of_timed_transitions", &GSPN::getNumberOfTimedTransitions, "Get the number of timed transitions in this GSPN") - .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a, "Returns the place with the corresponding id") - .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a, "Returns the place with the corresponding name") + .def("get_place", [](GSPN const& g, uint64_t id) -> const Place& {return *(g.getPlace(id)); }, "id"_a, R"doc( + Returns the place with the corresponding id. + + :param uint64_t id: The ID of the place. + :rtype: stormpy.Place + )doc") + .def("get_place", [](GSPN const& g, std::string const& name) -> const Place& {return *(g.getPlace(name)); }, "name"_a) .def("get_timed_transition", [](GSPN const& g, std::string const& name) -> const TimedTransition& {return *(g.getTimedTransition(name)); }, "name"_a, "Returns the timed transition with the corresponding name") .def("get_immediate_transition", [](GSPN const& g, std::string const& name) -> const ImmediateTransition& {return *(g.getImmediateTransition(name)); }, "name"_a, "Returns the immediate transition with the corresponding name") .def("get_transition",[](GSPN const& g, std::string const& name) -> const Transition& {return *(g.getTransition(name)); }, "name"_a, "Returns the transition with the corresponding name") .def("get_partitions", &GSPN::getPartitions, "Get the partitions of this GSPN") - .def("get_places", &GSPN::getPlaces, "Get the places of this GSPN") - .def("get_timed_transitions", &GSPN::getTimedTransitions, "Get the timed transitions of this GSPN") - .def("get_immediate_transitions", &GSPN::getImmediateTransitions, "Get the immediate transitions of this GSPN") + .def("get_places", &GSPN::getPlaces, R"doc( + Returns a vector of the places of this GSPN. + + :rtype: list[stormpy.Place] + )doc") + .def("get_timed_transitions", &GSPN::getTimedTransitions, R"doc( + Returns a vector of the timed transitions of this GSPN. + + :rtype: list[stormpy.TimedTransition] + )doc") + .def("get_immediate_transitions", &GSPN::getImmediateTransitions, R"doc( + Returns the immediate transitions of this GSPN. + + :rtype: list[stormpy.ImmediateTransition] + )doc") .def("get_initial_marking", &GSPN::getInitialMarking, "Computes the initial marking of this GSPN") .def("is_valid", &GSPN::isValid, "Perform some checks") diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index c18a9a1..cd797b6 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -128,6 +128,10 @@ class TestGSPNBuilder: assert gspn.get_number_of_timed_transitions() == 2 assert gspn.get_number_of_places() == 4 + assert len(gspn.get_places()) == 4 + assert len(gspn.get_immediate_transitions()) == 2 + assert len(gspn.get_timed_transitions()) == 2 + # test places p_0 = gspn.get_place(id_p_0) assert p_0.get_id() == id_p_0 From 80787fb3d802288ed5c59534a88e0d18d64bad38 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 May 2020 17:01:44 +0200 Subject: [PATCH 26/36] Consistently use Python naming scheme --- src/gspn/gspn.cpp | 26 +++++++++++++------------- tests/gspn/test_gspn.py | 18 +++++++++--------- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp index 378a626..a9b64de 100644 --- a/src/gspn/gspn.cpp +++ b/src/gspn/gspn.cpp @@ -18,14 +18,14 @@ using TransitionPartition = storm::gspn::TransitionPartition; using GSPNParser = storm::parser::GspnParser; -void gspnToFile(GSPN const& gspn, std::string const& filepath, std::string const& option) { +void gspnToFile(GSPN const& gspn, std::string const& filepath, bool toPnpro) { std::ofstream fs; storm::utility::openFile(filepath, fs); - if(option == "to-pnpro") { + if(toPnpro) { gspn.toPnpro(fs); } - else if (option == "to-pnml"){ + else { gspn.toPnml(fs); } storm::utility::closeFile(fs); @@ -39,7 +39,7 @@ void define_gspn(py::module& m) { .def(py::init(), "Constructor") .def("set_name", &GSPNBuilder::setGspnName, "Set name of GSPN", "name"_a) - .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initialTokens") = 0, py::arg("name") = "") + .def("add_place", &GSPNBuilder::addPlace, "Add a place to the GSPN", py::arg("capacity") = 1, py::arg("initial_tokens") = 0, py::arg("name") = "") .def("set_place_layout_info", &GSPNBuilder::setPlaceLayoutInfo, py::arg("place_id"), py::arg("layout_info"), R"doc( Set place layout information. @@ -49,8 +49,8 @@ void define_gspn(py::module& m) { .def("add_immediate_transition", &GSPNBuilder::addImmediateTransition, "Add an immediate transition to the GSPN", "priority"_a = 0, "weight"_a = 0, "name"_a = "") .def("add_timed_transition", py::overload_cast(&GSPNBuilder::addTimedTransition), "Add a timed transition to the GSPN", "priority"_a, "rate"_a, "name"_a = "") - .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "priority"_a, "rate"_a, "numServers"_a, "name"_a = "") - .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "transitionId"_a, "layoutInfo"_a, R"doc( + .def("add_timed_transition", py::overload_cast const&, std::string const&>(&GSPNBuilder::addTimedTransition), "priority"_a, "rate"_a, "num_servers"_a, "name"_a = "") + .def("set_transition_layout_info", &GSPNBuilder::setTransitionLayoutInfo, "transition_id"_a, "layout_info"_a, R"doc( Set transition layout information. :param uint64_t id: The ID of the transition. @@ -97,21 +97,21 @@ void define_gspn(py::module& m) { :param uint64_t multiplicity: Multiplicity of the arc, default = 1. )doc") - .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", "exprManager"_a = nullptr, "constantsSubstitution"_a = std::map()) + .def("build_gspn", &GSPNBuilder::buildGspn, "Construct GSPN", "expression_manager"_a = nullptr, "constants_substitution"_a = std::map()) ; // GspnParser class py::class_>(m, "GSPNParser") .def(py::init<>()) - .def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& {return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constantDefinitions"_a = "") + .def("parse", [](GSPNParser& p, std::string const& filename, std::string const& constantDefinitions) -> GSPN& {return *(p.parse(filename,constantDefinitions)); }, "filename"_a, "constant_definitions"_a = "") ; // GSPN class py::class_>(m, "GSPN", "Generalized Stochastic Petri Net") // Constructor - .def(py::init const& , std::vector const& , - std::vector const& , std::vector const& , std::shared_ptr const& , std::map const& > (), "name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map()) + .def(py::init const&, std::vector const&, + std::vector const&, std::vector const&, std::shared_ptr const&, std::map const&>(), "name"_a, "places"_a, "immediate_transitions"_a, "timed_transitions"_a, "partitions"_a, "expression_manager"_a, "constants_substitution"_a = std::map()) .def("get_name", &GSPN::getName, "Get name of GSPN") .def("set_name", &GSPN::setName, "Set name of GSPN") @@ -152,8 +152,8 @@ void define_gspn(py::module& m) { .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("export_gspn_pnpro_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, true); }, "filepath"_a, "Export GSPN to PNPRO file") + .def("export_gspn_pnml_file", [](GSPN& g, std::string const& filepath) -> void { gspnToFile(g, filepath, false); }, "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) diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index cd797b6..a89142e 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -27,7 +27,7 @@ class TestGSPNBuilder: place = stormpy.gspn.Place(id=p_id) assert p_id == place.get_id() - assert not place.has_restricted_capacity() + assert not place.has_restricted_capacity() place.set_capacity(cap=5) assert place.has_restricted_capacity() assert place.get_capacity() == 5 @@ -90,9 +90,9 @@ class TestGSPNBuilder: builder = stormpy.gspn.GSPNBuilder() id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens=1) - id_p_2 = builder.add_place(initialTokens=0, name="place_2") - id_p_3 = builder.add_place(capacity=2, initialTokens=3, name="place_3") + id_p_1 = builder.add_place(initial_tokens=1) + id_p_2 = builder.add_place(initial_tokens=0, name="place_2") + id_p_3 = builder.add_place(capacity=2, initial_tokens=3, name="place_3") p_layout = stormpy.gspn.LayoutInfo(1, 2) builder.set_place_layout_info(id_p_0, p_layout) @@ -100,7 +100,7 @@ class TestGSPNBuilder: id_ti_1 = builder.add_immediate_transition() id_tt_0 = builder.add_timed_transition(priority=2, rate=0.4, name="tt_0") - id_tt_1 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_1") + id_tt_1 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_1") t_layout = stormpy.gspn.LayoutInfo(1, 2) builder.set_transition_layout_info(id_ti_0, t_layout) @@ -176,9 +176,9 @@ class TestGSPNBuilder: # add places and transitions id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens=3, name="place_1", capacity=2) + id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2) id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") - id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") + id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0") gspn = builder.build_gspn() @@ -217,9 +217,9 @@ class TestGSPNBuilder: # add places and transitions id_p_0 = builder.add_place() - id_p_1 = builder.add_place(initialTokens=3, name="place_1", capacity=2) + id_p_1 = builder.add_place(initial_tokens=3, name="place_1", capacity=2) id_ti_0 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_0") - id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, numServers=2, name="tt_0") + id_tt_0 = builder.add_timed_transition(priority=0, rate=0.5, num_servers=2, name="tt_0") gspn = builder.build_gspn() From 42d2f1be01cc6b6ecc08340d28a42eed26fbf702 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 May 2020 17:10:18 +0200 Subject: [PATCH 27/36] Small revision in GSPN doc --- doc/source/doc/gspns.rst | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst index e02769e..1af0fae 100644 --- a/doc/source/doc/gspns.rst +++ b/doc/source/doc/gspns.rst @@ -4,10 +4,7 @@ Generalized Stochastic Petri Nets Loading GSPNs ============== - -.. - .. seealso:: `01-gspn.py `_ -.. +.. seealso:: `01-gspn.py `_ Generalized stochastic Petri nets can be given either in the PNPRO format or in the PNML format. @@ -35,12 +32,10 @@ After loading, we can display some properties of the GSPN:: Building GSPNs ============================= -.. - todo .. seealso:: `02-gspn.py `_ -.. +.. 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:: +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") @@ -68,7 +63,7 @@ Next, we add two places to the GSPN and set their layouts:: >>> 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. +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) @@ -80,7 +75,7 @@ We can now build the GSPN:: >>> gspn = builder.build_gspn() -After building, we can export the 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:: From e2e7919427f4815585e61a427b7abd1070c5f218 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 May 2020 19:34:27 +0200 Subject: [PATCH 28/36] Fixed links in GSPN doc --- doc/source/doc/gspns.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/source/doc/gspns.rst b/doc/source/doc/gspns.rst index 1af0fae..f5847e6 100644 --- a/doc/source/doc/gspns.rst +++ b/doc/source/doc/gspns.rst @@ -4,7 +4,7 @@ Generalized Stochastic Petri Nets Loading GSPNs ============== -.. seealso:: `01-gspn.py `_ +.. seealso:: `01-gspns.py `_ Generalized stochastic Petri nets can be given either in the PNPRO format or in the PNML format. @@ -32,7 +32,7 @@ After loading, we can display some properties of the GSPN:: Building GSPNs ============================= -.. seealso:: `02-gspn.py `_ +.. seealso:: `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:: From 2059add7cdfad0cec093fec01e4f2c103b497128 Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 8 Apr 2020 11:17:29 +0200 Subject: [PATCH 29/36] SparseMatrixBuilder class --- src/storage/matrix.cpp | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index a0d87b3..21da419 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -6,6 +6,7 @@ #include "src/helpers.h" template using SparseMatrix = storm::storage::SparseMatrix; +template using SparseMatrixBuilder = storm::storage::SparseMatrixBuilder; template using entry_index = typename storm::storage::SparseMatrix::index_type; template using MatrixEntry = storm::storage::MatrixEntry, ValueType>; using RationalFunction = storm::RationalFunction; @@ -30,6 +31,42 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("column", &MatrixEntry::getColumn, "Column") ; + // SparseMatrixBuilder + py::class_>(m, "SparseMatrixBuilder", "Builder of sparse matrix") + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "forceDimensions"_a = true, "hasCustomRowGrouping"_a = false, "rowGroups"_a = 0) + + .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( + + Sets the matrix entry at the given row and column to the given value. After all entries have been added, + a call to finalize(false) is mandatory. + + Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and + column by column. As multiple entries per column are admitted, consecutive calls to this method are + admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are + treated as empty. If these constraints are not met, an exception is thrown. + + :param double row: The row in which the matrix entry is to be set + :param double column: The column in which the matrix entry is to be set + :param double const& value: The value that is to be set at the specified row and column + )dox", py::arg("row"), py::arg("column"), py::arg("value")) + + .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overriddenRowCount") = 0, py::arg("overriddenColumnCount") = 0, py::arg("overriddenRowGroupCount") = 0, "Finalize the sparse matrix") + .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") + .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") + .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") + .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( + + Replaces all columns with id >= offset according to replacements. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + + :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i + :param double offset: Offset to add to each id in vector index. + )dox", py::arg("replacements"), py::arg("offset")) + ; + + // todo py::class_>(m, "SparseMatrixBuilder", "Builder of parametric sparse matrix") + // SparseMatrix py::class_>(m, "SparseMatrix", "Sparse matrix") .def("__iter__", [](SparseMatrix& matrix) { From b3d99eae89074cb3261644ab2ddaefa0dbf5741f Mon Sep 17 00:00:00 2001 From: hannah Date: Wed, 8 Apr 2020 17:26:35 +0200 Subject: [PATCH 30/36] convert numpy to SparseMatrix, tests --- lib/stormpy/storage/__init__.py | 27 ++++++- src/storage/matrix.cpp | 4 +- tests/storage/test_matrix_builder.py | 102 +++++++++++++++++++++++++++ 3 files changed, 130 insertions(+), 3 deletions(-) create mode 100644 tests/storage/test_matrix_builder.py diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 60c473c..93188a0 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,4 +1,29 @@ - import stormpy.utility from . import storage from .storage import * + + +def build_sparse_matrix(array, row_group_indices=[]): + """ + Build a sparse matrix from numpy array. + + :param numpy array: The array. + :param List[double] row_group_indices: List containing the starting row of each row group. + :return: Sparse matrix. + """ + num_row = array.shape[0] + num_col = array.shape[1] + + if 0 < len(row_group_indices): + builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, + row_groups=len(row_group_indices)) + else: + builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col) + + for r in range(num_row): + if r in row_group_indices: + builder.new_row_group(r) + for c in range(num_col): + builder.add_next_value(r, c, array[r, c]) + + return builder.build() diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 21da419..6149e37 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -33,7 +33,7 @@ void define_sparse_matrix(py::module& m) { // SparseMatrixBuilder py::class_>(m, "SparseMatrixBuilder", "Builder of sparse matrix") - .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "forceDimensions"_a = true, "hasCustomRowGrouping"_a = false, "rowGroups"_a = 0) + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( @@ -51,7 +51,7 @@ void define_sparse_matrix(py::module& m) { )dox", py::arg("row"), py::arg("column"), py::arg("value")) .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") - .def("build", &SparseMatrixBuilder::build, py::arg("overriddenRowCount") = 0, py::arg("overriddenColumnCount") = 0, py::arg("overriddenRowGroupCount") = 0, "Finalize the sparse matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py new file mode 100644 index 0000000..769876a --- /dev/null +++ b/tests/storage/test_matrix_builder.py @@ -0,0 +1,102 @@ +import stormpy +import numpy as np +from helpers.helper import get_example_path + +import math + + +class TestMatrixBuilder: + def test_matrix_builder(self): + builder = stormpy.SparseMatrixBuilder(force_dimensions=True) + matrix = builder.build() + assert matrix.nr_columns == 0 + assert matrix.nr_rows == 0 + assert matrix.nr_entries == 0 + + builder_5x5 = stormpy.SparseMatrixBuilder(5, 5, force_dimensions=False) + + builder_5x5.add_next_value(0, 0, 0) + builder_5x5.add_next_value(0, 2, 1) + + builder_5x5.add_next_value(2, 0, 4) + builder_5x5.add_next_value(2, 3, 5) + + assert builder_5x5.get_last_column() == 3 + assert builder_5x5.get_last_row() == 2 + + builder_5x5.add_next_value(3, 1, 0.5) + builder_5x5.add_next_value(3, 3, 0) + + builder_5x5.add_next_value(4, 4, 0.2) + + matrix_5x5 = builder_5x5.build() + + assert matrix_5x5.nr_columns == 5 + assert matrix_5x5.nr_rows == 5 + assert matrix_5x5.nr_entries == 7 + + # todo test Replace columns + # builder_5x5.replace_columns... + + def test_matrix_builder_row_grouping(self): + + num_rows = 5 + builder = stormpy.SparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) + + builder.new_row_group(1) + assert builder.get_current_row_group_count() == 1 + + builder.new_row_group(4) + assert builder.get_current_row_group_count() == 2 + matrix = builder.build() + + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 4 + + assert matrix.get_row_group_start(1) == 4 + assert matrix.get_row_group_end(1) == 5 + + def test_matrix_from_numpy(self): + array = np.array([[0, 2], + [3, 4], + [0.1, 24], + [-0.3, -4]], dtype='float64') + + matrix = stormpy.build_sparse_matrix(array) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + + def test_matrix_from_numpy_row_grouping(self): + array = np.array([[0, 2], + [3, 4], + [0.1, 24], + [-0.3, -4]], dtype='float64') + + matrix = stormpy.build_sparse_matrix(array, row_group_indices=[1, 3]) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + + # Check row groups + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 3 + + assert matrix.get_row_group_start(1) == 3 + assert matrix.get_row_group_end(1) == 4 From bfce55912df3dd45da0fc61ad718d4fe18cadc68 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 9 Apr 2020 01:41:43 +0200 Subject: [PATCH 31/36] added tests --- tests/storage/test_matrix_builder.py | 48 ++++++++++++++++++++-------- 1 file changed, 35 insertions(+), 13 deletions(-) diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index 769876a..ca0eaec 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -1,8 +1,5 @@ import stormpy import numpy as np -from helpers.helper import get_example_path - -import math class TestMatrixBuilder: @@ -16,18 +13,16 @@ class TestMatrixBuilder: builder_5x5 = stormpy.SparseMatrixBuilder(5, 5, force_dimensions=False) builder_5x5.add_next_value(0, 0, 0) - builder_5x5.add_next_value(0, 2, 1) - - builder_5x5.add_next_value(2, 0, 4) - builder_5x5.add_next_value(2, 3, 5) + builder_5x5.add_next_value(0, 1, 0.1) + builder_5x5.add_next_value(2, 2, 22) + builder_5x5.add_next_value(2, 3, 23) assert builder_5x5.get_last_column() == 3 assert builder_5x5.get_last_row() == 2 - builder_5x5.add_next_value(3, 1, 0.5) - builder_5x5.add_next_value(3, 3, 0) - - builder_5x5.add_next_value(4, 4, 0.2) + builder_5x5.add_next_value(3, 2, 32) + builder_5x5.add_next_value(3, 4, 34) + builder_5x5.add_next_value(4, 3, 43) matrix_5x5 = builder_5x5.build() @@ -35,8 +30,35 @@ class TestMatrixBuilder: assert matrix_5x5.nr_rows == 5 assert matrix_5x5.nr_entries == 7 - # todo test Replace columns - # builder_5x5.replace_columns... + for e in matrix_5x5: + assert (e.value() == 0.1 and e.column == 1) or e.value() == 0 or (e.value() > 20 and e.column > 1) + + def test_matrix_replace_columns(self): + builder = stormpy.SparseMatrixBuilder(3, 4, force_dimensions=False) + + builder.add_next_value(0, 0, 0) + builder.add_next_value(0, 1, 1) + builder.add_next_value(0, 2, 2) + builder.add_next_value(0, 3, 3) + + builder.add_next_value(1, 1, 1) + builder.add_next_value(1, 2, 2) + builder.add_next_value(1, 3, 3) + + builder.add_next_value(2, 1, 1) + builder.add_next_value(2, 2, 2) + builder.add_next_value(2, 3, 3) + + # replace rows + builder.replace_columns([3, 2, 1], 1) + matrix = builder.build() + + assert matrix.nr_entries == 10 + + # Check if columns where replaced + for e in matrix: + assert (e.value() == 0 and e.column == 0) or (e.value() == 3 and e.column == 1) or ( + e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) def test_matrix_builder_row_grouping(self): From e5a15eac6ef155901b14350f57f1863ac370903f Mon Sep 17 00:00:00 2001 From: hannah Date: Sat, 25 Apr 2020 14:43:27 +0200 Subject: [PATCH 32/36] Parametric sparse matrix builder and tests --- lib/stormpy/storage/__init__.py | 44 +++++++- src/storage/matrix.cpp | 35 +++++- tests/storage/test_matrix_builder.py | 153 ++++++++++++++++++++++++++- 3 files changed, 225 insertions(+), 7 deletions(-) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 93188a0..768dadc 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -8,22 +8,60 @@ def build_sparse_matrix(array, row_group_indices=[]): Build a sparse matrix from numpy array. :param numpy array: The array. - :param List[double] row_group_indices: List containing the starting row of each row group. + :param List[double] row_group_indices: List containing the starting row of each row group in ascending order. :return: Sparse matrix. """ + num_row = array.shape[0] num_col = array.shape[1] - if 0 < len(row_group_indices): + len_group_indices = len(row_group_indices) + if len_group_indices > 0: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, row_groups=len(row_group_indices)) else: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col) + row_group_index = 0 for r in range(num_row): - if r in row_group_indices: + # check whether to start a custom row group + if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: builder.new_row_group(r) + row_group_index += 1 + # insert values of the current row for c in range(num_col): builder.add_next_value(r, c, array[r, c]) return builder.build() + +def build_parametric_sparse_matrix(array, row_group_indices=[]): + """ + Build a sparse matrix from numpy array. + + :param numpy array: The array. + :param List[double] row_group_indices: List containing the starting row of each row group in ascending order. + :return: Parametric sparse matrix. + """ + + num_row = array.shape[0] + num_col = array.shape[1] + + len_group_indices = len(row_group_indices) + if len_group_indices > 0: + builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, + row_groups=len(row_group_indices)) + else: + builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col) + + row_group_index = 0 + for r in range(num_row): + # check whether to start a custom row group + if row_group_index < len_group_indices and r == row_group_indices[row_group_index]: + builder.new_row_group(r) + row_group_index += 1 + # insert values of the current row + for c in range(num_col): + builder.add_next_value(r, c, array[r, c]) + + return builder.build() + diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 6149e37..d39224b 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -63,9 +63,40 @@ void define_sparse_matrix(py::module& m) { :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i :param double offset: Offset to add to each id in vector index. )dox", py::arg("replacements"), py::arg("offset")) - ; + ; + + py::class_>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix") + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) + + .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( + + Sets the matrix entry at the given row and column to the given value. After all entries have been added, + a call to finalize(false) is mandatory. + + Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and + column by column. As multiple entries per column are admitted, consecutive calls to this method are + admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are + treated as empty. If these constraints are not met, an exception is thrown. - // todo py::class_>(m, "SparseMatrixBuilder", "Builder of parametric sparse matrix") + :param double row: The row in which the matrix entry is to be set + :param double column: The column in which the matrix entry is to be set + :param RationalFunction const& value: The value that is to be set at the specified row and column + )dox", py::arg("row"), py::arg("column"), py::arg("value")) + + .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") + .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") + .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") + .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") + .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( + + Replaces all columns with id >= offset according to replacements. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + + :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i + :param double offset: Offset to add to each id in vector index. + )dox", py::arg("replacements"), py::arg("offset")) + ; // SparseMatrix py::class_>(m, "SparseMatrix", "Sparse matrix") diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index ca0eaec..62e1d8e 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -33,6 +33,44 @@ class TestMatrixBuilder: for e in matrix_5x5: assert (e.value() == 0.1 and e.column == 1) or e.value() == 0 or (e.value() > 20 and e.column > 1) + def test_parametric_matrix_builder(self): + builder = stormpy.ParametricSparseMatrixBuilder(force_dimensions=True) + matrix = builder.build() + assert matrix.nr_columns == 0 + assert matrix.nr_rows == 0 + assert matrix.nr_entries == 0 + + builder_5x5 = stormpy.ParametricSparseMatrixBuilder(5, 5, force_dimensions=False) + + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol) + + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol) + + builder_5x5.add_next_value(0, 0, first_val) + builder_5x5.add_next_value(0, 1, first_val) + builder_5x5.add_next_value(2, 2, sec_val) + builder_5x5.add_next_value(2, 3, sec_val) + + assert builder_5x5.get_last_column() == 3 + assert builder_5x5.get_last_row() == 2 + + builder_5x5.add_next_value(3, 2, sec_val) + builder_5x5.add_next_value(3, 4, sec_val) + builder_5x5.add_next_value(4, 3, sec_val) + + matrix_5x5 = builder_5x5.build() + + assert matrix_5x5.nr_columns == 5 + assert matrix_5x5.nr_rows == 5 + assert matrix_5x5.nr_entries == 7 + + for e in matrix_5x5: + assert (e.value() == first_val and e.column < 2) or (e.value() == sec_val and e.column > 1) + def test_matrix_replace_columns(self): builder = stormpy.SparseMatrixBuilder(3, 4, force_dimensions=False) @@ -58,10 +96,43 @@ class TestMatrixBuilder: # Check if columns where replaced for e in matrix: assert (e.value() == 0 and e.column == 0) or (e.value() == 3 and e.column == 1) or ( - e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) + e.value() == 2 and e.column == 2) or (e.value() == 1 and e.column == 3) - def test_matrix_builder_row_grouping(self): + def test_parametric_matrix_replace_columns(self): + builder = stormpy.ParametricSparseMatrixBuilder(3, 4, force_dimensions=False) + + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + builder.add_next_value(0, 1, first_val) + builder.add_next_value(0, 2, sec_val) + builder.add_next_value(0, 3, third_val) + + builder.add_next_value(1, 1, first_val) + builder.add_next_value(1, 2, sec_val) + builder.add_next_value(1, 3, third_val) + + builder.add_next_value(2, 1, first_val) + builder.add_next_value(2, 2, sec_val) + builder.add_next_value(2, 3, third_val) + + # replace rows + builder.replace_columns([3, 2], 2) + matrix = builder.build() + + assert matrix.nr_entries == 9 + + # Check if columns where replaced + for e in matrix: + assert (e.value() == first_val and e.column == 1) or (e.value() == third_val and e.column == 2) or ( + e.value() == sec_val and e.column == 3) + def test_matrix_builder_row_grouping(self): num_rows = 5 builder = stormpy.SparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) @@ -78,6 +149,23 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 4 assert matrix.get_row_group_end(1) == 5 + def test_parametric_matrix_builder_row_grouping(self): + num_rows = 5 + builder = stormpy.ParametricSparseMatrixBuilder(num_rows, 6, has_custom_row_grouping=True, row_groups=2) + + builder.new_row_group(1) + assert builder.get_current_row_group_count() == 1 + + builder.new_row_group(4) + assert builder.get_current_row_group_count() == 2 + matrix = builder.build() + + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 4 + + assert matrix.get_row_group_start(1) == 4 + assert matrix.get_row_group_end(1) == 5 + def test_matrix_from_numpy(self): array = np.array([[0, 2], [3, 4], @@ -97,6 +185,33 @@ class TestMatrixBuilder: for e in row: assert (e.value() == array[r, e.column]) + def test_parametric_matrix_from_numpy(self): + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + array = np.array([[sec_val, first_val], + [first_val, sec_val], + [sec_val, sec_val], + [third_val, third_val]]) + + matrix = stormpy.build_parametric_sparse_matrix(array) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + def test_matrix_from_numpy_row_grouping(self): array = np.array([[0, 2], [3, 4], @@ -122,3 +237,37 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 3 assert matrix.get_row_group_end(1) == 4 + + def test_parametric_matrix_from_numpy_row_grouping(self): + one_pol = stormpy.RationalRF(1) + one_pol = stormpy.FactorizedPolynomial(one_pol) + first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalRF(2) + two_pol = stormpy.FactorizedPolynomial(two_pol) + sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) + third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + + array = np.array([[sec_val, first_val], + [first_val, sec_val], + [sec_val, sec_val], + [third_val, third_val]]) + + matrix = stormpy.build_parametric_sparse_matrix(array, row_group_indices=[1, 3]) + + # Check matrix dimension + assert matrix.nr_rows == array.shape[0] + assert matrix.nr_columns == array.shape[1] + assert matrix.nr_entries == 8 + + # Check matrix values + for r in range(array.shape[1]): + row = matrix.get_row(r) + for e in row: + assert (e.value() == array[r, e.column]) + + # Check row groups + assert matrix.get_row_group_start(0) == 1 + assert matrix.get_row_group_end(0) == 3 + + assert matrix.get_row_group_start(1) == 3 + assert matrix.get_row_group_end(1) == 4 From 105d9c40b5256eed595a7cf4d2b21b4ef1ed6491 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 17 Apr 2020 18:15:01 +0200 Subject: [PATCH 33/36] Skip tests if numpy is not available --- tests/configurations.py | 9 +++++++++ tests/storage/test_matrix_builder.py | 11 ++++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/tests/configurations.py b/tests/configurations.py index c57d259..a6c1377 100644 --- a/tests/configurations.py +++ b/tests/configurations.py @@ -7,6 +7,15 @@ has_dft = config.storm_with_dft has_gspn = config.storm_with_gspn has_pars = config.storm_with_pars +# Check if numpy is available +try: + import numpy + + has_numpy = True +except ImportError: + has_numpy = False + 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") +numpy_avail = pytest.mark.skipif(not has_numpy, reason="Numpy not available") diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index 62e1d8e..99a4f08 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -1,5 +1,6 @@ import stormpy -import numpy as np + +from configurations import numpy_avail class TestMatrixBuilder: @@ -166,7 +167,9 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 4 assert matrix.get_row_group_end(1) == 5 + @numpy_avail def test_matrix_from_numpy(self): + import numpy as np array = np.array([[0, 2], [3, 4], [0.1, 24], @@ -185,7 +188,9 @@ class TestMatrixBuilder: for e in row: assert (e.value() == array[r, e.column]) + @numpy_avail def test_parametric_matrix_from_numpy(self): + import numpy as np one_pol = stormpy.RationalRF(1) one_pol = stormpy.FactorizedPolynomial(one_pol) first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) @@ -212,7 +217,9 @@ class TestMatrixBuilder: for e in row: assert (e.value() == array[r, e.column]) + @numpy_avail def test_matrix_from_numpy_row_grouping(self): + import numpy as np array = np.array([[0, 2], [3, 4], [0.1, 24], @@ -238,7 +245,9 @@ class TestMatrixBuilder: assert matrix.get_row_group_start(1) == 3 assert matrix.get_row_group_end(1) == 4 + @numpy_avail def test_parametric_matrix_from_numpy_row_grouping(self): + import numpy as np one_pol = stormpy.RationalRF(1) one_pol = stormpy.FactorizedPolynomial(one_pol) first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) From eeffca7df56527eec4f8610ce9f94e794ae1a6ed Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 24 May 2020 18:24:53 +0200 Subject: [PATCH 34/36] Small revision for MatrixBuilder --- lib/stormpy/storage/__init__.py | 4 ++-- src/storage/matrix.cpp | 20 ++++++++++---------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 768dadc..4982069 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -18,7 +18,7 @@ def build_sparse_matrix(array, row_group_indices=[]): len_group_indices = len(row_group_indices) if len_group_indices > 0: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, - row_groups=len(row_group_indices)) + row_groups=len_group_indices) else: builder = storage.SparseMatrixBuilder(rows=num_row, columns=num_col) @@ -49,7 +49,7 @@ def build_parametric_sparse_matrix(array, row_group_indices=[]): len_group_indices = len(row_group_indices) if len_group_indices > 0: builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col, has_custom_row_grouping=True, - row_groups=len(row_group_indices)) + row_groups=len_group_indices) else: builder = storage.ParametricSparseMatrixBuilder(rows=num_row, columns=num_col) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index d39224b..bbbc859 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -33,12 +33,12 @@ void define_sparse_matrix(py::module& m) { // SparseMatrixBuilder py::class_>(m, "SparseMatrixBuilder", "Builder of sparse matrix") - .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( Sets the matrix entry at the given row and column to the given value. After all entries have been added, - a call to finalize(false) is mandatory. + calling function build() is mandatory. Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are @@ -47,7 +47,7 @@ void define_sparse_matrix(py::module& m) { :param double row: The row in which the matrix entry is to be set :param double column: The column in which the matrix entry is to be set - :param double const& value: The value that is to be set at the specified row and column + :param double value: The value that is to be set at the specified row and column )dox", py::arg("row"), py::arg("column"), py::arg("value")) .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") @@ -58,20 +58,20 @@ void define_sparse_matrix(py::module& m) { .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( Replaces all columns with id >= offset according to replacements. - Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i - :param double offset: Offset to add to each id in vector index. + :param int offset: Offset to add to each id in vector index. )dox", py::arg("replacements"), py::arg("offset")) ; py::class_>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix") - .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) + .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( Sets the matrix entry at the given row and column to the given value. After all entries have been added, - a call to finalize(false) is mandatory. + calling function build() is mandatory. Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and column by column. As multiple entries per column are admitted, consecutive calls to this method are @@ -80,7 +80,7 @@ void define_sparse_matrix(py::module& m) { :param double row: The row in which the matrix entry is to be set :param double column: The column in which the matrix entry is to be set - :param RationalFunction const& value: The value that is to be set at the specified row and column + :param RationalFunction value: The value that is to be set at the specified row and column )dox", py::arg("row"), py::arg("column"), py::arg("value")) .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") @@ -91,10 +91,10 @@ void define_sparse_matrix(py::module& m) { .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( Replaces all columns with id >= offset according to replacements. - Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. + Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i - :param double offset: Offset to add to each id in vector index. + :param int offset: Offset to add to each id in vector index. )dox", py::arg("replacements"), py::arg("offset")) ; From 886718bdb26da397e93f1b2990f6b89fbd269696 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 26 May 2020 16:19:50 -0700 Subject: [PATCH 35/36] state generation via stormpy is broken. to avoid compilation problems, this is disabled for now --- src/storage/prism.cpp | 112 ++++++++++++------------- tests/storage/test_state_generation.py | 2 + 2 files changed, 58 insertions(+), 56 deletions(-) diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 47b4bc1..6365911 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -122,7 +122,7 @@ void define_prism(py::module& m) { py::class_> boolean_variable(m, "PrismBooleanVariable", variable, "A program boolean variable in a Prism program"); boolean_variable.def("__str__", &streamToString); - define_stateGeneration(m); + //define_stateGeneration(m); } class ValuationMapping { @@ -364,59 +364,59 @@ std::map> simu template void define_stateGeneration(py::module& m) { - py::class_> valuation_mapping(m, "ValuationMapping", "A valuation mapping for a state consists of a mapping from variable to value for each of the three types."); - valuation_mapping - .def_readonly("boolean_values", &ValuationMapping::booleanValues) - .def_readonly("integer_values", &ValuationMapping::integerValues) - .def_readonly("rational_values", &ValuationMapping::rationalValues) - .def("__str__", &ValuationMapping::toString); - - py::class_, - std::shared_ptr>> - generator_choice(m, "GeneratorChoice", R"doc( - Representation of a choice taken by the generator. - - :ivar origins: A list of command ids that generated this choice. - :vartype origins: List[int] - :ivar distribution: The probability distribution of this choice. - :vartype distribution: List[Pair[StateId, Probability]] - )doc"); - generator_choice - .def_readonly("origins", &GeneratorChoice::origins) - .def_readonly("distribution", &GeneratorChoice::distribution); - - py::class_, std::shared_ptr>> state_generator(m, "StateGenerator", R"doc( - Interactively explore states using Storm's PrismNextStateGenerator. - - :ivar program: A PRISM program. - )doc"); - state_generator - .def(py::init()) - .def("load_initial_state", &StateGenerator::loadInitialState, R"doc( - Loads the (unique) initial state. - Multiple initial states are not supported. - - :rtype: the ID of the initial state. - )doc") - .def("load", &StateGenerator::load, R"doc( - :param state_id: The ID of the state to load. - )doc") - .def("current_state_to_valuation", &StateGenerator::currentStateToValuation, R"doc( - Return a valuation for the currently loaded state. - - :rtype: stormpy.ValuationMapping - )doc") - .def("current_state_satisfies", &StateGenerator::satisfies, R"doc( - Check if the currently loaded state satisfies the given expression. - - :param stormpy.Expression expression: The expression to check against. - :rtype: bool - )doc") - .def("expand", &StateGenerator::expand, R"doc( - Expand the currently loaded state and return its successors. - - :rtype: [GeneratorChoice] - )doc"); - - m.def("simulate", &simulate); +// py::class_> valuation_mapping(m, "ValuationMapping", "A valuation mapping for a state consists of a mapping from variable to value for each of the three types."); +// valuation_mapping +// .def_readonly("boolean_values", &ValuationMapping::booleanValues) +// .def_readonly("integer_values", &ValuationMapping::integerValues) +// .def_readonly("rational_values", &ValuationMapping::rationalValues) +// .def("__str__", &ValuationMapping::toString); +// +// py::class_, +// std::shared_ptr>> +// generator_choice(m, "GeneratorChoice", R"doc( +// Representation of a choice taken by the generator. +// +// :ivar origins: A list of command ids that generated this choice. +// :vartype origins: List[int] +// :ivar distribution: The probability distribution of this choice. +// :vartype distribution: List[Pair[StateId, Probability]] +// )doc"); +// generator_choice +// .def_readonly("origins", &GeneratorChoice::origins) +// .def_readonly("distribution", &GeneratorChoice::distribution); +// +// py::class_, std::shared_ptr>> state_generator(m, "StateGenerator", R"doc( +// Interactively explore states using Storm's PrismNextStateGenerator. +// +// :ivar program: A PRISM program. +// )doc"); +// state_generator +// .def(py::init()) +// .def("load_initial_state", &StateGenerator::loadInitialState, R"doc( +// Loads the (unique) initial state. +// Multiple initial states are not supported. +// +// :rtype: the ID of the initial state. +// )doc") +// .def("load", &StateGenerator::load, R"doc( +// :param state_id: The ID of the state to load. +// )doc") +// .def("current_state_to_valuation", &StateGenerator::currentStateToValuation, R"doc( +// Return a valuation for the currently loaded state. +// +// :rtype: stormpy.ValuationMapping +// )doc") +// .def("current_state_satisfies", &StateGenerator::satisfies, R"doc( +// Check if the currently loaded state satisfies the given expression. +// +// :param stormpy.Expression expression: The expression to check against. +// :rtype: bool +// )doc") +// .def("expand", &StateGenerator::expand, R"doc( +// Expand the currently loaded state and return its successors. +// +// :rtype: [GeneratorChoice] +// )doc"); +// +// m.def("simulate", &simulate); } diff --git a/tests/storage/test_state_generation.py b/tests/storage/test_state_generation.py index 4c909de..d139b97 100644 --- a/tests/storage/test_state_generation.py +++ b/tests/storage/test_state_generation.py @@ -1,5 +1,6 @@ import stormpy from stormpy.examples.files import prism_dtmc_die +import pytest class _DfsQueue: def __init__(self): @@ -55,6 +56,7 @@ def _find_variable(program, name): return var return None +@pytest.mark.skipif(True, reason="State generation is broken") def test_knuth_yao_die(): program, expression_parser = _load_program(prism_dtmc_die) s_variable = _find_variable(program, "s") From 80f044cc49fe4856187728080c47936168392493 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 26 May 2020 16:20:52 -0700 Subject: [PATCH 36/36] dft tests should be disabled if no dft support is given --- tests/dft/test_io.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/dft/test_io.py b/tests/dft/test_io.py index 33a8149..214209b 100644 --- a/tests/dft/test_io.py +++ b/tests/dft/test_io.py @@ -36,7 +36,7 @@ class TestDftLoad: assert dft.nr_dynamic() == 1 assert not dft.can_have_nondeterminism() - +@dft class TestDftExport: def test_export_dft_json_string(self): dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft"))