#/* Jul 05, 2005 Robert Meolic */
#/* testing ACTL model checking */

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

pa_read_process "actl.dat"

outline "===================================================="
outline "TEST 1 - explicit in deadlocked state"
outline "===================================================="

#mc_check_actl_file 0 LTS1explicit "actl1.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 1 - implicit in deadlocked state"
outline "===================================================="

#mc_check_actl_file 0 LTS1implicit "actl1.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 2 - explicit with deadlocked states"
outline "===================================================="

#mc_check_actl_file 0 LTS2explicit "actl1.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 2 - implicit with deadlocked states"
outline "===================================================="

#mc_check_actl_file 0 LTS2implicit "actl1.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 3 - without deadlocked states"
outline "===================================================="

#mc_check_actl_file 0 LTS3 "actl2.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 4 - deadlocked state = not divergent"
outline "===================================================="

mc_check_actl_file 0 LTS1explicit "actl3.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 5 - divergent state = not deadlocked"
outline "===================================================="

mc_check_actl_file 0 LTS1implicit "actl3.actl" [expr  $mc_simple | $mc_explain]
mc_check_actl_file 0 LTS2implicit "actl3.actl" [expr  $mc_simple | $mc_explain]
mc_check_actl_file 0 LTS5 "actl3.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 6 - deadlocked state is possible / divergent state is not possible"
outline "===================================================="

mc_check_actl_file 0 LTS2explicit "actl3.actl" [expr  $mc_simple | $mc_explain]
mc_check_actl_file 0 LTS4 "actl3.actl" [expr  $mc_simple | $mc_explain]
mc_check_actl_file 0 LTS6 "actl3.actl" [expr  $mc_simple | $mc_explain]
mc_check_actl_file 0 LTS7 "actl3.actl" [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 7 - deadlocked state/divergent state is not possible"
outline "===================================================="

mc_check_actl_file 0 LTS3 "actl3.actl" [expr  $mc_simple | $mc_explain]
