diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py
index 07e8151..a6b96f7 100644
--- a/tests/core/test_bisimulation.py
+++ b/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
diff --git a/tests/core/test_core.py b/tests/core/test_core.py
index 84234d0..df102c8 100644
--- a/tests/core/test_core.py
+++ b/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"
diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py
index b9f7f28..addbd44 100644
--- a/tests/core/test_modelchecking.py
+++ b/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:
diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py
index f4cd934..6cc6816 100644
--- a/tests/logic/test_formulas.py
+++ b/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)
diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py
index d29b04b..7efb786 100644
--- a/tests/storage/test_matrix.py
+++ b/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)
diff --git a/tests/storage/test_model_instantiator.py b/tests/storage/test_model_instantiator.py
index 3c86065..f34b5f9 100644
--- a/tests/storage/test_model_instantiator.py
+++ b/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])
diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py
index 55a7ec9..25a1a10 100644
--- a/tests/storage/test_state.py
+++ b/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