diff --git a/src/core/counterexample.cpp b/src/core/counterexample.cpp index b4cb1e2..c5e7b4f 100644 --- a/src/core/counterexample.cpp +++ b/src/core/counterexample.cpp @@ -1,4 +1,3 @@ -#include #include "counterexample.h" #include "storm/environment/Environment.h" @@ -10,16 +9,17 @@ using namespace storm::counterexamples; // Define python bindings void define_counterexamples(py::module& m) { + using FlatSet = boost::container::flat_set, boost::container::new_allocator>; - py::class_>(m, "FlatSet", "Container to pass to program") + py::class_(m, "FlatSet", "Container to pass to program") .def(py::init<>()) - .def(py::init>(), "other"_a) - .def("insert", [](boost::container::flat_set& flatset, uint64_t value) {flatset.insert(value);}) - .def("is_subset_of", [](boost::container::flat_set const& left, boost::container::flat_set const& right) {return std::includes(right.begin(), right.end(), left.begin(), left.end()); }) - .def("insert_set", [](boost::container::flat_set& left, boost::container::flat_set const& additional) { for(auto const& i : additional) {left.insert(i);}}) - .def("__str__", [](boost::container::flat_set const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); }) - .def("__len__", [](boost::container::flat_set const& set) { return set.size();}) - .def("__iter__", [](boost::container::flat_set &v) { + .def(py::init(), "other"_a) + .def("insert", [](FlatSet& flatset, uint64_t value) {flatset.insert(value);}) + .def("is_subset_of", [](FlatSet const& left, FlatSet const& right) {return std::includes(right.begin(), right.end(), left.begin(), left.end()); }) + .def("insert_set", [](FlatSet& left, FlatSet const& additional) { for(auto const& i : additional) {left.insert(i);}}) + .def("__str__", [](FlatSet const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); }) + .def("__len__", [](FlatSet const& set) { return set.size();}) + .def("__iter__", [](FlatSet &v) { return py::make_iterator(v.begin(), v.end()); }, py::keep_alive<0, 1>()) /* Keep vector alive while iterator is used */ ; diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 4f0c010..47b4bc1 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -35,7 +35,9 @@ void define_prism(py::module& m) { .def("restrict_commands", &Program::restrictCommands, "Restrict commands") .def("simplify", &Program::simplify, "Simplify") .def("used_constants",&Program::usedConstants, "Compute Used Constants") + .def("get_constant", &Program::getConstant, py::arg("name")) .def("get_module", [](Program const& prog, std::string const& name) {return prog.getModule(name);}, py::arg("module_name")) + // TODO the following is a duplicate and should be deprecated. .def_property_readonly("hasUndefinedConstants", &Program::hasUndefinedConstants, "Does the program have undefined constants?") .def_property_readonly("isDeterministicModel", &Program::isDeterministicModel, "Does the program describe a deterministic model?") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") @@ -100,6 +102,7 @@ void define_prism(py::module& m) { .def_property_readonly("defined", &Constant::isDefined, "Is the constant defined?") .def_property_readonly("type", &Constant::getType, "The type of the constant") .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "Expression variable") + .def_property_readonly("definition", &Constant::getExpression, "Defining expression") ; diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index b64ba2d..71dbbfa 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -153,6 +153,14 @@ class TestSparseModel: assert len(initial_states) == 1 assert 0 in initial_states + def test_choice_origins(self): + program, _ = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) + a = stormpy.FlatSet() + + options = stormpy.BuilderOptions([]) + options.set_build_with_choice_origins() + model = stormpy.build_sparse_model_with_options(program, options) + a = model.choice_origins.get_edge_index_set(3) class TestSymbolicSylvanModel: def test_build_dtmc_from_prism_program(self):