From 4c3b5c97842e9fa778296e7898ab14d5dc045094 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 13 Jul 2020 14:53:58 +0200 Subject: [PATCH] GSPN to Jani translation --- .../examples/files/gspn/philosophers_4.pnpro | 92 +++++++++++++++++++ src/gspn/gspn.cpp | 9 -- src/gspn/gspn_io.cpp | 26 ++++++ src/gspn/gspn_io.h | 6 ++ src/mod_gspn.cpp | 2 + tests/gspn/test_gspn_io.py | 71 ++++++++++++++ 6 files changed, 197 insertions(+), 9 deletions(-) create mode 100644 lib/stormpy/examples/files/gspn/philosophers_4.pnpro create mode 100644 src/gspn/gspn_io.cpp create mode 100644 src/gspn/gspn_io.h create mode 100644 tests/gspn/test_gspn_io.py 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)