From 64ec557309e1fce6bad7bc9c11f50b1ac387db1e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 2 Dec 2019 17:37:04 +0100 Subject: [PATCH] stormpy.model_checking(...) now supports both sparse and dd based models. --- lib/stormpy/__init__.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 5c66ad8..8445b17 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -262,8 +262,15 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler :return: Model checking result. :rtype: CheckResult """ - return check_model_sparse(model, property, only_initial_states=only_initial_states, + if model.is_sparse_model: + return check_model_sparse(model, property, only_initial_states=only_initial_states, extract_scheduler=extract_scheduler, environment=environment) + else: + assert(model.is_symbolic_model) + if extract_scheduler: + raise StormError("Model checking based on dd engine does not support extracting schedulers right now.") + return check_model_dd(model, property, only_initial_states=only_initial_states, + environment=environment) def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()):