# 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 example1.dat
mc_check_actl_file 0 S example1.actl [expr $mc_automaton | $mc_explain]

#ccs_read example1.ccs
#mc_check_actl_file 0 S1 example1.actl [expr $mc_automaton | $mc_explain]
