NO NON-Termination: ---------------- SCC: +--transitions: t135,t137 +--nodes: l89,l90 Closed walk: 2 -> t137, t135 Reachability checked! - Recurrent Set Found: { y___old7_0 -y___old7_post == 0, y___old6_0 -y___old6_post == 0, y___old5_0 -y___old5_post == 0, y___old4_0 -y___old4_post == 0, y___old3_0 -y___old3_post == 0, y___old2_0 -y___old2_post == 0, y___old16_0 -y___old16_post == 0, y___old15_0 -y___old15_post == 0, y___old14_0 -y___old14_post == 0, y_0 -y_post == 0, x___old7_0 -x___old7_post == 0, x___old6_0 -x___old6_post == 0, x___old5_0 -x___old5_post == 0, x___old4_0 -x___old4_post == 0, x___old3_0 -x___old3_post == 0, x___old2_0 -x___old2_post == 0, x___old16_0 -x___old16_post == 0, x___old15_0 -x___old15_post == 0, x___old14_0 -x___old14_post == 0, var_e_AGAFp_0_x_0 -x_post == 0, -1 + var_e_AGAFp_0_y_0 -var_e_AGAFp_0_y_post == 0, var_e_AGAFp_0_x_0 -var_e_AGAFp_0_x_post == 0, start_0 -var_e_AGAFp_0_start_post == 0, rv_init_0 -var_e_AGAFp_0_rv_init_post == 0, var_e_AGAFp_0_p_post == 0, __rho_2__0 -var_e_AGAFp_0___rho_2__post == 0, __rho_1__0 -var_e_AGAFp_0___rho_1__post == 0, var_Le_AFp_7_y_0 -var_Le_AFp_7_y_post == 0, var_Le_AFp_7_x_0 -var_Le_AFp_7_x_post == 0, var_Le_AFp_7_start_0 -var_Le_AFp_7_start_post == 0, var_Le_AFp_7_rv_init_0 -var_Le_AFp_7_rv_init_post == 0, var_Le_AFp_7_p_0 -var_Le_AFp_7_p_post == 0, var_Le_AFp_7___rho_2__0 -var_Le_AFp_7___rho_2__post == 0, var_Le_AFp_7___rho_1__0 -var_Le_AFp_7___rho_1__post == 0, var_Le_AFp_2_y_0 -var_Le_AFp_2_y_post == 0, var_Le_AFp_2_x_0 -var_Le_AFp_2_x_post == 0, var_Le_AFp_2_start_0 -var_Le_AFp_2_start_post == 0, var_Le_AFp_2_rv_init_0 -var_Le_AFp_2_rv_init_post == 0, var_Le_AFp_2_p_0 -var_Le_AFp_2_p_post == 0, var_Le_AFp_2___rho_2__0 -var_Le_AFp_2___rho_2__post == 0, var_Le_AFp_2___rho_1__0 -var_Le_AFp_2___rho_1__post == 0, var_Le_AFp_0_y_0 -var_Le_AFp_0_y_post == 0, var_Le_AFp_0_x_0 -var_Le_AFp_0_x_post == 0, var_Le_AFp_0_start_0 -var_Le_AFp_0_start_post == 0, var_Le_AFp_0_rv_init_0 -var_Le_AFp_0_rv_init_post == 0, var_Le_AFp_0_p_0 -var_Le_AFp_0_p_post == 0, var_Le_AFp_0___rho_2__0 -var_Le_AFp_0___rho_2__post == 0, var_Le_AFp_0___rho_1__0 -var_Le_AFp_0___rho_1__post == 0, var_LLe_p_7_y_0 -var_LLe_p_7_y_post == 0, var_LLe_p_7_x_0 -var_LLe_p_7_x_post == 0, var_LLe_p_7_start_0 -var_LLe_p_7_start_post == 0, var_LLe_p_7_rv_init_0 -var_LLe_p_7_rv_init_post == 0, var_LLe_p_7_p_0 -var_LLe_p_7_p_post == 0, var_LLe_p_7___rho_2__0 -var_LLe_p_7___rho_2__post == 0, var_LLe_p_7___rho_1__0 -var_LLe_p_7___rho_1__post == 0, var_LLe_p_2_y_0 -var_LLe_p_2_y_post == 0, var_LLe_p_2_x_0 -var_LLe_p_2_x_post == 0, var_LLe_p_2_start_0 -var_LLe_p_2_start_post == 0, var_LLe_p_2_rv_init_0 -var_LLe_p_2_rv_init_post == 0, var_LLe_p_2_p_0 -var_LLe_p_2_p_post == 0, var_LLe_p_2___rho_2__0 -var_LLe_p_2___rho_2__post == 0, var_LLe_p_2___rho_1__0 -var_LLe_p_2___rho_1__post == 0, var_LLe_p_0_y_0 -var_LLe_p_0_y_post == 0, var_LLe_p_0_x_0 -var_LLe_p_0_x_post == 0, var_LLe_p_0_start_0 -var_LLe_p_0_start_post == 0, var_LLe_p_0_rv_init_0 -var_LLe_p_0_rv_init_post == 0, var_LLe_p_0_p_0 -var_LLe_p_0_p_post == 0, var_LLe_p_0___rho_2__0 -var_LLe_p_0___rho_2__post == 0, var_LLe_p_0___rho_1__0 -var_LLe_p_0___rho_1__post == 0, start___old7_0 -start___old7_post == 0, start___old6_0 -start___old6_post == 0, start___old5_0 -start___old5_post == 0, start___old4_0 -start___old4_post == 0, start___old3_0 -start___old3_post == 0, start___old2_0 -start___old2_post == 0, start___old16_0 -start___old16_post == 0, start___old15_0 -start___old15_post == 0, start___old14_0 -start___old14_post == 0, start_0 -start_post == 0, rv_init___old7_0 -rv_init___old7_post == 0, rv_init___old6_0 -rv_init___old6_post == 0, rv_init___old5_0 -rv_init___old5_post == 0, rv_init___old4_0 -rv_init___old4_post == 0, rv_init___old3_0 -rv_init___old3_post == 0, rv_init___old2_0 -rv_init___old2_post == 0, rv_init___old16_0 -rv_init___old16_post == 0, rv_init___old15_0 -rv_init___old15_post == 0, rv_init___old14_0 -rv_init___old14_post == 0, rv_init_0 -rv_init_post == 0, rv_e_AGAFp_0 -rv_e_AGAFp_post == 0, rv_Le_AFp_0 -rv_Le_AFp_post == 0, rv_LLe_p_0 -rv_LLe_p_post == 0, ret_enc_e_AGAFp_01_0 -ret_enc_e_AGAFp_01_post == 0, ret_enc_Le_AFp_711_0 -ret_enc_Le_AFp_711_post == 0, ret_enc_Le_AFp_29_0 -ret_enc_Le_AFp_29_post == 0, ret_enc_Le_AFp_012_0 -ret_enc_Le_AFp_012_post == 0, ret_enc_Le_AFp_010_0 -ret_enc_Le_AFp_010_post == 0, ret_enc_LLe_p_741_0 -ret_enc_LLe_p_741_post == 0, ret_enc_LLe_p_740_0 -ret_enc_LLe_p_740_post == 0, ret_enc_LLe_p_240_0 -ret_enc_LLe_p_240_post == 0, ret_enc_LLe_p_239_0 -ret_enc_LLe_p_239_post == 0, ret_enc_LLe_p_042_0 -ret_enc_LLe_p_042_post == 0, ret_enc_LLe_p_040_0 -ret_enc_LLe_p_040_post == 0, pc_post == 0, p___old7_0 -p___old7_post == 0, p___old6_0 -p___old6_post == 0, p___old5_0 -p___old5_post == 0, p___old4_0 -p___old4_post == 0, p___old3_0 -p___old3_post == 0, p___old2_0 -p___old2_post == 0, p___old16_0 -p___old16_post == 0, p___old15_0 -p___old15_post == 0, p___old14_0 -p___old14_post == 0, p_post == 0, ndi7_0 -ndi7_post == 0, ndi6_0 -ndi6_post == 0, ndi5_0 -ndi5_post == 0, ndi4_0 -ndi4_post == 0, ndi3_0 -ndi3_post == 0, ndi2_0 -ndi2_post == 0, ndi16_0 -ndi16_post == 0, ndi15_0 -ndi15_post == 0, ndi14_0 -ndi14_post == 0, copied7_0 -copied7_post == 0, copied6_0 -copied6_post == 0, copied5_0 -copied5_post == 0, copied4_0 -copied4_post == 0, copied3_0 -copied3_post == 0, copied2_0 -copied2_post == 0, copied16_0 -copied16_post == 0, copied15_0 -copied15_post == 0, copied14_0 -copied14_post == 0, __rho_2____old7_0 -__rho_2____old7_post == 0, __rho_2____old6_0 -__rho_2____old6_post == 0, __rho_2____old5_0 -__rho_2____old5_post == 0, __rho_2____old4_0 -__rho_2____old4_post == 0, __rho_2____old3_0 -__rho_2____old3_post == 0, __rho_2____old2_0 -__rho_2____old2_post == 0, __rho_2____old16_0 -__rho_2____old16_post == 0, __rho_2____old15_0 -__rho_2____old15_post == 0, __rho_2____old14_0 -__rho_2____old14_post == 0, __rho_2__0 -__rho_2__post == 0, __rho_1____old7_0 -__rho_1____old7_post == 0, __rho_1____old6_0 -__rho_1____old6_post == 0, __rho_1____old5_0 -__rho_1____old5_post == 0, __rho_1____old4_0 -__rho_1____old4_post == 0, __rho_1____old3_0 -__rho_1____old3_post == 0, __rho_1____old2_0 -__rho_1____old2_post == 0, __rho_1____old16_0 -__rho_1____old16_post == 0, __rho_1____old15_0 -__rho_1____old15_post == 0, __rho_1____old14_0 -__rho_1____old14_post == 0, __rho_1__0 -__rho_1__post == 0, y___old7_0 -X151 == 0, y___old6_0 -X150 == 0, y___old5_0 -X149 == 0, y___old4_0 -X148 == 0, y___old3_0 -X147 == 0, y___old2_0 -X146 == 0, y___old16_0 -X145 == 0, y___old15_0 -X144 == 0, y___old14_0 -X143 == 0, y_0 -X142 == 0, x___old7_0 -X141 == 0, x___old6_0 -X140 == 0, x___old5_0 -X139 == 0, x___old4_0 -X138 == 0, x___old3_0 -X137 == 0, x___old2_0 -X136 == 0, x___old16_0 -X135 == 0, x___old15_0 -X134 == 0, x___old14_0 -X133 == 0, var_e_AGAFp_0_x_0 -X132 == 0, var_e_AGAFp_0_y_0 -X131 == 0, var_e_AGAFp_0_x_0 -X130 == 0, start_0 -X129 == 0, rv_init_0 -X128 == 0, X127 == 0, __rho_2__0 -X126 == 0, __rho_1__0 -X125 == 0, var_Le_AFp_7_y_0 -X124 == 0, var_Le_AFp_7_x_0 -X123 == 0, var_Le_AFp_7_start_0 -X122 == 0, var_Le_AFp_7_rv_init_0 -X121 == 0, var_Le_AFp_7_p_0 -X120 == 0, var_Le_AFp_7___rho_2__0 -X119 == 0, var_Le_AFp_7___rho_1__0 -X118 == 0, var_Le_AFp_2_y_0 -X117 == 0, var_Le_AFp_2_x_0 -X116 == 0, var_Le_AFp_2_start_0 -X115 == 0, var_Le_AFp_2_rv_init_0 -X114 == 0, var_Le_AFp_2_p_0 -X113 == 0, var_Le_AFp_2___rho_2__0 -X112 == 0, var_Le_AFp_2___rho_1__0 -X111 == 0, var_Le_AFp_0_y_0 -X110 == 0, var_Le_AFp_0_x_0 -X109 == 0, var_Le_AFp_0_start_0 -X108 == 0, var_Le_AFp_0_rv_init_0 -X107 == 0, var_Le_AFp_0_p_0 -X106 == 0, var_Le_AFp_0___rho_2__0 -X105 == 0, var_Le_AFp_0___rho_1__0 -X104 == 0, var_LLe_p_7_y_0 -X103 == 0, var_LLe_p_7_x_0 -X102 == 0, var_LLe_p_7_start_0 -X101 == 0, var_LLe_p_7_rv_init_0 -X100 == 0, var_LLe_p_7_p_0 -X99 == 0, var_LLe_p_7___rho_2__0 -X98 == 0, var_LLe_p_7___rho_1__0 -X97 == 0, var_LLe_p_2_y_0 -X96 == 0, var_LLe_p_2_x_0 -X95 == 0, var_LLe_p_2_start_0 -X94 == 0, var_LLe_p_2_rv_init_0 -X93 == 0, var_LLe_p_2_p_0 -X92 == 0, var_LLe_p_2___rho_2__0 -X91 == 0, var_LLe_p_2___rho_1__0 -X90 == 0, var_LLe_p_0_y_0 -X89 == 0, var_LLe_p_0_x_0 -X88 == 0, var_LLe_p_0_start_0 -X87 == 0, var_LLe_p_0_rv_init_0 -X86 == 0, var_LLe_p_0_p_0 -X85 == 0, var_LLe_p_0___rho_2__0 -X84 == 0, var_LLe_p_0___rho_1__0 -X83 == 0, start___old7_0 -X82 == 0, start___old6_0 -X81 == 0, start___old5_0 -X80 == 0, start___old4_0 -X79 == 0, start___old3_0 -X78 == 0, start___old2_0 -X77 == 0, start___old16_0 -X76 == 0, start___old15_0 -X75 == 0, start___old14_0 -X74 == 0, start_0 -X73 == 0, rv_init___old7_0 -X72 == 0, rv_init___old6_0 -X71 == 0, rv_init___old5_0 -X70 == 0, rv_init___old4_0 -X69 == 0, rv_init___old3_0 -X68 == 0, rv_init___old2_0 -X67 == 0, rv_init___old16_0 -X66 == 0, rv_init___old15_0 -X65 == 0, rv_init___old14_0 -X64 == 0, rv_init_0 -X63 == 0, rv_e_AGAFp_0 -X62 == 0, rv_Le_AFp_0 -X61 == 0, rv_LLe_p_0 -X60 == 0, ret_enc_e_AGAFp_01_0 -X59 == 0, ret_enc_Le_AFp_711_0 -X58 == 0, ret_enc_Le_AFp_29_0 -X57 == 0, ret_enc_Le_AFp_012_0 -X56 == 0, ret_enc_Le_AFp_010_0 -X55 == 0, ret_enc_LLe_p_741_0 -X54 == 0, ret_enc_LLe_p_740_0 -X53 == 0, ret_enc_LLe_p_240_0 -X52 == 0, ret_enc_LLe_p_239_0 -X51 == 0, ret_enc_LLe_p_042_0 -X50 == 0, ret_enc_LLe_p_040_0 -X49 == 0, X48 == 0, p___old7_0 -X47 == 0, p___old6_0 -X46 == 0, p___old5_0 -X45 == 0, p___old4_0 -X44 == 0, p___old3_0 -X43 == 0, p___old2_0 -X42 == 0, p___old16_0 -X41 == 0, p___old15_0 -X40 == 0, p___old14_0 -X39 == 0, X38 == 0, ndi7_0 -X37 == 0, ndi6_0 -X36 == 0, ndi5_0 -X35 == 0, ndi4_0 -X34 == 0, ndi3_0 -X33 == 0, ndi2_0 -X32 == 0, ndi16_0 -X31 == 0, ndi15_0 -X30 == 0, ndi14_0 -X29 == 0, copied7_0 -X28 == 0, copied6_0 -X27 == 0, copied5_0 -X26 == 0, copied4_0 -X25 == 0, copied3_0 -X24 == 0, copied2_0 -X23 == 0, copied16_0 -X22 == 0, copied15_0 -X21 == 0, copied14_0 -X20 == 0, __rho_2____old7_0 -X19 == 0, __rho_2____old6_0 -X18 == 0, __rho_2____old5_0 -X17 == 0, __rho_2____old4_0 -X16 == 0, __rho_2____old3_0 -X15 == 0, __rho_2____old2_0 -X14 == 0, __rho_2____old16_0 -X13 == 0, __rho_2____old15_0 -X12 == 0, __rho_2____old14_0 -X11 == 0, __rho_2__0 -X10 == 0, __rho_1____old7_0 -X9 == 0, __rho_1____old6_0 -X8 == 0, __rho_1____old5_0 -X7 == 0, __rho_1____old4_0 -X6 == 0, __rho_1____old3_0 -X5 == 0, __rho_1____old2_0 -X4 == 0, __rho_1____old16_0 -X3 == 0, __rho_1____old15_0 -X2 == 0, __rho_1____old14_0 -X1 == 0, __rho_1__0 -X0 == 0, var_e_AGAFp_0_x_0 -x_0 == 0, start_0 -var_e_AGAFp_0_start_0 == 0, rv_init_0 -var_e_AGAFp_0_rv_init_0 == 0, var_e_AGAFp_0_p_0 == 0, __rho_2__0 -var_e_AGAFp_0___rho_2__0 == 0, __rho_1__0 -var_e_AGAFp_0___rho_1__0 == 0, pc_0 == 0, p_0 == 0, -var_e_AGAFp_0_y_0 >= 0, -var_e_AGAFp_0_y_0 + y_0 >= 0, -var_e_AGAFp_0_x_0 >= 0 } Connected Subgraphs where we couldn't prove Termination: -------------------------------------------------------- SCC: +--transitions: t42,t43,t44,t46,t47,t48,t50 +--nodes: l32,l33,l34,l35,l36 SCC: +--transitions: t103,t118,t134,t195,t196,t198,t90 +--nodes: l127,l128,l3,l60,l70,l78,l88 SCC: +--transitions: t17,t18 +--nodes: l15,l16 method 1