Lsts_file Begin Header State_cnt = 11 Transition_cnt = 16 Action_cnt = 16 State_prop_cnt = 2 Initial_state = 1 End Header Begin Action_names 1 = "do_noncritical$i$1" 2 = "desire$i$1" 3 = "set_b_i$i$1" 4 = "read_b_j_true$i$1" 5 = "read_b_j_false$i$1" 6 = "read_k_eq_j$i$1" 7 = "read_k_ne_j$i$1" 8 = "enter$i$1" 9 = "clear_b_i$i$1" 10 = "exit$i$1" 11 = "read_k_again_eq_j$i$1" 12 = "read_k_again_ne_j$i$1" 13 = "set_k$i$1$z$1" 14 = "set_k$i$1$z$2" 15 = "set_b_i_again$i$1" 16 = "clear_b_i_again$i$1" End Action_names Begin State_props "wait_set_b_i_1": 2; "wait_set_k_1": 9; End State_props Begin Transitions 1 1 1 2 2; 2 3 3; 3 4 4 5 5; 4 3 7 6 6; 5 7 8; 6 8 9; 7 9 10; 8 8 11 10 12; 9 11 13 11 14; 10 3 15; 11 1 16; End Transitions End_lsts