// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// The module implements the well-known dining philosopher's example due to   //
// Dijstra.                                                                   //
// ************************************************************************** //

import DiningPhilosophers.Philosopher;
import DiningPhilosophers.Fork;


macro N = 5;

module DiningPhilosophers (
    event [N]bool ?trigger_hungry,
    event [N]bool ?done,
    event [N]bool ! requested_left_fork,
    event [N]bool ! requested_right_fork,
    event [N]bool ? give_access_left_fork,
    event [N]bool ? give_access_right_fork,
    event [N]bool ? force_release_forks
) {
    event [N]bool take_left_fork;
    event [N]bool take_right_fork;
    event [N]bool release_left_fork;
    event [N]bool release_right_fork;

    for(i=0..N-1) do || {
        Philosopher (
            trigger_hungry[i], done[i], 
            requested_left_fork[i], requested_right_fork[i],
            give_access_left_fork[i], give_access_right_fork[i],
            force_release_forks[i],
            take_left_fork[i], take_right_fork[i], release_left_fork[i], release_right_fork[i]
        );
        ||
        Fork (
            take_right_fork[i] | take_left_fork[(i + 1) % N],
            release_right_fork[i] | release_left_fork[(i + 1) % N]
        );
        ||
        loop {
            assert ( ! (take_right_fork[i] & take_left_fork[(i + 1) % N]));
            assert ( ! (release_right_fork[i] & release_left_fork[(i + 1) % N]));
            pause;
        }
    }
}