diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index cebeaaf..356621a 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -17,18 +17,63 @@ class TestSparseModelComponents: assert not components.rate_transitions def test_build_dtmc_from_model_components(self): - program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - options = stormpy.BuilderOptions(True, True) - options.set_build_with_choice_origins() - options.set_build_state_valuations() - options.set_build_all_labels() - model = stormpy.build_sparse_model_with_options(program, options) - - components = stormpy.SparseModelComponents(transition_matrix=model.transition_matrix, - state_labeling=model.labeling, - reward_models=model.reward_models) - components.choice_origins = model.choice_origins - components.state_valuations = model.state_valuations + nr_states = 13 + + # TransitionMatrix + builder = stormpy.SparseMatrixBuilder(rows = 0, columns = 0, entries = 0, force_dimensions = False, has_custom_row_grouping = False, row_groups = 0) + + # Add transitions + builder.add_next_value(0, 1, 0.5) + builder.add_next_value(0, 2, 0.5) + builder.add_next_value(1, 3, 0.5) + builder.add_next_value(1, 4, 0.5) + builder.add_next_value(2, 5, 0.5) + builder.add_next_value(2, 6, 0.5) + builder.add_next_value(3, 7, 0.5) + builder.add_next_value(3, 1, 0.5) + builder.add_next_value(4, 8, 0.5) + builder.add_next_value(4, 9, 0.5) + builder.add_next_value(5, 10, 0.5) + builder.add_next_value(5, 11, 0.5) + builder.add_next_value(6, 2, 0.5) + builder.add_next_value(6, 12, 0.5) + for s in range(7,13): + builder.add_next_value(s, s, 1) + + # Build transition matrix, update number of rows and columns + transition_matrix = builder.build(nr_states, nr_states) + + + # StateLabeling + state_labeling = stormpy.storage.StateLabeling(nr_states) + labels = {'init','one', 'two', 'three', 'four', 'five', 'six', 'done', 'deadlock'} + for label in labels: + state_labeling.add_label(label) + # Add label to one state + state_labeling.add_label_to_state('init', 0) + state_labeling.add_label_to_state('one', 7) + state_labeling.add_label_to_state('two', 8) + state_labeling.add_label_to_state('three', 9) + state_labeling.add_label_to_state('four', 10) + state_labeling.add_label_to_state('five', 11) + state_labeling.add_label_to_state('six', 12) + + # Set the labeling of states given in a bit vector, where length = nr_states + state_labeling.set_states('done', stormpy.BitVector(nr_states, [7, 8, 9, 10, 11, 12])) + + # RewardModels + reward_models = {} + # Create a vector representing the state-action rewards + action_reward = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0] + reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector = action_reward) + + + components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, + state_labeling=state_labeling, + reward_models=reward_models) + + # todo components.choice_origins = choice_origins + # todo components.state_valuations = state_valuations dtmc = stormpy.storage.SparseDtmc(components) @@ -39,8 +84,7 @@ class TestSparseModelComponents: assert dtmc.nr_choices == 13 assert dtmc.nr_states == 13 assert dtmc.nr_transitions == 20 - assert dtmc.transition_matrix.nr_entries == 20 - assert dtmc.transition_matrix.nr_entries == model.nr_transitions + assert dtmc.transition_matrix.nr_entries == dtmc.nr_transitions for e in dtmc.transition_matrix: assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) for state in dtmc.states: @@ -50,17 +94,17 @@ class TestSparseModelComponents: assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'} # test reward_models - assert len(model.reward_models) == 1 - assert not model.reward_models["coin_flips"].has_state_rewards - assert model.reward_models["coin_flips"].has_state_action_rewards - for reward in model.reward_models["coin_flips"].state_action_rewards: + assert len(dtmc.reward_models) == 1 + assert not dtmc.reward_models["coin_flips"].has_state_rewards + assert dtmc.reward_models["coin_flips"].has_state_action_rewards + for reward in dtmc.reward_models["coin_flips"].state_action_rewards: assert reward == 1.0 or reward == 0.0 - assert not model.reward_models["coin_flips"].has_transition_rewards + assert not dtmc.reward_models["coin_flips"].has_transition_rewards # choice_labeling assert not dtmc.has_choice_labeling() - # state_valuations - assert dtmc.has_state_valuations() - # choice_origins - assert dtmc.has_choice_origins() - assert dtmc.choice_origins is components.choice_origins # todo correct? + # todo state_valuations + # assert dtmc.has_state_valuations() + # todo choice_origins + # assert dtmc.has_choice_origins() + # assert dtmc.choice_origins is components.choice_origins # todo