|
@ -11,6 +11,36 @@ from stormpy import ModelType, StormError |
|
|
pars._set_up() |
|
|
pars._set_up() |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class ModelInstantiator: |
|
|
|
|
|
""" |
|
|
|
|
|
Class for instantiating models. |
|
|
|
|
|
""" |
|
|
|
|
|
|
|
|
|
|
|
def __init__(self, model): |
|
|
|
|
|
""" |
|
|
|
|
|
Constructor. |
|
|
|
|
|
:param model: Model. |
|
|
|
|
|
""" |
|
|
|
|
|
if model.model_type == ModelType.MDP: |
|
|
|
|
|
self._instantiator = PMdpInstantiator(model) |
|
|
|
|
|
elif model.model_type == ModelType.DTMC: |
|
|
|
|
|
self._instantiator = PDtmcInstantiator(model) |
|
|
|
|
|
elif model.model_type == ModelType.CTMC: |
|
|
|
|
|
self._instantiator = PCtmcInstantiator(model) |
|
|
|
|
|
elif model.model_type == ModelType.MA: |
|
|
|
|
|
self._instantiator = PMaInstantiator(model) |
|
|
|
|
|
else: |
|
|
|
|
|
raise StormError("Model type {} not supported".format(model.model_type)) |
|
|
|
|
|
|
|
|
|
|
|
def instantiate(self, valuation): |
|
|
|
|
|
""" |
|
|
|
|
|
Instantiate model with given valuation. |
|
|
|
|
|
:param valuation: Valuation from parameter to value. |
|
|
|
|
|
:return: Instantiated model. |
|
|
|
|
|
""" |
|
|
|
|
|
return self._instantiator.instantiate(valuation) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
def simplify_model(model, formula): |
|
|
def simplify_model(model, formula): |
|
|
""" |
|
|
""" |
|
|
Simplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities. |
|
|
Simplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities. |
|
|