Extended tests based on notebooks

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"
    ]
   },

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)"
    ]
   },
   {

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"
    ]

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.

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,13 +299,18 @@ 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])
         assert type(result) is stormpy.HybridQuantitativeCheckResult
         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"))

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)

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()

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()

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)

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")

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()

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

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"