Use stormpy definitions of pycarl types in tests

tests/core/test_bisimulation.py

@@ -32,9 +32,6 @@ class TestBisimulation:
         assert math.isclose(result.at(initial_state), result_bisim.at(initial_state_bisim), rel_tol=1e-4)
 
     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

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

tests/core/test_modelchecking.py

@@ -30,12 +30,6 @@ 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.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)
@@ -48,7 +42,7 @@ class TestModelChecking:
         assert initial_state == 0
         result = stormpy.model_checking(model, formulas[0])
         func = result.at(initial_state)
-        one = pycarl.cln.FactorizedPolynomial(pycarl.cln.Rational(1))
+        one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1))
         assert func.denominator == one
         #constraints_well_formed = result.constraints_well_formed
         # for constraint in constraints_well_formed:

tests/logic/test_formulas.py

@@ -1,4 +1,3 @@
-import pycarl
 import stormpy
 import stormpy.logic
 
@@ -41,17 +40,14 @@ class TestFormulas:
         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)
     def test_set_bounds(self):
-        import pycarl
-        import pycarl.gmp
         prop = "P<0.4 [F \"one\"]"
         formula = stormpy.parse_properties(prop)[0].raw_formula
         expression_manager = stormpy.ExpressionManager()
-        rational = pycarl.gmp.Rational("0.2")
+        rational = stormpy.Rational("0.2")
         expression = expression_manager.create_rational(rational)
         formula.set_bound(stormpy.logic.ComparisonType.GEQ, expression)
-        assert formula.threshold == pycarl.gmp.Rational("0.2")
+        assert formula.threshold == stormpy.Rational("0.2")
         assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ
         assert str(formula) == "P>=1/5 [F \"one\"]"
 

tests/pars/test_model_instantiator.py

@@ -1,4 +1,3 @@
-import pycarl
 import stormpy
 import stormpy.logic
 import stormpy.pars

tests/pars/test_parametric.py

@@ -1,14 +1,11 @@
 import stormpy
+import stormpy.info
 import stormpy.logic
 from helpers.helper import get_example_path
 
 class TestParametric:
 
     def test_constraints_collector(self):
-        #TODO decide whether we have CLN or GMP based on some flag in stormpy.
-        import pycarl
-        import pycarl.cln
-        import pycarl.gmp
         from pycarl.formula import FormulaType, Relation
         import pycarl.cln.formula
         import pycarl.gmp.formula

tests/pars/test_pla.py

@@ -5,7 +5,6 @@ from helpers.helper import get_example_path
 
 class TestModelChecking:
     def test_pla(self):
-        import pycarl
         program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
         prop = "P<=0.84 [F s=5 ]"
         formulas = stormpy.parse_properties_for_prism_program(prop, program)

tests/storage/test_expressions.py

@@ -24,9 +24,8 @@ class TestExpressions:
         assert not expression.has_rational_type()
 
     def test_rational_expression(self):
-        import pycarl.gmp
         manager = stormpy.ExpressionManager()
-        expression = manager.create_rational(pycarl.gmp.Rational(0.2))
+        expression = manager.create_rational(stormpy.Rational(0.2))
         assert expression.is_literal()
         assert not expression.contains_variables()
         assert not expression.has_boolean_type()