From 2cfa252278e85502ba61697044ab362c4b38341b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 7 Aug 2020 18:00:37 +0200 Subject: [PATCH] Fixed rounding problem in doctest --- doc/source/doc/reward_models.rst | 4 ++-- examples/reward_models/01-reward-models.py | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/source/doc/reward_models.rst b/doc/source/doc/reward_models.rst index 4e59faf..acce76c 100644 --- a/doc/source/doc/reward_models.rst +++ b/doc/source/doc/reward_models.rst @@ -28,8 +28,8 @@ We can do model checking analogous to probabilities:: >>> initial_state = model.initial_states[0] >>> result = stormpy.model_checking(model, properties[0]) - >>> print("Result: {}".format(result.at(initial_state))) - Result: 3.666666666666667 + >>> print("Result: {}".format(round(result.at(initial_state), 6))) + Result: 3.666667 The reward model has a name which we can obtain as follows:: diff --git a/examples/reward_models/01-reward-models.py b/examples/reward_models/01-reward-models.py index 1ce13dc..9eb46d4 100644 --- a/examples/reward_models/01-reward-models.py +++ b/examples/reward_models/01-reward-models.py @@ -10,11 +10,11 @@ def example_reward_models_01(): prop = "R=? [F \"done\"]" properties = stormpy.parse_properties_for_prism_program(prop, program, None) model = stormpy.build_model(program, properties) + assert len(model.reward_models) == 1 initial_state = model.initial_states[0] result = stormpy.model_checking(model, properties[0]) - print("Result: {}".format(result.at(initial_state))) + print("Result: {}".format(round(result.at(initial_state), 6))) - assert len(model.reward_models) == 1 reward_model_name = list(model.reward_models.keys())[0] print(reward_model_name) assert reward_model_name == "coin_flips" @@ -29,4 +29,4 @@ def example_reward_models_01(): assert reward_model_name == "coin_flips" if __name__ == '__main__': - example_reward_models_01() \ No newline at end of file + example_reward_models_01()