GSPN to Jani translation

5 years ago · 4c3b5c9784
6 changed files with 197 additions and 9 deletions
--- a/lib/stormpy/examples/files/gspn/philosophers_4.pnpro
+++ b/lib/stormpy/examples/files/gspn/philosophers_4.pnpro
@ -0,0 +1,92 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="Dining Philosophers" version="121">
+  <gspn name="Philosophers4">
+    <nodes>
+      <place marking="1" name="fork1" x="21.0" y="4.0"/>
+      <transition delay="lambda" delay-x="-0.5" delay-y="1.5" name="T0" rotation="0.7853981633974483" type="EXP" x="26.55" y="9.0"/>
+      <transition delay="lambda" name="T1" rotation="2.356194490192345" type="EXP" x="16.55" y="9.0"/>
+      <place marking="1" name="fork4" x="11.0" y="14.0"/>
+      <place marking="1" name="fork2" x="31.0" y="14.0"/>
+      <transition delay="lambda" delay-x="0.0" delay-y="1.5" name="T2" rotation="0.7853981633974483" type="EXP" x="16.55" y="19.0"/>
+      <transition delay="lambda" name="T3" rotation="2.356194490192345" type="EXP" x="26.55" y="19.0"/>
+      <place marking="1" name="fork3" x="21.0" y="24.0"/>
+      <place name="eating1" x="11.0" y="9.0"/>
+      <place label-y="-1.5" marking="1" name="thinking1" x="16.0" y="4.0"/>
+      <place label-y="-1.5" name="wait1" x="6.0" y="4.0"/>
+      <place label-y="-1.5" name="eating2" x="26.0" y="4.0"/>
+      <place marking="1" name="thinking2" x="31.0" y="9.0"/>
+      <place label-y="-1.5" name="wait2" x="36.0" y="4.0"/>
+      <place name="eating3" x="31.0" y="19.0"/>
+      <place marking="1" name="thinking4" x="11.0" y="19.0"/>
+      <place name="eating4" x="16.0" y="24.0"/>
+      <place marking="1" name="thinking3" x="26.0" y="24.0"/>
+      <place name="wait3" x="36.0" y="24.0"/>
+      <place name="wait4" x="6.0" y="24.0"/>
+      <transition delay="rho" delay-x="0.0" delay-y="1.5" name="T4" rotation="2.356194490192345" type="EXP" x="6.55" y="9.0"/>
+      <transition delay="rho" name="T5" rotation="2.356194490192345" type="EXP" x="36.55" y="19.0"/>
+      <transition delay="mu" delay-x="-0.5" name="T6" rotation="0.7853981633974483" type="EXP" x="36.55" y="9.0"/>
+      <transition delay="mu" delay-x="0.0" name="T7" rotation="0.7853981633974483" type="EXP" x="6.55" y="19.0"/>
+      <transition delay="mu" name="T8" type="EXP" x="11.55" y="4.0"/>
+      <transition delay="rho" name="T9" type="EXP" x="31.55" y="4.0"/>
+      <transition delay="mu" name="T10" type="EXP" x="31.55" y="24.0"/>
+      <transition delay="rho" delay-x="0.0" delay-y="1.5" name="T11" type="EXP" x="11.55" y="24.0"/>
+      <constant consttype="REAL" name="lambda" value="1" x="1.4375" y="2.0"/>
+      <constant consttype="REAL" name="mu" value="1" x="1.4375" y="3.0"/>
+      <constant consttype="REAL" name="rho" value="1" x="1.5" y="4.0"/>
+    </nodes>
+    <edges>
+      <arc head="fork4" kind="OUTPUT" mult-k="0.5" tail="T1"/>
+      <arc head="fork2" kind="OUTPUT" mult-k="0.5" tail="T0"/>
+      <arc head="fork3" kind="OUTPUT" mult-k="0.5" tail="T2"/>
+      <arc head="fork4" kind="OUTPUT" mult-k="0.18173828125000002" tail="T2"/>
+      <arc head="fork1" kind="OUTPUT" mult-k="0.5" tail="T1"/>
+      <arc head="fork1" kind="OUTPUT" mult-k="0.5" tail="T0"/>
+      <arc head="fork2" kind="OUTPUT" mult-k="0.5" tail="T3"/>
+      <arc head="fork3" kind="OUTPUT" mult-k="0.5" tail="T3"/>
+      <arc head="thinking1" kind="OUTPUT" mult-k="0.5" tail="T1"/>
+      <arc head="T8" kind="INPUT" mult-k="0.5" tail="thinking1"/>
+      <arc head="wait1" kind="OUTPUT" mult-k="0.5" tail="T8"/>
+      <arc head="T4" kind="INPUT" mult-k="0.5" tail="wait1"/>
+      <arc head="eating1" kind="OUTPUT" mult-k="0.5" tail="T4"/>
+      <arc head="T1" kind="INPUT" mult-k="0.5" tail="eating1"/>
+      <arc head="T4" kind="INPUT" mult-k="0.5" tail="fork4"/>
+      <arc head="T7" kind="INPUT" mult-k="0.5" tail="fork4"/>
+      <arc head="T5" kind="INPUT" mult-k="0.5" tail="fork2"/>
+      <arc head="T6" kind="INPUT" mult-k="0.5" tail="fork2"/>
+      <arc head="T0" kind="INPUT" mult-k="0.5" tail="eating2"/>
+      <arc head="thinking2" kind="OUTPUT" mult-k="0.5" tail="T0"/>
+      <arc head="T6" kind="INPUT" mult-k="0.5" tail="thinking2"/>
+      <arc head="wait2" kind="OUTPUT" mult-k="0.5" tail="T6"/>
+      <arc head="T9" kind="INPUT" mult-k="0.5" tail="wait2"/>
+      <arc head="eating2" kind="OUTPUT" mult-k="0.5" tail="T9"/>
+      <arc head="thinking3" kind="OUTPUT" mult-k="0.5" tail="T3"/>
+      <arc head="T10" kind="INPUT" mult-k="0.5" tail="thinking3"/>
+      <arc head="wait3" kind="OUTPUT" mult-k="0.5" tail="T10"/>
+      <arc head="T5" kind="INPUT" mult-k="0.5" tail="wait3"/>
+      <arc head="eating3" kind="OUTPUT" mult-k="0.5" tail="T5"/>
+      <arc head="T3" kind="INPUT" mult-k="0.5" tail="eating3"/>
+      <arc head="T2" kind="INPUT" mult-k="0.5" tail="eating4"/>
+      <arc head="thinking4" kind="OUTPUT" mult-k="0.5" tail="T2"/>
+      <arc head="T7" kind="INPUT" mult-k="0.5" tail="thinking4"/>
+      <arc head="wait4" kind="OUTPUT" mult-k="0.5" tail="T7"/>
+      <arc head="T11" kind="INPUT" mult-k="0.5" tail="wait4"/>
+      <arc head="eating4" kind="OUTPUT" mult-k="0.5" tail="T11"/>
+      <arc head="T8" kind="INPUT" mult-k="0.5" tail="fork1">
+        <point x="19.5" y="2.5"/>
+        <point x="14.0" y="2.5"/>
+      </arc>
+      <arc head="T9" kind="INPUT" mult-k="0.5" tail="fork1">
+        <point x="24.5" y="2.5"/>
+        <point x="30.0" y="2.5"/>
+      </arc>
+      <arc head="T11" kind="INPUT" mult-k="0.5" tail="fork3">
+        <point x="19.5" y="27.5"/>
+        <point x="14.5" y="27.5"/>
+      </arc>
+      <arc head="T10" kind="INPUT" mult-k="0.5" tail="fork3">
+        <point x="24.5" y="27.5"/>
+        <point x="30.0" y="27.5"/>
+      </arc>
+    </edges>
+  </gspn>
+</project>
--- 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<GSPN::RateType>;
 using ImmediateTransition = storm::gspn::ImmediateTransition<GSPN::WeightType>;
 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<storm::expressions::Variable, storm::expressions::Expression>())
    ;

-    // GspnParser class
-    py::class_<GSPNParser, std::shared_ptr<GSPNParser>>(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_<GSPN, std::shared_ptr<GSPN>>(m, "GSPN", "Generalized Stochastic Petri Net")
        // Constructor
--- a/src/gspn/gspn_io.cpp
+++ 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_<GSPNParser, std::shared_ptr<GSPNParser>>(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_<GSPNJaniBuilder, std::shared_ptr<GSPNJaniBuilder>>(m, "GSPNToJaniBuilder")
+         .def(py::init<GSPN const&>(), 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")
+    ;
+
+}
--- a/src/gspn/gspn_io.h
+++ b/src/gspn/gspn_io.h
@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+void define_gspn_io(py::module& m);
+
--- 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);
 }
--- a/tests/gspn/test_gspn_io.py
+++ 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)