From 845ba797aaebef25691a9804e927d69c5fde6628 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Aug 2026 18:07:04 +0200 Subject: [PATCH 1/3] Minor improvements in notebooks --- doc/source/doc/exploration.ipynb | 3 +-- doc/source/doc/parametric_models.ipynb | 6 ++++-- doc/source/doc/reward_models.ipynb | 2 +- 3 files changed, 6 insertions(+), 5 deletions(-) diff --git a/doc/source/doc/exploration.ipynb b/doc/source/doc/exploration.ipynb index f079549d3..6e85c2cb3 100644 --- a/doc/source/doc/exploration.ipynb +++ b/doc/source/doc/exploration.ipynb @@ -40,7 +40,6 @@ "source": [ "import doctest\n", "\n", - "doctest.ELLIPSIS_MARKER = \"-etc-\"\n", "import stormpy\n", "import stormpy.examples\n", "import stormpy.examples.files\n", @@ -94,7 +93,7 @@ "\n", "[02-exploration.py](https://github.com/stormchecker/stormpy/blob/master/examples/exploration/02-exploration.py)\n", "\n", - "Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before.\n", + "Internally, POMDPs extend MDPs. Thus, iterating over the POMDP is done as before.\n", "\n" ] }, diff --git a/doc/source/doc/parametric_models.ipynb b/doc/source/doc/parametric_models.ipynb index 334fcd696..64fc81605 100644 --- a/doc/source/doc/parametric_models.ipynb +++ b/doc/source/doc/parametric_models.ipynb @@ -81,7 +81,8 @@ " print(x.name)\n", " point[x] = stormpy.RationalRF(0.4)\n", "instantiated_model = instantiator.instantiate(point)\n", - "result = stormpy.model_checking(instantiated_model, properties[0])" + "result = stormpy.model_checking(instantiated_model, properties[0])\n", + "print(result.at(model.initial_states[0]))" ] }, { @@ -112,7 +113,8 @@ "source": [ "result = stormpy.model_checking(model, properties[0])\n", "initial_state = model.initial_states[0]\n", - "func = result.at(initial_state)" + "func = result.at(initial_state)\n", + "print(func)" ] }, { diff --git a/doc/source/doc/reward_models.ipynb b/doc/source/doc/reward_models.ipynb index cefcd031a..e20bd2d97 100644 --- a/doc/source/doc/reward_models.ipynb +++ b/doc/source/doc/reward_models.ipynb @@ -36,7 +36,7 @@ "program = stormpy.parse_prism_program(stormpy.examples.files.prism_dtmc_die)\n", "prop = 'R=? [F \"done\"]'\n", "\n", - "properties = stormpy.parse_properties(prop, program, None)\n", + "properties = stormpy.parse_properties(prop, program)\n", "model = stormpy.build_model(program, properties)\n", "assert len(model.reward_models) == 1" ] From 2559174293d9cde411e9ea578dfe7c981afc7815 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Aug 2026 18:07:17 +0200 Subject: [PATCH 2/3] Fixed typo --- lib/stormpy/info/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/stormpy/info/__init__.py b/lib/stormpy/info/__init__.py index 4cfa72092..9570529c7 100644 --- a/lib/stormpy/info/__init__.py +++ b/lib/stormpy/info/__init__.py @@ -67,7 +67,7 @@ def storm_directory() -> str | None: """ Return the Storm directory which is used by stormpy. - If a prexisting installation of Storm was used, then the path to this directory is returned. + If a preexisting installation of Storm was used, then the path to this directory is returned. If Storm was installed during the installation process, value ``None`` is returned. :return: Storm directory. From d6fdd47b9fcfec27a3f51bcfa1401a4967957a7d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 14 Aug 2026 18:08:14 +0200 Subject: [PATCH 3/3] Extended tests based on documentation notebooks --- tests/core/test_modelchecking.py | 34 ++++- tests/dft/test_analysis.py | 10 +- tests/gspn/test_gspn.py | 2 + tests/gspn/test_gspn_io.py | 8 + tests/info/test_info.py | 38 +++-- tests/pars/test_model_instantiator.py | 38 +++++ tests/pars/test_parametric.py | 35 +++++ tests/pars/test_parametric_model.py | 4 + tests/pycarl/core/test_polynomial.py | 11 ++ tests/simulator/test_simulator.py | 202 +++++++++++++++++++++++-- tests/storage/test_bitvector.py | 1 + tests/storage/test_model.py | 20 ++- tests/storage/test_model_components.py | 16 ++ tests/storage/test_scheduler.py | 1 + tests/storage/test_state.py | 43 ++++++ tests/utility/test_shortestpaths.py | 15 ++ 16 files changed, 449 insertions(+), 29 deletions(-) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 6975f1c94..2dd7dbc4f 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -7,7 +7,7 @@ class TestModelChecking: - def test_model_checking_prism_dtmc(self): + def test_model_checking_prism_dtmc_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_model(program, formulas) @@ -19,6 +19,30 @@ def test_model_checking_prism_dtmc(self): result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 1 / 6) + def test_model_checking_prism_dtmc_p(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=2 ]", program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 8 + assert model.nr_transitions == 12 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 1 / 2) + + def test_model_checking_prism_dtmc_reward(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties('R=? [F "done"]', program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 11 / 3) + @spot def test_model_checking_prism_dtmc_ltl(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -259,10 +283,13 @@ def test_model_checking_prism_dd_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_symbolic_model(program, formulas) + assert isinstance(model, stormpy.SymbolicSylvanDtmc) assert model.nr_states == 13 assert model.nr_transitions == 20 result = stormpy.check_model_dd(model, formulas[0]) assert type(result) is stormpy.SymbolicQuantitativeCheckResult + assert result.min == 0.0 + assert result.max == 1.0 filter = stormpy.create_filter_initial_states_symbolic(model) result.filter(filter) assert result.min == result.max @@ -272,6 +299,7 @@ def test_model_checking_prism_hybrid_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program('P=? [ F "one" ]', program) model = stormpy.build_symbolic_model(program, formulas) + assert isinstance(model, stormpy.SymbolicSylvanDtmc) assert model.nr_states == 13 assert model.nr_transitions == 20 result = stormpy.check_model_hybrid(model, formulas[0]) @@ -279,6 +307,10 @@ def test_model_checking_prism_hybrid_dtmc(self): values = result.get_values() assert len(values) == 3 assert math.isclose(values[0], 1 / 6) + filter = stormpy.create_filter_initial_states_symbolic(model) + result.filter(filter) + assert result.min == result.max + assert math.isclose(result.min, 1 / 6, rel_tol=1e-6) def test_compute_expected_number_of_visits(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/dft/test_analysis.py b/tests/dft/test_analysis.py index 8acb9b2f1..45d8d05ea 100644 --- a/tests/dft/test_analysis.py +++ b/tests/dft/test_analysis.py @@ -7,13 +7,21 @@ @dft class TestAnalysis: - def test_analyze_mttf(self): + def test_analyze_and_mttf(self): dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) formulas = stormpy.parse_properties('T=? [ F "failed" ]') assert dft.nr_elements() == 3 results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) assert math.isclose(results[0], 3) + def test_analyze_hecs_mttf(self): + dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "hecs.dft")) + formula_str = 'T=? [ F "failed" ]' + formulas = stormpy.parse_properties(formula_str) + results = stormpy.dft.analyze_dft(dft, [formulas[0].raw_formula]) + result = results[0] + assert math.isclose(result, 363.8947965815, rel_tol=1e-6) + def test_build_model(self): dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json")) model = stormpy.dft.build_model(dft) diff --git a/tests/gspn/test_gspn.py b/tests/gspn/test_gspn.py index c970f8a33..25685058b 100644 --- a/tests/gspn/test_gspn.py +++ b/tests/gspn/test_gspn.py @@ -187,6 +187,7 @@ def test_export_to_pnpro(self, tmpdir): # export gspn to pnml gspn.export_gspn_pnpro_file(export_file) + assert os.path.exists(export_file) # import gspn gspn_parser = stormpy.gspn.GSPNParser() @@ -229,6 +230,7 @@ def test_export_to_pnml(self, tmpdir): # export gspn to pnml gspn.export_gspn_pnml_file(export_file) + assert os.path.exists(export_file) # import gspn gspn_parser = stormpy.gspn.GSPNParser() diff --git a/tests/gspn/test_gspn_io.py b/tests/gspn/test_gspn_io.py index 85df29d20..02c188d61 100644 --- a/tests/gspn/test_gspn_io.py +++ b/tests/gspn/test_gspn_io.py @@ -9,6 +9,14 @@ @gspn class TestGSPNJani: + def test_simple_pnml(self): + gspn_parser = stormpy.gspn.GSPNParser() + gspn = gspn_parser.parse(get_example_path("gspn", "gspn_simple.pnml")) + assert gspn.get_name() == "simple_gspn" + assert gspn.get_number_of_places() == 4 + assert gspn.get_number_of_immediate_transitions() == 3 + assert gspn.get_number_of_timed_transitions() == 2 + @xml def test_custom_property(self): gspn_parser = stormpy.gspn.GSPNParser() diff --git a/tests/info/test_info.py b/tests/info/test_info.py index 0382dabb9..cac3d44aa 100644 --- a/tests/info/test_info.py +++ b/tests/info/test_info.py @@ -3,20 +3,38 @@ class TestInfo: def test_version(self): - assert isinstance(stormpy.info.Version.short, str) and "." in stormpy.info.Version.short - assert isinstance(stormpy.info.Version.long, str) and "Version" in stormpy.info.Version.long - assert isinstance(stormpy.info.Version.build_info, str) and "Compiled" in stormpy.info.Version.build_info - - def test_version_equal(self): + # Short version + assert isinstance(stormpy.info.Version.short, str) + assert "." in stormpy.info.Version.short + # Long version + assert isinstance(stormpy.info.Version.long, str) + assert stormpy.info.Version.long.startswith("Version ") + assert stormpy.info.Version.short in stormpy.info.Version.long + # storm_version() assert stormpy.info.storm_version() in stormpy.info.Version.short + assert "." in stormpy.info.storm_version() + # Development version + assert stormpy.info.storm_development_version() == stormpy.info.Version.development assert (stormpy.info.Version.development and stormpy.info.Version.short.endswith(" (dev)")) or not stormpy.info.Version.development - def test_build_type(self): - bt = stormpy.info.storm_build_type() - assert bt in ("Debug", "Release") + def test_build_info(self): + assert isinstance(stormpy.info.Version.build_info, str) + assert "Compiled" in stormpy.info.Version.build_info + assert stormpy.info.storm_build_type() in ("Debug", "Release") def test_origin_info(self): - repo, tag, h = stormpy.info.storm_origin_info() + assert isinstance(stormpy.info.storm_from_system(), bool) + assert stormpy.info.storm_from_system() == (stormpy.info.storm_directory() is not None) + repo, tag, hsh = stormpy.info.storm_origin_info() assert repo is None or isinstance(repo, str) assert tag is None or isinstance(tag, str) - assert isinstance(h, str) + if stormpy.info.storm_from_system(): + assert repo is None and tag is None + else: + assert isinstance(repo, str) and isinstance(tag, str) + assert isinstance(hsh, str) + assert hsh == stormpy.info.Version.git_hash + + def test_number_repressentations(self): + assert isinstance(stormpy.info.storm_exact_use_cln(), bool) + assert isinstance(stormpy.info.storm_ratfunc_use_cln(), bool) diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index b01483a77..5174367ac 100644 --- a/tests/pars/test_model_instantiator.py +++ b/tests/pars/test_model_instantiator.py @@ -25,6 +25,26 @@ def test_instantiate_dtmc(self): instantiated_model2 = instantiator.instantiate(point) assert "0.5" in str(instantiated_model2.transition_matrix[1]) + def test_instantiate_dtmc_die(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [F s=7 & d=2]", program) + model = stormpy.build_parametric_model(program, formulas) + parameters = model.collect_all_parameters() + assert len(parameters) == 2 + instantiator = stormpy.pars.PDtmcInstantiator(model) + point = dict() + for x in parameters: + assert x.name in {"p", "q"} + point[x] = stormpy.RationalRF(0.4) + instantiated_model = instantiator.instantiate(point) + assert instantiated_model.nr_states == model.nr_states + assert not instantiated_model.has_parameters + + result = stormpy.model_checking(instantiated_model, formulas[0]) + initial_state = instantiated_model.initial_states[0] + assert initial_state == 0 + assert math.isclose(result.at(initial_state), 4 / 35) + def test_sample_pdtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) formulas = stormpy.parse_properties_for_prism_program('P=? [F "error"]', program) @@ -78,3 +98,21 @@ def test_pdtmc_exact_instantiation_checker(self): res = result.at(model.initial_states[0]) assert isinstance(res, stormpy.Rational) assert res == stormpy.Rational("29/15") + + def test_pdtmc_exact_instantiation_checker_die(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [F s=7 & d=2]", program) + model = stormpy.build_parametric_model(program, formulas) + + parameters = model.collect_all_parameters() + inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(model) + inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) + inst_checker.set_graph_preserving(True) + env = stormpy.Environment() + + point = {p: stormpy.RationalRF("2/5") for p in parameters} + result = inst_checker.check(env, point) + assert isinstance(result, stormpy.ExplicitExactQuantitativeCheckResult) + res = result.at(model.initial_states[0]) + assert isinstance(res, stormpy.Rational) + assert res == stormpy.Rational("4/35") diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 85df6a7cd..15d31ef2f 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -23,6 +23,39 @@ def test_parametric_model_checking_sparse(self): one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) assert func.denominator == one + def test_parametric_model_checking_sparse_die(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) + prop = "P=? [F s=7 & d=2]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + func = result.at(initial_state) + + # Create rational function for comparison + if stormpy.info.storm_ratfunc_use_cln(): + from stormpy.pycarl import cln as pc + else: + from stormpy.pycarl import gmp as pc + parameters = model.collect_all_parameters() + for par in parameters: + if par.name == "p": + p = pc.create_factorized_polynomial(pc.Polynomial(par)) + else: + assert par.name == "q" + q = pc.create_factorized_polynomial(pc.Polynomial(par)) + + one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) + num = p * p * (q - one) + denom = p * q - one + assert func.numerator == num + assert func.denominator == denom + def test_parametric_model_checking_dd(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "parametric_die.pm")) prop = "P=? [F s=5]" @@ -108,11 +141,13 @@ def test_constraints_collector(self): model = stormpy.build_parametric_model(program, formulas) collector = stormpy.ConstraintCollector(model) constraints_well_formed = collector.wellformed_constraints + assert len(constraints_well_formed) == 4 for formula in constraints_well_formed: assert formula.type == FormulaType.CONSTRAINT constraint = formula.get_constraint() assert constraint.relation == Relation.LEQ constraints_graph_preserving = collector.graph_preserving_constraints + assert len(constraints_graph_preserving) == 4 for formula in constraints_graph_preserving: assert formula.type == FormulaType.CONSTRAINT constraint = formula.get_constraint() diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py index 64bc5b6f8..d15ad150c 100644 --- a/tests/pars/test_parametric_model.py +++ b/tests/pars/test_parametric_model.py @@ -17,6 +17,7 @@ def test_build_parametric_dtmc(self): assert model.supports_parameters assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc + assert {x.name for x in model.collect_all_parameters()} == {"pL", "pK"} def test_build_parametric_dtmc_preprocess(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) @@ -30,6 +31,7 @@ def test_build_parametric_dtmc_preprocess(self): assert model.supports_parameters assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc + assert {x.name for x in model.collect_all_parameters()} == {"p"} def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -41,6 +43,7 @@ def test_build_dtmc_supporting_parameters(self): assert model.supports_parameters assert not model.has_parameters assert type(model) is stormpy.SparseParametricDtmc + assert len(model.collect_all_parameters()) == 0 def test_build_parametric_mdp(self): program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) @@ -51,6 +54,7 @@ def test_build_parametric_mdp(self): assert model.model_type == stormpy.ModelType.MDP assert model.supports_parameters assert type(model) is stormpy.SparseParametricMdp + assert {x.name for x in model.collect_all_parameters()} == {"p1", "p2"} @pars diff --git a/tests/pycarl/core/test_polynomial.py b/tests/pycarl/core/test_polynomial.py index a956ea86d..20f14bb7f 100644 --- a/tests/pycarl/core/test_polynomial.py +++ b/tests/pycarl/core/test_polynomial.py @@ -89,3 +89,14 @@ def test_substitute(self, package): z = pycarl.Variable("z") sub2 = {z: package.Polynomial(3)} assert pol1.substitute(sub2) == pol1 + + def test_to_string(self, package): + pycarl.clear_pools() + x = pycarl.Variable("x") + y = pycarl.Variable("y") + pol1 = x * x + package.Integer(2) + pol2 = y + package.Integer(1) + result = pol1 * pol2 + assert str(pol1) == "x^2+2" + assert str(pol2) == "y+1" + assert str(result) == "x^2*y+2*y+x^2+2" diff --git a/tests/simulator/test_simulator.py b/tests/simulator/test_simulator.py index a7fce27c1..d9eb1dd8d 100644 --- a/tests/simulator/test_simulator.py +++ b/tests/simulator/test_simulator.py @@ -2,24 +2,162 @@ import stormpy.simulator from helpers.helper import get_example_path +import random + + +class TestSparseModelSimulator: + def test_simulate_die_steps(self): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + model = stormpy.build_model(prism_program) + simulator = stormpy.simulator.create_simulator(model, seed=42) + + assert model.labeling.get_labels_of_state(11) == {"done", "five"} + # Perform 3 steps + # each steps returns (state, reward, labels) + assert simulator.restart() == (0, [0.0], {"init"}) + assert simulator.step() == (2, [1.0], set()) + assert simulator.step() == (5, [1.0], set()) + assert simulator.step() == (11, [1.0], {"done", "five"}) + assert simulator.step() == (11, [0.0], {"done", "five"}) + assert simulator.step() == (11, [0.0], {"done", "five"}) + assert simulator.is_done() + + def test_simulate_die(self): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + model = stormpy.build_model(prism_program) + simulator = stormpy.simulator.create_simulator(model, seed=42) + + final_outcomes = dict() + for n in range(10): + assert not simulator.is_done() + while not simulator.is_done(): + observation, reward, labels = simulator.step() + assert len(labels) == 2 + assert "done" in labels + if observation not in final_outcomes: + final_outcomes[observation] = 1 + else: + final_outcomes[observation] += 1 + simulator.restart() + assert len(final_outcomes) == 6 + assert set(final_outcomes.keys()) == {7, 8, 9, 10, 11, 12} + assert sum(final_outcomes.values()) == 10 + + def test_simulate_die_steps_vals(self): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + options = stormpy.BuilderOptions() + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + simulator = stormpy.simulator.create_simulator(model, seed=42) + simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) + + state, reward, label = simulator.restart() + assert state["d"] == 0 + assert state["s"] == 0 + assert reward == [0.0] + assert label == {"init"} + + def test_simulate_die_vals(self): + path = stormpy.examples.files.prism_dtmc_die + prism_program = stormpy.parse_prism_program(path) + options = stormpy.BuilderOptions() + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + simulator = stormpy.simulator.create_simulator(model, seed=42) + simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) + assert simulator.get_reward_names() == ["coin_flips"] -class TestSparseSimulator: - path = stormpy.examples.files.prism_dtmc_die - prism_program = stormpy.parse_prism_program(path) - - model = stormpy.build_model(prism_program) - simulator = stormpy.simulator.create_simulator(model, seed=42) - final_outcomes = dict() - for n in range(7): - while not simulator.is_done(): - observation, reward, labels = simulator.step() - assert len(labels) == 2 - assert "done" in labels - if observation not in final_outcomes: - final_outcomes[observation] = 1 - else: - final_outcomes[observation] += 1 simulator.restart() + final_outcomes = dict() + print(simulator.get_reward_names()) + for n in range(10): + assert not simulator.is_done() + while not simulator.is_done(): + observation, reward, labels = simulator.step() + if observation not in final_outcomes: + final_outcomes[observation] = 1 + else: + final_outcomes[observation] += 1 + simulator.restart() + + assert len(final_outcomes) == 6 + assert sum(final_outcomes.values()) == 10 + for vals, count in final_outcomes.items(): + assert 1 <= int(vals["d"]) <= 6 + assert vals["s"] == 7 + assert 1 <= count <= 10 + + def test_simulate_mdp(self): + random.seed(23) + path = stormpy.examples.files.prism_mdp_slipgrid + prism_program = stormpy.parse_prism_program(path) + model = stormpy.build_model(prism_program) + simulator = stormpy.simulator.create_simulator(model, seed=42) + + # 3 paths of at most 20 steps. + paths = [] + for m in range(3): + state, reward, labels = simulator.restart() + path = [state] + for n in range(20): + actions = simulator.available_actions() + assert len(actions) <= 4 + select_action = random.randint(0, len(actions) - 1) + path.append(actions[select_action]) + state, reward, labels = simulator.step(actions[select_action]) + assert 0 <= state <= 15 + path.append(state) + if simulator.is_done(): + break + paths.append(path) + + assert len(paths) == 3 + for path in paths: + assert path[0] == 0 + assert isinstance(len(path) % 2, int) + assert len(path) <= 41 + + def test_simulate_mdp_valuations(self): + random.seed(23) + path = stormpy.examples.files.prism_mdp_slipgrid + prism_program = stormpy.parse_prism_program(path) + options = stormpy.BuilderOptions() + options.set_build_choice_labels() + options.set_build_state_valuations() + model = stormpy.build_sparse_model_with_options(prism_program, options) + simulator = stormpy.simulator.create_simulator(model, seed=42) + simulator.set_action_mode(stormpy.simulator.SimulatorActionMode.GLOBAL_NAMES) + simulator.set_observation_mode(stormpy.simulator.SimulatorObservationMode.PROGRAM_LEVEL) + + # 3 paths of at most 20 steps. + paths = [] + for m in range(3): + path = [] + state, reward, labels = simulator.restart() + path = [state] + for n in range(20): + actions = simulator.available_actions() + assert len(actions) <= 4 + select_action = random.randint(0, len(actions) - 1) + assert actions[select_action] in ["north", "east", "south", "west"] + path.append(actions[select_action]) + state, reward, labels = simulator.step(actions[select_action]) + path.append(state) + assert 1 <= int(state["x"]) <= 4 + assert 1 <= int(state["y"]) <= 4 + if simulator.is_done(): + break + paths.append(path) + + assert len(paths) == 3 + for path in paths: + assert path[0]["x"] == 1 + assert path[0]["y"] == 1 + assert isinstance(len(path) % 2, int) + assert len(path) <= 41 class TestPrismSimulator: @@ -32,3 +170,35 @@ def test_negative_values(self): state, rew, labels = simulator.restart() assert state["s"] == -1 assert int(state["s"]) == -1 + + def test_simulate_mdp(self): + random.seed(23) + path = stormpy.examples.files.prism_mdp_slipgrid + prism_program = stormpy.parse_prism_program(path) + simulator = stormpy.simulator.create_simulator(prism_program, seed=42) + + # 3 paths of at most 20 steps. + paths = [] + for m in range(3): + state, reward, labels = simulator.restart() + path = [state] + for n in range(20): + actions = simulator.available_actions() + assert len(actions) <= 4 + select_action = random.randint(0, len(actions) - 1) + assert actions[select_action] < 4 + path.append(actions[select_action]) + state, reward, labels = simulator.step(actions[select_action]) + path.append(state) + assert 1 <= int(state["x"]) <= 4 + assert 1 <= int(state["y"]) <= 4 + if simulator.is_done(): + break + paths.append(path) + + assert len(paths) == 3 + for path in paths: + assert path[0]["x"] == 1 + assert path[0]["y"] == 1 + assert isinstance(len(path) % 2, int) + assert len(path) <= 41 diff --git a/tests/storage/test_bitvector.py b/tests/storage/test_bitvector.py index 06248dcc3..a03b8597a 100644 --- a/tests/storage/test_bitvector.py +++ b/tests/storage/test_bitvector.py @@ -13,6 +13,7 @@ def test_init_length(self): assert bit.number_of_set_bits() == 0 bit = stormpy.BitVector(5, True) assert bit.size() == 5 + assert len(bit) == 5 assert bit.number_of_set_bits() == 5 def test_init_vector(self): diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index ae875d766..9ea6a836f 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -14,8 +14,9 @@ def test_build_dtmc_from_prism_program(self): assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc + assert model.labeling.get_labels() == {"one", "two", "three", "four", "five", "six", "done", "init", "deadlock"} - def test_build_dtmc_from_prism_program_formulas(self): + def test_build_dtmc_from_prism_program_formulas_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) prop = 'P=? [F "one"]' properties = stormpy.parse_properties_for_prism_program(prop, program, None) @@ -26,6 +27,20 @@ def test_build_dtmc_from_prism_program_formulas(self): assert len(model.reward_models) == 0 assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc + assert set(model.labeling.get_labels()) == {"init", "deadlock", "one"} + + def test_build_dtmc_from_prism_program_formulas_ap(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + prop = "P=? [F s=2]" + properties = stormpy.parse_properties_for_prism_program(prop, program, None) + model = stormpy.build_model(program, properties) + assert model.nr_states == 8 + assert model.nr_transitions == 12 + assert model.model_type == stormpy.ModelType.DTMC + assert len(model.reward_models) == 0 + assert not model.supports_parameters + assert type(model) is stormpy.SparseDtmc + assert set(model.labeling.get_labels()) == {"init", "deadlock", "(s = 2)"} def test_build_dtmc_from_prism_program_reward_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -36,8 +51,11 @@ def test_build_dtmc_from_prism_program_reward_formulas(self): assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC assert len(model.reward_models) == 1 + assert "coin_flips" in model.reward_models assert not model.reward_models["coin_flips"].has_state_rewards assert model.reward_models["coin_flips"].has_state_action_rewards + assert len(model.reward_models["coin_flips"].state_action_rewards) == 13 + assert sum(model.reward_models["coin_flips"].state_action_rewards) == 7.0 for reward in model.reward_models["coin_flips"].state_action_rewards: assert reward == 1.0 or reward == 0.0 assert not model.reward_models["coin_flips"].has_transition_rewards diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index e30712c7b..231e80cdd 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -98,6 +98,7 @@ def test_build_dtmc(self): dtmc = stormpy.storage.SparseDtmc(components) assert type(dtmc) is stormpy.SparseDtmc + assert dtmc.model_type == stormpy.ModelType.DTMC assert not dtmc.supports_parameters # Test transition matrix @@ -112,9 +113,21 @@ def test_build_dtmc(self): # Test state labeling assert dtmc.labeling.get_labels() == {"init", "deadlock", "done", "one", "two", "three", "four", "five", "six"} + assert dtmc.labeling.get_states("done").number_of_set_bits() == 6 + assert dtmc.labeling.get_states("six").number_of_set_bits() == 1 + + # Test initial states + initial_states = dtmc.initial_states + assert len(initial_states) == 1 + assert initial_states[0] == 0 + initial_states = dtmc.labeling.get_states("init") + assert initial_states.number_of_set_bits() == 1 + assert initial_states.size() == nr_states + assert initial_states.get(0) # Test reward_models assert len(dtmc.reward_models) == 1 + assert "coin_flips" in dtmc.reward_models assert not dtmc.reward_models["coin_flips"].has_state_rewards assert dtmc.reward_models["coin_flips"].has_state_action_rewards for reward in dtmc.reward_models["coin_flips"].state_action_rewards: @@ -252,6 +265,7 @@ def test_build_mdp(self): mdp = stormpy.storage.SparseMdp(components) assert type(mdp) is stormpy.SparseMdp + assert mdp.model_type == stormpy.ModelType.MDP assert not mdp.supports_parameters # Test transition matrix @@ -269,6 +283,7 @@ def test_build_mdp(self): # Test reward models assert len(mdp.reward_models) == 1 + assert "coin_flips" in mdp.reward_models assert not mdp.reward_models["coin_flips"].has_state_rewards assert mdp.reward_models["coin_flips"].has_state_action_rewards for reward in mdp.reward_models["coin_flips"].state_action_rewards: @@ -402,6 +417,7 @@ def test_build_ctmc(self): # Build CTMC ctmc = stormpy.storage.SparseCtmc(components) assert type(ctmc) is stormpy.SparseCtmc + assert ctmc.model_type == stormpy.ModelType.CTMC assert not ctmc.supports_parameters # Test transition matrix diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index 86a4a9a14..fb547af39 100644 --- a/tests/storage/test_scheduler.py +++ b/tests/storage/test_scheduler.py @@ -16,6 +16,7 @@ def test_scheduler_mdp(self): model = stormpy.build_sparse_model_with_options(program, options) assert model.nr_states == 272 assert model.nr_transitions == 492 + assert model.nr_choices == 400 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] assert initial_state == 0 diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py index c39b77ece..f7a4e6346 100644 --- a/tests/storage/test_state.py +++ b/tests/storage/test_state.py @@ -1,3 +1,5 @@ +import math + import stormpy from helpers.helper import get_example_path @@ -185,3 +187,44 @@ def test_parametric_transitions(self): j += 1 for transition in action.transitions: assert transition.value().denominator == one + + def test_states_mdp_maze(self): + program = stormpy.parse_prism_program(get_example_path("mdp", "maze_2.nm")) + properties = stormpy.parse_properties_for_prism_program('R=? [F "goal"]', program, None) + model = stormpy.build_model(program, properties) + assert model.nr_states == 15 + assert model.nr_transitions == 66 + assert len(model.initial_states) == 1 + assert list(model.initial_states) == [0] + + expected = { # built state -> targets per action [east, west, north, south] + 1: [2, 1, 1, 6], + 2: [3, 1, 2, 2], + 3: [4, 2, 3, 7], + 4: [5, 3, 4, 4], + 5: [5, 4, 5, 8], + 6: [6, 6, 1, 9], + 7: [7, 7, 3, 10], + 8: [8, 8, 5, 11], + 9: [9, 9, 6, 12], + 10: [10, 10, 7, 14], + 11: [11, 11, 8, 13], + 12: [12, 12, 9, 12], + 13: [13, 13, 11, 13], + 14: [14], + } + for state in model.states: + if state.id == 0: + assert len(state.actions) == 1 + else: + assert len(state.actions) == len(expected[state.id]) + for action in state.actions: + if state.id == 0: + assert len(action.transitions) == 13 + for transition in action.transitions: + assert math.isclose(transition.value(), 1 / 13) + else: + assert len(action.transitions) == 1 + for transition in action.transitions: + assert transition.value() == 1 + assert transition.column == expected[state.id][action.id] diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index ea63cbaad..2922b21bf 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -143,3 +143,18 @@ def test_spg_state_set(self, model, target_label, index, expected_state_set): def test_spg_state_list(self, model, target_label, index, expected_path): spg = ShortestPathsGenerator(model, target_label) assert spg.get_path_as_list(index) == expected_path(index) + + +def test_shortest_paths_die(): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + model = stormpy.build_model(program) + spg = ShortestPathsGenerator(model, 8) + + expected = { + 1: ([8, 4, 1, 0], 0.125), + 2: ([8, 4, 1, 3, 1, 0], 0.03125), + 3: ([8, 4, 1, 3, 1, 3, 1, 0], 0.0078125), + } + for k, (path, distance) in expected.items(): + assert spg.get_path_as_list(k) == path + assert math.isclose(spg.get_distance(k), distance)