diff --git a/CHANGELOG.md b/CHANGELOG.md index efd88d4da..75d95e814 100644 --- a/CHANGELOG.md +++ b/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. diff --git a/cmake/core_config.py.in b/cmake/core_config.py.in index dfdab957b..de7840ff2 100644 --- a/cmake/core_config.py.in +++ b/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 diff --git a/doc/source/doc/parametric_models.md b/doc/source/doc/parametric_models.md index 9bf34902e..d0a5bc5f1 100644 --- a/doc/source/doc/parametric_models.md +++ b/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])) diff --git a/examples/building_models/02-building-models.py b/examples/building_models/02-building-models.py index 506cdaf71..bf4770cb4 100644 --- a/examples/building_models/02-building-models.py +++ b/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 diff --git a/examples/parametric_models/01-parametric-models.py b/examples/parametric_models/01-parametric-models.py index 8218c5fd3..ff82ed10c 100644 --- a/examples/parametric_models/01-parametric-models.py +++ b/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) diff --git a/examples/parametric_models/04-parametric-models.py b/examples/parametric_models/04-parametric-models.py index 5c105467f..b0260d500 100644 --- a/examples/parametric_models/04-parametric-models.py +++ b/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 diff --git a/src/core/valuetype.cpp b/src/core/valuetype.cpp new file mode 100644 index 000000000..ca377e380 --- /dev/null +++ b/src/core/valuetype.cpp @@ -0,0 +1,33 @@ +#include "valuetype.h" + +#include +#include +#include +#include + +// 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(); }, "Representative value of C++ type 'double'"); + m.def( + "_valuetype_rationalnumber", []() { return storm::utility::one(); }, "Representative value of C++ type 'storm::RationalNumber'"); + m.def( + "_valuetype_rationalfunction", []() { return storm::utility::one(); }, + "Representative value of C++ type 'storm::RationalFunction'"); + m.def( + "_valuetype_rationalfunctioncoefficient", []() { return storm::utility::one(); }, + "Representative value of C++ type 'storm::RationalFunctionCoefficient'"); + m.def("_valuetype_interval", []() { return storm::utility::one(); }, "Representative value of C++ type 'storm::Interval'"); + m.def( + "_valuetype_rationalinterval", []() { return storm::utility::one(); }, + "Representative value of C++ type 'storm::RationalInterval'"); + m.def("_valuetype_polynomial", []() { return storm::utility::one(); }, "Representative value of C++ type 'storm::Polynomial'"); + m.def( + "_valuetype_gmprationalnumber", []() { return storm::utility::one(); }, + "Representative value of C++ type 'storm::GmpRationalNumber'"); +#ifdef STORM_HAVE_CLN + m.def( + "_valuetype_clnrationalnumber", []() { return storm::utility::one(); }, + "Representative value of C++ type 'storm::ClnRationalNumber'"); +#endif +} diff --git a/src/core/valuetype.h b/src/core/valuetype.h new file mode 100644 index 000000000..2761d2e2a --- /dev/null +++ b/src/core/valuetype.h @@ -0,0 +1,5 @@ +#pragma once + +#include "src/core/common.h" + +void define_value_types(py::module& m); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 7e069428f..be567941a 100644 --- a/src/mod_core.cpp +++ b/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); diff --git a/tests/core/test_core.py b/tests/core/test_core.py index 13fdb6cbf..28c7a3182 100644 --- a/tests/core/test_core.py +++ b/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" diff --git a/tests/core/test_valuetype.py b/tests/core/test_valuetype.py new file mode 100644 index 000000000..edde3e3ac --- /dev/null +++ b/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 diff --git a/tests/dft/test_transformations.py b/tests/dft/test_transformations.py index a9dd697a4..0d00e87af 100644 --- a/tests/dft/test_transformations.py +++ b/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 diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index 5174367ac..1e75d8126 100644 --- a/tests/pars/test_model_instantiator.py +++ b/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]) diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 15d31ef2f..8d7dbca8b 100644 --- a/tests/pars/test_parametric.py +++ b/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,7 +198,7 @@ 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 @@ -206,7 +206,10 @@ def test_region(self): 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) diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 468f9f5b1..8cdc64c98 100644 --- a/tests/pars/test_pla.py +++ b/tests/pars/test_pla.py @@ -61,17 +61,17 @@ def test_pla_region_valuation(self): else: assert False region_valuation = dict() - region_valuation[pL] = (stormpy.RationalRF(0.7), stormpy.RationalRF(0.9)) - region_valuation[pK] = (stormpy.RationalRF(0.75), stormpy.RationalRF(0.95)) + region_valuation[pL] = (stormpy.RationalFunctionCoefficient(0.7), stormpy.RationalFunctionCoefficient(0.9)) + region_valuation[pK] = (stormpy.RationalFunctionCoefficient(0.75), stormpy.RationalFunctionCoefficient(0.95)) region = stormpy.pars.ParameterRegion(region_valuation) result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLSAT - region_valuation[pL] = (stormpy.RationalRF(0.4), stormpy.RationalRF(0.65)) + region_valuation[pL] = (stormpy.RationalFunctionCoefficient(0.4), stormpy.RationalFunctionCoefficient(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 - region_valuation[pK] = (stormpy.RationalRF(0.2), stormpy.RationalRF(0.715)) - region_valuation[pL] = (stormpy.RationalRF(0.1), stormpy.RationalRF(0.73)) + region_valuation[pK] = (stormpy.RationalFunctionCoefficient(0.2), stormpy.RationalFunctionCoefficient(0.715)) + region_valuation[pL] = (stormpy.RationalFunctionCoefficient(0.1), stormpy.RationalFunctionCoefficient(0.73)) region = stormpy.pars.ParameterRegion(region_valuation) result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLVIOLATED @@ -151,9 +151,9 @@ def test_compute_extremum(self): region = stormpy.pars.ParameterRegion.create_from_string("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) refinement_checker = stormpy.pars.create_region_refinement_checker(env, model, formulas[0].raw_formula) - precision = stormpy.RationalRF(1e-6) + precision = stormpy.RationalFunctionCoefficient(1e-6) value, point = refinement_checker.compute_extremum(env, region, stormpy.OptimizationDirection.Maximize, precision, False) - assert isinstance(value, stormpy.RationalRF) + assert isinstance(value, stormpy.RationalFunctionCoefficient) assert isinstance(point, dict) assert len(point) == 2 assert 0.83 <= float(value) <= 0.84 diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 54bde027f..b5be8c853 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -111,9 +111,9 @@ def test_change_parametric_matrix_modelchecking(self): assert initial_state == 0 matrix = model.transition_matrix # Check matrix - one_pol = stormpy.RationalRF(1) - one_pol = stormpy.FactorizedPolynomial(one_pol) - one = stormpy.FactorizedRationalFunction(one_pol, one_pol) + one_pol = stormpy.RationalFunctionCoefficient(1) + one_pol = stormpy.Polynomial(one_pol) + one = stormpy.RationalFunction(one_pol, one_pol) for e in matrix: assert e.value() == one or len(e.value().gather_variables()) > 0 # First model checking @@ -122,9 +122,9 @@ def test_change_parametric_matrix_modelchecking(self): assert len(ratFunc.gather_variables()) > 0 # Change probabilities - two_pol = stormpy.RationalRF(2) - two_pol = stormpy.FactorizedPolynomial(two_pol) - new_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + two_pol = stormpy.RationalFunctionCoefficient(2) + two_pol = stormpy.Polynomial(two_pol) + new_val = stormpy.RationalFunction(one_pol, two_pol) for e in matrix: if len(e.value().gather_variables()) > 0: e.set_value(new_val) diff --git a/tests/storage/test_matrix_builder.py b/tests/storage/test_matrix_builder.py index b346e81fe..aa9efc21c 100644 --- a/tests/storage/test_matrix_builder.py +++ b/tests/storage/test_matrix_builder.py @@ -76,13 +76,13 @@ def test_parametric_matrix_builder(self): builder_5x5 = stormpy.ParametricSparseMatrixBuilder(5, 5, force_dimensions=False) - one_pol = stormpy.RationalRF(1) - one_pol = stormpy.FactorizedPolynomial(one_pol) - first_val = stormpy.FactorizedRationalFunction(one_pol) + one_pol = stormpy.RationalFunctionCoefficient(1) + one_pol = stormpy.Polynomial(one_pol) + first_val = stormpy.RationalFunction(one_pol) - two_pol = stormpy.RationalRF(2) - two_pol = stormpy.FactorizedPolynomial(two_pol) - sec_val = stormpy.FactorizedRationalFunction(two_pol) + two_pol = stormpy.RationalFunctionCoefficient(2) + two_pol = stormpy.Polynomial(two_pol) + sec_val = stormpy.RationalFunction(two_pol) builder_5x5.add_next_value(0, 0, first_val) builder_5x5.add_next_value(0, 1, first_val) @@ -139,13 +139,13 @@ def test_matrix_replace_columns(self): def test_parametric_matrix_replace_columns(self): builder = stormpy.ParametricSparseMatrixBuilder(3, 4, force_dimensions=False) - one_pol = stormpy.RationalRF(1) - one_pol = stormpy.FactorizedPolynomial(one_pol) - first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) - two_pol = stormpy.RationalRF(2) - two_pol = stormpy.FactorizedPolynomial(two_pol) - sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) - third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + one_pol = stormpy.RationalFunctionCoefficient(1) + one_pol = stormpy.Polynomial(one_pol) + first_val = stormpy.RationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalFunctionCoefficient(2) + two_pol = stormpy.Polynomial(two_pol) + sec_val = stormpy.RationalFunction(two_pol, two_pol) + third_val = stormpy.RationalFunction(one_pol, two_pol) builder.add_next_value(0, 1, first_val) builder.add_next_value(0, 2, sec_val) @@ -245,13 +245,13 @@ def test_matrix_from_numpy_zeros(self): def test_parametric_matrix_from_numpy(self): import numpy as np - one_pol = stormpy.RationalRF(1) - one_pol = stormpy.FactorizedPolynomial(one_pol) - first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) - two_pol = stormpy.RationalRF(2) - two_pol = stormpy.FactorizedPolynomial(two_pol) - sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) - third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + one_pol = stormpy.RationalFunctionCoefficient(1) + one_pol = stormpy.Polynomial(one_pol) + first_val = stormpy.RationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalFunctionCoefficient(2) + two_pol = stormpy.Polynomial(two_pol) + sec_val = stormpy.RationalFunction(two_pol, two_pol) + third_val = stormpy.RationalFunction(one_pol, two_pol) array = np.array([[sec_val, first_val], [first_val, 0], [0, sec_val], [third_val, third_val]]) @@ -298,13 +298,13 @@ def test_matrix_from_numpy_row_grouping(self): def test_parametric_matrix_from_numpy_row_grouping(self): import numpy as np - one_pol = stormpy.RationalRF(1) - one_pol = stormpy.FactorizedPolynomial(one_pol) - first_val = stormpy.FactorizedRationalFunction(one_pol, one_pol) - two_pol = stormpy.RationalRF(2) - two_pol = stormpy.FactorizedPolynomial(two_pol) - sec_val = stormpy.FactorizedRationalFunction(two_pol, two_pol) - third_val = stormpy.FactorizedRationalFunction(one_pol, two_pol) + one_pol = stormpy.RationalFunctionCoefficient(1) + one_pol = stormpy.Polynomial(one_pol) + first_val = stormpy.RationalFunction(one_pol, one_pol) + two_pol = stormpy.RationalFunctionCoefficient(2) + two_pol = stormpy.Polynomial(two_pol) + sec_val = stormpy.RationalFunction(two_pol, two_pol) + third_val = stormpy.RationalFunction(one_pol, two_pol) array = np.array([[sec_val, first_val], [first_val, sec_val], [sec_val, sec_val], [third_val, third_val]]) diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index 231e80cdd..99877aed8 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -818,12 +818,12 @@ def test_build_parametric_dtmc(self): from stormpy.pycarl import gmp as pc def create_polynomial(pol): - num = pc.create_factorized_polynomial(pc.Polynomial(pol)) - return pc.FactorizedRationalFunction(num) + num = pc.create_factorized_polynomial(stormpy.RawPolynomial(pol)) + return stormpy.RationalFunction(num) def create_number(num): - num = pc.FactorizedPolynomial(pc.Rational(num)) - return pc.FactorizedRationalFunction(num) + num = stormpy.Polynomial(stormpy.RationalFunctionCoefficient(num)) + return stormpy.RationalFunction(num) from stormpy.pycarl import Variable @@ -896,7 +896,7 @@ def create_number(num): assert dtmc.nr_transitions == 20 assert dtmc.transition_matrix.nr_entries == dtmc.nr_transitions for e in dtmc.transition_matrix: - assert type(e.value()) is pc.FactorizedRationalFunction + assert type(e.value()) is stormpy.RationalFunction for state in dtmc.states: assert len(state.actions) <= 1 diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py index f7a4e6346..7dd0e93b2 100644 --- a/tests/storage/test_state.py +++ b/tests/storage/test_state.py @@ -176,7 +176,7 @@ def test_parametric_transitions(self): program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) model = stormpy.build_parametric_model(program) assert model.states[1].id == 1 - one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) + one = stormpy.Polynomial(stormpy.RationalFunctionCoefficient(1)) i = 0 for state in model.states: assert state.id == i