Merge branch 'master' into almostsurepomdp

src/core/counterexample.cpp

@@ -1,4 +1,3 @@
-#include <algorithm>
 
 #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<unsigned long long, std::__1::less<unsigned long long>, boost::container::new_allocator<unsigned long long>>;
 
-    py::class_<boost::container::flat_set<uint_fast64_t>>(m, "FlatSet", "Container to pass to program")
+    py::class_<FlatSet>(m, "FlatSet", "Container to pass to program")
             .def(py::init<>())
-            .def(py::init<boost::container::flat_set<uint64_t>>(), "other"_a)
-            .def("insert", [](boost::container::flat_set<uint_fast64_t>& flatset, uint64_t value) {flatset.insert(value);})
-            .def("is_subset_of", [](boost::container::flat_set<uint64_t> const& left, boost::container::flat_set<uint64_t> const& right) {return std::includes(right.begin(), right.end(), left.begin(), left.end()); })
-            .def("insert_set", [](boost::container::flat_set<uint64_t>& left, boost::container::flat_set<uint64_t> const& additional) { for(auto const& i : additional) {left.insert(i);}})
-            .def("__str__", [](boost::container::flat_set<uint64_t> const& set) { std::stringstream str; str << "["; for(auto const& i : set) { str << i << ", ";} str << "]"; return str.str(); })
-            .def("__len__", [](boost::container::flat_set<uint64_t> const& set) { return set.size();})
-            .def("__iter__", [](boost::container::flat_set<uint_fast64_t> &v) {
+            .def(py::init<FlatSet>(), "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 */
             ;

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")
             ;
 
 

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):