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

pa_write_process_ccs S
pa_write_process_ccs WC1S
pa_write_process_ccs WC2S
pa_write_process_ccs WC3S
pa_write_process_ccs WC4S
pa_write_process_ccs WC5S
pa_write_process_ccs WC6S
pa_write_process_ccs WC7S
pa_write_process_ccs WC8S
pa_write_process_ccs WC9S
pa_write_process_ccs WC10S
pa_write_process_ccs WC11S
pa_write_process_ccs WC12S
pa_write_process_ccs WC13S
pa_write_process_ccs WC14S
pa_write_process_ccs WC15S
pa_write_process_ccs WC16S
pa_write_process_ccs WC17S
pa_write_process_ccs WC18S
pa_write_process_ccs WC19S
pa_write_process_ccs WC20S
