fixed tests to be compatible with pycarl v2

tests/core/test_bisimulation.py

@@ -33,6 +33,8 @@ class TestBisimulation:
 
     def test_parametric_bisimulation(self):
         import pycarl
+        import pycarl.cln
+        import pycarl.gmp
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
         assert program.nr_modules == 5
         assert program.model_type == stormpy.PrismModelType.DTMC

tests/core/test_core.py

@@ -5,9 +5,11 @@ class TestCore:
     def test_pycarl(self):
         import stormpy
         import pycarl
+        import pycarl.cln
+        import pycarl.gmp
         import pycarl.formula
         import pycarl.parse
-        pol1 = pycarl.FactorizedPolynomial(32)
-        pol2 = pycarl.FactorizedPolynomial(2)
-        rat = pycarl.FactorizedRationalFunction(pol1, pol2)
+        pol1 = pycarl.gmp.FactorizedPolynomial(32)
+        pol2 = pycarl.gmp.FactorizedPolynomial(2)
+        rat = pycarl.gmp.FactorizedRationalFunction(pol1, pol2)
         assert str(rat) == "16"

tests/core/test_modelchecking.py

@@ -30,8 +30,12 @@ class TestModelChecking:
         assert all(map(math.isclose, result.get_values(), reference))
     
     def test_parametric_state_elimination(self):
+        #TODO decide whether we have CLN or GMP based on some flag in stormpy.
         import pycarl
-        import pycarl.formula
+        import pycarl.cln
+        import pycarl.gmp
+        import pycarl.cln.formula
+        import pycarl.gmp.formula
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
         prop = "P=? [F s=5]"
         formulas = stormpy.parse_properties_for_prism_program(prop, program)
@@ -44,7 +48,7 @@ class TestModelChecking:
         assert initial_state == 0
         result = stormpy.model_checking(model, formulas[0])
         func = result.result.at(initial_state)
-        one = pycarl.FactorizedPolynomial(pycarl.Rational(1))
+        one = pycarl.cln.FactorizedPolynomial(pycarl.cln.Rational(1))
         assert func.denominator == one
         constraints_well_formed = result.constraints_well_formed
         for constraint in constraints_well_formed:

tests/logic/test_formulas.py

@@ -38,7 +38,7 @@ class TestFormulas:
         prop = "P<0.4 [F \"one\"]"
         formula = stormpy.parse_properties(prop)[0].raw_formula
         assert formula.has_bound
-        assert formula.threshold == pycarl.Rational("0.4")
+        assert formula.threshold == stormpy.Rational("0.4")
         assert formula.comparison_type == stormpy.logic.ComparisonType.LESS
 
     # setter not currently implemented (non-trivial due to Expression container)

tests/storage/test_matrix.py

@@ -83,7 +83,7 @@ class TestMatrix:
     
     def test_change_parametric_sparse_matrix_modelchecking(self):
         import stormpy.logic
-        import pycarl
+
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
         formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program)
         model = stormpy.build_parametric_model(program, formulas)
@@ -91,9 +91,9 @@ class TestMatrix:
         assert initial_state == 0
         matrix = model.transition_matrix
         # Check matrix
-        one_pol = pycarl.Rational(1)
-        one_pol = pycarl.FactorizedPolynomial(one_pol)
-        one = pycarl.FactorizedRationalFunction(one_pol, one_pol)
+        one_pol = stormpy.RationalRF(1)
+        one_pol = stormpy.FactorizedPolynomial(one_pol)
+        one = stormpy.FactorizedRationalFunction(one_pol, one_pol)
         for e in matrix:
             assert e.value() == one or len(e.value().gather_variables()) > 0
         # First model checking
@@ -102,9 +102,9 @@ class TestMatrix:
         assert len(ratFunc.gather_variables()) > 0
         
         # Change probabilities
-        two_pol = pycarl.Rational(2)
-        two_pol = pycarl.FactorizedPolynomial(two_pol)
-        new_val = pycarl.FactorizedRationalFunction(one_pol, two_pol)
+        two_pol = stormpy.RationalRF(2)
+        two_pol = stormpy.FactorizedPolynomial(two_pol)
+        new_val = stormpy.FactorizedRationalFunction(one_pol, two_pol)
         for e in matrix:
             if len(e.value().gather_variables()) > 0:
                 e.set_value(new_val)

tests/storage/test_model_instantiator.py

@@ -12,12 +12,12 @@ class TestModel:
         parameters = model.collect_probability_parameters()
         instantiator = stormpy.ModelInstantiator(model)
 
-        point = {p: 0.4 for p in parameters}
+        point = {p: stormpy.RationalRF("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: 0.5 for p in parameters}
+        point = {p: stormpy.RationalRF("0.5") for p in parameters}
         instantiated_model2 = instantiator.instantiate(point)
         assert "0.5" in str(instantiated_model2.transition_matrix[1])

tests/storage/test_state.py

@@ -102,11 +102,10 @@ class TestState:
                 assert transition.value() == transition_orig[2]
 
     def test_parametric_transitions(self):
-        import pycarl
         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 = pycarl.FactorizedPolynomial(pycarl.Rational(1))
+        one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1))
         i = 0
         for state in model.states:
             assert state.id == i