Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .git-blame-ignore-revs
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,4 @@

534f29c9e329007d67428da3ef7be84141140fe2
111723001581254265076802b8b50f581fae43fd
d3d0d3f399c918728db73c13a777fcee41bda4cc
10 changes: 5 additions & 5 deletions src/boost.h
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@
namespace pybind11 {
namespace detail {

template <typename T>
template<typename T>
struct type_caster<boost::optional<T>> : optional_caster<boost::optional<T>> {};

template<> struct type_caster<boost::none_t>
: public void_caster<boost::none_t> {};
template<>
struct type_caster<boost::none_t> : public void_caster<boost::none_t> {};

}
}
} // namespace detail
} // namespace pybind11
2 changes: 1 addition & 1 deletion src/common.h
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@

#include "config.h"

#include <pybind11/pybind11.h>
#include <pybind11/operators.h>
#include <pybind11/pybind11.h>
#include <pybind11/stl.h>
#include <tuple>

Expand Down
14 changes: 7 additions & 7 deletions src/core/analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,12 @@

// Define python bindings
void define_graph_constraints(py::module& m) {

// ConstraintCollector
py::class_<storm::analysis::ConstraintCollector<storm::RationalFunction>, std::shared_ptr<storm::analysis::ConstraintCollector<storm::RationalFunction>>>(m, "ConstraintCollector", "Collector for constraints on parametric Markov chains")
.def(py::init<storm::models::sparse::Model<storm::RationalFunction> const&>(), py::arg("model"))
.def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints, "Get the constraints ensuring a wellformed model")
.def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getGraphPreservingConstraints, "Get the constraints ensuring the graph is preserved")
;

py::class_<storm::analysis::ConstraintCollector<storm::RationalFunction>, std::shared_ptr<storm::analysis::ConstraintCollector<storm::RationalFunction>>>(
m, "ConstraintCollector", "Collector for constraints on parametric Markov chains")
.def(py::init<storm::models::sparse::Model<storm::RationalFunction> const&>(), py::arg("model"))
.def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getWellformedConstraints,
"Get the constraints ensuring a wellformed model")
.def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector<storm::RationalFunction>::getGraphPreservingConstraints,
"Get the constraints ensuring the graph is preserved");
}
30 changes: 16 additions & 14 deletions src/core/bisimulation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2,31 +2,33 @@
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/models/symbolic/StandardRewardModel.h"


template <storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> performBisimulationMinimization(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType, storm::dd::bisimulation::QuotientFormat const& quotientFormat) {
return storm::api::performBisimulationMinimization<DdType, ValueType, ValueType>(model, formulas, bisimulationType, storm::dd::bisimulation::SignatureMode::Eager, quotientFormat);
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::Model<ValueType>> performBisimulationMinimization(
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
storm::storage::BisimulationType const& bisimulationType, storm::dd::bisimulation::QuotientFormat const& quotientFormat) {
return storm::api::performBisimulationMinimization<DdType, ValueType, ValueType>(model, formulas, bisimulationType,
storm::dd::bisimulation::SignatureMode::Eager, quotientFormat);
}

// Define python bindings
void define_bisimulation(py::module& m) {

// Bisimulation
m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"));
m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"));
m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"));
m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"));
m.def("_perform_bisimulation", &storm::api::performBisimulationMinimization<double>, "Perform bisimulation", py::arg("model"), py::arg("formulas"),
py::arg("bisimulation_type"), py::arg("graph_preserving"));
m.def("_perform_parametric_bisimulation", &storm::api::performBisimulationMinimization<storm::RationalFunction>, "Perform bisimulation on parametric model",
py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("graph_preserving"));
m.def("_perform_symbolic_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, double>, "Perform bisimulation", py::arg("model"),
py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"));
m.def("_perform_symbolic_parametric_bisimulation", &performBisimulationMinimization<storm::dd::DdType::Sylvan, storm::RationalFunction>,
"Perform bisimulation on parametric model", py::arg("model"), py::arg("formulas"), py::arg("bisimulation_type"), py::arg("quotient_format"));

// BisimulationType
py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
.value("STRONG", storm::storage::BisimulationType::Strong)
.value("WEAK", storm::storage::BisimulationType::Weak)
;
.value("WEAK", storm::storage::BisimulationType::Weak);

// QuotientFormat
py::enum_<storm::dd::bisimulation::QuotientFormat>(m, "QuotientFormat", "Return format of bisimulation quotient")
.value("SPARSE", storm::dd::bisimulation::QuotientFormat::Sparse)
.value("DD", storm::dd::bisimulation::QuotientFormat::Dd)
;

.value("DD", storm::dd::bisimulation::QuotientFormat::Dd);
}
1 change: 0 additions & 1 deletion src/core/bisimulation.h
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,3 @@
#include "common.h"

void define_bisimulation(py::module& m);

2 changes: 1 addition & 1 deletion src/core/common.h
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#pragma once

#include <pybind11/stl.h>
#include "src/common.h"
#include "storm/api/storm.h"
#include <pybind11/stl.h>
Loading