The source code and dockerfile for the GSW2024 AI Lab.
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.
This repo is archived. You can view files and clone it, but cannot push or open issues/pull-requests.
 
 
 
 
 
 

37 lines
1.7 KiB

import stormpy
import stormpy.logic
from helpers.helper import get_example_path
import pytest
class TestPrism:
def test_prism_to_jani_states(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program)
assert len(orig_properties) == 1
jani_model, new_properties = program.to_jani(orig_properties)
assert len(new_properties) == len(orig_properties)
def test_prism_to_jani_labels(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program)
assert len(orig_properties) == 1
jani_model, new_properties = program.to_jani(orig_properties)
assert len(new_properties) == len(orig_properties)
def test_prism_to_jani_repetitive(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
orig_properties = stormpy.parse_properties_for_prism_program("P=? [F \"two\"]", program)
jani_model, new_properties = program.to_jani(orig_properties)
assert len(new_properties) == len(orig_properties)
orig_properties = stormpy.parse_properties_for_prism_program("P=? [F s=7]", program)
jani_model, new_properties = program.to_jani(orig_properties, suffix = "2")
assert len(new_properties) == len(orig_properties)
def test_prism_variables(selfs):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
module = program.modules[0]
assert len(module.integer_variables) == 2
assert len(module.boolean_variables) == 0