|
@ -1,5 +1,6 @@ |
|
|
import stormpy |
|
|
import stormpy |
|
|
import stormpy.logic |
|
|
import stormpy.logic |
|
|
|
|
|
from helpers.helper import get_example_path |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class TestFormulas: |
|
|
class TestFormulas: |
|
@ -30,6 +31,12 @@ class TestFormulas: |
|
|
assert str(formulas[0]) == "P" + prop |
|
|
assert str(formulas[0]) == "P" + prop |
|
|
assert str(formulas[1]) == "R[exp]" + prop |
|
|
assert str(formulas[1]) == "R[exp]" + prop |
|
|
|
|
|
|
|
|
|
|
|
def test_jani_formula(self): |
|
|
|
|
|
_, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) |
|
|
|
|
|
for name, prop in properties.items(): |
|
|
|
|
|
assert "Property_brp_" in name |
|
|
|
|
|
assert isinstance(prop, stormpy.Property) |
|
|
|
|
|
|
|
|
def test_bounds(self): |
|
|
def test_bounds(self): |
|
|
prop = "P=? [F \"one\"]" |
|
|
prop = "P=? [F \"one\"]" |
|
|
formula = stormpy.parse_properties(prop)[0].raw_formula |
|
|
formula = stormpy.parse_properties(prop)[0].raw_formula |
|
|