// ************************************************************************** // // // // 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; } } }