tempestpy/examples/schedulers/01-schedulers.py

import stormpy
import stormpy.core

import stormpy.examples
import stormpy.examples.files


def example_schedulers_01():
    path = stormpy.examples.files.prism_mdp_coin_2_2

    formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]"

    program = stormpy.parse_prism_program(path)
    formulas = stormpy.parse_properties_for_prism_program(formula_str, program)
    model = stormpy.build_model(program, formulas)
    initial_state = model.initial_states[0]
    assert initial_state == 0
    result = stormpy.model_checking(model, formulas[0], extract_scheduler = True)
    assert result.has_scheduler
    print(result.scheduler)
    assert result.scheduler.memoryless
    assert result.scheduler.deterministic

    for i in range(0,model.nr_states):
        print("In state {} choose action {}".format(i,result.scheduler.get_choice(i).get_deterministic_choice()))



if __name__ == '__main__':
    example_schedulers_01()