DtmcParameterLiftingModelChecker¶Region model checker for DTMCs
get_bound_all_states()¶Get bound
MdpParameterLiftingModelChecker¶Region model checker for MPDs
get_bound_all_states()¶Get bound
ModelInstantiator(model)¶Class for instantiating models.
instantiate(valuation)¶Instantiate model with given valuation. :param valuation: Valuation from parameter to value. :return: Instantiated model.
ModelType¶Type of the model
CTMC = ModelType.CTMC¶DTMC = ModelType.DTMC¶MA = ModelType.MA¶MDP = ModelType.MDP¶POMDP = ModelType.POMDP¶PCtmcInstantiator¶Instantiate PCTMCs to CTMCs
instantiate()¶Instantiate model with given parameter values
PDtmcInstantiator¶Instantiate PDTMCs to DTMCs
instantiate()¶Instantiate model with given parameter values
PMaInstantiator¶Instantiate PMAs to MAs
instantiate()¶Instantiate model with given parameter values
PMdpInstantiator¶Instantiate PMDPs to MDPs
instantiate()¶Instantiate model with given parameter values
ParameterRegion¶Parameter region
RegionModelChecker¶Region model checker via paramater lifting
check_region()¶Check region
get_bound()¶Get bound
get_split_suggestion()¶Get estimate
specify()¶specify arguments
RegionResult¶Types of region check results
ALLSAT = RegionResult.ALLSAT¶ALLVIOLATED = RegionResult.ALLVIOLATED¶CENTERSAT = RegionResult.CENTERSAT¶CENTERVIOLATED = RegionResult.CENTERVIOLATED¶EXISTSBOTH = RegionResult.EXISTSBOTH¶EXISTSSAT = RegionResult.EXISTSSAT¶EXISTSVIOLATED = RegionResult.EXISTSVIOLATED¶UNKNOWN = RegionResult.UNKNOWN¶RegionResultHypothesis¶Hypothesis for the result of a parameter region
ALLSAT = RegionResultHypothesis.ALLSAT¶ALLVIOLATED = RegionResultHypothesis.ALLVIOLATED¶UNKNOWN = RegionResultHypothesis.UNKNOWN¶StormError(message)¶Base class for exceptions in Storm.
create_region_checker()¶Create region checker
gather_derivatives()¶Gather all derivatives of transition probabilities
simplify_model(model, formula)¶Simplify parametric model preserving the given formula by eliminating states with constant outgoing probabilities. :param model: Model. :param formula: Formula. :return: Tuple of simplified model and simplified formula.