sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

write gspn to Pnpro

refactoring
hannah 5 years ago
committed by Matthias Volk
parent
e69c181462
commit
4d357a7409
2 changed files with 116 additions and 56 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 135
      src/gspn/gspn.cpp
  2. 37
      tests/gspn/test_gspn.py

135
src/gspn/gspn.cpp
View File

@ -4,6 +4,7 @@
#include "storm-gspn/storage/gspn/GspnBuilder.h" #include "storm-gspn/storage/gspn/GspnBuilder.h"
#include "storm/settings/SettingsManager.h" #include "storm/settings/SettingsManager.h"
#include "storm/utility/file.h"
using GSPN = storm::gspn::GSPN; using GSPN = storm::gspn::GSPN;
using GSPNBuilder = storm::gspn::GspnBuilder; using GSPNBuilder = storm::gspn::GspnBuilder;
@ -12,17 +13,87 @@ using Place = storm::gspn::Place;
using TimedTransition = storm::gspn::TimedTransition<GSPN::RateType>; using TimedTransition = storm::gspn::TimedTransition<GSPN::RateType>;
using ImmediateTransition = storm::gspn::ImmediateTransition<GSPN::WeightType>; using ImmediateTransition = storm::gspn::ImmediateTransition<GSPN::WeightType>;
using Transition = storm::gspn::Transition; 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) { void define_gspn(py::module& m) {
// GSPN_Builder class
py::class_<GSPNBuilder, std::shared_ptr<GSPNBuilder>>(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<uint64_t> 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<uint64_t> capacity = boost::optional<uint64_t>(1), uint_fast64_t const& initialTokens = 0, std::string const& name = "") {
// b.addPlace(capacity, initialTokens, name); } , py::arg("capacity") = boost::optional<uint64_t>(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<uint64_t> + write tests:
.def("add_timed_transition", py::overload_cast<uint_fast64_t const&, double const& , std::string const&>(&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<uint_fast64_t const&, double const& , boost::optional<uint64_t>, 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<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_input_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_inhibition_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_inhibition_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_output_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_output_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&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<storm::expressions::Variable, storm::expressions::Expression>())
;
// GSPN class
py::class_<GSPN, std::shared_ptr<GSPN>>(m, "GSPN", "Generalized Stochastic Petri Net")
// Constructor
.def(py::init<std::string const& , std::vector<Place> const& , std::vector<ImmediateTransition> const& ,
std::vector<TimedTransition> const& , std::vector<TransitionPartition> const& ,
std::shared_ptr<storm::expressions::ExpressionManager> const& , std::map<storm::expressions::Variable,
storm::expressions::Expression> const& > (),
"name"_a, "places"_a, "itransitions"_a, "ttransitions"_a, "partitions"_a, "exprManager"_a, "constantsSubstitution"_a = std::map<storm::expressions::Variable, storm::expressions::Expression>())
.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 // LayoutInfo class
py::class_<LayoutInfo>(m, "LayoutInfo") py::class_<LayoutInfo>(m, "LayoutInfo")
.def(py::init<>())
.def(py::init<double, double, double>(), "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<double, double, double>(), "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 // Place class
@ -33,11 +104,19 @@ void define_gspn(py::module& m) {
.def("get_id", &Place::getID, "Get the id 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("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("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("get_capacity", &Place::getCapacity, "Get the capacity of tokens of this place")
.def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted") .def("has_restricted_capacity", &Place::hasRestrictedCapacity, "Is capacity of this place restricted")
; ;
// TransitionPartition class
py::class_<TransitionPartition>(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 // Transition class
py::class_<Transition, std::shared_ptr<Transition>>(m, "Transition", "Transition in a GSPN") py::class_<Transition, std::shared_ptr<Transition>>(m, "Transition", "Transition in a GSPN")
.def(py::init<>()) .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") .def("no_weight_attached", &ImmediateTransition::noWeightAttached, "True iff no weight is attached")
; ;
// GSPN class
py::class_<GSPN, std::shared_ptr<GSPN>>(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<std::string const&, std::vector<Place>, ... >())
// 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_<GSPNBuilder, std::shared_ptr<GSPNBuilder>>(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<uint64_t> 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<uint64_t> + write tests:
.def("add_timed_transition", py::overload_cast<uint_fast64_t const&, double const& , std::string const&>(&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<uint_fast64_t const&, double const& , boost::optional<uint64_t>, 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<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_input_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_inhibition_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_inhibition_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&GSPNBuilder::addInhibitionArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_output_arc", py::overload_cast<uint_fast64_t const&, uint_fast64_t const&, uint_fast64_t const&>(&GSPNBuilder::addOutputArc), py::arg("from"), py::arg("to"), py::arg("multiplicity"))
.def("add_output_arc", py::overload_cast<std::string const&, std::string const&, uint64_t>(&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<storm::expressions::Variable, storm::expressions::Expression>())
;
} }

37
tests/gspn/test_gspn.py
View File

@ -4,6 +4,8 @@ import stormpy
from configurations import gspn from configurations import gspn
from helpers.helper import get_example_path
@gspn @gspn
class TestGSPNBuilder: class TestGSPNBuilder:
@ -62,6 +64,10 @@ class TestGSPNBuilder:
assert ti_weight == ti.get_weight() assert ti_weight == ti.get_weight()
assert ti.no_weight_attached() == False 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): def test_build_gspn(self):
@ -69,8 +75,10 @@ class TestGSPNBuilder:
builder = stormpy.gspn.GSPNBuilder() builder = stormpy.gspn.GSPNBuilder()
builder.set_name(gspn_name) builder.set_name(gspn_name)
# todo place tests, set_place_layout_info (boost) # 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_0 = builder.add_immediate_transition()
ti_id_1 = builder.add_immediate_transition(priority=0, weight=0.5, name="ti_1") 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) # todo tests for add_ (add_place needed)
# builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2) # builder.add_input_arc(ti_id_0, ti_id_1, multiplicity = 2)
# todo test addNormalArc # 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() gspn = builder.build_gspn()
assert gspn.name() == gspn_name assert gspn.name() == gspn_name
gspn_new_name = "new_name" gspn_new_name = "new_name"
gspn.set_name(gspn_new_name) gspn.set_name(gspn_new_name)
assert gspn.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):
Write Preview
Loading…
Cancel
Save