Lsts_file
Begin Header
 State_cnt = 3
 Transition_cnt = 34
 Action_cnt = 34
 State_prop_cnt = 2
 Initial_state = 1
End Header
Begin Action_names
 1 = "choose_i$i$1"
 2 = "choose_i$i$2"
 3 = "do_noncritical$i$1"
 4 = "desire$i$1"
 5 = "set_b_i$i$1"
 6 = "read_b_j_true$i$1"
 7 = "read_b_j_false$i$1"
 8 = "read_k_eq_j$i$1"
 9 = "read_k_ne_j$i$1"
 10 = "clear_b_i$i$1"
 11 = "read_k_again_eq_j$i$1"
 12 = "read_k_again_ne_j$i$1"
 13 = "set_b_i_again$i$1"
 14 = "enter$i$1"
 15 = "exit$i$1"
 16 = "set_k$i$1$z$1"
 17 = "set_k$i$1$z$2"
 18 = "clear_b_i_again$i$1"
 19 = "do_noncritical$i$2"
 20 = "desire$i$2"
 21 = "set_b_i$i$2"
 22 = "read_b_j_true$i$2"
 23 = "read_b_j_false$i$2"
 24 = "read_k_eq_j$i$2"
 25 = "read_k_ne_j$i$2"
 26 = "clear_b_i$i$2"
 27 = "read_k_again_eq_j$i$2"
 28 = "read_k_again_ne_j$i$2"
 29 = "set_b_i_again$i$2"
 30 = "enter$i$2"
 31 = "exit$i$2"
 32 = "set_k$i$2$z$1"
 33 = "set_k$i$2$z$2"
 34 = "clear_b_i_again$i$2"
End Action_names
Begin State_props
  "scheduler_1": 2;
  "scheduler_2": 3;
End State_props
Begin Transitions
 1 2 1 3 2;
 2 1 3 1 4 1 5 1 6 1 7 1 8 1 9 1 10 1 11 1 12 1 13 1 14 1 15 1 16 1 17 1
 18;
 3 1 19 1 20 1 21 1 22 1 23 1 24 1 25 1 26 1 27 1 28 1 29 1 30 1 31 1 32
 1 33 1 34;
End Transitions
End_lsts