From 9919a4f309d1a216a68efa89391d2935236936b2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 25 Sep 2020 15:20:21 -0700 Subject: [PATCH] support for partially observable models, and better model-dependent creation --- lib/stormpy/__init__.py | 23 ++++++++++++++++++++--- lib/stormpy/pomdp/__init__.py | 28 +++++++++++++++++++++++++++- src/storage/model.cpp | 1 + 3 files changed, 48 insertions(+), 4 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 9aae889..90a5f3c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -256,7 +256,7 @@ def perform_symbolic_bisimulation(model, properties): return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type) -def model_checking(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()): +def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()): """ Perform model checking on model for property. :param model: Model. @@ -268,7 +268,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler """ if model.is_sparse_model: return check_model_sparse(model, property, only_initial_states=only_initial_states, - extract_scheduler=extract_scheduler, environment=environment) + extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment) else: assert (model.is_symbolic_model) if extract_scheduler: @@ -277,13 +277,14 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler environment=environment) -def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, environment=Environment()): +def check_model_sparse(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment()): """ Perform model checking on model for property. :param model: Model. :param property: Property to check for. :param only_initial_states: If True, only results for initial states are computed, otherwise for all states. :param extract_scheduler: If True, try to extract a scheduler + :param force_fully_observable: If True, treat a POMDP as an MDP :return: Model checking result. :rtype: CheckResult """ @@ -292,6 +293,22 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched else: formula = property + if force_fully_observable: + if model.is_partially_observable: + # Note that casting a model to a fully observable model wont work with python/pybind, so we actually have other access points + if model.supports_parameters: + raise NotImplementedError("") + elif model.is_exact: + task = core.ExactCheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) + return core._exact_model_checking_fully_observable(model, task, environment=environment) + else: + task = core.CheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) + return core._model_checking_fully_observable(model, task, environment=environment) + else: + raise RuntimeError("Forcing models that are fully observable is not possible") + if model.supports_parameters: task = core.ParametricCheckTask(formula, only_initial_states) task.set_produce_schedulers(extract_scheduler) diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index 8f93f3e..a258c1c 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -42,4 +42,30 @@ def apply_unknown_fsc(model, mode): if model.supports_parameters: return pomdp._apply_unknown_fsc_Rf(model, mode) else: - return pomdp._apply_unknown_fsc_Double(model, mode) \ No newline at end of file + return pomdp._apply_unknown_fsc_Double(model, mode) + + +def create_nondeterminstic_belief_tracker(model): + """ + + :param model: A POMDP + :return: + """ + if model.is_exact: + return pomdp.NondeterministicBeliefTrackerExactSparse(model) + else: + return pomdp.NondeterministicBeliefTrackerDoubleSparse(model) + + +def create_observation_trace_unfolder(model, risk_assessment, expr_manager): + """ + + :param model: + :param risk_assessment: + :param expr_manager: + :return: + """ + if model.is_exact: + return pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager) + else: + return pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager) \ No newline at end of file diff --git a/src/storage/model.cpp b/src/storage/model.cpp index dee8661..cf955df 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -108,6 +108,7 @@ void define_model(py::module& m) { .def_property_readonly("supports_parameters", &ModelBase::supportsParameters, "Flag whether model supports parameters") .def_property_readonly("has_parameters", &ModelBase::hasParameters, "Flag whether model has parameters") .def_property_readonly("is_exact", &ModelBase::isExact, "Flag whether model is exact") + .def_property_readonly("is_partially_observable", &ModelBase::isPartiallyObservable, "Flag whether the model has observation labels") .def_property_readonly("is_sparse_model", &ModelBase::isSparseModel, "Flag whether the model is stored as a sparse model") .def_property_readonly("is_symbolic_model", &ModelBase::isSymbolicModel, "Flag whether the model is stored using decision diagrams") .def_property_readonly("is_discrete_time_model", &ModelBase::isDiscreteTimeModel, "Flag whether the model is a discrete time model")