diff --git a/examples/parametric_models/04-parametric-models.py b/examples/parametric_models/04-parametric-models.py new file mode 100644 index 0000000..7fbf8a0 --- /dev/null +++ b/examples/parametric_models/04-parametric-models.py @@ -0,0 +1,54 @@ +import stormpy +import stormpy.core + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files +import stormpy._config as config + + + +def example_parametric_models_04(): + # Check support for parameters + if not config.storm_with_pars: + print("Support parameters is missing. Try building storm-pars.") + return + + import stormpy.pars + path = stormpy.examples.files.prism_pdtmc_die + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties(formula_str, prism_program) + model = stormpy.build_parametric_model(prism_program, properties) + + # Modify + i = 0 + for state in model.states: + if state.id in model.initial_states: + print(state) + for action in state.actions: + for transition in action.transitions: + if len(transition.value().gather_variables()) > 0: + + new_var = pycarl.Variable("p{}".format(i)) + i += 1 + new_pol = stormpy.Polynomial(new_var) + pol_in_right_format = stormpy.FactorizedPolynomial(new_pol, transition.value().numerator.cache()) + + new_factorized_ratfunc = stormpy.FactorizedRationalFunction(pol_in_right_format) + transition.set_value(new_factorized_ratfunc) + + # Display + for state in model.states: + if state.id in model.initial_states: + print(state) + for action in state.actions: + for transition in action.transitions: + print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) + + +if __name__ == '__main__': + example_parametric_models_04()