view src/mcDPP.cbc @ 0:67e6ca3c7e6c

model checking
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 27 Apr 2021 14:25:56 +0900
parents
children
line wrap: on
line source

void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker,
	   StateDB now,StateDB next, int check) {
   PhilsImpl* phils =
	(PhilsImpl*)GearImpl(mcWorker->mcContext, Phils, phils);
   int prev_now = now->flag; 
   int prev_next = next->flag; 
      if (phils->self != 1) return;
      enum Code nextc = mcWorker->mcContext->next;
      if (nextc == C_putdown_rforkPhilsImpl ) {
        next->flag |= t_eating; 
      }
      if ((next->flag & t_eating )||(next->flag & t_F_eating) ) {
        now->flag |= t_F_eating; 
      }
      if ( prev_now != now->flag || prev_next != next->flag )
         mcWorker->change = 1;
      if (check) {
         if (!(now->flag & t_F_eating)) {
             printf("not <> eating\n");
       }
   }
}