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

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 ""

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 ""

#versis_strong_equivalence 1 EURO 1 EURODAT
#versis_weak_equivalence 1 EURO 1 EURODAT
#versis_testing_equivalence 1 EURO 1 EURODAT
#versis_trace_equivalence 1 EURO 1 EURODAT

ccs_read "euro2000-net2.ccs"

outline "process MATCHES"
outline "pa_state_number: [pa_state_number MATCHES]"
outline "pa_transition_number: [pa_transition_number MATCHES]"
outline "pa_transition_visible: [pa_transition_visible MATCHES]"
outline ""
outline "process ORDERING"
outline "pa_state_number: [pa_state_number ORDERING]"
outline "pa_transition_number: [pa_transition_number ORDERING]"
outline "pa_transition_visible: [pa_transition_visible ORDERING]"
outline ""

ccs_read "euro2000-test.ccs"

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

#versis_strong_equivalence 1 EURO 1 EURO2
#versis_weak_equivalence 1 EURO 1 EURO2
#versis_testing_equivalence 1 EURO 1 EURO2
#versis_trace_equivalence 1 EURO 1 EURO2
