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

pa_read_process alessandro.dat
mc_check_actl_file 0 Mod0 alessandro.actl [expr $mc_automaton + $mc_explain]
