You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
535 lines
23 KiB
535 lines
23 KiB
import sys
|
|
|
|
if sys.version_info[0] == 2:
|
|
raise ImportError('Python 2.x is not supported for stormpy.')
|
|
|
|
from . import core
|
|
from .core import *
|
|
from . import storage
|
|
from .storage import *
|
|
from ._config import *
|
|
from .logic import *
|
|
from .exceptions import *
|
|
|
|
from pycarl import Variable # needed for building parametric models
|
|
|
|
__version__ = "unknown"
|
|
try:
|
|
from ._version import __version__
|
|
except ImportError:
|
|
# We're running in a tree that doesn't have a _version.py, so we don't know what our version is.
|
|
pass
|
|
|
|
core._set_up("")
|
|
|
|
|
|
def _convert_sparse_model(model, parametric=False):
|
|
"""
|
|
Convert (parametric) model in sparse representation into model corresponding to exact model type.
|
|
:param model: Sparse model.
|
|
:param parametric: Flag indicating if the model is parametric.
|
|
:return: Model corresponding to exact model type.
|
|
"""
|
|
if parametric:
|
|
assert model.supports_parameters
|
|
if model.model_type == ModelType.DTMC:
|
|
return model._as_sparse_pdtmc()
|
|
elif model.model_type == ModelType.MDP:
|
|
return model._as_sparse_pmdp()
|
|
elif model.model_type == ModelType.POMDP:
|
|
return model._as_sparse_ppomdp()
|
|
elif model.model_type == ModelType.CTMC:
|
|
return model._as_sparse_pctmc()
|
|
elif model.model_type == ModelType.MA:
|
|
return model._as_sparse_pma()
|
|
else:
|
|
raise StormError("Not supported parametric model constructed")
|
|
else:
|
|
assert not model.supports_parameters
|
|
if model.model_type == ModelType.DTMC:
|
|
return model._as_sparse_dtmc()
|
|
elif model.model_type == ModelType.MDP:
|
|
return model._as_sparse_mdp()
|
|
elif model.model_type == ModelType.POMDP:
|
|
return model._as_sparse_pomdp()
|
|
elif model.model_type == ModelType.CTMC:
|
|
return model._as_sparse_ctmc()
|
|
elif model.model_type == ModelType.MA:
|
|
return model._as_sparse_ma()
|
|
else:
|
|
raise StormError("Not supported non-parametric model constructed")
|
|
|
|
|
|
def _convert_symbolic_model(model, parametric=False):
|
|
"""
|
|
Convert (parametric) model in symbolic representation into model corresponding to exact model type.
|
|
:param model: Symbolic model.
|
|
:param parametric: Flag indicating if the model is parametric.
|
|
:return: Model corresponding to exact model type.
|
|
"""
|
|
if parametric:
|
|
assert model.supports_parameters
|
|
if model.model_type == ModelType.DTMC:
|
|
return model._as_symbolic_pdtmc()
|
|
elif model.model_type == ModelType.MDP:
|
|
return model._as_symbolic_pmdp()
|
|
elif model.model_type == ModelType.CTMC:
|
|
return model._as_symbolic_pctmc()
|
|
elif model.model_type == ModelType.MA:
|
|
return model._as_symbolic_pma()
|
|
else:
|
|
raise StormError("Not supported parametric model constructed")
|
|
else:
|
|
assert not model.supports_parameters
|
|
if model.model_type == ModelType.DTMC:
|
|
return model._as_symbolic_dtmc()
|
|
elif model.model_type == ModelType.MDP:
|
|
return model._as_symbolic_mdp()
|
|
elif model.model_type == ModelType.CTMC:
|
|
return model._as_symbolic_ctmc()
|
|
elif model.model_type == ModelType.MA:
|
|
return model._as_symbolic_ma()
|
|
else:
|
|
raise StormError("Not supported non-parametric model constructed")
|
|
|
|
|
|
def build_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a model in sparse representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Model in sparse representation.
|
|
"""
|
|
return build_sparse_model(symbolic_description, properties=properties)
|
|
|
|
|
|
def build_parametric_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a parametric model in sparse representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Parametric model in sparse representation.
|
|
"""
|
|
return build_sparse_parametric_model(symbolic_description, properties=properties)
|
|
|
|
|
|
def build_sparse_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a model in sparse representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Model in sparse representation.
|
|
"""
|
|
if not symbolic_description.undefined_constants_are_graph_preserving:
|
|
raise StormError("Program still contains undefined constants")
|
|
|
|
if 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)
|
|
return _convert_sparse_model(intermediate, parametric=False)
|
|
|
|
|
|
def build_sparse_parametric_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a parametric model in sparse representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Parametric model in sparse representation.
|
|
"""
|
|
if not symbolic_description.undefined_constants_are_graph_preserving:
|
|
raise StormError("Program still contains undefined constants")
|
|
|
|
if 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)
|
|
return _convert_sparse_model(intermediate, parametric=True)
|
|
|
|
|
|
def build_symbolic_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a model in symbolic representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Model in symbolic representation.
|
|
"""
|
|
if not symbolic_description.undefined_constants_are_graph_preserving:
|
|
raise StormError("Program still contains undefined constants")
|
|
|
|
if properties:
|
|
formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
|
|
intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description, formulae)
|
|
else:
|
|
intermediate = core._build_symbolic_model_from_symbolic_description(symbolic_description)
|
|
return _convert_symbolic_model(intermediate, parametric=False)
|
|
|
|
|
|
def build_symbolic_parametric_model(symbolic_description, properties=None):
|
|
"""
|
|
Build a parametric model in symbolic representation from a symbolic description.
|
|
|
|
:param symbolic_description: Symbolic model description to translate into a model.
|
|
:param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
|
|
:return: Parametric model in symbolic representation.
|
|
"""
|
|
if not symbolic_description.undefined_constants_are_graph_preserving:
|
|
raise StormError("Program still contains undefined constants")
|
|
|
|
if 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)
|
|
return _convert_symbolic_model(intermediate, parametric=True)
|
|
|
|
|
|
def build_model_from_drn(file, options = DirectEncodingParserOptions()):
|
|
"""
|
|
Build a model in sparse representation from the explicit DRN representation.
|
|
|
|
:param String file: DRN file containing the model.
|
|
:param DirectEncodingParserOptions: Options for the parser.
|
|
:return: Model in sparse representation.
|
|
"""
|
|
intermediate = core._build_sparse_model_from_drn(file, options)
|
|
return _convert_sparse_model(intermediate, parametric=False)
|
|
|
|
|
|
def build_parametric_model_from_drn(file, options = DirectEncodingParserOptions()):
|
|
"""
|
|
Build a parametric model in sparse representation from the explicit DRN representation.
|
|
|
|
:param String file: DRN file containing the model.
|
|
:param DirectEncodingParserOptions: Options for the parser.
|
|
:return: Parametric model in sparse representation.
|
|
"""
|
|
intermediate = core._build_sparse_parametric_model_from_drn(file, options)
|
|
return _convert_sparse_model(intermediate, parametric=True)
|
|
|
|
|
|
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.
|
|
"""
|
|
return perform_sparse_bisimulation(model, properties, bisimulation_type)
|
|
|
|
|
|
def perform_sparse_bisimulation(model, properties, bisimulation_type):
|
|
"""
|
|
Perform bisimulation on model in sparse representation.
|
|
: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 if isinstance(prop, Property) else prop) for prop in properties]
|
|
if model.supports_parameters:
|
|
return core._perform_parametric_bisimulation(model, formulae, bisimulation_type)
|
|
else:
|
|
return core._perform_bisimulation(model, formulae, bisimulation_type)
|
|
|
|
|
|
def perform_symbolic_bisimulation(model, properties):
|
|
"""
|
|
Perform bisimulation on model in symbolic representation.
|
|
:param model: Model.
|
|
:param properties: Properties to preserve during bisimulation.
|
|
:return: Model after bisimulation.
|
|
"""
|
|
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)
|
|
else:
|
|
return core._perform_symbolic_bisimulation(model, formulae, bisimulation_type)
|
|
|
|
|
|
def model_checking(model, property, only_initial_states=False, extract_scheduler=False, force_fully_observable=False, environment=Environment(), shield_expression=None):
|
|
"""
|
|
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
|
|
:return: Model checking result.
|
|
:rtype: CheckResult
|
|
"""
|
|
if model.is_sparse_model:
|
|
return check_model_sparse(model, property, only_initial_states=only_initial_states,
|
|
extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment, shield_expression=shield_expression)
|
|
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, force_fully_observable=False, environment=Environment(), shield_expression=None):
|
|
"""
|
|
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
|
|
"""
|
|
if isinstance(property, Property):
|
|
formula = property.raw_formula
|
|
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)
|
|
return core._parametric_model_checking_sparse_engine(model, task, environment=environment)
|
|
else:
|
|
|
|
if model.is_exact:
|
|
task = core.ExactCheckTask(formula, only_initial_states)
|
|
task.set_produce_schedulers(extract_scheduler)
|
|
return core._exact_model_checking_sparse_engine(model, task, environment=environment)
|
|
else:
|
|
task = core.CheckTask(formula, only_initial_states)
|
|
task.set_produce_schedulers(extract_scheduler)
|
|
|
|
if shield_expression is not None:
|
|
task.set_shielding_expression(shield_expression)
|
|
|
|
return core._model_checking_sparse_engine(model, task, environment=environment)
|
|
|
|
|
|
def check_model_dd(model, property, only_initial_states=False, environment=Environment()):
|
|
"""
|
|
Perform model checking using dd engine.
|
|
: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.
|
|
:return: Model checking result.
|
|
:rtype: CheckResult
|
|
"""
|
|
if isinstance(property, Property):
|
|
formula = property.raw_formula
|
|
else:
|
|
formula = property
|
|
|
|
if model.supports_parameters:
|
|
task = core.ParametricCheckTask(formula, only_initial_states)
|
|
return core._parametric_model_checking_dd_engine(model, task, environment=environment)
|
|
else:
|
|
task = core.CheckTask(formula, only_initial_states)
|
|
return core._model_checking_dd_engine(model, task, environment=environment)
|
|
|
|
|
|
def check_model_hybrid(model, property, only_initial_states=False, environment=Environment()):
|
|
"""
|
|
Perform model checking using hybrid engine.
|
|
: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.
|
|
:return: Model checking result.
|
|
:rtype: CheckResult
|
|
"""
|
|
if isinstance(property, Property):
|
|
formula = property.raw_formula
|
|
else:
|
|
formula = property
|
|
|
|
if model.supports_parameters:
|
|
task = core.ParametricCheckTask(formula, only_initial_states)
|
|
return core._parametric_model_checking_hybrid_engine(model, task, environment=environment)
|
|
else:
|
|
task = core.CheckTask(formula, only_initial_states)
|
|
return core._model_checking_hybrid_engine(model, task, environment=environment)
|
|
|
|
|
|
def transform_to_sparse_model(model):
|
|
"""
|
|
Transform model in symbolic representation into model in sparse representation.
|
|
:param model: Symbolic model.
|
|
:return: Sparse model.
|
|
"""
|
|
if model.supports_parameters:
|
|
return core._transform_to_sparse_parametric_model(model)
|
|
else:
|
|
return core._transform_to_sparse_model(model)
|
|
|
|
|
|
def transform_to_discrete_time_model(model, properties):
|
|
"""
|
|
Transform continuous-time model to discrete time model.
|
|
:param model: Continuous-time model.
|
|
:param properties: List of properties to transform as well.
|
|
:return: Tuple (Discrete-time model, converted properties).
|
|
"""
|
|
formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
|
|
if model.supports_parameters:
|
|
return core._transform_to_discrete_time_parametric_model(model, formulae)
|
|
else:
|
|
return core._transform_to_discrete_time_model(model, formulae)
|
|
|
|
|
|
def eliminate_non_markovian_chains(ma, properties, label_behavior):
|
|
"""
|
|
Eliminate chains of non-Markovian states if possible.
|
|
:param ma: Markov automaton.
|
|
:param properties: List of properties to transform as well.
|
|
:param label_behavior: Behavior of labels while elimination.
|
|
:return: Tuple (converted MA, converted properties).
|
|
"""
|
|
formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
|
|
if ma.supports_parameters:
|
|
return core._eliminate_non_markovian_chains_parametric(ma, formulae, label_behavior)
|
|
else:
|
|
return core._eliminate_non_markovian_chains(ma, formulae, label_behavior)
|
|
|
|
|
|
def prob01min_states(model, eventually_formula):
|
|
assert type(eventually_formula) == logic.EventuallyFormula
|
|
labelform = eventually_formula.subformula
|
|
labelprop = core.Property("label-prop", labelform)
|
|
phiStates = BitVector(model.nr_states, True)
|
|
psiStates = model_checking(model, labelprop).get_truth_values()
|
|
return compute_prob01min_states(model, phiStates, psiStates)
|
|
|
|
|
|
def prob01max_states(model, eventually_formula):
|
|
assert type(eventually_formula) == logic.EventuallyFormula
|
|
labelform = eventually_formula.subformula
|
|
labelprop = core.Property("label-prop", labelform)
|
|
phiStates = BitVector(model.nr_states, True)
|
|
psiStates = model_checking(model, labelprop).get_truth_values()
|
|
return compute_prob01min_states(model, phiStates, psiStates)
|
|
|
|
|
|
def compute_prob01_states(model, phi_states, psi_states):
|
|
"""
|
|
Compute prob01 states for properties of the form phi_states until psi_states
|
|
|
|
:param SparseDTMC model:
|
|
:param BitVector phi_states:
|
|
:param BitVector psi_states: Target states
|
|
"""
|
|
if model.model_type != ModelType.DTMC:
|
|
raise StormError("Prob 01 is only defined for DTMCs -- model must be a DTMC")
|
|
|
|
if model.supports_parameters:
|
|
return core._compute_prob01states_rationalfunc(model, phi_states, psi_states)
|
|
else:
|
|
return core._compute_prob01states_double(model, phi_states, psi_states)
|
|
|
|
|
|
def compute_prob01min_states(model, phi_states, psi_states):
|
|
if model.model_type == ModelType.DTMC:
|
|
return compute_prob01_states(model, phi_states, psi_states)
|
|
if model.supports_parameters:
|
|
return core._compute_prob01states_min_rationalfunc(model, phi_states, psi_states)
|
|
else:
|
|
return core._compute_prob01states_min_double(model, phi_states, psi_states)
|
|
|
|
|
|
def compute_prob01max_states(model, phi_states, psi_states):
|
|
if model.model_type == ModelType.DTMC:
|
|
return compute_prob01_states(model, phi_states, psi_states)
|
|
if model.supports_parameters:
|
|
return core._compute_prob01states_max_rationalfunc(model, phi_states, psi_states)
|
|
else:
|
|
return core._compute_prob01states_max_double(model, phi_states, psi_states)
|
|
|
|
|
|
def topological_sort(model, forward=True, initial=[]):
|
|
"""
|
|
|
|
:param model:
|
|
:param forward:
|
|
:return:
|
|
"""
|
|
matrix = model.transition_matrix if forward else model.backward_transition_matrix
|
|
if isinstance(model, storage._SparseParametricModel):
|
|
return storage._topological_sort_rf(matrix, initial)
|
|
elif isinstance(model, storage._SparseModel):
|
|
return storage._topological_sort_double(matrix, initial)
|
|
else:
|
|
raise StormError("Unknown kind of model.")
|
|
|
|
|
|
def construct_submodel(model, states, actions, keep_unreachable_states=True, options=SubsystemBuilderOptions()):
|
|
"""
|
|
|
|
:param model: The model
|
|
:param states: Which states should be preserved
|
|
:param actions: Which actions should be preserved
|
|
:param keep_unreachable_states: If False, run a reachability analysis.
|
|
:return: A model with fewer states/actions
|
|
"""
|
|
if isinstance(model, storage._SparseModel):
|
|
return core._construct_subsystem_double(model, states, actions, keep_unreachable_states, options)
|
|
else:
|
|
raise NotImplementedError()
|
|
|
|
|
|
def parse_properties(properties, context=None, filters=None):
|
|
"""
|
|
|
|
:param properties: A string with the pctl properties
|
|
:param context: A symbolic model that gives meaning to variables and constants.
|
|
:param filters: filters, if applicable.
|
|
:return: A list of properties
|
|
"""
|
|
if context is None:
|
|
return core.parse_properties_without_context(properties, filters)
|
|
elif type(context) == core.SymbolicModelDescription:
|
|
if context.is_prism_program():
|
|
return core.parse_properties_for_prism_program(properties, context.as_prism_program(), filters)
|
|
else:
|
|
core.parse_properties_for_jani_program(properties, context.as_jani_model(), filters)
|
|
elif type(context) == storage.PrismProgram:
|
|
return core.parse_properties_for_prism_program(properties, context, filters)
|
|
elif type(context) == storage.JaniModel:
|
|
core.parse_properties_for_jani_model(properties, context, filters)
|
|
else:
|
|
raise StormError("Unclear context. Please pass a symbolic model description")
|
|
|
|
def export_to_drn(model, file, options=DirectEncodingOptions()):
|
|
"""
|
|
Export a model to DRN format
|
|
:param model: The model
|
|
:param file: A path
|
|
:param options: DirectEncodingOptions
|
|
:return:
|
|
"""
|
|
if model.supports_parameters:
|
|
return core._export_parametric_to_drn(model, file, options)
|
|
if model.is_exact:
|
|
return core._export_exact_to_drn(model, file, options)
|
|
return core._export_to_drn(model, file, options)
|