From 4d357a7409600032861b2cd846cea87cee5f4ef3 Mon Sep 17 00:00:00 2001 From: hannah Date: Fri, 13 Mar 2020 11:28:38 +0100 Subject: [PATCH] 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): +