# /* The Dining Philosophers  - iz magisterija */
# /* Robert Meolic, 14. 10. 1999 */
# /* Robert Meolic, Feb 9, 2004, ISTI */

outline ""
outline "==========================="
outline "SPECIFICATION IN RAW FORMAT"
outline "==========================="
outline ""

pa_read_process "philo5.dat"
pa_encode_process "FLZF1 VLC1 FLZF2 VLC2 FLZF3 VLC3 FLZF4 VLC4 FLZF5 VLC5"
versis_compose 1 S \
  "FLZF1 VLC1 FLZF2 VLC2 FLZF3 VLC3 FLZF4 VLC4 FLZF5 VLC5" \
  "think1 think2 think3 think4 think5 eat1 eat2 eat3 eat4 eat5"

outline ""
outline "==========================="
outline "  SPECIFICATION IN CCS   "
outline "==========================="
outline ""

ccs_read philo5dat-v1.ccs
ccs_read philo5dat-v2.ccs

outline ""
outline "==========================="
outline "    CHECKING EQUIVALENCE   "
outline "==========================="
outline ""

versis_strong_equivalence 0 S1 1 S
versis_strong_equivalence 0 S2 1 S
versis_strong_equivalence 0 S1 0 S2
