Skip to content

Commit

Permalink
fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
YouGuessedMyName committed Feb 22, 2025
1 parent e64ba0b commit 437f3c2
Show file tree
Hide file tree
Showing 6 changed files with 55 additions and 51 deletions.
5 changes: 3 additions & 2 deletions stormvogel/model_checking.py
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
import stormvogel.result
import stormvogel.model
import stormvogel.property_builder
import examples.monty_hall

try:
import stormpy
Expand Down Expand Up @@ -52,7 +51,9 @@ def model_checking(


if __name__ == "__main__":
mdp = examples.monty_hall.create_monty_hall_mdp()
import stormvogel.examples.monty_hall

mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

rewardmodel = mdp.add_rewards("rewardmodel")
rewardmodel.set_from_rewards_vector(list(range(67)))
Expand Down
5 changes: 3 additions & 2 deletions stormvogel/property_builder.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import stormvogel.model
import examples.monty_hall


def build_property_string_interactive(model: stormvogel.model.Model) -> str:
Expand Down Expand Up @@ -102,6 +101,8 @@ def labels() -> str:


if __name__ == "__main__":
mdp = examples.monty_hall.create_monty_hall_mdp()
import stormvogel.examples.monty_hall

mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

build_property_string_interactive(mdp)
42 changes: 22 additions & 20 deletions tests/test_mapping.py
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
import examples.monty_hall
import examples.stormpy_mdp
import stormvogel.examples.monty_hall
import stormvogel.examples.stormpy_mdp
import stormvogel.mapping
import stormvogel.model
import examples.stormpy_dtmc
import examples.die
import examples.stormpy_ctmc
import examples.stormpy_pomdp
import examples.nuclear_fusion_ctmc
import examples.monty_hall_pomdp
import examples.stormpy_ma
import examples.simple_ma
import stormvogel.examples.stormpy_dtmc
import stormvogel.examples.die
import stormvogel.examples.stormpy_ctmc
import stormvogel.examples.stormpy_pomdp
import stormvogel.examples.nuclear_fusion_ctmc
import stormvogel.examples.monty_hall_pomdp
import stormvogel.examples.stormpy_ma
import stormvogel.examples.simple_ma
from stormvogel.model import EmptyAction

try:
Expand Down Expand Up @@ -100,7 +100,7 @@ def sparse_equal(

def test_stormpy_to_stormvogel_and_back_dtmc():
# we test it for an example stormpy representation of a dtmc
stormpy_dtmc = examples.stormpy_dtmc.example_building_dtmcs_01()
stormpy_dtmc = stormvogel.examples.stormpy_dtmc.example_building_dtmcs_01()
# print(stormpy_dtmc.transition_matrix)
stormvogel_dtmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_dtmc)
# print(stormvogel_dtmc)
Expand All @@ -113,7 +113,7 @@ def test_stormpy_to_stormvogel_and_back_dtmc():

def test_stormvogel_to_stormpy_and_back_dtmc():
# we test it for the die dtmc
stormvogel_dtmc = examples.die.create_die_dtmc()
stormvogel_dtmc = stormvogel.examples.die.create_die_dtmc()

# we test if rewardmodels work:
rewardmodel = stormvogel_dtmc.add_rewards("rewardmodel")
Expand All @@ -134,7 +134,7 @@ def test_stormvogel_to_stormpy_and_back_dtmc():

def test_stormpy_to_stormvogel_and_back_mdp():
# we test it for an example stormpy representation of an mdp
stormpy_mdp = examples.stormpy_mdp.example_building_mdps_01()
stormpy_mdp = stormvogel.examples.stormpy_mdp.example_building_mdps_01()
# print(stormpy_mdp)
stormvogel_mdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_mdp)
# print(stormvogel_mdp)
Expand All @@ -147,7 +147,7 @@ def test_stormpy_to_stormvogel_and_back_mdp():

def test_stormvogel_to_stormpy_and_back_mdp():
# we test it for monty hall mdp
stormvogel_mdp = examples.monty_hall.create_monty_hall_mdp()
stormvogel_mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

# we additionally test if reward models work
rewardmodel = stormvogel_mdp.add_rewards("rewardmodel")
Expand Down Expand Up @@ -184,7 +184,9 @@ def test_stormvogel_to_stormpy_and_back_mdp():

def test_stormvogel_to_stormpy_and_back_ctmc():
# we create a stormpy representation of an example ctmc
stormvogel_ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
stormvogel_ctmc = (
stormvogel.examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
)
# print(stormvogel_ctmc)
stormpy_ctmc = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ctmc)
# print(stormpy_ctmc)
Expand All @@ -196,7 +198,7 @@ def test_stormvogel_to_stormpy_and_back_ctmc():

def test_stormpy_to_stormvogel_and_back_ctmc():
# we create a stormpy representation of an example ctmc
stormpy_ctmc = examples.stormpy_ctmc.example_building_ctmcs_01()
stormpy_ctmc = stormvogel.examples.stormpy_ctmc.example_building_ctmcs_01()
# print(stormpy_ctmc)
stormvogel_ctmc = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ctmc)
# print(stormvogel_ctmc)
Expand All @@ -209,7 +211,7 @@ def test_stormpy_to_stormvogel_and_back_ctmc():

def test_stormvogel_to_stormpy_and_back_pomdp():
# we create a stormpy representation of an example pomdp
stormvogel_pomdp = examples.monty_hall_pomdp.create_monty_hall_pomdp()
stormvogel_pomdp = stormvogel.examples.monty_hall_pomdp.create_monty_hall_pomdp()
# print(stormvogel_pomdp)
stormpy_pomdp = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_pomdp)
# print(stormpy_pomdp)
Expand All @@ -225,7 +227,7 @@ def test_stormvogel_to_stormpy_and_back_pomdp():

def test_stormpy_to_stormvogel_and_back_pomdp():
# we create a stormpy representation of an example pomdp
stormpy_pomdp = examples.stormpy_pomdp.example_building_pomdps_01()
stormpy_pomdp = stormvogel.examples.stormpy_pomdp.example_building_pomdps_01()
# print(stormpy_pomdp)
stormvogel_pomdp = stormvogel.mapping.stormpy_to_stormvogel(stormpy_pomdp)
# print(stormvogel_pomdp)
Expand All @@ -239,7 +241,7 @@ def test_stormpy_to_stormvogel_and_back_pomdp():
# TODO for some reason, this test crashes but only in Github workflows?
# def test_stormvogel_to_stormpy_and_back_ma():
# # we create a stormpy representation of an example ma
# stormvogel_ma = examples.simple_ma.create_simple_ma()
# stormvogel_ma = stormvogel.examples.simple_ma.create_simple_ma()
# # print(stormvogel_ma)
# stormpy_ma = stormvogel.mapping.stormvogel_to_stormpy(stormvogel_ma)
# # print(stormpy_ma)
Expand All @@ -251,7 +253,7 @@ def test_stormpy_to_stormvogel_and_back_pomdp():

def test_stormpy_to_stormvogel_and_back_ma():
# we create a stormpy representation of an example ma
stormpy_ma = examples.stormpy_ma.example_building_mas_01()
stormpy_ma = stormvogel.examples.stormpy_ma.example_building_mas_01()
# print(stormpy_ma)
stormvogel_ma = stormvogel.mapping.stormpy_to_stormvogel(stormpy_ma)
# print(stormvogel_ma)
Expand Down
8 changes: 4 additions & 4 deletions tests/test_model_checking.py
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
import stormvogel.model_checking
import examples.monty_hall
import examples.die
import stormvogel.examples.monty_hall
import stormvogel.examples.die

try:
import stormpy
Expand All @@ -12,7 +12,7 @@ def test_model_checking():
assert stormpy is not None

# we get our result using the stormvogel model checker function indirectly
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()
prop = 'Pmax=? [F "done"]'
result = stormvogel.model_checking.model_checking(mdp, prop, True)

Expand All @@ -31,7 +31,7 @@ def test_model_checking():
)

# now we do it for a dtmc:
dtmc = examples.die.create_die_dtmc()
dtmc = stormvogel.examples.die.create_die_dtmc()
prop = 'P=? [F "rolled1"]'
result = stormvogel.model_checking.model_checking(dtmc, prop, True)

Expand Down
26 changes: 13 additions & 13 deletions tests/test_model_methods.py
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
import stormvogel.model
import examples.monty_hall
import examples.die
import examples.nuclear_fusion_ctmc
import stormvogel.examples.monty_hall
import stormvogel.examples.die
import stormvogel.examples.nuclear_fusion_ctmc
import pytest
from typing import cast


def test_available_actions():
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

action = [
stormvogel.model.Action(labels=frozenset({"open0"})),
Expand All @@ -22,7 +22,7 @@ def test_available_actions():


def test_get_outgoing_transitions():
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

transitions = mdp.get_initial_state().get_outgoing_transitions(
stormvogel.model.EmptyAction
Expand All @@ -40,14 +40,14 @@ def test_get_outgoing_transitions():

def test_is_absorbing():
# one example of a ctmc state that is absorbing and one that isn't
ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
ctmc = stormvogel.examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
state0 = ctmc.get_state_by_id(4)
state1 = ctmc.get_state_by_id(3)
assert state0.is_absorbing()
assert not state1.is_absorbing()

# one example of a dtmc state that is absorbing and one that isn't
dtmc = examples.die.create_die_dtmc()
dtmc = stormvogel.examples.die.create_die_dtmc()
state0 = dtmc.get_initial_state()
state1 = dtmc.get_state_by_id(1)
assert state1.is_absorbing()
Expand Down Expand Up @@ -154,7 +154,7 @@ def test_normalize():

def test_remove_state():
# we make a normal ctmc and remove a state
ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
ctmc = stormvogel.examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
ctmc.remove_state(ctmc.get_state_by_id(3), reassign_ids=True)

# we make a ctmc with the state already missing
Expand Down Expand Up @@ -204,7 +204,7 @@ def test_remove_state():
assert mdp == new_mdp

# this should fail:
new_dtmc = examples.die.create_die_dtmc()
new_dtmc = stormvogel.examples.die.create_die_dtmc()
state0 = new_dtmc.get_state_by_id(0)
new_dtmc.remove_state(new_dtmc.get_initial_state(), reassign_ids=True)
state1 = new_dtmc.get_state_by_id(0)
Expand Down Expand Up @@ -331,7 +331,7 @@ def test_add_transitions():

def test_get_sub_model():
# we create the die dtmc and take a submodel
dtmc = examples.die.create_die_dtmc()
dtmc = stormvogel.examples.die.create_die_dtmc()
states = [dtmc.get_state_by_id(0), dtmc.get_state_by_id(1), dtmc.get_state_by_id(2)]
sub_model = dtmc.get_sub_model(states)

Expand All @@ -347,7 +347,7 @@ def test_get_sub_model():

def test_get_state_action_id():
# we create an mdp:
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()
state = mdp.get_state_by_id(2)
action = state.available_actions()[1]

Expand All @@ -356,7 +356,7 @@ def test_get_state_action_id():

def test_get_state_action_reward():
# we create an mdp:
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

# we add a reward model:
rewardmodel = mdp.add_rewards("rewardmodel")
Expand Down Expand Up @@ -390,7 +390,7 @@ def test_get_state_action_reward():
# assert rewardmodel == other_rewardmodel

# # we create an mdp:
# mdp = examples.monty_hall.create_monty_hall_mdp()
# mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

# # we add a reward model with only one reward
# rewardmodel = mdp.add_rewards("rewardmodel")
Expand Down
20 changes: 10 additions & 10 deletions tests/test_simulator.py
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
import examples.die
import examples.monty_hall
import examples.nuclear_fusion_ctmc
import examples.monty_hall_pomdp
import stormvogel.examples.die
import stormvogel.examples.monty_hall
import stormvogel.examples.nuclear_fusion_ctmc
import stormvogel.examples.monty_hall_pomdp
from stormvogel.model import EmptyAction
import stormvogel.model
import stormvogel.simulator


def test_simulate():
# we make a die dtmc and run the simulator with it
dtmc = examples.die.create_die_dtmc()
dtmc = stormvogel.examples.die.create_die_dtmc()
rewardmodel = dtmc.add_rewards("rewardmodel")
for stateid in dtmc.states.keys():
rewardmodel.rewards[(stateid, EmptyAction)] = 3
Expand Down Expand Up @@ -44,7 +44,7 @@ def test_simulate():
assert partial_model == other_dtmc
######################################################################################################################
# we make a monty hall mdp and run the simulator with it
mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()
rewardmodel = mdp.add_rewards("rewardmodel")
rewardmodel.set_from_rewards_vector(list(range(67)))
rewardmodel2 = mdp.add_rewards("rewardmodel2")
Expand Down Expand Up @@ -86,7 +86,7 @@ def scheduler(state: stormvogel.model.State) -> stormvogel.model.Action:
actions = state.available_actions()
return actions[0]

mdp = examples.monty_hall.create_monty_hall_mdp()
mdp = stormvogel.examples.monty_hall.create_monty_hall_mdp()

partial_model = stormvogel.simulator.simulate(
mdp, runs=1, steps=3, seed=1, scheduler=scheduler
Expand All @@ -107,7 +107,7 @@ def scheduler(state: stormvogel.model.State) -> stormvogel.model.Action:

def test_simulate_path():
# we make the nuclear fusion ctmc and run simulate path with it
ctmc = examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
ctmc = stormvogel.examples.nuclear_fusion_ctmc.create_nuclear_fusion_ctmc()
path = stormvogel.simulator.simulate_path(ctmc, steps=5, seed=1)

# we make the path that the simulate path function should create
Expand All @@ -124,7 +124,7 @@ def test_simulate_path():
assert path == other_path
##############################################################################################
# we make the monty hall pomdp and run simulate path with it
pomdp = examples.monty_hall_pomdp.create_monty_hall_pomdp()
pomdp = stormvogel.examples.monty_hall_pomdp.create_monty_hall_pomdp()
taken_actions = {}
for id, state in pomdp.states.items():
taken_actions[id] = state.available_actions()[
Expand Down Expand Up @@ -166,7 +166,7 @@ def scheduler(state: stormvogel.model.State) -> stormvogel.model.Action:
actions = state.available_actions()
return actions[0]

pomdp = examples.monty_hall_pomdp.create_monty_hall_pomdp()
pomdp = stormvogel.examples.monty_hall_pomdp.create_monty_hall_pomdp()
path = stormvogel.simulator.simulate_path(
pomdp, steps=4, seed=1, scheduler=scheduler
)
Expand Down

0 comments on commit 437f3c2

Please sign in to comment.