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
PDtmcInstantiationChecker¶Instantiate pDTMCs to DTMCs and immediately check
check()¶set_graph_preserving()¶PDtmcInstantiator¶Instantiate PDTMCs to DTMCs
instantiate()¶Instantiate model with given parameter values
PMaInstantiator¶Instantiate PMAs to MAs
instantiate()¶Instantiate model with given parameter values
PMdpInstantiationChecker¶Instantiate PMDP to MDPs and immediately check
check()¶set_graph_preserving()¶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.