diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index 9a126cbfe..721810266 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/stormpy/lib/stormpy/__init__.py @@ -1,6 +1,8 @@ from . import core from .core import * +core.set_up("") + def build_model(program, formulae): intermediate = core._build_model(program, formulae) diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py new file mode 100644 index 000000000..17c5fa706 --- /dev/null +++ b/stormpy/tests/core/test_bisimulation.py @@ -0,0 +1,40 @@ +import stormpy +import stormpy.logic + +class TestBisimulation: + def test_bisimulation(self): + program = stormpy.parse_program("../examples/dtmc/crowds/crowds5_5.pm") + assert program.nr_modules() == 1 + assert program.model_type() == stormpy.PrismModelType.DTMC + prop = "P=? [F \"observe0Greater1\"]" + formulas = stormpy.parse_formulas_for_program(prop, program) + pair = stormpy.build_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 7403 + assert model.nr_transitions() == 13041 + assert model.model_type() == stormpy.ModelType.DTMC + assert not model.parametric() + model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) + assert model_bisim.nr_states() == 64 + assert model_bisim.nr_transitions() == 104 + assert model_bisim.model_type() == stormpy.ModelType.DTMC + assert not model_bisim.parametric() + + def test_parametric_bisimulation(self): + program = stormpy.parse_program("../examples/pdtmc/crowds/crowds_3-5.pm") + assert program.nr_modules() == 1 + assert program.model_type() == stormpy.PrismModelType.DTMC + assert program.has_undefined_constants() + prop = "P=? [F \"observe0Greater1\"]" + formulas = stormpy.parse_formulas_for_program(prop, program) + pair = stormpy.build_parametric_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 1367 + assert model.nr_transitions() == 2027 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() + model_bisim = stormpy.perform_parametric_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) + assert model_bisim.nr_states() == 80 + assert model_bisim.nr_transitions() == 120 + assert model_bisim.model_type() == stormpy.ModelType.DTMC + assert model_bisim.parametric() diff --git a/stormpy/tests/core/test_core.py b/stormpy/tests/core/test_core.py index 416b7e894..d711e12be 100644 --- a/stormpy/tests/core/test_core.py +++ b/stormpy/tests/core/test_core.py @@ -4,76 +4,7 @@ class TestCore: def test_init(self): stormpy.set_up("") - def test_build_parametric_model_from_prism_program(self): - program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") - assert program.nr_modules() == 5 - assert program.model_type() == stormpy.PrismModelType.DTMC - assert program.has_undefined_constants() - prop = "P=? [F \"target\"]" - formulas = stormpy.parse_formulas_for_program(prop, program) - pair = stormpy.build_parametric_model_from_prism_program(program, formulas) - model = pair.model - assert model.nr_states() == 613 - assert model.nr_transitions() == 803 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.parametric() - - def test_bisimulation(self): - program = stormpy.parse_program("../examples/dtmc/crowds/crowds5_5.pm") - assert program.nr_modules() == 1 - assert program.model_type() == stormpy.PrismModelType.DTMC - prop = "P=? [F \"observe0Greater1\"]" - formulas = stormpy.parse_formulas_for_program(prop, program) - pair = stormpy.build_model_from_prism_program(program, formulas) - model = pair.model - assert model.nr_states() == 7403 - assert model.nr_transitions() == 13041 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.parametric() - model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) - assert model_bisim.nr_states() == 64 - assert model_bisim.nr_transitions() == 104 - assert model_bisim.model_type() == stormpy.ModelType.DTMC - assert not model_bisim.parametric() - - def test_parametric_bisimulation(self): - program = stormpy.parse_program("../examples/pdtmc/crowds/crowds_3-5.pm") - assert program.nr_modules() == 1 - assert program.model_type() == stormpy.PrismModelType.DTMC - assert program.has_undefined_constants() - prop = "P=? [F \"observe0Greater1\"]" - formulas = stormpy.parse_formulas_for_program(prop, program) - pair = stormpy.build_parametric_model_from_prism_program(program, formulas) - model = pair.model - assert model.nr_states() == 1367 - assert model.nr_transitions() == 2027 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.parametric() - model_bisim = stormpy.perform_parametric_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) - assert model_bisim.nr_states() == 80 - assert model_bisim.nr_transitions() == 120 - assert model_bisim.model_type() == stormpy.ModelType.DTMC - assert model_bisim.parametric() - - def test_state_elimination(self): + def test_pycarl(self): import pycarl import pycarl.formula - program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") - prop = "P=? [F \"target\"]" - formulas = stormpy.parse_formulas_for_program(prop, program) - pair = stormpy.build_parametric_model_from_prism_program(program, formulas) - model = pair.model - assert model.nr_states() == 613 - assert model.nr_transitions() == 803 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.parametric() - result = stormpy.perform_state_elimination(model, formulas[0]) - func = result.result_function - one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) - assert func.denominator == one - constraints_well_formed = result.constraints_well_formed - for constraint in constraints_well_formed: - assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ - constraints_graph_preserving = result.constraints_graph_preserving - for constraint in constraints_graph_preserving: - assert constraint.rel() == pycarl.formula.Relation.GREATER + import pycarl.parse diff --git a/stormpy/tests/core/test_model.py b/stormpy/tests/core/test_model.py new file mode 100644 index 000000000..843b4ff88 --- /dev/null +++ b/stormpy/tests/core/test_model.py @@ -0,0 +1,51 @@ +import stormpy +import stormpy.logic + +class TestModel: + def test_build_dtmc_from_prism_program(self): + stormpy.set_up("") + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + prop = "P=? [F \"one\"]" + formulas = stormpy.parse_formulas_for_program(prop, program) + pair = stormpy.build_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 13 + assert model.nr_transitions() == 20 + assert model.model_type() == stormpy.ModelType.DTMC + assert not model.parametric() + assert type(model) is stormpy.SparseDtmc + + def test_build_parametric_dtmc_from_prism_program(self): + program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") + assert program.nr_modules() == 5 + assert program.model_type() == stormpy.PrismModelType.DTMC + assert program.has_undefined_constants() + prop = "P=? [F \"target\"]" + formulas = stormpy.parse_formulas_for_program(prop, program) + pair = stormpy.build_parametric_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 613 + assert model.nr_transitions() == 803 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() + assert type(model) is stormpy.SparseParametricDtmc + + def test_build_dtmc(self): + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas[0]) + assert model.nr_states() == 13 + assert model.nr_transitions() == 20 + assert model.model_type() == stormpy.ModelType.DTMC + assert not model.parametric() + assert type(model) is stormpy.SparseDtmc + + def test_build_parametric_dtmc(self): + program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") + formulas = stormpy.parse_formulas_for_program("P=? [ F \"target\" ]", program) + model = stormpy.build_parametric_model(program, formulas[0]) + assert model.nr_states() == 613 + assert model.nr_transitions() == 803 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() + assert type(model) is stormpy.SparseParametricDtmc diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py new file mode 100644 index 000000000..4bcb9a4e7 --- /dev/null +++ b/stormpy/tests/core/test_modelchecking.py @@ -0,0 +1,26 @@ +import stormpy +import stormpy.logic + +class TestModelChecking: + def test_state_elimination(self): + import pycarl + import pycarl.formula + program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") + prop = "P=? [F \"target\"]" + formulas = stormpy.parse_formulas_for_program(prop, program) + pair = stormpy.build_parametric_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 613 + assert model.nr_transitions() == 803 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() + result = stormpy.perform_state_elimination(model, formulas[0]) + func = result.result_function + one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) + assert func.denominator == one + constraints_well_formed = result.constraints_well_formed + for constraint in constraints_well_formed: + assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ + constraints_graph_preserving = result.constraints_graph_preserving + for constraint in constraints_graph_preserving: + assert constraint.rel() == pycarl.formula.Relation.GREATER diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py index fe1c92ba0..6335eb6c5 100644 --- a/stormpy/tests/core/test_parse.py +++ b/stormpy/tests/core/test_parse.py @@ -1,4 +1,5 @@ import stormpy +import stormpy.logic class TestParse: def test_parse_program(self): @@ -12,23 +13,3 @@ class TestParse: formulas = stormpy.parse_formulas(prop) assert len(formulas) == 1 assert str(formulas[0]) == prop - - def test_build_model_from_prism_program(self): - program = stormpy.parse_program("../examples/dtmc/die/die.pm") - prop = "P=? [F \"one\"]" - formulas = stormpy.parse_formulas_for_program(prop, program) - pair = stormpy.build_model_from_prism_program(program, formulas) - model = pair.model - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.parametric() - - def test_build_model(self): - program = stormpy.parse_program("../examples/dtmc/die/die.pm") - formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.parametric()