# 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 sudoku.ccs

outline ""
outline "bdd_table_foa = [bdd_table_foa]"
outline "bdd_table_add = [bdd_table_add]"
outline "bdd_garbage_number = [bdd_garbage_number]"
outline ""

mc_check_actl_string 1 SUDOKU "EEF {!complete}" [expr  $mc_diagnostic]

outline "bdd_table_foa = [bdd_table_foa]"
outline "bdd_table_add = [bdd_table_add]"
outline "bdd_garbage_number = [bdd_garbage_number]"

#SOME RESULTS
#N,     cas,        st/tr,         foa/add/gar
#0X,  0.192,          1/9,         2034/1598/0
#1X,  0.201,        10/98,         6016/4882/0
#2X,  0.236,     100/1060,       34100/30885/0
#3X,  1.089,   1000/11400,     323370/305284/1
#4X, 90.284, 10000/122000,   3996449/3433467/1
