Consistent use of UPPER_CASE for enums.

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

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)"
    ]
   },

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)

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:

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."

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

src/core/core.cpp

@@ -221,8 +221,8 @@ void define_build(py::module& m) {
 
 void define_optimality_type(py::module& m) {
     py::native_enum<storm::solver::OptimizationDirection>(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<storm::solver::UncertaintyResolutionMode>(m, "UncertaintyResolutionMode", "enum.Enum")

src/core/environment.cpp

@@ -15,80 +15,80 @@
 
 void define_environment(py::module& m) {
     py::native_enum<storm::solver::EquationSolverType>(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<storm::solver::NativeLinearEquationSolverMethod>(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<storm::solver::MinMaxMethod>(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<storm::modelchecker::multiobjective::MultiObjectiveMethod>(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<storm::SteadyStateDistributionAlgorithm>(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<storm::ConditionalAlgorithmSetting>(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<storm::MultiObjectiveModelCheckerEnvironment::PrecisionType>(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<storm::MultiObjectiveModelCheckerEnvironment::EncodingType>(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<storm::storage::SchedulerClass::MemoryPattern>(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_<storm::storage::SchedulerClass>(m, "SchedulerClass", "Scheduler class restriction")

src/dft/analysis.cpp

@@ -38,7 +38,7 @@ void define_analysis(py::module& m) {
     py::native_enum<storm::dft::builder::ApproximationHeuristic>(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