diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 28634cd..5c6d212 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -108,6 +108,13 @@ def build_parametric_model_from_drn(file): def perform_bisimulation(model, properties, bisimulation_type): + """ + Perform bisimulation on model. + :param model: Model. + :param properties: Properties to preserve during bisimulation. + :param bisimulation_type: Type of bisimulation (weak or strong). + :return: Model after bisimulation. + """ formulae = [prop.raw_formula for prop in properties] if model.supports_parameters: return core._perform_parametric_bisimulation(model, formulae, bisimulation_type) @@ -116,6 +123,13 @@ def perform_bisimulation(model, properties, bisimulation_type): def model_checking(model, property): + """ + Perform model checking on model for property. + :param model: Model. + :param property: Property to check for. + :return: Model checking result. + :rtype: CheckResult + """ if model.supports_parameters: task = core.ParametricCheckTask(property.raw_formula, False) return core._parametric_model_checking_sparse_engine(model, task) diff --git a/lib/stormpy/examples/__init__.py b/lib/stormpy/examples/__init__.py index e69de29..94456ab 100644 --- a/lib/stormpy/examples/__init__.py +++ b/lib/stormpy/examples/__init__.py @@ -0,0 +1 @@ +# intentionally left blank diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index f825f91..0dffe66 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -4,7 +4,12 @@ testfile_dir = os.path.join(os.path.dirname(os.path.abspath(__file__)), "files") def _path(folder, file): - """Internal method for simpler listing of examples""" + """ + Internal method for simpler listing of examples. + :param folder: Folder. + :param file: Example file. + :return: Complete path to example file. + """ return os.path.join(testfile_dir, folder, file) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 08aeb77..a258a89 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,8 +1,17 @@ from . import storage from .storage import * + 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: @@ -14,5 +23,10 @@ class ModelInstantiator: else: raise ValueError("Model type {} not supported".format(model.model_type)) - def instantiate(self, point): - return self._instantiator.instantiate(point) + def instantiate(self, valuation): + """ + Instantiate model with given valuation. + :param valuation: Valuation from parameter to value. + :return: Instantiated model. + """ + return self._instantiator.instantiate(valuation) diff --git a/lib/stormpy/utility/__init__.py b/lib/stormpy/utility/__init__.py index bdc2591..3bdf0e7 100644 --- a/lib/stormpy/utility/__init__.py +++ b/lib/stormpy/utility/__init__.py @@ -1,2 +1,2 @@ from . import utility -from .utility import * \ No newline at end of file +from .utility import *