# Transitions to solve: t_7 t_16 t_26 t_36 t_37 t_30 t_31 t_32 t_33 t_34 t_35 t_28 t_39 ____inittransition # Transitions to solve: t_16 t_37 t_30 t_31 t_32 t_33 t_34 t_35 # Transitions to solve: t_30 t_31 t_32 t_33 t_35 # Transitions to solve: t_30 YES, realshellsort.fstb terminates. max_dim = 4 +-----------------------------------------------------------------------------+ | Ranking Function | +-----------------------------------------------------------------------------+ state stop: 0 state start: 3 state lbl_12_1: 1 1+(3*increment) state lbl_12_3: 1 6*increment state lbl_10_1: 1 2+(3*increment) (-2+(3*array_size))+(-3*i) j state lbl_7_1: 1 2+(3*increment) (-1+(3*array_size))+(-3*i) state lbl_5_3: 1 2+(3*increment) (3*array_size)+(-3*i) state lbl_2_1: 2 state ____start: 4 +-----------------------------------------------------------------------------+ | Worst Case Execution Time | +-----------------------------------------------------------------------------+ /--- / | -2+array_size__o' >= 0 | 1 >= 0 \ (((((((1+1)+-1)+-1)+(((-1/6)*array_size__o')+((1/6)*((array_size__o'*array_size__o')*array_size__o'))))+-1)+-1)+1)+1 / | -1*array_size__o' >= 0 | 1 >= 0 \ ((1+1)+1)+1 / | -1+array_size__o' = 0 | 1 >= 0 \ ((((((1+1)+-1)+-1)+-1)+-1)+1)+1 \---