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

# known model checker's settings
global mc_diagnostic
global mc_explain
global mc_tracepath
global mc_automaton
global mc_minimize
global mc_progress

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

ccs_read philo2.ccs
ccs_read philo3.ccs
ccs_read philo4.ccs
ccs_read philo5.ccs
#ccs_read philo6.ccs
#ccs_read philo7.ccs
#ccs_read philo8.ccs

pa_write_process TABLE2 0
pa_write_process TABLE3 0
pa_write_process TABLE4 0
pa_write_process TABLE5 0
#pa_write_process TABLE6 0
#pa_write_process TABLE7 0
#pa_write_process TABLE8 0

outline "==========================="
outline "      MODEL CHECKING       "
outline "==========================="
outline ""

mc_check_actl_file 0 TABLE2 philo.actl
mc_check_actl_file 0 TABLE3 philo.actl
mc_check_actl_file 0 TABLE4 philo.actl
mc_check_actl_file 0 TABLE5 philo.actl
#mc_check_actl_file 0 TABLE6 philo.actl
#mc_check_actl_file 0 TABLE7 philo.actl
#mc_check_actl_file 0 TABLE8 philo.actl

outline "==================================="
outline "WITNESS AND COUNTEREXAMPLE AUTOMATA"
outline "==================================="
outline ""

# set parameters for model checking
set MCPAR1 [expr $mc_diagnostic | $mc_explain | $mc_tracepath]
set MCPAR2 [expr $mc_automaton | $mc_minimize]

mc_read_actl STARVE "AAG \[hungry1!\] AAF {eat1!} true;"

mc_check_actl 0 TABLE2 STARVE $MCPAR1
mc_check_actl 0 TABLE2 STARVE $MCPAR2
