SetUp when importing stormpy

Former-commit-id: 8e31469f38

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)
     

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

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

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

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

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