diff --git a/stormpy/tests/conftest.py b/stormpy/tests/conftest.py
new file mode 100644
index 000000000..5e85fe646
--- /dev/null
+++ b/stormpy/tests/conftest.py
@@ -0,0 +1,3 @@
+import sys
+import os
+sys.path.append(os.path.join(os.path.dirname(__file__), 'helpers'))
diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py
index 072f6cd07..7e845ffce 100644
--- a/stormpy/tests/core/test_bisimulation.py
+++ b/stormpy/tests/core/test_bisimulation.py
@@ -1,9 +1,10 @@
import stormpy
import stormpy.logic
+from helpers.helper import get_example_path
class TestBisimulation:
def test_bisimulation(self):
- program = stormpy.parse_prism_program("../examples/dtmc/crowds/crowds5_5.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds", "crowds5_5.pm"))
assert program.nr_modules() == 1
assert program.model_type() == stormpy.PrismModelType.DTMC
prop = "P=? [F \"observe0Greater1\"]"
@@ -21,7 +22,7 @@ class TestBisimulation:
assert not model_bisim.supports_parameters()
def test_parametric_bisimulation(self):
- program = stormpy.parse_prism_program("../examples/pdtmc/crowds/crowds_3-5.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds", "crowds_3-5.pm"))
assert program.nr_modules() == 1
assert program.model_type() == stormpy.PrismModelType.DTMC
assert program.has_undefined_constants()
diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py
index 673e489b7..ba0b5f74a 100644
--- a/stormpy/tests/core/test_modelchecking.py
+++ b/stormpy/tests/core/test_modelchecking.py
@@ -1,9 +1,10 @@
import stormpy
import stormpy.logic
+from helpers.helper import get_example_path
class TestModelChecking:
def test_model_checking_dtmc(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states() == 13
@@ -12,7 +13,7 @@ class TestModelChecking:
assert result == 0.16666666666666663
def test_model_checking_all_dtmc(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states() == 13
@@ -24,7 +25,7 @@ class TestModelChecking:
def test_parametric_state_elimination(self):
import pycarl
import pycarl.formula
- program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
prop = "P=? [F \"target\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program)
pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py
index 54fe7ef3a..a8f41f4e1 100644
--- a/stormpy/tests/core/test_parse.py
+++ b/stormpy/tests/core/test_parse.py
@@ -1,9 +1,10 @@
import stormpy
import stormpy.logic
+from helpers.helper import get_example_path
class TestParse:
def test_parse_prism_program(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
assert program.nr_modules() == 1
assert program.model_type() == stormpy.PrismModelType.DTMC
assert not program.has_undefined_constants()
@@ -15,7 +16,7 @@ class TestParse:
assert str(formulas[0]) == prop
def test_parse_explicit_dtmc(self):
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
assert model.nr_states() == 13
assert model.nr_transitions() == 20
assert model.model_type() == stormpy.ModelType.DTMC
@@ -23,7 +24,7 @@ class TestParse:
assert type(model) is stormpy.SparseDtmc
def test_parse_explicit_mdp(self):
- model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
+ model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
assert model.nr_states() == 169
assert model.nr_transitions() == 436
assert model.model_type() == stormpy.ModelType.MDP
diff --git a/stormpy/tests/helpers/helper.py b/stormpy/tests/helpers/helper.py
new file mode 100644
index 000000000..d07b6ef0f
--- /dev/null
+++ b/stormpy/tests/helpers/helper.py
@@ -0,0 +1,5 @@
+import os
+example_dir = os.path.abspath(os.path.join(os.path.dirname(__file__), os.pardir, os.pardir, os.pardir, "examples"))
+
+def get_example_path(*paths):
+ return os.path.join(example_dir, *paths)
diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py
index 3310bb1fe..3cc3a5a16 100644
--- a/stormpy/tests/storage/test_matrix.py
+++ b/stormpy/tests/storage/test_matrix.py
@@ -1,8 +1,9 @@
import stormpy
+from helpers.helper import get_example_path
class TestMatrix:
def test_sparse_matrix(self):
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
matrix = model.transition_matrix()
assert type(matrix) is stormpy.storage.SparseMatrix
assert matrix.nr_rows() == model.nr_states()
@@ -12,7 +13,7 @@ class TestMatrix:
assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column() > 6)
def test_change_sparse_matrix(self):
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
matrix = model.transition_matrix()
for e in matrix:
assert e.value() == 0.5 or e.value() == 0 or e.value() == 1
@@ -27,7 +28,7 @@ class TestMatrix:
def test_change_sparse_matrix_modelchecking(self):
import stormpy.logic
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
matrix = model.transition_matrix()
# Check matrix
for e in matrix:
@@ -67,7 +68,7 @@ class TestMatrix:
def test_change_parametric_sparse_matrix_modelchecking(self):
import stormpy.logic
import pycarl
- program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
matrix = model.transition_matrix()
diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py
index 94abdad61..7fc4894dc 100644
--- a/stormpy/tests/storage/test_model.py
+++ b/stormpy/tests/storage/test_model.py
@@ -1,9 +1,10 @@
import stormpy
import stormpy.logic
+from helpers.helper import get_example_path
class TestModel:
def test_build_dtmc_from_prism_program(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
prop = "P=? [F \"one\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program)
pair = stormpy.build_model_from_prism_program(program, formulas)
@@ -15,7 +16,7 @@ class TestModel:
assert type(model) is stormpy.SparseDtmc
def test_build_parametric_dtmc_from_prism_program(self):
- program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
assert program.nr_modules() == 5
assert program.model_type() == stormpy.PrismModelType.DTMC
assert program.has_undefined_constants()
@@ -31,7 +32,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_build_dtmc(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
assert model.nr_states() == 13
@@ -41,7 +42,7 @@ class TestModel:
assert type(model) is stormpy.SparseDtmc
def test_build_parametric_dtmc(self):
- program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
assert model.nr_states() == 613
@@ -52,7 +53,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_build_dtmc_supporting_parameters(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
assert model.nr_states() == 13
@@ -63,7 +64,7 @@ class TestModel:
assert type(model) is stormpy.SparseParametricDtmc
def test_label(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
labels = model.labels()
@@ -74,7 +75,7 @@ class TestModel:
assert "one" in model.labels_state(7)
def test_initial_states(self):
- program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+ program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0])
initial_states = model.initial_states()
@@ -82,7 +83,7 @@ class TestModel:
assert 0 in initial_states
def test_label_parametric(self):
- program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0])
labels = model.labels()
diff --git a/stormpy/tests/storage/test_model_iterators.py b/stormpy/tests/storage/test_model_iterators.py
index 8ab2e3ea3..04a8fadc4 100644
--- a/stormpy/tests/storage/test_model_iterators.py
+++ b/stormpy/tests/storage/test_model_iterators.py
@@ -1,8 +1,9 @@
import stormpy
+from helpers.helper import get_example_path
class TestModelIterators:
def test_states_dtmc(self):
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@@ -11,7 +12,7 @@ class TestModelIterators:
assert i == model.nr_states()
def test_states_mdp(self):
- model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
+ model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@@ -20,14 +21,14 @@ class TestModelIterators:
assert i == model.nr_states()
def test_actions_dtmc(self):
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
for action in state.actions():
assert action.row == 0
def test_actions_mdp(self):
- model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
+ model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
for action in state.actions():
@@ -40,7 +41,7 @@ class TestModelIterators:
(6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
s = stormpy.state.State(0, model)
i = 0
for state in stormpy.state.State(0, model):
@@ -53,7 +54,7 @@ class TestModelIterators:
assert transition.value() == transition_orig[2]
def test_transitions_mdp(self):
- model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
+ model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab"))
s = stormpy.state.State(0, model)
for state in stormpy.state.State(0, model):
i = 0
@@ -70,7 +71,7 @@ class TestModelIterators:
(6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
- model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+ model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab"))
i = 0
for state in stormpy.state.State(0, model):
for transition in model.transition_matrix().row_iter(state.id, state.id):