add model checking related function to 51_2_4_slots.dats