Skip to content

Commit

Permalink
stormpy is now also optional in the tests
Browse files Browse the repository at this point in the history
  • Loading branch information
PimLeerkes committed Feb 18, 2025
1 parent 2603a0b commit b7e7b8c
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 13 deletions.
5 changes: 2 additions & 3 deletions stormvogel/result.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@

try:
import stormpy

stormpy_installed = True
except ImportError:
stormpy_installed = False
stormpy = None


class Scheduler:
Expand Down Expand Up @@ -148,6 +146,7 @@ def convert_model_checking_result(
"""
Takes a model checking result from stormpy and its associated model and converts it to a stormvogel representation
"""
assert stormpy is not None

if (
type(stormpy_result) == stormpy.core.ExplicitQuantitativeCheckResult
Expand Down
3 changes: 0 additions & 3 deletions stormvogel/simulator.py
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,8 @@

try:
import stormpy.simulator

stormpy_installed = True
except ImportError:
stormpy = None
stormpy_installed = False


class Path:
Expand Down
7 changes: 5 additions & 2 deletions tests/test_mapping.py
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,10 @@
import examples.simple_ma
from stormvogel.model import EmptyAction


import stormpy.storage
try:
import stormpy
except ImportError:
stormpy = None


def sparse_equal(
Expand All @@ -24,6 +26,7 @@ def sparse_equal(
outputs true if the sparse models are the same and false otherwise
Note: this function is only here because the equality functions in storm do not work currently.
"""
assert stormpy is not None

# check if states are the same:
states_equal = True
Expand Down
8 changes: 5 additions & 3 deletions tests/test_model_checking.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,14 @@
import examples.monty_hall
import examples.die


import stormpy
try:
import stormpy
except ImportError:
stormpy = None


def test_model_checking():
# TODO this test is maybe too trivial?
assert stormpy is not None

# we get our result using the stormvogel model checker function indirectly
mdp = examples.monty_hall.create_monty_hall_mdp()
Expand Down
10 changes: 8 additions & 2 deletions tests/test_result.py
Original file line number Diff line number Diff line change
@@ -1,11 +1,14 @@
import stormvogel.result
import pytest


import stormpy
try:
import stormpy
except ImportError:
stormpy = None


def test_convert_model_checker_results_dtmc():
assert stormpy is not None
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P=? [F s=7 & d=2]"
Expand Down Expand Up @@ -38,6 +41,7 @@ def test_convert_model_checker_results_dtmc():


def test_convert_model_checker_results_dtmc_qualitative():
assert stormpy is not None
path = stormpy.examples.files.prism_dtmc_die
prism_program = stormpy.parse_prism_program(path)
formula_str = "P>=0.5 [F s=7 & d=2]"
Expand Down Expand Up @@ -71,6 +75,7 @@ def test_convert_model_checker_results_dtmc_qualitative():


def test_convert_model_checker_results_mdp():
assert stormpy is not None
path = stormpy.examples.files.prism_mdp_coin_2_2

prism_program = stormpy.parse_prism_program(path)
Expand Down Expand Up @@ -643,6 +648,7 @@ def test_convert_model_checker_results_mdp():


def test_convert_model_checker_results_mdp_qualitative():
assert stormpy is not None
path = stormpy.examples.files.prism_mdp_coin_2_2

prism_program = stormpy.parse_prism_program(path)
Expand Down

0 comments on commit b7e7b8c

Please sign in to comment.