From 9a73e0cd4556eec844ae9e2ac7a11b78dd97c9a3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 2 Aug 2017 18:01:26 +0200 Subject: [PATCH] Use stormpy definitions of pycarl types in tests --- tests/core/test_bisimulation.py | 3 --- tests/core/test_core.py | 14 ++++++-------- tests/core/test_modelchecking.py | 10 ++-------- tests/logic/test_formulas.py | 8 ++------ tests/pars/test_model_instantiator.py | 1 - tests/pars/test_parametric.py | 5 +---- tests/pars/test_pla.py | 1 - tests/storage/test_expressions.py | 3 +-- 8 files changed, 12 insertions(+), 33 deletions(-) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index a57f837..a1c0178 100644 --- a/tests/core/test_bisimulation.py +++ b/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 diff --git a/tests/core/test_core.py b/tests/core/test_core.py index 08125d3..fc79932 100644 --- a/tests/core/test_core.py +++ b/tests/core/test_core.py @@ -1,14 +1,12 @@ class TestCore: def test_init(self): import stormpy - + 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" diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index eecd468..6195cf8 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -28,14 +28,8 @@ class TestModelChecking: assert result.result_for_all_states reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] 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: diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index a81846f..dca2d12 100644 --- a/tests/logic/test_formulas.py +++ b/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\"]" diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index 046dbbb..98d5dad 100644 --- a/tests/pars/test_model_instantiator.py +++ b/tests/pars/test_model_instantiator.py @@ -1,4 +1,3 @@ -import pycarl import stormpy import stormpy.logic import stormpy.pars diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index c5330e3..dae63b4 100644 --- a/tests/pars/test_parametric.py +++ b/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 diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 1fbcf1f..9f0e5f1 100644 --- a/tests/pars/test_pla.py +++ b/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) diff --git a/tests/storage/test_expressions.py b/tests/storage/test_expressions.py index 9aed379..c78421c 100644 --- a/tests/storage/test_expressions.py +++ b/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()