|
@ -99,12 +99,18 @@ class TestSparseModel: |
|
|
def test_build_ctmc(self): |
|
|
def test_build_ctmc(self): |
|
|
program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) |
|
|
program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True) |
|
|
formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) |
|
|
formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) |
|
|
model = stormpy.build_model(program, formulas) |
|
|
|
|
|
|
|
|
model = stormpy.build_model(program) |
|
|
assert model.nr_states == 12 |
|
|
assert model.nr_states == 12 |
|
|
assert model.nr_transitions == 22 |
|
|
assert model.nr_transitions == 22 |
|
|
assert model.model_type == stormpy.ModelType.CTMC |
|
|
assert model.model_type == stormpy.ModelType.CTMC |
|
|
assert not model.supports_parameters |
|
|
assert not model.supports_parameters |
|
|
assert type(model) is stormpy.SparseCtmc |
|
|
assert type(model) is stormpy.SparseCtmc |
|
|
|
|
|
model_for_formula = stormpy.build_model(program, formulas) |
|
|
|
|
|
assert model_for_formula.nr_states == 1 |
|
|
|
|
|
assert model_for_formula.nr_transitions == 1 |
|
|
|
|
|
assert model_for_formula.model_type == stormpy.ModelType.CTMC |
|
|
|
|
|
assert not model_for_formula.supports_parameters |
|
|
|
|
|
assert type(model_for_formula) is stormpy.SparseCtmc |
|
|
|
|
|
|
|
|
def test_build_pomdp(self): |
|
|
def test_build_pomdp(self): |
|
|
program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) |
|
|
program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) |
|
@ -115,11 +121,11 @@ class TestSparseModel: |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def test_build_ma(self): |
|
|
def test_build_ma(self): |
|
|
program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma")) |
|
|
|
|
|
formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program) |
|
|
|
|
|
|
|
|
program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) |
|
|
|
|
|
formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ F<=2 s=2 ]", program) |
|
|
model = stormpy.build_model(program, formulas) |
|
|
model = stormpy.build_model(program, formulas) |
|
|
assert model.nr_states == 5 |
|
|
|
|
|
assert model.nr_transitions == 8 |
|
|
|
|
|
|
|
|
assert model.nr_states == 4 |
|
|
|
|
|
assert model.nr_transitions == 7 |
|
|
assert model.model_type == stormpy.ModelType.MA |
|
|
assert model.model_type == stormpy.ModelType.MA |
|
|
assert not model.supports_parameters |
|
|
assert not model.supports_parameters |
|
|
assert type(model) is stormpy.SparseMA |
|
|
assert type(model) is stormpy.SparseMA |
|
|