Mc_CheckAGOnlySpec()
This function checks for SPEC of the form AG alpha in "context".
Mc_CheckCTLSpec()
Verifies that M,s0 |= alpha
Mc_CheckCompute()
Compute quantitative characteristics on the model.
Mc_CheckInvar()
Verifies that M,s0 |= AG alpha
Mc_CheckLanguageEmptiness()
Checks whether the language is empty
Mc_End()
Quit the mc package
Mc_Init()
Initializes the mc package.
Mc_check_psl_property()
Top-level function for mc of PSL properties
Mc_fair_si_iteration()
Mc_get_fair_si_subset()

Last updated on 2009/01/30 14h:53