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

set PARAM [expr $mc_diagnostic + $mc_automaton]

pa_read_process "complex.dat"
mc_check_actl_file 0 Mod1 "complex.actl" $PARAM
mc_check_actl_file 0 Mod2 "complex.actl" $PARAM
mc_check_actl_file 0 Mod3 "complex.actl" $PARAM
mc_check_actl_file 0 Mod4 "complex.actl" $PARAM
