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

ccs_read topsys.ccs

outline "STATISTICS ABOUT PROCESSES"
outline ""

pa_write_process_ccs S1 0
pa_write_process_ccs Q 0
pa_write_process_ccs P4 0
pa_write_process_ccs TOPSYS 0

outline "STATISTICS ABOUT WCAs"
outline ""

pa_write_process_ccs WCA_TOPSYS 0
pa_write_process_ccs WCA_P4 0
pa_write_process_ccs WCA_Q 0
pa_write_process_ccs WCA_S1 0

outline "EQUIVALENCE CHECKING"
outline ""

versis_strong_equivalence 0 WCA_TOPSYS 0 WCA_S1

outline ""
outline "AND NOW... THE SAME BUT STEP-BY-STEP"
outline ""

mc_check_actl 0 TOPSYS F1 [expr $mc_automaton | $mc_minimize]
mc_check_actl 0 P4 F1 [expr  $mc_automaton | $mc_minimize]
strucval_sync_product Q1 Q MIN_WC1P4 "a2 b c"
versis_wca_minimization 0 Q1
strucval_sync_product Q2 S1 MIN_Q1 "a1 x y"
versis_wca_minimization 0 Q2
versis_strong_equivalence 0 MIN_WC1TOPSYS 0 MIN_Q2
