Module IvcMcs

complement_of_ivc in_sys sys ivc returns the complement of ivc. The parameters in_sys and sys must be the same as the ones used to generate ivc.

separate_ivc_by_category scope ivc separates ivc into two IVCs: the first one only contains elements from the categories selected by the user, and the second one contains the remaining elements of ivc. The parameter scope should refer to the top-level system the ivc was generated from.

minimize_lustre_ast in_sys ivc ast minimizes the lustre AST ast according to the inductive validity core ivc. The parameters in_sys should be the same as the one used to generate ivc. The optional parameter valid_lustre (default: false) determine whether the generated AST must be a valid lustre program or a more concise and easily readable program.

ivc_uc in_sys sys props computes an approximation of a minimal inductive validity core for the input system in_sys and the transition system sys. Only properties props are considered. The optional parameter approximate determines whether the unsat core computed internally must be minimal or not (in any case, the resulting IVC is NOT guaranteed to be minimal).

must_set in_sys param analyze_func sys props computes the MUST set for the input system in_sys, the analysis parameter param and the transition system sys. Only properties props are considered.

ivc_ucbf in_sys param analyze_func sys props computes a minimal inductive validity core for the input system in_sys, the analysis parameter param and the transition system sys. Only properties props are considered. This function first computes an approximation of a minimal IVC, and then tries to reduce it further. Most of time, it is faster than using ivc_bf. If the optional parameter use_must_set is not None, a MUST set will be computed first and passed to the given continuation.

umivc in_sys param analyze_func sys props k cont computes all minimal inductive validity cores for the input system in_sys, the analysis parameter param and the transition system sys. Only properties props are considered. Each IVC is passed to the continuation cont as soon as it is found. The parameter k determines up to which cardinality MCSes must be computed before starting searching for IVC. A value of -1 will compute all the MCSes, and in this case the first IVC found is guaranteed to have a minimal cardinality. If the optional parameter use_must_set is not None, a MUST set will be computed first and passed to the given continuation. If stop_after is n > 0, the search will stop after n minimal IVCs being found. This function returns a couple (isComplete, ivcs) with isComplete being a boolean that indicates whether the solutions found cover all the real solutions or not (it might not be the case in case of a timeout).

complement_of_mcs in_sys sys mcs returns the complement of mcs (the complement of a MCS is a MUA). The parameters in_sys and sys must be the same as the ones used to generate mcs.

separate_mcs_by_category scope mcs separates mcs into two MCSes: the first one only contains elements from the categories selected by the user, and the second one contains the remaining elements of mcs. The parameter scope should refer to the top-level system the mcs was generated from.

mcs in_sys param analyze_func sys props all cont computes a maximal unsafe abstraction for the input system in_sys, the analysis parameter param and the transition system sys. Only properties props are considered. If all is true, all the MCSes will be computed. Each MCS is passed to the continuation cont as soon as it is found. If the optional parameter max_mcs_cardinality is n >= 0, only MCSes of cardinality greater or equal to (total_number_of_model_elements - n) will be computed. If a global initial MCS analysis has been performed, its result should be passed in initial_solution, otherwise you can omit this parameter. This function returns a couple (isComplete, mcs) with isComplete being a boolean that indicates whether the solutions found cover all the real solutions or not (it might not be the case in case of a timeout).