Stormpy's types match Storm's ValueTypes

CHANGELOG.md

@@ -4,6 +4,14 @@ Changelog
 Version 1.14.x
 --------------
 
+### Version 1.14.1 (in development)
+
+- Revised number types:
+    * `stormpy.Polynomial` and `stormpy.RationalFunction` now refer to the correct (factorized) Storm number types and were formerly named `stormpy.FactorizedPolynomial` and `stormpy.FactorizedRationalFunction`.
+    * `stormpy.RawPolynomial` refers to the non-factorized polynomial.
+    * `stormpy.RationalFunctionCoefficient` replaces `stormpy.RationalRF`.
+    * Added `stormpy.Interval` and `stormpy.RationalInterval` aliases.
+
 ### Version 1.14.0 (2026/08)
 Requires Storm version >= 1.14.0.
 

cmake/core_config.py.in

@@ -2,9 +2,11 @@
 
 @PYCARL_IMPORTS@
 
+# Each name refers to matching Storm C++ type.
 Rational = pycarl.@PYCARL_EA_PACKAGE@.Rational
-RationalRF = pycarl.@PYCARL_RF_PACKAGE@.Rational
-Polynomial = pycarl.@PYCARL_RF_PACKAGE@.Polynomial
-FactorizedPolynomial = pycarl.@PYCARL_RF_PACKAGE@.FactorizedPolynomial
-RationalFunction = pycarl.@PYCARL_RF_PACKAGE@.RationalFunction
-FactorizedRationalFunction = pycarl.@PYCARL_RF_PACKAGE@.FactorizedRationalFunction
+RationalFunctionCoefficient = pycarl.@PYCARL_RF_PACKAGE@.Rational
+RawPolynomial = pycarl.@PYCARL_RF_PACKAGE@.Polynomial
+Polynomial = pycarl.@PYCARL_RF_PACKAGE@.FactorizedPolynomial
+RationalFunction = pycarl.@PYCARL_RF_PACKAGE@.FactorizedRationalFunction
+Interval = pycarl.Interval
+RationalInterval = pycarl.@PYCARL_EA_PACKAGE@.Interval

doc/source/doc/parametric_models.md

@@ -50,7 +50,7 @@ Before we obtain an instantiated model, we need to map parameters to values: We
 point = dict()
 for x in parameters:
     print(x.name)
-    point[x] = stormpy.RationalRF(0.4)
+    point[x] = stormpy.RationalFunctionCoefficient(0.4)
 instantiated_model = instantiator.instantiate(point)
 result = stormpy.model_checking(instantiated_model, properties[0])
 print(result.at(model.initial_states[0]))

examples/building_models/02-building-models.py

@@ -3,20 +3,15 @@
 import stormpy.pars
 from stormpy import pycarl
 
-if stormpy.info.storm_ratfunc_use_cln():
-    from stormpy.pycarl import cln as pc
-else:
-    from stormpy.pycarl import gmp as pc
-
 import stormpy.examples
 import stormpy.examples.files
 
 
 def example_building_models_02():
     def make_factorized_rf(var, cache):
-        num = pc.FactorizedPolynomial(pc.Polynomial(var), cache)
-        denom = pc.FactorizedPolynomial(pc.Rational(1))
-        return pc.FactorizedRationalFunction(num, denom)
+        num = stormpy.Polynomial(stormpy.RawPolynomial(var), cache)
+        denom = stormpy.Polynomial(stormpy.RationalFunctionCoefficient(1))
+        return stormpy.RationalFunction(num, denom)
 
         # And the parametric
 
@@ -30,7 +25,7 @@ def make_factorized_rf(var, cache):
         assert pycarl.variable_with_name(p.name + "_bar").is_no_variable
         bar_parameters[p] = pycarl.Variable(p.name + "_bar")
 
-    substitutions = dict([[pc.Polynomial(1) - p, bar_parameters[p]] for p in parameters])
+    substitutions = dict([[stormpy.RawPolynomial(1) - p, bar_parameters[p]] for p in parameters])
     print(substitutions)
 
     matrix = model.transition_matrix

examples/parametric_models/01-parametric-models.py

@@ -20,7 +20,7 @@ def example_parametric_models_01():
     point = dict()
     for x in parameters:
         print(x.name)
-        point[x] = stormpy.RationalRF(0.4)
+        point[x] = stormpy.RationalFunctionCoefficient(0.4)
     instantiated_model = instantiator.instantiate(point)
     result = stormpy.model_checking(instantiated_model, properties[0])
     print(result)

examples/parametric_models/04-parametric-models.py

@@ -24,10 +24,10 @@ def example_parametric_models_04():
                 if len(transition.value().gather_variables()) > 0:
                     new_var = pycarl.Variable("p{}".format(i))
                     i += 1
-                    new_pol = stormpy.Polynomial(new_var)
-                    pol_in_right_format = stormpy.FactorizedPolynomial(new_pol, transition.value().numerator.cache())
+                    new_pol = stormpy.RawPolynomial(new_var)
+                    pol_in_right_format = stormpy.Polynomial(new_pol, transition.value().numerator.cache())
 
-                    new_factorized_ratfunc = stormpy.FactorizedRationalFunction(pol_in_right_format)
+                    new_factorized_ratfunc = stormpy.RationalFunction(pol_in_right_format)
                     transition.set_value(new_factorized_ratfunc)
 
     # Display

src/core/valuetype.cpp

@@ -0,0 +1,33 @@
+#include "valuetype.h"
+
+#include <storm/adapters/IntervalAdapter.h>
+#include <storm/adapters/RationalFunctionAdapter.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/utility/constants.h>
+
+// Bindings that return a representative value of each Storm C++ ValueType back to Python.
+// These are used to check that Storm's C++ ValueTypes match stormpy's Python types.
+void define_value_types(py::module& m) {
+    m.def("_valuetype_double", []() { return storm::utility::one<double>(); }, "Representative value of C++ type 'double'");
+    m.def(
+        "_valuetype_rationalnumber", []() { return storm::utility::one<storm::RationalNumber>(); }, "Representative value of C++ type 'storm::RationalNumber'");
+    m.def(
+        "_valuetype_rationalfunction", []() { return storm::utility::one<storm::RationalFunction>(); },
+        "Representative value of C++ type 'storm::RationalFunction'");
+    m.def(
+        "_valuetype_rationalfunctioncoefficient", []() { return storm::utility::one<storm::RationalFunctionCoefficient>(); },
+        "Representative value of C++ type 'storm::RationalFunctionCoefficient'");
+    m.def("_valuetype_interval", []() { return storm::utility::one<storm::Interval>(); }, "Representative value of C++ type 'storm::Interval'");
+    m.def(
+        "_valuetype_rationalinterval", []() { return storm::utility::one<storm::RationalInterval>(); },
+        "Representative value of C++ type 'storm::RationalInterval'");
+    m.def("_valuetype_polynomial", []() { return storm::utility::one<storm::Polynomial>(); }, "Representative value of C++ type 'storm::Polynomial'");
+    m.def(
+        "_valuetype_gmprationalnumber", []() { return storm::utility::one<storm::GmpRationalNumber>(); },
+        "Representative value of C++ type 'storm::GmpRationalNumber'");
+#ifdef STORM_HAVE_CLN
+    m.def(
+        "_valuetype_clnrationalnumber", []() { return storm::utility::one<storm::ClnRationalNumber>(); },
+        "Representative value of C++ type 'storm::ClnRationalNumber'");
+#endif
+}

src/core/valuetype.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "src/core/common.h"
+
+void define_value_types(py::module& m);

src/mod_core.cpp

@@ -12,6 +12,7 @@
 #include "src/core/result.h"
 #include "src/core/simulator.h"
 #include "src/core/transformation.h"
+#include "src/core/valuetype.h"
 
 PYBIND11_MODULE(_core, m) {
     m.doc() = "core";
@@ -23,6 +24,7 @@ PYBIND11_MODULE(_core, m) {
 
     define_environment(m);
     define_core(m);
+    define_value_types(m);
 
     define_property(m);
     define_parse(m);

tests/core/test_core.py

@@ -7,7 +7,7 @@ def test_pycarl(self):
 
         rational = stormpy.Rational(0.25)
         assert str(rational) == "1/4"
-        pol1 = stormpy.FactorizedPolynomial(32)
-        pol2 = stormpy.FactorizedPolynomial(2)
-        rat = stormpy.FactorizedRationalFunction(pol1, pol2)
+        pol1 = stormpy.Polynomial(32)
+        pol2 = stormpy.Polynomial(2)
+        rat = stormpy.RationalFunction(pol1, pol2)
         assert str(rat) == "16"

tests/core/test_valuetype.py

@@ -0,0 +1,103 @@
+import stormpy
+import stormpy.info
+from stormpy import pycarl
+from helpers.helper import get_example_path
+
+from configurations import pars, pycarl_cln
+
+
+def exact_package():
+    """Pycarl package (gmp/cln) which is the base for storm::RationalNumber and storm::RationalInterval."""
+    return pycarl.cln if stormpy.info.storm_exact_use_cln() else pycarl.gmp
+
+
+def ratfunc_package():
+    """Pycarl package (gmp/cln) which is the base for storm::RationalFunction."""
+    return pycarl.cln if stormpy.info.storm_ratfunc_use_cln() else pycarl.gmp
+
+
+def first_matrix_value(model):
+    for entry in model.transition_matrix:
+        return entry.value()
+    raise AssertionError("Model has no transition matrix entries")
+
+
+class TestValueType:
+    """Check that Storm's C++ ValueTypes match stormpy's Python types."""
+
+    def test_double(self):
+        value = stormpy._core._valuetype_double()
+        assert type(value) is float
+
+    def test_rationalnumber(self):
+        value = stormpy._core._valuetype_rationalnumber()
+        assert type(value) is stormpy.Rational
+        assert type(value) is exact_package().Rational
+
+    def test_gmprationalnumber(self):
+        value = stormpy._core._valuetype_gmprationalnumber()
+        assert type(value) is pycarl.gmp.Rational
+
+    @pycarl_cln
+    def test_clnrationalnumber(self):
+        value = stormpy._core._valuetype_clnrationalnumber()
+        assert type(value) is pycarl.cln.Rational
+
+    def test_polynomial(self):
+        value = stormpy._core._valuetype_polynomial()
+        assert type(value) is stormpy.Polynomial
+        assert type(value) is ratfunc_package().FactorizedPolynomial
+        assert type(value) is not ratfunc_package().Polynomial
+
+    def test_rationalfunction(self):
+        value = stormpy._core._valuetype_rationalfunction()
+        assert type(value) is stormpy.RationalFunction
+        assert type(value) is ratfunc_package().FactorizedRationalFunction
+        # Also test RationalFunctionCoefficient
+        value_rf = stormpy._core._valuetype_rationalfunctioncoefficient()
+        assert type(value_rf) is stormpy.RationalFunctionCoefficient
+        assert type(value_rf) is ratfunc_package().Rational
+
+    def test_interval(self):
+        value = stormpy._core._valuetype_interval()
+        assert type(value) is stormpy.Interval
+        assert type(value) is pycarl.Interval
+        assert type(value) is not exact_package().Interval
+
+    def test_rationalinterval(self):
+        value = stormpy._core._valuetype_rationalinterval()
+        assert type(value) is stormpy.RationalInterval
+        assert type(value) is exact_package().Interval
+        assert type(value) is not pycarl.Interval
+
+
+class TestValueTypeMatrix:
+    """Check the ValueType against values read out of a model's transition matrix."""
+
+    def test_double(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        model = stormpy.build_model(program)
+        assert type(first_matrix_value(model)) is float
+
+    def test_rationalnumber(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        model = stormpy.build_sparse_exact_model(program)
+        assert type(first_matrix_value(model)) is stormpy.Rational
+        assert type(first_matrix_value(model)) is exact_package().Rational
+
+    @pars
+    def test_rationalfunction(self):
+        program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm"))
+        model = stormpy.build_parametric_model(program)
+        assert type(first_matrix_value(model)) is stormpy.RationalFunction
+        assert type(first_matrix_value(model).constant_part()) is ratfunc_package().Rational
+
+    def test_interval(self):
+        program = stormpy.parse_prism_program(get_example_path("idtmc", "die-intervals.pm"))
+        model = stormpy.build_sparse_interval_model(program)
+        assert type(first_matrix_value(model)) is pycarl.Interval
+
+    def test_rationalinterval(self):
+        program = stormpy.parse_prism_program(get_example_path("idtmc", "die-intervals.pm"))
+        model = stormpy.build_sparse_exact_interval_model(program)
+        assert type(first_matrix_value(model)) is exact_package().Interval

tests/dft/test_transformations.py

@@ -17,7 +17,7 @@ def test_instantiate_dft(self):
         instantiator = stormpy.dft.DFTInstantiator(dft)
         x = pycarl.variable_with_name("x")
         y = pycarl.variable_with_name("y")
-        valuation = {x: stormpy.RationalRF("5"), y: stormpy.RationalRF("0.01")}
+        valuation = {x: stormpy.RationalFunctionCoefficient("5"), y: stormpy.RationalFunctionCoefficient("0.01")}
         inst_dft = instantiator.instantiate(valuation)
         assert inst_dft.nr_elements() == 7
         assert inst_dft.nr_be() == 4

tests/pars/test_model_instantiator.py

@@ -15,13 +15,13 @@ def test_instantiate_dtmc(self):
         assert len(parameters) == 2
         instantiator = stormpy.pars.ModelInstantiator(model)
 
-        point = {p: stormpy.RationalRF("0.4") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("0.4") for p in parameters}
         instantiated_model = instantiator.instantiate(point)
         assert instantiated_model.nr_states == model.nr_states
         assert not instantiated_model.has_parameters
         assert "0.4" in str(instantiated_model.transition_matrix[1])
 
-        point = {p: stormpy.RationalRF("0.5") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("0.5") for p in parameters}
         instantiated_model2 = instantiator.instantiate(point)
         assert "0.5" in str(instantiated_model2.transition_matrix[1])
 
@@ -35,7 +35,7 @@ def test_instantiate_dtmc_die(self):
         point = dict()
         for x in parameters:
             assert x.name in {"p", "q"}
-            point[x] = stormpy.RationalRF(0.4)
+            point[x] = stormpy.RationalFunctionCoefficient(0.4)
         instantiated_model = instantiator.instantiate(point)
         assert instantiated_model.nr_states == model.nr_states
         assert not instantiated_model.has_parameters
@@ -53,13 +53,13 @@ def test_sample_pdtmc(self):
         parameters = model.collect_all_parameters()
         instantiator = stormpy.pars.PDtmcInstantiator(model)
 
-        point = {p: stormpy.RationalRF("0.4") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("0.4") for p in parameters}
         instantiated_model = instantiator.instantiate(point)
         assert instantiated_model.nr_states == model.nr_states
         assert not instantiated_model.has_parameters
         assert "0.4" in str(instantiated_model.transition_matrix[1])
 
-        point = {p: stormpy.RationalRF("0.5") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("0.5") for p in parameters}
         instantiated_model2 = instantiator.instantiate(point)
         assert "0.5" in str(instantiated_model2.transition_matrix[1])
 
@@ -74,7 +74,7 @@ def test_pdtmc_instantiation_checker(self):
         inst_checker.set_graph_preserving(True)
         env = stormpy.Environment()
 
-        point = {p: stormpy.RationalRF(1 / 2) for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient(1 / 2) for p in parameters}
         result = inst_checker.check(env, point)
         assert isinstance(result, stormpy.ExplicitQuantitativeCheckResult)
         res = result.at(model.initial_states[0])
@@ -92,7 +92,7 @@ def test_pdtmc_exact_instantiation_checker(self):
         inst_checker.set_graph_preserving(True)
         env = stormpy.Environment()
 
-        point = {p: stormpy.RationalRF("1/2") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("1/2") for p in parameters}
         result = inst_checker.check(env, point)
         assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult)
         res = result.at(model.initial_states[0])
@@ -110,7 +110,7 @@ def test_pdtmc_exact_instantiation_checker_die(self):
         inst_checker.set_graph_preserving(True)
         env = stormpy.Environment()
 
-        point = {p: stormpy.RationalRF("2/5") for p in parameters}
+        point = {p: stormpy.RationalFunctionCoefficient("2/5") for p in parameters}
         result = inst_checker.check(env, point)
         assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult)
         res = result.at(model.initial_states[0])

tests/pars/test_parametric.py

@@ -20,7 +20,7 @@ def test_parametric_model_checking_sparse(self):
         assert initial_state == 0
         result = stormpy.model_checking(model, formulas[0])
         func = result.at(initial_state)
-        one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1))
+        one = stormpy.Polynomial(stormpy.RationalFunctionCoefficient(1))
         assert func.denominator == one
 
     def test_parametric_model_checking_sparse_die(self):
@@ -45,12 +45,12 @@ def test_parametric_model_checking_sparse_die(self):
         parameters = model.collect_all_parameters()
         for par in parameters:
             if par.name == "p":
-                p = pc.create_factorized_polynomial(pc.Polynomial(par))
+                p = pc.create_factorized_polynomial(stormpy.RawPolynomial(par))
             else:
                 assert par.name == "q"
-                q = pc.create_factorized_polynomial(pc.Polynomial(par))
+                q = pc.create_factorized_polynomial(stormpy.RawPolynomial(par))
 
-        one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1))
+        one = stormpy.Polynomial(stormpy.RationalFunctionCoefficient(1))
         num = p * p * (q - one)
         denom = p * q - one
         assert func.numerator == num
@@ -198,15 +198,18 @@ def test_region(self):
         parameters = model.collect_all_parameters()
         assert len(parameters) == 2
         region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
-        assert region.area == stormpy.RationalRF(1) / stormpy.RationalRF(25)
+        assert region.area == stormpy.RationalFunctionCoefficient(1) / stormpy.RationalFunctionCoefficient(25)
         for par in parameters:
             if par.name == "pL":
                 pL = par
             elif par.name == "pK":
                 pK = par
             else:
                 assert False
-        dec = stormpy.RationalRF(100)
-        region_valuation = {pL: (stormpy.RationalRF(70) / dec, stormpy.RationalRF(90) / dec), pK: (stormpy.RationalRF(75) / dec, stormpy.RationalRF(95) / dec)}
+        dec = stormpy.RationalFunctionCoefficient(100)
+        region_valuation = {
+            pL: (stormpy.RationalFunctionCoefficient(70) / dec, stormpy.RationalFunctionCoefficient(90) / dec),
+            pK: (stormpy.RationalFunctionCoefficient(75) / dec, stormpy.RationalFunctionCoefficient(95) / dec),
+        }
         region = stormpy.pars.ParameterRegion(region_valuation)
-        assert region.area == stormpy.RationalRF(1) / stormpy.RationalRF(25)
+        assert region.area == stormpy.RationalFunctionCoefficient(1) / stormpy.RationalFunctionCoefficient(25)