From 3fcce60c78747906a8ee101d3b90a8f131eeae00 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Jun 2026 14:21:47 +0200 Subject: [PATCH 1/2] All enums are using UPPER_CASE naming --- doc/source/doc/analysis.ipynb | 4 +- examples/analysis/03-analysis.py | 4 +- examples/pomdp/01-pomdps.py | 8 +- lib/stormpy/pycarl/parse/__init__.py | 16 ++-- .../utility/multiobjective_plotting.py | 6 +- src/core/core.cpp | 4 +- src/core/environment.cpp | 84 +++++++++---------- src/dft/analysis.cpp | 2 +- src/pars/pla.cpp | 18 ++-- src/pomdp/memory.cpp | 14 ++-- src/pomdp/transformations.cpp | 10 +-- src/pycarl/mod_parse.cpp | 16 ++-- src/storage/dd.cpp | 6 +- src/storage/expressions.cpp | 46 +++++----- src/storage/umb.cpp | 24 +++--- src/utility/shortestPaths.cpp | 4 +- src/utility/smtsolver.cpp | 6 +- tests/core/test_modelchecking.py | 8 +- tests/pars/test_pla.py | 24 +++--- tests/storage/test_umb.py | 48 +++++------ tests/utility/test_shortestpaths.py | 2 +- tests/utility/test_smtsolver.py | 14 ++-- 22 files changed, 184 insertions(+), 184 deletions(-) diff --git a/doc/source/doc/analysis.ipynb b/doc/source/doc/analysis.ipynb index baa1b0ae31..467f05071d 100644 --- a/doc/source/doc/analysis.ipynb +++ b/doc/source/doc/analysis.ipynb @@ -135,8 +135,8 @@ "outputs": [], "source": [ "env = stormpy.Environment()\n", - "env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native)\n", - "env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.power_iteration\n", + "env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.NATIVE)\n", + "env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.POWER_ITERATION\n", "result = stormpy.model_checking(model, properties[0], environment=env)" ] }, diff --git a/examples/analysis/03-analysis.py b/examples/analysis/03-analysis.py index f7411913f8..e900b884ee 100644 --- a/examples/analysis/03-analysis.py +++ b/examples/analysis/03-analysis.py @@ -12,8 +12,8 @@ def example_analysis_03(): properties = stormpy.parse_properties(formula_str, prism_program) model = stormpy.build_model(prism_program, properties) env = stormpy.Environment() - env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.native) - env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.optimistic_value_iteration + env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.NATIVE) + env.solver_environment.native_solver_environment.method = stormpy.NativeLinearEquationSolverMethod.OPTIMISTIC_VALUE_ITERATION env.solver_environment.native_solver_environment.precision = stormpy.Rational("0.9") # env.solver_environment.native_solver_environment.maximum_iterations = 2 result = stormpy.model_checking(model, properties[0], environment=env) diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py index 87c1210351..cce061a1e2 100644 --- a/examples/pomdp/01-pomdps.py +++ b/examples/pomdp/01-pomdps.py @@ -33,11 +33,11 @@ def example_pomdps_01(): # # construct the memory for the FSC # # in this case, a selective counter with two states # memory_builder = stormpy.pomdp.PomdpMemoryBuilder() - # memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2) + # memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.SELECTIVE_COUNTER, 2) # # apply the memory onto the POMDP to get the cartesian product # pomdp = stormpy.pomdp.unfold_memory(pomdp, memory) # # apply the memory onto the POMDP to get the cartesian product - # pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear) + # pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.SIMPLE_LINEAR) #### # How to apply an unknown FSC to obtain a pMC from a pPOMDP @@ -57,13 +57,13 @@ def example_pomdps_01(): # construct the memory for the FSC # in this case, a selective counter with two states memory_builder = stormpy.pomdp.PomdpMemoryBuilder() - memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 3) + memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.SELECTIVE_COUNTER, 3) # apply the memory onto the POMDP to get the cartesian product pomdp = stormpy.pomdp.unfold_memory(pomdp, memory, add_memory_labels=True, keep_state_valuations=True) # make the POMDP simple. This step is optional but often beneficial pomdp = stormpy.pomdp.make_simple(pomdp, keep_state_valuations=True) # apply the unknown FSC to obtain a pmc from the POMDP - pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear) + pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.SIMPLE_LINEAR) export_pmc = False # Set to True to export the pMC as drn. if export_pmc: diff --git a/lib/stormpy/pycarl/parse/__init__.py b/lib/stormpy/pycarl/parse/__init__.py index 69d9486680..0ef0475765 100644 --- a/lib/stormpy/pycarl/parse/__init__.py +++ b/lib/stormpy/pycarl/parse/__init__.py @@ -31,20 +31,20 @@ def deserialize(input, package): if error: raise ParserError(error + " when parsing '" + input + "'") res_type = res.get_type() - if res_type == _parse._ParserReturnType.Rational: + if res_type == _parse._ParserReturnType.RATIONAL: return res.as_rational() - elif res_type == _parse._ParserReturnType.Variable: + elif res_type == _parse._ParserReturnType.VARIABLE: return res.as_variable() - elif res_type == _parse._ParserReturnType.Monomial: + elif res_type == _parse._ParserReturnType.MONOMIAL: return res.as_monomial() - elif res_type == _parse._ParserReturnType.Term: + elif res_type == _parse._ParserReturnType.TERM: return res.as_term() - elif res_type == _parse._ParserReturnType.Polynomial: + elif res_type == _parse._ParserReturnType.POLYNOMIAL: return res.as_polynomial() - elif res_type == _parse._ParserReturnType.RationalFunction: + elif res_type == _parse._ParserReturnType.RATIONAL_FUNCTION: return res.as_rational_function() - elif res_type == _parse._ParserReturnType.Constraint: + elif res_type == _parse._ParserReturnType.CONSTRAINT: return res.as_constraint() - elif res_type == _parse._ParserReturnType.Formula: + elif res_type == _parse._ParserReturnType.FORMULA: return res.as_formula() assert False, "Internal error." diff --git a/lib/stormpy/utility/multiobjective_plotting.py b/lib/stormpy/utility/multiobjective_plotting.py index 117510b3df..e7edab6cb2 100644 --- a/lib/stormpy/utility/multiobjective_plotting.py +++ b/lib/stormpy/utility/multiobjective_plotting.py @@ -35,14 +35,14 @@ def _prepare_points_for_convex_pareto_plotting(points, lower_corner, upper_corne """ def direction_as_operation(dir: stormpy.OptimizationDirection): - return max if dir == stormpy.OptimizationDirection.Maximize else min + return max if dir == stormpy.OptimizationDirection.MAXIMIZE else min if multi_obj_formula.nr_subformulas != 2: raise RuntimeError("Plotting is only supported for two dimensions") directions = [f.optimality_type for f in multi_obj_formula.subformulas] - origin_x = min(lower_corner[0], upper_corner[0]) if directions[0] == stormpy.OptimizationDirection.Maximize else max(lower_corner[0], upper_corner[0]) - origin_y = min(lower_corner[1], upper_corner[1]) if directions[1] == stormpy.OptimizationDirection.Maximize else max(lower_corner[1], upper_corner[1]) + origin_x = min(lower_corner[0], upper_corner[0]) if directions[0] == stormpy.OptimizationDirection.MAXIMIZE else max(lower_corner[0], upper_corner[0]) + origin_y = min(lower_corner[1], upper_corner[1]) if directions[1] == stormpy.OptimizationDirection.MAXIMIZE else max(lower_corner[1], upper_corner[1]) origin = np.array([[origin_x, origin_y]]) x_cut_x = direction_as_operation(directions[0])([p[0] for p in points]) x_cut = np.array([[x_cut_x, origin_y]]) diff --git a/src/core/core.cpp b/src/core/core.cpp index 7abecbf29f..ae9d335fe8 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -221,8 +221,8 @@ void define_build(py::module& m) { void define_optimality_type(py::module& m) { py::native_enum(m, "OptimizationDirection", "enum.Enum") - .value("Minimize", storm::solver::OptimizationDirection::Minimize) - .value("Maximize", storm::solver::OptimizationDirection::Maximize) + .value("MINIMIZE", storm::solver::OptimizationDirection::Minimize) + .value("MAXIMIZE", storm::solver::OptimizationDirection::Maximize) .finalize(); py::native_enum(m, "UncertaintyResolutionMode", "enum.Enum") diff --git a/src/core/environment.cpp b/src/core/environment.cpp index 4130b33d0b..57eca705b2 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -15,80 +15,80 @@ void define_environment(py::module& m) { py::native_enum(m, "EquationSolverType", "enum.Enum", "Solver type for equation systems") - .value("native", storm::solver::EquationSolverType::Native) - .value("eigen", storm::solver::EquationSolverType::Eigen) - .value("elimination", storm::solver::EquationSolverType::Elimination) - .value("gmmxx", storm::solver::EquationSolverType::Gmmxx) - .value("topological", storm::solver::EquationSolverType::Topological) + .value("NATIVE", storm::solver::EquationSolverType::Native) + .value("EIGEN", storm::solver::EquationSolverType::Eigen) + .value("ELIMINATION", storm::solver::EquationSolverType::Elimination) + .value("GMMXX", storm::solver::EquationSolverType::Gmmxx) + .value("TOPOLOGICAL", storm::solver::EquationSolverType::Topological) .finalize(); py::native_enum(m, "NativeLinearEquationSolverMethod", "enum.Enum", "Method for linear equation systems with the native solver") - .value("power_iteration", storm::solver::NativeLinearEquationSolverMethod::Power) - .value("sound_value_iteration", storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration) - .value("optimistic_value_iteration", storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration) - .value("interval_iteration", storm::solver::NativeLinearEquationSolverMethod::IntervalIteration) - .value("rational_search", storm::solver::NativeLinearEquationSolverMethod::RationalSearch) - .value("jacobi", storm::solver::NativeLinearEquationSolverMethod::Jacobi) + .value("POWER_ITERATION", storm::solver::NativeLinearEquationSolverMethod::Power) + .value("SOUND_VALUE_ITERATION", storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration) + .value("OPTIMISTIC_VALUE_ITERATION", storm::solver::NativeLinearEquationSolverMethod::OptimisticValueIteration) + .value("INTERVAL_ITERATION", storm::solver::NativeLinearEquationSolverMethod::IntervalIteration) + .value("RATIONAL_SEARCH", storm::solver::NativeLinearEquationSolverMethod::RationalSearch) + .value("JACOBI", storm::solver::NativeLinearEquationSolverMethod::Jacobi) .value("SOR", storm::solver::NativeLinearEquationSolverMethod::SOR) - .value("gauss_seidel", storm::solver::NativeLinearEquationSolverMethod::GaussSeidel) - .value("walker_chae", storm::solver::NativeLinearEquationSolverMethod::WalkerChae) + .value("GAUSS_SEIDEL", storm::solver::NativeLinearEquationSolverMethod::GaussSeidel) + .value("WALKER_CHAE", storm::solver::NativeLinearEquationSolverMethod::WalkerChae) .finalize(); py::native_enum(m, "MinMaxMethod", "enum.Enum", "Method for min-max equation systems") - .value("policy_iteration", storm::solver::MinMaxMethod::PolicyIteration) - .value("value_iteration", storm::solver::MinMaxMethod::ValueIteration) - .value("linear_programming", storm::solver::MinMaxMethod::LinearProgramming) - .value("topological", storm::solver::MinMaxMethod::Topological) - .value("rational_search", storm::solver::MinMaxMethod::RationalSearch) - .value("interval_iteration", storm::solver::MinMaxMethod::IntervalIteration) - .value("sound_value_iteration", storm::solver::MinMaxMethod::SoundValueIteration) - .value("optimistic_value_iteration", storm::solver::MinMaxMethod::OptimisticValueIteration) + .value("POLICY_ITERATION", storm::solver::MinMaxMethod::PolicyIteration) + .value("VALUE_ITERATION", storm::solver::MinMaxMethod::ValueIteration) + .value("LINEAR_PROGRAMMING", storm::solver::MinMaxMethod::LinearProgramming) + .value("TOPOLOGICAL", storm::solver::MinMaxMethod::Topological) + .value("RATIONAL_SEARCH", storm::solver::MinMaxMethod::RationalSearch) + .value("INTERVAL_ITERATION", storm::solver::MinMaxMethod::IntervalIteration) + .value("SOUND_VALUE_ITERATION", storm::solver::MinMaxMethod::SoundValueIteration) + .value("OPTIMISTIC_VALUE_ITERATION", storm::solver::MinMaxMethod::OptimisticValueIteration) .finalize(); // Multi-objective related enums py::native_enum(m, "MultiObjectiveMethod", "enum.Enum", "Multi-objective model checking method") - .value("pcaa", storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa) - .value("constraint_based", storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased) + .value("PCAA", storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa) + .value("CONSTRAINT_BASED", storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased) .finalize(); // Added enums for model checker environment py::native_enum(m, "SteadyStateDistributionAlgorithm", "enum.Enum", "Algorithm for steady state distribution computation") - .value("automatic", storm::SteadyStateDistributionAlgorithm::Automatic) - .value("equation_system", storm::SteadyStateDistributionAlgorithm::EquationSystem) - .value("expected_visiting_times", storm::SteadyStateDistributionAlgorithm::ExpectedVisitingTimes) - .value("classic", storm::SteadyStateDistributionAlgorithm::Classic) + .value("AUTOMATIC", storm::SteadyStateDistributionAlgorithm::Automatic) + .value("EQUATION_SYSTEM", storm::SteadyStateDistributionAlgorithm::EquationSystem) + .value("EXPECTED_VISITING_TIMES", storm::SteadyStateDistributionAlgorithm::ExpectedVisitingTimes) + .value("CLASSIC", storm::SteadyStateDistributionAlgorithm::Classic) .finalize(); py::native_enum(m, "ConditionalAlgorithmSetting", "enum.Enum", "Algorithm used for conditional model checking") - .value("default", storm::ConditionalAlgorithmSetting::Default) - .value("restart", storm::ConditionalAlgorithmSetting::Restart) - .value("bisection", storm::ConditionalAlgorithmSetting::Bisection) - .value("bisection_advanced", storm::ConditionalAlgorithmSetting::BisectionAdvanced) - .value("bisection_pt", storm::ConditionalAlgorithmSetting::BisectionPolicyTracking) - .value("bisection_advanced_pt", storm::ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking) - .value("policy_iteration", storm::ConditionalAlgorithmSetting::PolicyIteration) + .value("DEFAULT", storm::ConditionalAlgorithmSetting::Default) + .value("RESTART", storm::ConditionalAlgorithmSetting::Restart) + .value("BISECTION", storm::ConditionalAlgorithmSetting::Bisection) + .value("BISECTION_ADVANCED", storm::ConditionalAlgorithmSetting::BisectionAdvanced) + .value("BISECTION_PT", storm::ConditionalAlgorithmSetting::BisectionPolicyTracking) + .value("BISECTION_ADVANCED_PT", storm::ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking) + .value("POLICY_ITERATION", storm::ConditionalAlgorithmSetting::PolicyIteration) .finalize(); py::native_enum(m, "MultiObjectivePrecisionType", "enum.Enum", "Type of precision for multi-objective model checking") - .value("absolute", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute) - .value("relative_to_diff", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::RelativeToDiff) + .value("ABSOLUTE", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute) + .value("RELATIVE_TO_DIFF", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::RelativeToDiff) .finalize(); py::native_enum(m, "MultiObjectiveEncodingType", "enum.Enum", "Encoding type for multi-objective model checking") - .value("auto", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) - .value("classic", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic) - .value("flow", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow) + .value("AUTO", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) + .value("CLASSIC", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic) + .value("FLOW", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow) .finalize(); // Scheduler class bindings (needed for scheduler restriction) py::native_enum(m, "SchedulerMemoryPattern", "enum.Enum", "Memory pattern of a scheduler") - .value("arbitrary", storm::storage::SchedulerClass::MemoryPattern::Arbitrary) - .value("goal_memory", storm::storage::SchedulerClass::MemoryPattern::GoalMemory) - .value("counter", storm::storage::SchedulerClass::MemoryPattern::Counter) + .value("ARBITRARY", storm::storage::SchedulerClass::MemoryPattern::Arbitrary) + .value("GOAL_MEMORY", storm::storage::SchedulerClass::MemoryPattern::GoalMemory) + .value("COUNTER", storm::storage::SchedulerClass::MemoryPattern::Counter) .finalize(); py::class_(m, "SchedulerClass", "Scheduler class restriction") diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index 7599e7cbfe..9ae13689aa 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -38,7 +38,7 @@ void define_analysis(py::module& m) { py::native_enum(m, "ApproximationHeuristic", "enum.Enum", "Heuristic for selecting states to explore next") .value("DEPTH", storm::dft::builder::ApproximationHeuristic::DEPTH) .value("PROBABILITY", storm::dft::builder::ApproximationHeuristic::PROBABILITY) - .value("BOUNDDIFFERENCE", storm::dft::builder::ApproximationHeuristic::BOUNDDIFFERENCE) + .value("BOUND_DIFFERENCE", storm::dft::builder::ApproximationHeuristic::BOUNDDIFFERENCE) .finalize(); // RelevantEvents diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 178470ea2c..627c50276b 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -95,13 +95,13 @@ std::set gatherDerivatives(storm::models::sparse::Model(m, "RegionResult", "enum.Enum", "Types of region check results") - .value("EXISTSSAT", storm::modelchecker::RegionResult::ExistsSat) - .value("EXISTSVIOLATED", storm::modelchecker::RegionResult::ExistsViolated) - .value("EXISTSBOTH", storm::modelchecker::RegionResult::ExistsBoth) - .value("CENTERSAT", storm::modelchecker::RegionResult::CenterSat) - .value("CENTERVIOLATED", storm::modelchecker::RegionResult::CenterViolated) - .value("ALLSAT", storm::modelchecker::RegionResult::AllSat) - .value("ALLVIOLATED", storm::modelchecker::RegionResult::AllViolated) + .value("EXISTS_SAT", storm::modelchecker::RegionResult::ExistsSat) + .value("EXISTS_VIOLATED", storm::modelchecker::RegionResult::ExistsViolated) + .value("EXISTS_BOTH", storm::modelchecker::RegionResult::ExistsBoth) + .value("CENTER_SAT", storm::modelchecker::RegionResult::CenterSat) + .value("CENTER_VIOLATED", storm::modelchecker::RegionResult::CenterViolated) + .value("ALL_SAT", storm::modelchecker::RegionResult::AllSat) + .value("ALL_VIOLATED", storm::modelchecker::RegionResult::AllViolated) .value("UNKNOWN", storm::modelchecker::RegionResult::Unknown) .finalize(); m.attr("RegionResult").attr("friendly_name") = @@ -110,8 +110,8 @@ void define_pla(py::module& m) { // RegionResultHypothesis py::native_enum(m, "RegionResultHypothesis", "enum.Enum", "Hypothesis for the result of a parameter region") .value("UNKNOWN", storm::modelchecker::RegionResultHypothesis::Unknown) - .value("ALLSAT", storm::modelchecker::RegionResultHypothesis::AllSat) - .value("ALLVIOLATED", storm::modelchecker::RegionResultHypothesis::AllViolated) + .value("ALL_SAT", storm::modelchecker::RegionResultHypothesis::AllSat) + .value("ALL_VIOLATED", storm::modelchecker::RegionResultHypothesis::AllViolated) .finalize(); m.attr("RegionResultHypothesis").attr("friendly_name") = py::cpp_function(&streamToString, py::name("friendly_name"), py::is_method(m.attr("RegionResultHypothesis"))); diff --git a/src/pomdp/memory.cpp b/src/pomdp/memory.cpp index f5fb9166a3..acbb4acc5d 100644 --- a/src/pomdp/memory.cpp +++ b/src/pomdp/memory.cpp @@ -10,13 +10,13 @@ void define_memory(py::module& m) { // Trivial, FixedCounter, SelectiveCounter, FixedRing, SelectiveRing, SettableBits, Full py::native_enum(m, "PomdpMemoryPattern", "enum.Enum", "Memory pattern for POMDP memory") - .value("trivial", storm::storage::PomdpMemoryPattern::Trivial) - .value("fixed_counter", storm::storage::PomdpMemoryPattern::FixedCounter) - .value("selective_counter", storm::storage::PomdpMemoryPattern::SelectiveCounter) - .value("fixed_ring", storm::storage::PomdpMemoryPattern::FixedRing) - .value("selective_ring", storm::storage::PomdpMemoryPattern::SelectiveRing) - .value("settable_bits", storm::storage::PomdpMemoryPattern::SettableBits) - .value("full", storm::storage::PomdpMemoryPattern::Full) + .value("TRIVIAL", storm::storage::PomdpMemoryPattern::Trivial) + .value("FIXED_COUNTER", storm::storage::PomdpMemoryPattern::FixedCounter) + .value("SELECTIVE_COUNTER", storm::storage::PomdpMemoryPattern::SelectiveCounter) + .value("FIXED_RING", storm::storage::PomdpMemoryPattern::FixedRing) + .value("SELECTIVE_RING", storm::storage::PomdpMemoryPattern::SelectiveRing) + .value("SETTABLE_BITS", storm::storage::PomdpMemoryPattern::SettableBits) + .value("FULL", storm::storage::PomdpMemoryPattern::Full) .finalize(); py::class_ memorybuilder(m, "PomdpMemoryBuilder", "MemoryBuilder for POMDP policies"); diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 5eb5503b97..da5629e6dd 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -49,11 +49,11 @@ std::shared_ptr> unfold_trace(storm::model // STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL void define_transformations_nt(py::module &m) { py::native_enum(m, "PomdpFscApplicationMode", "enum.Enum") - .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) - .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) - .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) - .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) - .value("full", storm::transformer::PomdpFscApplicationMode::FULL) + .value("STANDARD", storm::transformer::PomdpFscApplicationMode::STANDARD) + .value("SIMPLE_LINEAR", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) + .value("SIMPLE_LINEAR_INVERSE", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) + .value("SIMPLE_LOG", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) + .value("FULL", storm::transformer::PomdpFscApplicationMode::FULL) .finalize(); py::class_ options(m, "ObservationTraceUnfolderOptions", "Options for unfolding observation traces"); options.def(py::init<>()); diff --git a/src/pycarl/mod_parse.cpp b/src/pycarl/mod_parse.cpp index dc3375d227..d01b30e8ef 100644 --- a/src/pycarl/mod_parse.cpp +++ b/src/pycarl/mod_parse.cpp @@ -14,13 +14,13 @@ PYBIND11_MODULE(_parse, m) { m.import("stormpy.pycarl"); py::native_enum(m, "_ParserReturnType", "enum.Enum") - .value("Rational", carlparser::ParserReturnType::Rational) - .value("Variable", carlparser::ParserReturnType::Variable) - .value("Monomial", carlparser::ParserReturnType::Monomial) - .value("Term", carlparser::ParserReturnType::Term) - .value("Polynomial", carlparser::ParserReturnType::Polynomial) - .value("RationalFunction", carlparser::ParserReturnType::RationalFunction) - .value("Constraint", carlparser::ParserReturnType::Constraint) - .value("Formula", carlparser::ParserReturnType::Formula) + .value("RATIONAL", carlparser::ParserReturnType::Rational) + .value("VARIABLE", carlparser::ParserReturnType::Variable) + .value("MONOMIAL", carlparser::ParserReturnType::Monomial) + .value("TERM", carlparser::ParserReturnType::Term) + .value("POLYNOMIAL", carlparser::ParserReturnType::Polynomial) + .value("RATIONAL_FUNCTION", carlparser::ParserReturnType::RationalFunction) + .value("CONSTRAINT", carlparser::ParserReturnType::Constraint) + .value("FORMULA", carlparser::ParserReturnType::Formula) .finalize(); } diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp index 0419dd78ca..d08eaf51bd 100644 --- a/src/storage/dd.cpp +++ b/src/storage/dd.cpp @@ -41,9 +41,9 @@ void define_dd(py::module& m, std::string const& libstring) { void define_dd_nt(py::module& m) { py::native_enum(m, "DdMetaVariableType", "enum.Enum") - .value("Int", storm::dd::MetaVariableType::Int) - .value("Bool", storm::dd::MetaVariableType::Bool) - .value("Bitvector", storm::dd::MetaVariableType::BitVector) + .value("INT", storm::dd::MetaVariableType::Int) + .value("BOOL", storm::dd::MetaVariableType::Bool) + .value("BITVECTOR", storm::dd::MetaVariableType::BitVector) .finalize(); } diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 6d4950c8c2..878a2b4501 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -53,29 +53,29 @@ void define_expressions(py::module& m) { .def("__hash__", &storm::expressions::Variable::getIndex); py::native_enum(m, "OperatorType", "enum.Enum", "Type of an operator (of any sort)") - .value("And", storm::expressions::OperatorType::And) - .value("Or", storm::expressions::OperatorType::Or) - .value("Xor", storm::expressions::OperatorType::Xor) - .value("Implies", storm::expressions::OperatorType::Implies) - .value("Iff", storm::expressions::OperatorType::Iff) - .value("Plus", storm::expressions::OperatorType::Plus) - .value("Minus", storm::expressions::OperatorType::Minus) - .value("Times", storm::expressions::OperatorType::Times) - .value("Divide", storm::expressions::OperatorType::Divide) - .value("Min", storm::expressions::OperatorType::Min) - .value("Max", storm::expressions::OperatorType::Max) - .value("Power", storm::expressions::OperatorType::Power) - .value("Modulo", storm::expressions::OperatorType::Modulo) - .value("Equal", storm::expressions::OperatorType::Equal) - .value("NotEqual", storm::expressions::OperatorType::NotEqual) - .value("Less", storm::expressions::OperatorType::Less) - .value("LessOrEqual", storm::expressions::OperatorType::LessOrEqual) - .value("Greater", storm::expressions::OperatorType::Greater) - .value("GreaterOrEqual", storm::expressions::OperatorType::GreaterOrEqual) - .value("Not", storm::expressions::OperatorType::Not) - .value("Floor", storm::expressions::OperatorType::Floor) - .value("Ceil", storm::expressions::OperatorType::Ceil) - .value("Ite", storm::expressions::OperatorType::Ite) + .value("AND", storm::expressions::OperatorType::And) + .value("OR", storm::expressions::OperatorType::Or) + .value("XOR", storm::expressions::OperatorType::Xor) + .value("IMPLIES", storm::expressions::OperatorType::Implies) + .value("IFF", storm::expressions::OperatorType::Iff) + .value("PLUS", storm::expressions::OperatorType::Plus) + .value("MINUS", storm::expressions::OperatorType::Minus) + .value("TIMES", storm::expressions::OperatorType::Times) + .value("DIVIDE", storm::expressions::OperatorType::Divide) + .value("MIN", storm::expressions::OperatorType::Min) + .value("MAX", storm::expressions::OperatorType::Max) + .value("POWER", storm::expressions::OperatorType::Power) + .value("MODULO", storm::expressions::OperatorType::Modulo) + .value("EQUAL", storm::expressions::OperatorType::Equal) + .value("NOT_EQUAL", storm::expressions::OperatorType::NotEqual) + .value("LESS", storm::expressions::OperatorType::Less) + .value("LESS_OR_EQUAL", storm::expressions::OperatorType::LessOrEqual) + .value("GREATER", storm::expressions::OperatorType::Greater) + .value("GREATER_OR_EQUAL", storm::expressions::OperatorType::GreaterOrEqual) + .value("NOT", storm::expressions::OperatorType::Not) + .value("FLOOR", storm::expressions::OperatorType::Floor) + .value("CEIL", storm::expressions::OperatorType::Ceil) + .value("ITE", storm::expressions::OperatorType::Ite) .finalize(); // Expression diff --git a/src/storage/umb.cpp b/src/storage/umb.cpp index a03638e1e8..d1829f3d3f 100644 --- a/src/storage/umb.cpp +++ b/src/storage/umb.cpp @@ -16,16 +16,16 @@ void define_umb(py::module& m) { py::native_enum(m, "CompressionMode", "enum.Enum", "Compression mode for UMB archives") - .value("Default", storm::io::CompressionMode::Default) - .value("NoCompression", storm::io::CompressionMode::None) - .value("Gzip", storm::io::CompressionMode::Gzip) - .value("Xz", storm::io::CompressionMode::Xz) + .value("DEFAULT", storm::io::CompressionMode::Default) + .value("NO_COMPRESSION", storm::io::CompressionMode::None) + .value("GZIP", storm::io::CompressionMode::Gzip) + .value("XZ", storm::io::CompressionMode::Xz) .finalize(); py::native_enum(m, "UmbImportValueType", "enum.Enum", "Value type for UMB import") - .value("Default", storm::umb::ImportOptions::ValueType::Default) - .value("Rational", storm::umb::ImportOptions::ValueType::Rational) - .value("Double", storm::umb::ImportOptions::ValueType::Double) + .value("DEFAULT", storm::umb::ImportOptions::ValueType::Default) + .value("RATIONAL", storm::umb::ImportOptions::ValueType::Rational) + .value("DOUBLE", storm::umb::ImportOptions::ValueType::Double) .finalize(); py::class_(m, "UmbImportOptions", "Options for importing UMB models") @@ -35,11 +35,11 @@ void define_umb(py::module& m) { .def_readwrite("build_state_valuations", &storm::umb::ImportOptions::buildStateValuations, "Whether to build state valuations"); py::native_enum(m, "UmbExportValueType", "enum.Enum", "Value type for UMB export") - .value("Default", storm::umb::ExportOptions::ValueType::Default) - .value("Rational", storm::umb::ExportOptions::ValueType::Rational) - .value("Double", storm::umb::ExportOptions::ValueType::Double) - .value("DoubleInterval", storm::umb::ExportOptions::ValueType::DoubleInterval) - .value("RationalInterval", storm::umb::ExportOptions::ValueType::RationalInterval) + .value("DEFAULT", storm::umb::ExportOptions::ValueType::Default) + .value("RATIONAL", storm::umb::ExportOptions::ValueType::Rational) + .value("DOUBLE", storm::umb::ExportOptions::ValueType::Double) + .value("DOUBLE_INTERVAL", storm::umb::ExportOptions::ValueType::DoubleInterval) + .value("RATIONAL_INTERVAL", storm::umb::ExportOptions::ValueType::RationalInterval) .finalize(); py::class_(m, "UmbExportOptions", "Options for exporting UMB models") diff --git a/src/utility/shortestPaths.cpp b/src/utility/shortestPaths.cpp index 82f86eda32..1fdb216d48 100644 --- a/src/utility/shortestPaths.cpp +++ b/src/utility/shortestPaths.cpp @@ -40,8 +40,8 @@ void define_ksp(py::module& m) { .def_readwrite("distance", &Path::distance); py::native_enum(m, "MatrixFormat", "enum.Enum") - .value("Straight", MatrixFormat::straight) - .value("I_Minus_P", MatrixFormat::iMinusP) + .value("STRAIGHT", MatrixFormat::straight) + .value("I_MINUS_P", MatrixFormat::iMinusP) .finalize(); py::class_(m, "ShortestPathsGenerator") diff --git a/src/utility/smtsolver.cpp b/src/utility/smtsolver.cpp index ce3f3b8ac3..daeee88ffd 100644 --- a/src/utility/smtsolver.cpp +++ b/src/utility/smtsolver.cpp @@ -11,9 +11,9 @@ void define_smt(py::module& m) { using ModelReference = storm::solver::SmtSolver::ModelReference; py::native_enum(m, "SmtCheckResult", "enum.Enum", "Result type") - .value("Sat", SmtSolver::CheckResult::Sat) - .value("Unsat", SmtSolver::CheckResult::Unsat) - .value("Unknown", SmtSolver::CheckResult::Unknown) + .value("SAT", SmtSolver::CheckResult::Sat) + .value("UNSAT", SmtSolver::CheckResult::Unsat) + .value("UNKNOWN", SmtSolver::CheckResult::Unknown) .finalize(); py::class_> modelref(m, "ModelReference", "Lightweight Wrapper around results"); diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 6975f1c94e..a06b6a764c 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -52,7 +52,7 @@ def test_model_checking_interval_dtmc(self): assert initial_state == 0 env = stormpy.Environment() - env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION task = stormpy.CheckTask(formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() @@ -72,7 +72,7 @@ def test_model_checking_interval_mdp(self): assert initial_state == 0 env = stormpy.Environment() - env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION task = stormpy.CheckTask(formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() @@ -104,7 +104,7 @@ def test_model_checking_exact_interval_dtmc(self): assert initial_state == 0 env = stormpy.Environment() - env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() @@ -124,7 +124,7 @@ def test_model_checking_exact_interval_mdp(self): assert initial_state == 0 env = stormpy.Environment() - env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.VALUE_ITERATION task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) task.set_produce_schedulers() diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 468f9f5b11..3184fe4ec8 100644 --- a/tests/pars/test_pla.py +++ b/tests/pars/test_pla.py @@ -9,13 +9,13 @@ class TestPLA: def test_to_string(self): assert stormpy.pars.RegionResultHypothesis.UNKNOWN.friendly_name() == "Unknown" - assert stormpy.pars.RegionResultHypothesis.ALLSAT.friendly_name() == "AllSat?" - assert stormpy.pars.RegionResult.EXISTSVIOLATED.friendly_name() == "ExistsViolated" - assert stormpy.pars.RegionResult.ALLSAT.friendly_name() == "AllSat" + assert stormpy.pars.RegionResultHypothesis.ALL_SAT.friendly_name() == "AllSat?" + assert stormpy.pars.RegionResult.EXISTS_VIOLATED.friendly_name() == "ExistsViolated" + assert stormpy.pars.RegionResult.ALL_SAT.friendly_name() == "AllSat" def test_name(self): - assert stormpy.pars.RegionResult.ALLSAT.name == "ALLSAT" - assert stormpy.pars.RegionResultHypothesis.ALLSAT.name == "ALLSAT" + assert stormpy.pars.RegionResult.ALL_SAT.name == "ALL_SAT" + assert stormpy.pars.RegionResultHypothesis.ALL_SAT.name == "ALL_SAT" def test_pla(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) @@ -32,13 +32,13 @@ def test_pla(self): assert len(parameters) == 2 region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) result = checker.check_region(env, region) - assert result == stormpy.pars.RegionResult.ALLSAT + assert result == stormpy.pars.RegionResult.ALL_SAT region = stormpy.pars.ParameterRegion.create_from_string("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters) result = checker.check_region(env, region, stormpy.pars.RegionResultHypothesis.UNKNOWN, True) - assert result == stormpy.pars.RegionResult.EXISTSBOTH + assert result == stormpy.pars.RegionResult.EXISTS_BOTH region = stormpy.pars.ParameterRegion.create_from_string("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) result = checker.check_region(env, region) - assert result == stormpy.pars.RegionResult.ALLVIOLATED + assert result == stormpy.pars.RegionResult.ALL_VIOLATED def test_pla_region_valuation(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) @@ -65,16 +65,16 @@ def test_pla_region_valuation(self): region_valuation[pK] = (stormpy.RationalRF(0.75), stormpy.RationalRF(0.95)) region = stormpy.pars.ParameterRegion(region_valuation) result = checker.check_region(env, region) - assert result == stormpy.pars.RegionResult.ALLSAT + assert result == stormpy.pars.RegionResult.ALL_SAT region_valuation[pL] = (stormpy.RationalRF(0.4), stormpy.RationalRF(0.65)) region = stormpy.pars.ParameterRegion(region_valuation) result = checker.check_region(env, region, stormpy.pars.RegionResultHypothesis.UNKNOWN, True) - assert result == stormpy.pars.RegionResult.EXISTSBOTH + assert result == stormpy.pars.RegionResult.EXISTS_BOTH region_valuation[pK] = (stormpy.RationalRF(0.2), stormpy.RationalRF(0.715)) region_valuation[pL] = (stormpy.RationalRF(0.1), stormpy.RationalRF(0.73)) region = stormpy.pars.ParameterRegion(region_valuation) result = checker.check_region(env, region) - assert result == stormpy.pars.RegionResult.ALLVIOLATED + assert result == stormpy.pars.RegionResult.ALL_VIOLATED def test_pla_bounds(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) @@ -152,7 +152,7 @@ def test_compute_extremum(self): refinement_checker = stormpy.pars.create_region_refinement_checker(env, model, formulas[0].raw_formula) precision = stormpy.RationalRF(1e-6) - value, point = refinement_checker.compute_extremum(env, region, stormpy.OptimizationDirection.Maximize, precision, False) + value, point = refinement_checker.compute_extremum(env, region, stormpy.OptimizationDirection.MAXIMIZE, precision, False) assert isinstance(value, stormpy.RationalRF) assert isinstance(point, dict) assert len(point) == 2 diff --git a/tests/storage/test_umb.py b/tests/storage/test_umb.py index b383c6c939..ba8cd761f7 100644 --- a/tests/storage/test_umb.py +++ b/tests/storage/test_umb.py @@ -28,49 +28,49 @@ def test_import_options_defaults(self): opts = stormpy.UmbImportOptions() assert opts.build_choice_labeling is True assert opts.build_state_valuations is True - assert opts.value_type == stormpy.UmbImportValueType.Default + assert opts.value_type == stormpy.UmbImportValueType.DEFAULT def test_export_options_defaults(self): opts = stormpy.UmbExportOptions() assert opts.allow_choice_labeling_as_actions is True assert opts.allow_choice_origins_as_actions is False assert opts.canonicize_pomdp is True - assert opts.compression == stormpy.CompressionMode.Default - assert opts.value_type == stormpy.UmbExportValueType.Default + assert opts.compression == stormpy.CompressionMode.DEFAULT + assert opts.value_type == stormpy.UmbExportValueType.DEFAULT def test_import_options_set(self): opts = stormpy.UmbImportOptions() - opts.value_type = stormpy.UmbImportValueType.Double + opts.value_type = stormpy.UmbImportValueType.DOUBLE opts.build_choice_labeling = False opts.build_state_valuations = False - assert opts.value_type == stormpy.UmbImportValueType.Double + assert opts.value_type == stormpy.UmbImportValueType.DOUBLE assert opts.build_choice_labeling is False assert opts.build_state_valuations is False def test_export_options_set(self): opts = stormpy.UmbExportOptions() - opts.compression = stormpy.CompressionMode.Gzip - opts.value_type = stormpy.UmbExportValueType.Rational - assert opts.compression == stormpy.CompressionMode.Gzip - assert opts.value_type == stormpy.UmbExportValueType.Rational + opts.compression = stormpy.CompressionMode.GZIP + opts.value_type = stormpy.UmbExportValueType.RATIONAL + assert opts.compression == stormpy.CompressionMode.GZIP + assert opts.value_type == stormpy.UmbExportValueType.RATIONAL def test_compression_mode_enum(self): - assert stormpy.CompressionMode.Default - assert stormpy.CompressionMode.Gzip - assert stormpy.CompressionMode.Xz - assert stormpy.CompressionMode.NoCompression + assert stormpy.CompressionMode.DEFAULT + assert stormpy.CompressionMode.GZIP + assert stormpy.CompressionMode.XZ + assert stormpy.CompressionMode.NO_COMPRESSION def test_import_value_type_enum(self): - assert stormpy.UmbImportValueType.Default - assert stormpy.UmbImportValueType.Rational - assert stormpy.UmbImportValueType.Double + assert stormpy.UmbImportValueType.DEFAULT + assert stormpy.UmbImportValueType.RATIONAL + assert stormpy.UmbImportValueType.DOUBLE def test_export_value_type_enum(self): - assert stormpy.UmbExportValueType.Default - assert stormpy.UmbExportValueType.Rational - assert stormpy.UmbExportValueType.Double - assert stormpy.UmbExportValueType.DoubleInterval - assert stormpy.UmbExportValueType.RationalInterval + assert stormpy.UmbExportValueType.DEFAULT + assert stormpy.UmbExportValueType.RATIONAL + assert stormpy.UmbExportValueType.DOUBLE + assert stormpy.UmbExportValueType.DOUBLE_INTERVAL + assert stormpy.UmbExportValueType.RATIONAL_INTERVAL class TestUmbModel: @@ -117,7 +117,7 @@ def test_export_and_build_mdp(self, mdp, tmp_umb): def test_export_with_gzip(self, dtmc, tmp_umb): opts = stormpy.UmbExportOptions() - opts.compression = stormpy.CompressionMode.Gzip + opts.compression = stormpy.CompressionMode.GZIP stormpy.export_to_umb(dtmc, tmp_umb, opts) model2 = stormpy.build_from_umb(tmp_umb) assert type(dtmc) == type(model2) @@ -144,7 +144,7 @@ def test_mdp_short_round_trip(self, mdp): def test_dtmc_gzip_round_trip(self, dtmc, tmp_umb): export_opts = stormpy.UmbExportOptions() - export_opts.compression = stormpy.CompressionMode.Gzip + export_opts.compression = stormpy.CompressionMode.GZIP umb = stormpy.sparse_model_to_umb(dtmc, export_opts) stormpy.umb_to_archive(umb, tmp_umb, export_opts) assert os.path.getsize(tmp_umb) > 0 @@ -154,7 +154,7 @@ def test_dtmc_gzip_round_trip(self, dtmc, tmp_umb): def test_dtmc_xz_round_trip(self, dtmc, tmp_umb): export_opts = stormpy.UmbExportOptions() - export_opts.compression = stormpy.CompressionMode.Xz + export_opts.compression = stormpy.CompressionMode.XZ umb = stormpy.sparse_model_to_umb(dtmc, export_opts) stormpy.umb_to_archive(umb, tmp_umb, export_opts) assert os.path.getsize(tmp_umb) > 0 diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index ea63cbaada..e2b09210cc 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -110,7 +110,7 @@ def initial_states(model): @pytest.fixture def matrix_format(): - return MatrixFormat.Straight + return MatrixFormat.STRAIGHT class TestShortestPaths: diff --git a/tests/utility/test_smtsolver.py b/tests/utility/test_smtsolver.py index c2e8fe00ca..afdd7d5d8b 100644 --- a/tests/utility/test_smtsolver.py +++ b/tests/utility/test_smtsolver.py @@ -12,11 +12,11 @@ def test_smtsolver_trivial(self): manager = stormpy.ExpressionManager() solver = stormpy.utility.Z3SmtSolver(manager) solver.add(manager.create_boolean(True)) - assert solver.check() != stormpy.utility.SmtCheckResult.Unsat - assert solver.check() == stormpy.utility.SmtCheckResult.Sat + assert solver.check() != stormpy.utility.SmtCheckResult.UNSAT + assert solver.check() == stormpy.utility.SmtCheckResult.SAT solver.add(manager.create_boolean(False)) - assert solver.check() == stormpy.utility.SmtCheckResult.Unsat - assert solver.check() != stormpy.utility.SmtCheckResult.Sat + assert solver.check() == stormpy.utility.SmtCheckResult.UNSAT + assert solver.check() != stormpy.utility.SmtCheckResult.SAT def test_smtsolver_arithmetic_unsat(self): manager = stormpy.ExpressionManager() @@ -27,7 +27,7 @@ def test_smtsolver_arithmetic_unsat(self): solver = stormpy.utility.Z3SmtSolver(manager) solver.add(c1) solver.add(c2) - assert solver.check() == stormpy.utility.SmtCheckResult.Unsat + assert solver.check() == stormpy.utility.SmtCheckResult.UNSAT def test_smtsolver_arithmetic_unsat(self): manager = stormpy.ExpressionManager() @@ -38,7 +38,7 @@ def test_smtsolver_arithmetic_unsat(self): solver = stormpy.utility.Z3SmtSolver(manager) solver.add(c1) solver.add(c2) - assert solver.check() == stormpy.utility.SmtCheckResult.Unsat + assert solver.check() == stormpy.utility.SmtCheckResult.UNSAT def test_smtsolver_arithmetic_unsat(self): manager = stormpy.ExpressionManager() @@ -49,5 +49,5 @@ def test_smtsolver_arithmetic_unsat(self): solver = stormpy.utility.Z3SmtSolver(manager) solver.add(c1) solver.add(c2) - assert solver.check() == stormpy.utility.SmtCheckResult.Sat + assert solver.check() == stormpy.utility.SmtCheckResult.SAT assert solver.model.get_integer_value(x) == 1 From 0c49ea69f3c2dc241777b7391f8e77d1ce937ef7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 9 Jun 2026 14:48:28 +0200 Subject: [PATCH 2/2] Added enum convention to developer's guide --- doc/source/development.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/source/development.md b/doc/source/development.md index ee939896ac..571813534e 100644 --- a/doc/source/development.md +++ b/doc/source/development.md @@ -14,6 +14,12 @@ The following contains some general guidelines for developers. Proper formatting can be ensured by executing ``black .``. The CI automatically checks for proper formatting as well. +### Enum naming +- Enum values exposed to Python via `py::native_enum` must use `UPPER_CASE_WITH_UNDERSCORES`. + The string name in `.value("NAME", ...)` calls must match `[A-Z][A-Z0-9]*(_[A-Z0-9]+)*`. + Compound words must use underscores (e.g., `POWER_ITERATION`, not `POWERITERATION` or `power_iteration`). + Short abbreviations (e.g., `DTMC`, `SOR`, `EQ`) are acceptable. + ## Dependencies - The bindings are created with [pybind11](https://pybind11.readthedocs.io).