You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

135 lines
6.6 KiB

8 years ago
8 years ago
8 years ago
8 years ago
  1. import stormpy
  2. import stormpy.logic
  3. from helpers.helper import get_example_path
  4. import pytest
  5. class TestModel:
  6. def test_build_dtmc_from_prism_program(self):
  7. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  8. model = stormpy.build_model(program)
  9. assert model.nr_states == 13
  10. assert model.nr_transitions == 20
  11. assert model.model_type == stormpy.ModelType.DTMC
  12. assert not model.supports_parameters
  13. assert type(model) is stormpy.SparseDtmc
  14. def test_build_dtmc_from_prism_program_formulas(self):
  15. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  16. prop = "P=? [F \"one\"]"
  17. properties = stormpy.parse_properties_for_prism_program(prop, program, None)
  18. model = stormpy.build_model(program, properties)
  19. assert model.nr_states == 13
  20. assert model.nr_transitions == 20
  21. assert model.model_type == stormpy.ModelType.DTMC
  22. assert len(model.reward_models) == 0
  23. assert not model.supports_parameters
  24. assert type(model) is stormpy.SparseDtmc
  25. def test_build_dtmc_from_prism_program_formulas(self):
  26. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  27. prop = "R=? [F \"done\"]"
  28. properties = stormpy.parse_properties_for_prism_program(prop, program, None)
  29. model = stormpy.build_model(program, properties)
  30. assert model.nr_states == 13
  31. assert model.nr_transitions == 20
  32. assert model.model_type == stormpy.ModelType.DTMC
  33. assert len(model.reward_models) == 1
  34. assert not model.reward_models["coin_flips"].has_state_rewards
  35. assert model.reward_models["coin_flips"].has_state_action_rewards
  36. for reward in model.reward_models["coin_flips"].state_action_rewards:
  37. assert reward == 1.0 or reward == 0.0
  38. assert not model.reward_models["coin_flips"].has_transition_rewards
  39. assert not model.supports_parameters
  40. assert type(model) is stormpy.SparseDtmc
  41. def test_reduce_to_state_based_rewards(self):
  42. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  43. prop = "R=? [F \"done\"]"
  44. properties = stormpy.parse_properties_for_prism_program(prop, program, None)
  45. model = stormpy.build_model(program, properties)
  46. model.reduce_to_state_based_rewards()
  47. assert len(model.reward_models) == 1
  48. assert model.reward_models["coin_flips"].has_state_rewards
  49. assert not model.reward_models["coin_flips"].has_state_action_rewards
  50. for reward in model.reward_models["coin_flips"].state_rewards:
  51. assert reward == 1.0 or reward == 0.0
  52. assert not model.reward_models["coin_flips"].has_transition_rewards
  53. def test_build_dtmc_from_jani_model(self):
  54. jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani"))
  55. model = stormpy.build_model(jani_model)
  56. assert model.nr_states == 13
  57. assert model.nr_transitions == 20
  58. assert model.model_type == stormpy.ModelType.DTMC
  59. assert not model.supports_parameters
  60. assert type(model) is stormpy.SparseDtmc
  61. def test_build_dtmc(self):
  62. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  63. formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)
  64. model = stormpy.build_model(program, formulas)
  65. assert model.nr_states == 13
  66. assert model.nr_transitions == 20
  67. assert model.model_type == stormpy.ModelType.DTMC
  68. assert not model.supports_parameters
  69. assert type(model) is stormpy.SparseDtmc
  70. def test_build_dtmc_with_undefined_constants(self):
  71. jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani"))
  72. assert jani_model.has_undefined_constants
  73. assert not jani_model.undefined_constants_are_graph_preserving
  74. with pytest.raises(stormpy.StormError):
  75. model = stormpy.build_model(jani_model)
  76. def test_build_instantiated_dtmc(self):
  77. jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani"))
  78. assert jani_model.has_undefined_constants
  79. assert not jani_model.undefined_constants_are_graph_preserving
  80. description = stormpy.SymbolicModelDescription(jani_model)
  81. constant_definitions = description.parse_constant_definitions("N=16, MAX=2")
  82. instantiated_jani_model = description.instantiate_constants(constant_definitions).as_jani_model()
  83. model = stormpy.build_model(instantiated_jani_model)
  84. assert model.nr_states == 677
  85. assert model.nr_transitions == 867
  86. assert model.model_type == stormpy.ModelType.DTMC
  87. assert not model.supports_parameters
  88. assert type(model) is stormpy.SparseDtmc
  89. def test_build_mdp(self):
  90. program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm"))
  91. formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program)
  92. model = stormpy.build_model(program, formulas)
  93. assert model.nr_states == 169
  94. assert model.nr_transitions == 435
  95. assert model.model_type == stormpy.ModelType.MDP
  96. assert not model.supports_parameters
  97. assert type(model) is stormpy.SparseMdp
  98. def test_build_ctmc(self):
  99. program = stormpy.parse_prism_program(get_example_path("ctmc", "polling2.sm"), True)
  100. formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program)
  101. model = stormpy.build_model(program, formulas)
  102. assert model.nr_states == 12
  103. assert model.nr_transitions == 22
  104. assert model.model_type == stormpy.ModelType.CTMC
  105. assert not model.supports_parameters
  106. assert type(model) is stormpy.SparseCtmc
  107. def test_build_ma(self):
  108. program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"))
  109. formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=2 s=2 ]", program)
  110. model = stormpy.build_model(program, formulas)
  111. assert model.nr_states == 5
  112. assert model.nr_transitions == 8
  113. assert model.model_type == stormpy.ModelType.MA
  114. assert not model.supports_parameters
  115. assert type(model) is stormpy.SparseMA
  116. def test_initial_states(self):
  117. program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
  118. formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)
  119. model = stormpy.build_model(program, formulas)
  120. initial_states = model.initial_states
  121. assert len(initial_states) == 1
  122. assert 0 in initial_states