# /* Robert Meolic, 27. 7. 2005 */
# /* Ph.D. */

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

# set parameters for model checking
set MCPAR [expr $mc_diagnostic]

set dir [pwd]; cd ../circuits; source init.tcl; cd $dir
ccs_read dme-martin.ccs
ccs_read dme-martin-abstract.ccs

outline ""
outline "======================"
outline "INFO ABOUT PROCESSES"
outline "======================"
outline ""

outline "DME-MARTIN-FALSE has [pa_state_number DME-MARTIN-FALSE] states / [pa_transition_number DME-MARTIN-FALSE] transitions / [bdd_node_number D_DME-MARTIN-FALSE] BDD nodes."
outline "DME-MARTIN-TRUE has [pa_state_number DME-MARTIN-TRUE] states / [pa_transition_number DME-MARTIN-TRUE] transitions / [bdd_node_number D_DME-MARTIN-TRUE] BDD nodes."
outline ""
outline "DME-MARTIN-FALSE-UA has [pa_state_number DME-MARTIN-FALSE-UA] states / [pa_transition_number DME-MARTIN-FALSE-UA] transitions / [bdd_node_number D_DME-MARTIN-FALSE-UA] BDD nodes."
outline "DME-MARTIN-FALSE-LA has [pa_state_number DME-MARTIN-FALSE-LA] states / [pa_transition_number DME-MARTIN-FALSE-LA] transitions / [bdd_node_number D_DME-MARTIN-FALSE-LA] BDD nodes."
outline "DME-MARTIN-FALSE-RR has [pa_state_number DME-MARTIN-FALSE-RR] states / [pa_transition_number DME-MARTIN-FALSE-RR] transitions / [bdd_node_number D_DME-MARTIN-FALSE-RR] BDD nodes."
outline "DME-MARTIN-TRUE-UA has [pa_state_number DME-MARTIN-TRUE-UA] states / [pa_transition_number DME-MARTIN-TRUE-UA] transitions / [bdd_node_number D_DME-MARTIN-TRUE-UA] BDD nodes."
outline "DME-MARTIN-TRUE-LA has [pa_state_number DME-MARTIN-TRUE-LA] states / [pa_transition_number DME-MARTIN-TRUE-LA] transitions / [bdd_node_number D_DME-MARTIN-TRUE-LA] BDD nodes."
outline "DME-MARTIN-TRUE-RR has [pa_state_number DME-MARTIN-TRUE-RR] states / [pa_transition_number DME-MARTIN-TRUE-RR] transitions / [bdd_node_number D_DME-MARTIN-TRUE-RR] BDD nodes."
outline ""

# -----------------------------------------------

outline "======================================="
outline "CHECKING PROPERTIES OF DME-MARTIN-FALSE"
outline "======================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-FALSE "dme-cell-properties.actl"

# -----------------------------------------------

outline "=================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-FALSE on line UA"
outline "=================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-FALSE-UA "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-UA "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-UA "dme-cell-steady.actl" $MCPAR

# -----------------------------------------------

outline "=================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-FALSE on line LA"
outline "=================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-FALSE-LA "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-LA "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-LA "dme-cell-steady.actl" $MCPAR

# -----------------------------------------------

outline "=================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-FALSE on line RR"
outline "=================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-FALSE-RR "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-RR "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-FALSE-RR "dme-cell-steady.actl" $MCPAR

# -----------------------------------------------

outline "================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-TRUE on line UA"
outline "================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-TRUE-UA "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-UA "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-UA "dme-cell-steady.actl" $MCPAR

# -----------------------------------------------

outline "================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-TRUE on line LA"
outline "================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-TRUE-LA "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-LA "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-LA "dme-cell-steady.actl" $MCPAR

# -----------------------------------------------

outline "================================================="
outline "LOOKING FOR HAZARDS in DME-MARTIN-TRUE on line RR"
outline "================================================="
outline ""

mc_check_actl_file 0 DME-MARTIN-TRUE-RR "dme-cell-static.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-RR "dme-cell-dynamic.actl" $MCPAR
mc_check_actl_file 0 DME-MARTIN-TRUE-RR "dme-cell-steady.actl" $MCPAR
