diff --git a/lib/stormpy/examples/files/gspn/philosophers_4.pnpro b/lib/stormpy/examples/files/gspn/philosophers_4.pnpro
new file mode 100644
index 0000000..bdad898
--- /dev/null
+++ b/lib/stormpy/examples/files/gspn/philosophers_4.pnpro
@@ -0,0 +1,92 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/src/gspn/gspn.cpp b/src/gspn/gspn.cpp
index a9b64de..1dabb5d 100644
--- a/src/gspn/gspn.cpp
+++ b/src/gspn/gspn.cpp
@@ -3,8 +3,6 @@
#include "storm-gspn/storage/gspn/GSPN.h"
#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;
@@ -15,7 +13,6 @@ 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;
void gspnToFile(GSPN const& gspn, std::string const& filepath, bool toPnpro) {
@@ -100,12 +97,6 @@ void define_gspn(py::module& m) {
.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, "constant_definitions"_a = "")
- ;
-
// GSPN class
py::class_>(m, "GSPN", "Generalized Stochastic Petri Net")
// Constructor
diff --git a/src/gspn/gspn_io.cpp b/src/gspn/gspn_io.cpp
new file mode 100644
index 0000000..9ed9330
--- /dev/null
+++ b/src/gspn/gspn_io.cpp
@@ -0,0 +1,26 @@
+#include "gspn_io.h"
+#include "src/helpers.h"
+#include "storm-gspn/storage/gspn/GSPN.h"
+#include "storm-gspn/parser/GspnParser.h"
+
+using GSPN = storm::gspn::GSPN;
+using GSPNParser = storm::parser::GspnParser;
+using GSPNJaniBuilder = storm::builder::JaniGSPNBuilder;
+
+
+void define_gspn_io(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, "constant_definitions"_a = "")
+ ;
+
+ // GspnToJani builder
+ py::class_>(m, "GSPNToJaniBuilder")
+ .def(py::init(), py::arg("gspn"))
+ .def("build", &GSPNJaniBuilder::build, py::arg("automaton_name") = "gspn_automaton", "Build Jani model from GSPN")
+ .def("create_deadlock_properties", &GSPNJaniBuilder::getDeadlockProperties, py::arg("jani_model"), "Create standard properties for deadlocks")
+ ;
+
+}
diff --git a/src/gspn/gspn_io.h b/src/gspn/gspn_io.h
new file mode 100644
index 0000000..ef4c1e1
--- /dev/null
+++ b/src/gspn/gspn_io.h
@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+void define_gspn_io(py::module& m);
+
diff --git a/src/mod_gspn.cpp b/src/mod_gspn.cpp
index 19adacd..1d91985 100644
--- a/src/mod_gspn.cpp
+++ b/src/mod_gspn.cpp
@@ -1,6 +1,7 @@
#include "common.h"
#include "gspn/gspn.h"
+#include "gspn/gspn_io.h"
PYBIND11_MODULE(gspn, m) {
m.doc() = "Support for GSPNs";
@@ -11,4 +12,5 @@ PYBIND11_MODULE(gspn, m) {
#endif
define_gspn(m);
+ define_gspn_io(m);
}
diff --git a/tests/gspn/test_gspn_io.py b/tests/gspn/test_gspn_io.py
new file mode 100644
index 0000000..ff37406
--- /dev/null
+++ b/tests/gspn/test_gspn_io.py
@@ -0,0 +1,71 @@
+import os
+import math
+
+import stormpy
+
+from helpers.helper import get_example_path
+from configurations import gspn, xml
+
+
+@gspn
+class TestGSPNJani:
+ def test_custom_property(self):
+ gspn_parser = stormpy.gspn.GSPNParser()
+ gspn = gspn_parser.parse(get_example_path("gspn", "philosophers_4.pnpro"))
+ assert gspn.get_name() == "Philosophers4"
+ assert gspn.get_number_of_timed_transitions() == 12
+ assert gspn.get_number_of_immediate_transitions() == 0
+ assert gspn.get_number_of_places() == 16
+
+ # Build jani program
+ jani_builder = stormpy.gspn.GSPNToJaniBuilder(gspn)
+ jani_program = jani_builder.build()
+
+ # Set properties
+ properties = stormpy.parse_properties_for_jani_model('P=? [F<=10 eating1=1]', jani_program)
+
+ # Build model
+ model = stormpy.build_model(jani_program, properties)
+
+ # Model checking
+ initial_state = model.initial_states[0]
+ assert initial_state == 0
+ result = stormpy.model_checking(model, properties[0])
+ assert math.isclose(result.at(initial_state), 0.4372171069840004)
+
+
+ def test_standard_properties(self):
+ gspn_parser = stormpy.gspn.GSPNParser()
+ gspn = gspn_parser.parse(get_example_path("gspn", "philosophers_4.pnpro"))
+ assert gspn.get_name() == "Philosophers4"
+ assert gspn.get_number_of_timed_transitions() == 12
+ assert gspn.get_number_of_immediate_transitions() == 0
+ assert gspn.get_number_of_places() == 16
+
+ # Build jani program
+ jani_builder = stormpy.gspn.GSPNToJaniBuilder(gspn)
+ jani_program = jani_builder.build()
+
+ # Use standard properties
+ properties = jani_builder.create_deadlock_properties(jani_program)
+
+ # Instantiate constants
+ description = stormpy.SymbolicModelDescription(jani_program)
+ constant_definitions = description.parse_constant_definitions("TIME_BOUND=1")
+ jani_program = description.instantiate_constants(constant_definitions).as_jani_model()
+
+ # Build model
+ # Leads to incorrect result
+ #model = stormpy.build_model(jani_program, properties)
+ model = stormpy.build_model(jani_program)
+
+ # Model checking
+ initial_state = model.initial_states[0]
+ assert initial_state == 0
+ result = stormpy.model_checking(model, properties[0])
+ assert math.isclose(result.at(initial_state), 1.0)
+ # Not parsable
+ #result = stormpy.model_checking(model, properties[1])
+ #assert math.isclose(result.at(initial_state), 0.09123940783)
+ result = stormpy.model_checking(model, properties[2])
+ assert math.isclose(result.at(initial_state), 5.445544554455446)