sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Relaxed relative tolerance for some model checking results

refactoring
Matthias Volk 6 years ago
parent
9b1c64860a
commit
ae8615533b
2 changed files with 15 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 17
      tests/core/test_modelchecking.py
  2. 17
      tests/pars/test_pla.py

17
tests/core/test_modelchecking.py
View File

@ -16,7 +16,7 @@ class TestModelChecking:
initial_state = model.initial_states[0] initial_state = model.initial_states[0]
assert initial_state == 0 assert initial_state == 0
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert math.isclose(result.at(initial_state), 0.16666666666666663)
assert math.isclose(result.at(initial_state), 1 / 6)
def test_model_checking_prism_mdp(self): def test_model_checking_prism_mdp(self):
program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm"))
@ -28,8 +28,7 @@ class TestModelChecking:
initial_state = model.initial_states[0] initial_state = model.initial_states[0]
assert initial_state == 0 assert initial_state == 0
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert math.isclose(result.at(initial_state), 0.3828117384)
assert math.isclose(result.at(initial_state), 49 / 128, rel_tol=1e-5)
def test_model_checking_jani_dtmc(self): def test_model_checking_jani_dtmc(self):
jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani"))
@ -41,7 +40,7 @@ class TestModelChecking:
initial_state = model.initial_states[0] initial_state = model.initial_states[0]
assert initial_state == 0 assert initial_state == 0
result = stormpy.model_checking(model, formula) result = stormpy.model_checking(model, formula)
assert math.isclose(result.at(initial_state), 0.16666666666666663)
assert math.isclose(result.at(initial_state), 1 / 6)
def test_model_checking_jani_dtmc(self): def test_model_checking_jani_dtmc(self):
jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani"))
@ -66,10 +65,10 @@ class TestModelChecking:
initial_state = model.initial_states[0] initial_state = model.initial_states[0]
assert initial_state == 0 assert initial_state == 0
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert math.isclose(result.at(initial_state), 0.16666666666666663)
assert math.isclose(result.at(initial_state), 1 / 6)
formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program)
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert math.isclose(result.at(initial_state), 0.16666666666666663)
assert math.isclose(result.at(initial_state), 1 / 6)
def test_model_checking_all_dtmc(self): def test_model_checking_all_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
@ -79,7 +78,7 @@ class TestModelChecking:
assert model.nr_transitions == 20 assert model.nr_transitions == 20
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result.result_for_all_states assert result.result_for_all_states
reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0]
reference = [1 / 6, 1 / 3, 0, 2 / 3, 0, 0, 0, 1, 0, 0, 0, 0, 0]
assert all(map(math.isclose, result.get_values(), reference)) assert all(map(math.isclose, result.get_values(), reference))
def test_model_checking_only_initial(self): def test_model_checking_only_initial(self):
@ -91,7 +90,7 @@ class TestModelChecking:
assert initial_state == 0 assert initial_state == 0
result = stormpy.model_checking(model, formulas[0], only_initial_states=True) result = stormpy.model_checking(model, formulas[0], only_initial_states=True)
assert not result.result_for_all_states assert not result.result_for_all_states
assert math.isclose(result.at(initial_state), 0.125)
assert math.isclose(result.at(initial_state), 1 / 8)
def test_model_checking_prob01(self): def test_model_checking_prob01(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
@ -147,4 +146,4 @@ class TestModelChecking:
assert type(result) is stormpy.HybridQuantitativeCheckResult assert type(result) is stormpy.HybridQuantitativeCheckResult
values = result.get_values() values = result.get_values()
assert len(values) == 3 assert len(values) == 3
assert math.isclose(values[0], 0.16666666666666663)
assert math.isclose(values[0], 1 / 6)

17
tests/pars/test_pla.py
View File

@ -44,10 +44,10 @@ class TestPLA:
assert len(parameters) == 2 assert len(parameters) == 2
region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True) result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.8369631383670559)
#result_vec = checker.get_bound_all_states(env, region, True)
#result = result_vec.at(model.initial_states[0])
#assert math.isclose(float(result.constant_part()), 0.8369631383670559)
assert math.isclose(float(result.constant_part()), 0.8369631383670559, rel_tol=1e-6)
result_vec = checker.get_bound_all_states(env, region, True)
result = result_vec.at(model.initial_states[0])
assert math.isclose(result, 0.8369631383670559, rel_tol=1e-6)
def test_pla_manual(self): def test_pla_manual(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
@ -62,7 +62,7 @@ class TestPLA:
assert len(parameters) == 2 assert len(parameters) == 2
region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True) result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.8369631383670559)
assert math.isclose(float(result.constant_part()), 0.8369631383670559, rel_tol=1e-6)
def test_pla_manual_no_simplification(self): def test_pla_manual_no_simplification(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
@ -77,7 +77,7 @@ class TestPLA:
assert len(parameters) == 2 assert len(parameters) == 2
region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result = checker.get_bound(env, region, True) result = checker.get_bound(env, region, True)
assert math.isclose(float(result.constant_part()), 0.836963056082918)
assert math.isclose(float(result.constant_part()), 0.836963056082918, rel_tol=1e-6)
def test_pla_state_bounds(self): def test_pla_state_bounds(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
@ -93,7 +93,4 @@ class TestPLA:
region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
result_vec = checker.get_bound_all_states(env, region, True) result_vec = checker.get_bound_all_states(env, region, True)
assert len(result_vec.get_values()) == model.nr_states assert len(result_vec.get_values()) == model.nr_states
assert math.isclose(result_vec.at(model.initial_states[0]), 0.836963056082918)
assert math.isclose(result_vec.at(model.initial_states[0]), 0.836963056082918, rel_tol=1e-6)
Write Preview
Loading…
Cancel
Save