# /* 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

set TYPE 1
set MCPAR [expr $mc_diagnostic]

pa_read_process "euro2000.sort"
pa_read_process "euro2000si.dat"
pa_read_process "euro2000yu.dat"
pa_read_process "euro2000es.dat"
pa_read_process "euro2000no.dat"

pa_encode_process "si yu es no"

versis_compose 1 EURODAT \
  "si yu es no" \
  "si1 si2 si3 si4 yu1 yu2 yu3 yu4 es1 es2 es3 es4 no1 no2 no3 no4 \
   siwin siequal silose yuwin yuequal yulose \
   eswin esequal eslose nowin noequal nolose \
   si0points si1points si2points si3points si4points \
   si5points si6points si7points si9points \
   yu0points yu1points yu2points yu3points yu4points \
   yu5points yu6points yu7points yu9points \
   es0points es1points es2points es3points es4points \
   es5points es6points es7points es9points \
   no0points no1points no2points no3points no4points \
   no5points no6points no7points no9points"

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

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