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

ccs_read example2.ccs
mc_check_actl_file 0 S example2.actl [expr $mc_automaton | $mc_minimize]

pa_write_process_ccs S
pa_write_process_ccs WC1S
pa_write_process_ccs MIN_WC1S
pa_write_process_ccs WC2S
pa_write_process_ccs MIN_WC2S
pa_write_process_ccs WC3S
pa_write_process_ccs MIN_WC3S
pa_write_process_ccs WC4S
pa_write_process_ccs MIN_WC4S
pa_write_process_ccs WC5S
pa_write_process_ccs MIN_WC5S
pa_write_process_ccs WC6S
pa_write_process_ccs MIN_WC6S
pa_write_process_ccs WC7S
pa_write_process_ccs MIN_WC7S
pa_write_process_ccs WC8S
pa_write_process_ccs MIN_WC8S
