Skip to content
Merged
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
3 changes: 0 additions & 3 deletions src/common.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,4 @@
namespace py = pybind11;
using namespace pybind11::literals;

PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T>)
PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T const>)

#include "src/boost.h"
3 changes: 1 addition & 2 deletions src/core/analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,7 @@
// 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")
py::classh<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")
Expand Down
2 changes: 1 addition & 1 deletion src/core/bisimulation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ void define_bisimulation(py::module& m) {
.value("DD", storm::dd::bisimulation::QuotientFormat::Dd)
.finalize();

py::class_<storm::dd::bisimulation::BisimulationOptions>(m, "BisimulationOptionsDd", "Options for Dd bisimulation")
py::classh<storm::dd::bisimulation::BisimulationOptions>(m, "BisimulationOptionsDd", "Options for Dd bisimulation")
.def(py::init<>(), "Create")
.def_readwrite("reuse_mode", &storm::dd::bisimulation::BisimulationOptions::reuseMode, "Reuse mode")
.def_readwrite("refinement_mode", &storm::dd::bisimulation::BisimulationOptions::refinementMode, "Refinement mode")
Expand Down
21 changes: 10 additions & 11 deletions src/core/core.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,7 @@ void define_build_sparse_model_defs(py::module& m) {
("Build the " + desc + "model from DRN" + (std::is_same_v<ValueType, storm::RationalFunction> ? " (parametric)" : "")).c_str(), py::arg("file"),
py::arg("options") = storm::parser::DirectEncodingParserOptions());

py::class_<typename storm::builder::ExplicitModelBuilder<ValueType>::Options>(m, ("Explicit" + classType + "ModelBuilderOptions").c_str(),
py::classh<typename storm::builder::ExplicitModelBuilder<ValueType>::Options>(m, ("Explicit" + classType + "ModelBuilderOptions").c_str(),
"Options for the explicit model builder")
.def(py::init<>(), "Create")
.def_readwrite("exploration_order", &storm::builder::ExplicitModelBuilder<ValueType>::Options::explorationOrder,
Expand All @@ -164,7 +164,7 @@ void define_build_sparse_model_defs(py::module& m) {
m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"),
py::arg("options"), py::arg("action_mask") = nullptr,
py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
py::classh<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
.def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
.def("export_lookup", &storm::builder::ExplicitModelBuilder<double>::exportExplicitStateLookup, "Export a lookup model");
} else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
Expand All @@ -174,7 +174,7 @@ void define_build_sparse_model_defs(py::module& m) {
m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<storm::RationalFunction>, "Construct a builder instance",
py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr,
py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
py::class_<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models")
py::classh<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models")
.def("build", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::build, "Build the model", py::call_guard<py::gil_scoped_release>())
.def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::exportExplicitStateLookup, "Export a lookup model");
} else if constexpr (std::is_same_v<ValueType, storm::RationalNumber>) {
Expand All @@ -185,7 +185,7 @@ void define_build_sparse_model_defs(py::module& m) {
}

void define_build(py::module& m) {
py::class_<storm::parser::DirectEncodingParserOptions>(m, "DirectEncodingParserOptions", "Options for the .drn parser")
py::classh<storm::parser::DirectEncodingParserOptions>(m, "DirectEncodingParserOptions", "Options for the .drn parser")
.def(py::init<>(), "initialise")
.def_readwrite("build_choice_labels", &storm::parser::DirectEncodingParserOptions::buildChoiceLabeling, "Build with choice labels");

Expand All @@ -194,7 +194,7 @@ void define_build(py::module& m) {
.value("BFS", storm::builder::ExplorationOrder::Bfs)
.finalize();

py::class_<typename storm::parser::ExplicitModelParserOptions>(m, "ExplicitModelParserOptions", "Options for the explicit model parser")
py::classh<typename storm::parser::ExplicitModelParserOptions>(m, "ExplicitModelParserOptions", "Options for the explicit model parser")
.def(py::init<>(), "Create")
.def_readwrite("fix_deadlocks", &storm::parser::ExplicitModelParserOptions::fixDeadlocks,
"If set, deadlocks states will be fixed by adding a self-loop with probability 1.")
Expand All @@ -207,7 +207,7 @@ void define_build(py::module& m) {
define_build_sparse_model_defs<storm::Interval>(m);
define_build_sparse_model_defs<storm::RationalInterval>(m);

py::class_<storm::builder::ExplicitStateLookup<uint32_t>>(m, "ExplicitStateLookup", "Lookup model for states")
py::classh<storm::builder::ExplicitStateLookup<uint32_t>>(m, "ExplicitStateLookup", "Lookup model for states")
.def(
"lookup",
[](storm::builder::ExplicitStateLookup<uint32_t> const& lookup,
Expand All @@ -223,7 +223,7 @@ void define_build(py::module& m) {

;

py::class_<storm::builder::BuilderOptions>(m, "BuilderOptions", "Options for building process")
py::classh<storm::builder::BuilderOptions>(m, "BuilderOptions", "Options for building process")
.def(py::init<std::vector<std::shared_ptr<storm::logic::Formula const>> const&>(), "Initialise with formulae to preserve", py::arg("formulae"))
.def(py::init<bool, bool>(), "Initialise without formulae", py::arg("build_all_reward_models") = true, py::arg("build_all_labels") = true)
.def_property_readonly("preserved_label_names", &storm::builder::BuilderOptions::getLabelNames, "Labels preserved")
Expand All @@ -242,9 +242,8 @@ void define_build(py::module& m) {
.def("set_build_all_reward_models", &storm::builder::BuilderOptions::setBuildAllRewardModels, "Build with all reward models",
py::arg("new_value") = true);

py::class_<storm::generator::ActionMask<double>, std::shared_ptr<storm::generator::ActionMask<double>>> actionmask(m, "ActionMaskDouble");
py::class_<storm::generator::StateValuationFunctionMask<double>, std::shared_ptr<storm::generator::StateValuationFunctionMask<double>>> actfuncmask(
m, "StateValuationFunctionActionMaskDouble", actionmask);
py::classh<storm::generator::ActionMask<double>> actionmask(m, "ActionMaskDouble");
py::classh<storm::generator::StateValuationFunctionMask<double>> actfuncmask(m, "StateValuationFunctionActionMaskDouble", actionmask);
actfuncmask.def(py::init<std::function<bool(storm::expressions::SimpleValuation const&, uint64_t)>>(), py::arg("f"));
}

Expand Down Expand Up @@ -296,7 +295,7 @@ void define_export_drn(py::module& m) {
}

void define_export(py::module& m) {
py::class_<storm::io::DirectEncodingExporterOptions>(m, "DirectEncodingExporterOptions")
py::classh<storm::io::DirectEncodingExporterOptions>(m, "DirectEncodingExporterOptions")
.def(py::init<>())
.def_readwrite("allow_placeholders", &storm::io::DirectEncodingExporterOptions::allowPlaceholders)
.def_readwrite("outputPrecision", &storm::io::DirectEncodingExporterOptions::outputPrecision);
Expand Down
10 changes: 5 additions & 5 deletions src/core/counterexample.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ using namespace storm::counterexamples;
void define_counterexamples(py::module& m) {
using FlatSet = boost::container::flat_set<uint64_t, std::less<uint64_t>, boost::container::new_allocator<uint64_t>>;

py::class_<FlatSet>(m, "FlatSet", "Container to pass to program")
py::classh<FlatSet>(m, "FlatSet", "Container to pass to program")
.def(py::init<>())
.def(py::init<FlatSet>(), "other"_a)
.def("insert", [](FlatSet& flatset, uint64_t value) { flatset.insert(value); })
Expand Down Expand Up @@ -37,7 +37,7 @@ void define_counterexamples(py::module& m) {

using CexGeneratorStats = SMTMinimalLabelSetGenerator<double>::GeneratorStats;

py::class_<CexGeneratorStats>(m, "SMTCounterExampleGeneratorStats", "Stats for highlevel counterexample generation")
py::classh<CexGeneratorStats>(m, "SMTCounterExampleGeneratorStats", "Stats for highlevel counterexample generation")
.def(py::init<>())
.def_readonly("analysis_time", &CexGeneratorStats::analysisTime)
.def_readonly("setup_time", &CexGeneratorStats::setupTime)
Expand All @@ -47,7 +47,7 @@ void define_counterexamples(py::module& m) {
.def_readonly("iterations", &CexGeneratorStats::iterations);

using CexGeneratorOptions = SMTMinimalLabelSetGenerator<double>::Options;
py::class_<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
py::classh<CexGeneratorOptions>(m, "SMTCounterExampleGeneratorOptions", "Options for highlevel counterexample generation")
.def(py::init<>())
.def_readwrite("check_threshold_feasible", &CexGeneratorOptions::checkThresholdFeasible)
.def_readwrite("encode_reachability", &CexGeneratorOptions::encodeReachability)
Expand All @@ -57,7 +57,7 @@ void define_counterexamples(py::module& m) {
.def_readwrite("maximum_counterexamples", &CexGeneratorOptions::maximumCounterexamples)
.def_readwrite("continue_after_first_counterexample", &CexGeneratorOptions::continueAfterFirstCounterexampleUntil)
.def_readwrite("maximum_iterations_after_counterexample", &CexGeneratorOptions::maximumExtraIterations);
py::class_<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend")
py::classh<SMTMinimalLabelSetGenerator<double>>(m, "SMTCounterExampleGenerator", "Highlevel Counterexample Generator with SMT as backend")
.def_static("precompute", &SMTMinimalLabelSetGenerator<double>::precompute, "Precompute input for counterexample generation", py::arg("env"),
py::arg("symbolic_model"), py::arg("model"), py::arg("formula"))
.def_static("build", &SMTMinimalLabelSetGenerator<double>::computeCounterexampleLabelSet, "Compute counterexample", py::arg("env"), py::arg("stats"),
Expand All @@ -66,7 +66,7 @@ void define_counterexamples(py::module& m) {
;

using CexInput = SMTMinimalLabelSetGenerator<double>::CexInput;
py::class_<CexInput>(m, "SMTCounterExampleInput", "Precomputed input for counterexample generation")
py::classh<CexInput>(m, "SMTCounterExampleInput", "Precomputed input for counterexample generation")
.def("add_reward_and_threshold", &CexInput::addRewardThresholdCombination, "add another reward structure and threshold", py::arg("reward_name"),
py::arg("threshold"));
}
22 changes: 11 additions & 11 deletions src/core/environment.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ void define_environment(py::module& m) {
.value("counter", storm::storage::SchedulerClass::MemoryPattern::Counter)
.finalize();

py::class_<storm::storage::SchedulerClass>(m, "SchedulerClass", "Scheduler class restriction")
py::classh<storm::storage::SchedulerClass>(m, "SchedulerClass", "Scheduler class restriction")
.def(py::init<>())
.def_property("deterministic", &storm::storage::SchedulerClass::isDeterministic,
[](storm::storage::SchedulerClass& sc, bool v) { sc.setIsDeterministic(v); })
Expand All @@ -133,15 +133,15 @@ void define_environment(py::module& m) {
.def("set_memory_pattern", [](storm::storage::SchedulerClass& sc, storm::storage::SchedulerClass::MemoryPattern p) { sc.setMemoryPattern(p); })
.def("set_positional", &storm::storage::SchedulerClass::setPositional);

py::class_<storm::Environment>(m, "Environment", "Environment")
py::classh<storm::Environment>(m, "Environment", "Environment")
.def(py::init<>(), "Construct default environment")
.def_property_readonly(
"solver_environment", [](storm::Environment& env) -> auto& { return env.solver(); }, "solver part of environment")
.def_property_readonly(
"model_checker_environment", [](storm::Environment& env) -> auto& { return env.modelchecker(); }, "model checker part of environment")
.def_property_readonly("dd_environment", [](storm::Environment& env) -> auto& { return env.dd(); }, "dd part of environment");

py::class_<storm::ConditionalModelCheckerEnvironment>(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking")
py::classh<storm::ConditionalModelCheckerEnvironment>(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking")
.def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm,
"algorithm for conditional model checking")
.def_property(
Expand All @@ -151,7 +151,7 @@ void define_environment(py::module& m) {
.def_property("relative", &storm::ConditionalModelCheckerEnvironment::isRelativePrecision,
&storm::ConditionalModelCheckerEnvironment::setRelativePrecision, "whether the precision is relative");

py::class_<storm::ModelCheckerEnvironment>(m, "ModelCheckerEnvironment", "Environment for the model checker")
py::classh<storm::ModelCheckerEnvironment>(m, "ModelCheckerEnvironment", "Environment for the model checker")
.def_property("steady_state_distribution_algorithm", &storm::ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm,
&storm::ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm, "steady state distribution algorithm used")
.def_property(
Expand All @@ -175,7 +175,7 @@ void define_environment(py::module& m) {
"multi", [](storm::ModelCheckerEnvironment& env) -> storm::MultiObjectiveModelCheckerEnvironment& { return env.multi(); },
py::return_value_policy::reference, "Access multi-objective sub-environment");

py::class_<storm::MultiObjectiveModelCheckerEnvironment>(m, "MultiObjectiveModelCheckerEnvironment", "Environment for multi-objective model checking")
py::classh<storm::MultiObjectiveModelCheckerEnvironment>(m, "MultiObjectiveModelCheckerEnvironment", "Environment for multi-objective model checking")
.def_property(
"method", [](storm::MultiObjectiveModelCheckerEnvironment const& env) { return env.getMethod(); },
&storm::MultiObjectiveModelCheckerEnvironment::setMethod, "multi-objective model checking method")
Expand Down Expand Up @@ -262,35 +262,35 @@ void define_environment(py::module& m) {
.def_property("print_results", &storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet,
&storm::MultiObjectiveModelCheckerEnvironment::setPrintResults);

py::class_<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers")
py::classh<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers")
.def("set_force_sound", &storm::SolverEnvironment::setForceSoundness, "force soundness", py::arg("new_value") = true)
.def("set_force_exact", &storm::SolverEnvironment::setForceExact, "force exact solving", py::arg("new_value") = true)
.def("set_linear_equation_solver_type", &storm::SolverEnvironment::setLinearEquationSolverType, "set solver type to use", py::arg("new_value"),
py::arg("set_from_default") = false)
.def_property_readonly("minmax_solver_environment", [](storm::SolverEnvironment& senv) -> auto& { return senv.minMax(); })
.def_property_readonly("native_solver_environment", [](storm::SolverEnvironment& senv) -> auto& { return senv.native(); });

py::class_<storm::NativeSolverEnvironment>(m, "NativeSolverEnvironment", "Environment for Native solvers")
py::classh<storm::NativeSolverEnvironment>(m, "NativeSolverEnvironment", "Environment for Native solvers")
.def_property("method", &storm::NativeSolverEnvironment::getMethod,
[](storm::NativeSolverEnvironment& nsenv, storm::solver::NativeLinearEquationSolverMethod const& m) { nsenv.setMethod(m); })
.def_property("maximum_iterations", &storm::NativeSolverEnvironment::getMaximalNumberOfIterations,
[](storm::NativeSolverEnvironment& nsenv, uint64_t iters) { nsenv.setMaximalNumberOfIterations(iters); })
.def_property("precision", &storm::NativeSolverEnvironment::getPrecision, &storm::NativeSolverEnvironment::setPrecision);

py::class_<storm::MinMaxSolverEnvironment>(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers")
py::classh<storm::MinMaxSolverEnvironment>(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers")
.def_property("method", &storm::MinMaxSolverEnvironment::getMethod,
[](storm::MinMaxSolverEnvironment& mmenv, storm::solver::MinMaxMethod const& m) { mmenv.setMethod(m, false); })
.def_property("precision", &storm::MinMaxSolverEnvironment::getPrecision, &storm::MinMaxSolverEnvironment::setPrecision);

py::class_<storm::DdEnvironment>(m, "DdEnvironment", "Environment for DD libraries")
py::classh<storm::DdEnvironment>(m, "DdEnvironment", "Environment for DD libraries")
.def_property_readonly("sylvan", [](storm::DdEnvironment& senv) -> auto& { return senv.sylvan(); })
.def_property_readonly("cudd", [](storm::DdEnvironment& senv) -> auto& { return senv.cudd(); });

py::class_<storm::SylvanDdManagerEnvironment>(m, "SylvanDdManagerEnvironment", "Environment for Sylvan Dd manager")
py::classh<storm::SylvanDdManagerEnvironment>(m, "SylvanDdManagerEnvironment", "Environment for Sylvan Dd manager")
.def_property("maximal_memory", &storm::SylvanDdManagerEnvironment::getMaximalMemory, &storm::SylvanDdManagerEnvironment::setMaximalMemory)
.def_property("number_threads", &storm::SylvanDdManagerEnvironment::getNumberOfThreads, &storm::SylvanDdManagerEnvironment::setNumberOfThreads);

py::class_<storm::CuddDdManagerEnvironment>(m, "CuddDdManagerEnvironment", "Environment for CUDD Dd manager")
py::classh<storm::CuddDdManagerEnvironment>(m, "CuddDdManagerEnvironment", "Environment for CUDD Dd manager")
.def_property("maximal_memory", &storm::CuddDdManagerEnvironment::getMaximalMemory, &storm::CuddDdManagerEnvironment::setMaximalMemory)
.def_property("constant_precision", &storm::CuddDdManagerEnvironment::getConstantPrecision, &storm::CuddDdManagerEnvironment::setConstantPrecision)
.def_property("reordering_enabled", &storm::CuddDdManagerEnvironment::isReorderingEnabled, &storm::CuddDdManagerEnvironment::setReorderingEnabled)
Expand Down
Loading
Loading