view src/PhilsImpl2.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

Phils* createPhilsImpl(struct Context* context, int id, AtomicT_int* right, AtomicT_int* left) {
    struct Phils* phils  = new Phils();
    struct PhilsImpl* phils_impl = new PhilsImpl();
    phils->phils = (union Data*)phils_impl;
    phils_impl->Leftfork = left;
    phils_impl->Rightfork = right;
    phils_impl->self = id;
    phils->putdown_lfork = C_putdown_lforkPhilsImpl;
    phils->putdown_rfork = C_putdown_rforkPhilsImpl;
    phils->eating = C_eatingPhilsImpl;
    phils->pickup_rfork = C_pickup_rforkPhilsImpl;
    phils->pickup_lfork = C_pickup_lforkPhilsImpl;
    phils->thinking = C_thinkingPhilsImpl;
    return phils;
}


__code putdown_rfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* right_fork = phils->Rightfork;
    goto right_fork->set(-1, putdown_lfork);
}

__code putdown_lfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    goto left_fork->set(-1, thinking);

}

__code thinking(struct PhilsImpl* phils, struct Fork* fork, __code next(...)) {
    printf("%d: thinking\n", phils->self);
    goto pickup_lfork();
}

__code pickup_rfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* right_fork = phils->Rightfork;
    goto right_fork->checkAndSet(-1, phils->self, pickup_lfork, pickup_rfork);
}

__code pickup_lfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    goto left_fork->checkAndSet(-1, phils->self, pickup_rfork, eating);

}

__code eating(struct PhilsImpl* phils, __code next(...)) {
    printf("%d: eating\n", phils->self);
    goto putdown_rfork();
}