====================================== F_MC_CLIENT (invariant admissibility) Successfully verified. ====================================== ANY.default_create (creator, inherited by F_MC_CLIENT) Successfully verified. ====================================== F_MC_CLIENT.test Successfully verified. ====================================== F_MC_CLIENT.test_d Successfully verified. ====================================== F_MC_CLOCK (invariant admissibility) Successfully verified. ====================================== F_MC_CLOCK.make (creator) Successfully verified. ====================================== F_MC_CLOCK.sync Successfully verified. ====================================== F_MC_CLOCK_D (invariant admissibility) Successfully verified. ====================================== F_MC_CLOCK_D.make (creator) Successfully verified. ====================================== F_MC_CLOCK_D.sync Successfully verified. ====================================== F_MC_MASTER (invariant admissibility) Successfully verified. ====================================== F_MC_MASTER.make (creator) Successfully verified. ====================================== F_MC_MASTER.tick Successfully verified. ====================================== F_MC_MASTER.reset Successfully verified. ====================================== F_MC_MASTER.time_increased Successfully verified. ====================================== F_MC_MASTER_D (invariant admissibility) Successfully verified. ====================================== F_MC_MASTER_D.make (creator) Successfully verified. ====================================== F_MC_MASTER_D.tick Successfully verified. ====================================== F_MC_MASTER_D.reset Successfully verified. ====================================== F_MC_MASTER_D.time_increased Successfully verified.