# /* 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-smv.ccs
ccs_read dme-smv-abstract.ccs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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