#ifndef MCDPP_H
#define MCDPP_H 0

#include "context.h"
#include "ModelChecking/state_db.h"

/*
   00  don't care 
   01  true
   11  false
 */

enum DPPMC_F {
   t_eating = 0x1,       // eating
   f_eating = 0x3,       // ¬eating
   t_F_eating  = 0x4,     // <> eating
   f_F_eating  = 0xc,     // ¬<> eating
   t_GF_eating  = 0x10,     // [] <> eating
   f_GF_eating  = 0x30,     // ¬[] <> eating
};

extern void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcworker, StateDB now,StateDB next, int checking) ;

#endif