#/* Jul 01, 2005 Robert Meolic */
#/* ACTLW and ACTL patterns */

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

pa_read_process "patterns.dat"

outline "===================================================="
outline "TEST 1"
outline "===================================================="

set TEST "patterns-test1.actl"
mc_check_actl_file 0 PATTERNS $TEST [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 2"
outline "===================================================="

set TEST "patterns-test2.actl"
mc_check_actl_file 0 PATTERNS $TEST [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 3"
outline "===================================================="

set TEST "patterns-test3.actl"
mc_check_actl_file 0 PATTERNS $TEST [expr  $mc_simple | $mc_explain]

outline "===================================================="
outline "TEST 4"
outline "===================================================="

set TEST "patterns-test4.actl"
mc_check_actl_file 0 PATTERNS $TEST [expr  $mc_simple | $mc_explain]
