# /* Robert Meolic, 1. 12. 2002 */
# /* Clanek za Midem */

# 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]

pa_read_process "sortDME.dat"

pa_read_process "dme-smv-false-ua.dat"
pa_read_process "dme-smv-false-la.dat"
pa_read_process "dme-smv-false-rr.dat"

set define ""
append define "#define IN (ur? OR lr? OR ra?)\n"
append define "#define OUT (ua! OR la! OR rr!)\n"
mc_read_actl STATIC "$define EEF {\$IN} <\$OUT> <\$OUT> <\$IN> true;"
mc_read_actl DYNAMIC "$define EEF {\$IN} <\$OUT> <\$OUT> <\$OUT> true;"
mc_read_actl STEADY "$define EEF {\$IN} ((<\$IN> TRUE) AND (<\$OUT> <\$IN> TRUE));"

pa_encode_process DME-false-ua
pa_encode_process DME-false-la
pa_encode_process DME-false-rr
pa_encode_process DME-false-rr-1
pa_encode_process DME-false-rr-2
pa_encode_process DME-false-rr-3
pa_encode_process DME-false-rr-4

outline ""

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

outline "=================================================="
outline "LOOKING FOR STATIC HAZARDS in DME-false on line UA"
outline "=================================================="
outline ""

mc_check_actl 0 DME-false-ua STATIC $MCPAR

outline "==================================================="
outline "LOOKING FOR DYNAMIC HAZARDS in DME-false on line UA"
outline "==================================================="
outline ""

mc_check_actl 0 DME-false-ua DYNAMIC $MCPAR

outline "=================================================="
outline "LOOKING FOR STEADY HAZARDS in DME-false on line UA"
outline "=================================================="
outline ""

mc_check_actl 0 DME-false-ua STEADY $MCPAR

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

outline "=================================================="
outline "LOOKING FOR STATIC HAZARDS in DME-false on line LA"
outline "=================================================="
outline ""

mc_check_actl 0 DME-false-la STATIC $MCPAR

outline "==================================================="
outline "LOOKING FOR DYNAMIC HAZARDS in DME-false on line LA"
outline "==================================================="
outline ""

mc_check_actl 0 DME-false-la DYNAMIC $MCPAR

outline "=================================================="
outline "LOOKING FOR STEADY HAZARDS in DME-false on line LA"
outline "=================================================="
outline ""

mc_check_actl 0 DME-false-la STEADY $MCPAR

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

outline "==================================================="
outline "LOOKING FOR STATIC HAZARDS in DME-false on line RR"
outline "==================================================="
outline ""

mc_check_actl 0 DME-false-rr STATIC $MCPAR
mc_check_actl 0 DME-false-rr-1 STATIC $MCPAR
mc_check_actl 0 DME-false-rr-2 STATIC $MCPAR
mc_check_actl 0 DME-false-rr-3 STATIC $MCPAR
mc_check_actl 0 DME-false-rr-4 STATIC $MCPAR

outline "===================================================="
outline "LOOKING FOR DYNAMIC HAZARDS in DME-false on line RR"
outline "===================================================="
outline ""

mc_check_actl 0 DME-false-rr DYNAMIC $MCPAR

outline "=================================================="
outline "LOOKING FOR STEADY HAZARDS in DME-false on line RR"
outline "=================================================="
outline ""

mc_check_actl 0 DME-false-rr STEADY $MCPAR
