From af5872d6336125bb84f857fd717c91c864d6a7a4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 6 Dec 2018 18:48:19 +0100 Subject: [PATCH] Fixed conversion to raw_formula for properties --- lib/stormpy/__init__.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 91607e2..6f5a652 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -125,7 +125,7 @@ def build_sparse_model(symbolic_description, properties=None): raise StormError("Program still contains undefined constants") if properties: - formulae = [prop.raw_formula for prop in properties] + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description, formulae) else: intermediate = core._build_sparse_model_from_symbolic_description(symbolic_description) @@ -144,7 +144,7 @@ def build_sparse_parametric_model(symbolic_description, properties=None): raise StormError("Program still contains undefined constants") if properties: - formulae = [prop.raw_formula for prop in properties] + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description, formulae) else: intermediate = core._build_sparse_parametric_model_from_symbolic_description(symbolic_description) @@ -182,7 +182,7 @@ def build_symbolic_parametric_model(symbolic_description, properties=None): raise StormError("Program still contains undefined constants") if properties: - formulae = [(prop.raw_formula if isinstance(property, Property) else prop) for prop in properties] + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description, formulae) else: intermediate = core._build_symbolic_parametric_model_from_symbolic_description(symbolic_description) @@ -230,7 +230,7 @@ def perform_sparse_bisimulation(model, properties, bisimulation_type): :param bisimulation_type: Type of bisimulation (weak or strong). :return: Model after bisimulation. """ - formulae = [prop.raw_formula for prop in properties] + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] if model.supports_parameters: return core._perform_parametric_bisimulation(model, formulae, bisimulation_type) else: @@ -244,7 +244,7 @@ def perform_symbolic_bisimulation(model, properties): :param properties: Properties to preserve during bisimulation. :return: Model after bisimulation. """ - formulae = [prop.raw_formula for prop in properties] + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] bisimulation_type = BisimulationType.STRONG if model.supports_parameters: return core._perform_symbolic_parametric_bisimulation(model, formulae, bisimulation_type) @@ -425,4 +425,4 @@ def construct_submodel(model, states, actions, keep_unreachable_states = True, o if isinstance(model, storage._SparseModel): return core._construct_subsystem_double(model, states, actions, keep_unreachable_states, options) else: - raise NotImplementedError() \ No newline at end of file + raise NotImplementedError()