# /* Circuits with hazards */
# /* from MIDEM paper */
# /* Robert Meolic, Mar 2007 */

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

# use TYPE=1 for raw and onthefly composition
# use TYPE=0 otherwise
set TYPE 1

# set parameters for model checking
set MCPAR [expr !$mc_progress]

source init.tcl
ccs_read "test-hazards.ccs"

outline ""
outline "==========================="
outline " LOOKING FOR STATIC HAZARDS"
outline "==========================="
outline ""

mc_check_actl 0 STATIC STATIC1 $MCPAR
mc_check_actl 0 STATIC STATIC2 $MCPAR
mc_check_actl 0 DYNAMIC STATIC1 $MCPAR
mc_check_actl 0 DYNAMIC STATIC2 $MCPAR
mc_check_actl 0 TRANSIENT STATIC1 $MCPAR
mc_check_actl 0 TRANSIENT STATIC2 $MCPAR
mc_check_actl 0 STEADY1 STATIC1 $MCPAR
mc_check_actl 0 STEADY1 STATIC2 $MCPAR
mc_check_actl 0 STEADY2 STATIC1 $MCPAR
mc_check_actl 0 STEADY2 STATIC2 $MCPAR

outline ""
outline "============================"
outline " LOOKING FOR DYNAMIC HAZARDS"
outline "============================"
outline ""

mc_check_actl 0 STATIC DYNAMIC1 $MCPAR
mc_check_actl 0 STATIC DYNAMIC2 $MCPAR
mc_check_actl 0 DYNAMIC DYNAMIC1 $MCPAR
mc_check_actl 0 DYNAMIC DYNAMIC2 $MCPAR
mc_check_actl 0 TRANSIENT DYNAMIC1 $MCPAR
mc_check_actl 0 TRANSIENT DYNAMIC2 $MCPAR
mc_check_actl 0 STEADY1 DYNAMIC1 $MCPAR
mc_check_actl 0 STEADY1 DYNAMIC2 $MCPAR
mc_check_actl 0 STEADY2 DYNAMIC1 $MCPAR
mc_check_actl 0 STEADY2 DYNAMIC2 $MCPAR

outline ""
outline "==========================="
outline " LOOKING FOR STEADY HAZARDS"
outline "==========================="
outline ""

mc_check_actl 0 STATIC STEADY1 $MCPAR
mc_check_actl 0 STATIC STEADY2 $MCPAR
mc_check_actl 0 DYNAMIC STEADY1 $MCPAR
mc_check_actl 0 DYNAMIC STEADY2 $MCPAR
mc_check_actl 0 TRANSIENT STEADY1 $MCPAR
mc_check_actl 0 TRANSIENT STEADY2 $MCPAR
mc_check_actl 0 STEADY1 STEADY1 $MCPAR
mc_check_actl 0 STEADY1 STEADY2 $MCPAR
mc_check_actl 0 STEADY2 STEADY1 $MCPAR
mc_check_actl 0 STEADY2 STEADY2 $MCPAR
