# /* 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-martin-false-ua.dat"
pa_read_process "dme-martin-false-la.dat"
pa_read_process "dme-martin-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-ua-1
pa_encode_process DME-false-ua-2
pa_encode_process DME-false-ua-3
pa_encode_process DME-false-ua-4
pa_encode_process DME-false-ua-5
pa_encode_process DME-false-la
pa_encode_process DME-false-la-1
pa_encode_process DME-false-la-2
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
pa_encode_process DME-false-rr-5
pa_encode_process DME-false-rr-6
pa_encode_process DME-false-rr-7
pa_encode_process DME-false-rr-8
pa_encode_process DME-false-rr-9
pa_encode_process DME-false-rr-10
pa_encode_process DME-false-rr-11
pa_encode_process DME-false-rr-12
pa_encode_process DME-false-rr-13

outline ""

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

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

mc_check_actl 0 DME-false-ua STATIC $MCPAR
mc_check_actl 0 DME-false-ua-1 STATIC $MCPAR
mc_check_actl 0 DME-false-ua-2 STATIC $MCPAR
mc_check_actl 0 DME-false-ua-3 STATIC $MCPAR
mc_check_actl 0 DME-false-ua-4 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
mc_check_actl 0 DME-false-ua-5 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
mc_check_actl 0 DME-false-la-1 STEADY $MCPAR
mc_check_actl 0 DME-false-la-2 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
mc_check_actl 0 DME-false-rr-5 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-6 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-7 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-8 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-9 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-10 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-11 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-12 STEADY $MCPAR
mc_check_actl 0 DME-false-rr-13 STEADY $MCPAR
