# /* EURO 2000 */
# /* Robert Meolic, an example for ACTLW model checking. */

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

ccs_read "euro2000.ccs"
ccs_read "euro2000-net.ccs"

outline "composition EURO"
outline "pa_comp_state_number: [pa_comp_state_number EURO]"
outline "pa_comp_transition_number: [pa_comp_transition_number EURO]"
outline "pa_comp_transition_visible: [pa_comp_transition_visible EURO]"
outline ""

mc_read_actl_file "euro2000.actl"
mc_check_actl $TYPE EURO euro2000_F1 $MCPAR
mc_check_actl $TYPE EURO euro2000_F2 $MCPAR
mc_check_actl $TYPE EURO euro2000_F3 $MCPAR
mc_check_actl $TYPE EURO euro2000_F4 $MCPAR
mc_check_actl $TYPE EURO euro2000_F5 $MCPAR
mc_check_actl $TYPE EURO euro2000_F6 $MCPAR
mc_check_actl $TYPE EURO euro2000_F7 $MCPAR
mc_check_actl $TYPE EURO euro2000_F8 $MCPAR
mc_check_actl $TYPE EURO euro2000_F9 $MCPAR
mc_check_actl $TYPE EURO euro2000_F10 $MCPAR
mc_check_actl $TYPE EURO euro2000_F11 $MCPAR
mc_check_actl $TYPE EURO euro2000_F12 $MCPAR
mc_check_actl $TYPE EURO euro2000_F13 $MCPAR
mc_check_actl $TYPE EURO euro2000_F14 $MCPAR
mc_check_actl $TYPE EURO euro2000_F15 $MCPAR
mc_check_actl $TYPE EURO euro2000_F16 $MCPAR
mc_check_actl $TYPE EURO euro2000_F17 $MCPAR
mc_check_actl $TYPE EURO euro2000_F18 $MCPAR
mc_check_actl $TYPE EURO euro2000_F19 $MCPAR
mc_check_actl $TYPE EURO euro2000_F20 $MCPAR
mc_check_actl $TYPE EURO euro2000_F21 $MCPAR
mc_check_actl $TYPE EURO euro2000_F22 $MCPAR
mc_check_actl $TYPE EURO euro2000_F23 $MCPAR
mc_check_actl $TYPE EURO euro2000_F24 $MCPAR
