From 06e397f9f97c1b0e668bd1b538e9f50a89359c94 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 10 Aug 2017 10:54:19 +0200 Subject: [PATCH] support model checking from formulas (instead of just from properties) --- lib/stormpy/__init__.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 04471f1..630001c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -137,11 +137,16 @@ def model_checking(model, property): :return: Model checking result. :rtype: CheckResult """ + if isinstance(property, Property): + formula = property.raw_formula + else: + formula = property + if model.supports_parameters: - task = core.ParametricCheckTask(property.raw_formula, False) + task = core.ParametricCheckTask(formula, False) return core._parametric_model_checking_sparse_engine(model, task) else: - task = core.CheckTask(property.raw_formula, False) + task = core.CheckTask(formula, False) return core._model_checking_sparse_engine(model, task)