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

ccs_read "euro2000.ccs"
ccs_read "euro2000-net2.ccs"
ccs_read "euro2000-product.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 ""
pa_write_process MATCHES 0

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 ""
pa_write_process ORDERING 0

outline "automaton MATCHES_F1"
outline "pa_state_number: [pa_state_number MATCHES_F1]"
outline "pa_transition_number: [pa_transition_number MATCHES_F1]"
outline "pa_transition_visible: [pa_transition_visible MATCHES_F1]"
outline ""
pa_write_process MATCHES_F1 0

outline "automaton ORDERING_F1"
outline "pa_state_number: [pa_state_number ORDERING_F1]"
outline "pa_transition_number: [pa_transition_number ORDERING_F1]"
outline "pa_transition_visible: [pa_transition_visible ORDERING_F1]"
outline ""
pa_write_process ORDERING_F1 0

outline "product EURO_A1 = MATCHES * ORDERING_F1"
outline "pa_state_number: [pa_state_number EURO_A1]"
outline "pa_transition_number: [pa_transition_number EURO_A1]"
outline "pa_transition_visible: [pa_transition_visible EURO_A1]"
outline ""
pa_write_process EURO_A1 0

outline "product EURO_A2 = ORDERING_F1 * MATCHES"
outline "pa_state_number: [pa_state_number EURO_A2]"
outline "pa_transition_number: [pa_transition_number EURO_A2]"
outline "pa_transition_visible: [pa_transition_visible EURO_A2]"
outline ""
pa_write_process EURO_A2 0

outline "product EURO_B1 = MATCHES_F1 * ORDERING"
outline "pa_state_number: [pa_state_number EURO_B1]"
outline "pa_transition_number: [pa_transition_number EURO_B1]"
outline "pa_transition_visible: [pa_transition_visible EURO_B1]"
outline ""
pa_write_process EURO_B1 0

outline "product EURO_B2 = ORDERING * MATCHES_F1"
outline "pa_state_number: [pa_state_number EURO_B2]"
outline "pa_transition_number: [pa_transition_number EURO_B2]"
outline "pa_transition_visible: [pa_transition_visible EURO_B2]"
outline ""
pa_write_process EURO_B2 0

outline "product EURO_C1 = MATCHES_F1 * ORDERING_F1"
outline "pa_state_number: [pa_state_number EURO_C1]"
outline "pa_transition_number: [pa_transition_number EURO_C1]"
outline "pa_transition_visible: [pa_transition_visible EURO_C1]"
outline ""
pa_write_process EURO_C1 0

outline "product EURO_C2 = ORDERING_F1 * MATCHES_F1"
outline "pa_state_number: [pa_state_number EURO_C2]"
outline "pa_transition_number: [pa_transition_number EURO_C2]"
outline "pa_transition_visible: [pa_transition_visible EURO_C2]"
outline ""
pa_write_process EURO_C2 0
