NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: 0}> 0}> 0}> (0 + DName^0), num^0 -> (1 + num^0)}> 0}> (1 + i^0)}> undef391, a66^0 -> (0 + DName^0), a77^0 -> (0 + Pdoi^0), pc^0 -> 0, ret_IoCreateDevice88^0 -> undef406, status^0 -> (0 + undef406)}> (0 + undef504), ___rho_9_^0 -> undef490, a11^0 -> (0 + lptNamei^0), b22^0 -> (0 + PdoType^0), c33^0 -> (0 + dcIdi^0), d44^0 -> (0 + num^0), ret_PPMakeDeviceName55^0 -> undef504}> undef561, set^0 -> (0 + undef579), unset^0 -> undef579}> Fresh variables: undef49, undef146, undef391, undef406, undef411, undef490, undef504, undef561, undef579, Undef variables: undef49, undef146, undef391, undef406, undef411, undef490, undef504, undef561, undef579, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (1 + i^0)}> 0, num^0 -> 0}> 0, num^0 -> 0}> 0, num^0 -> 0}> 0, num^0 -> 0}> 0, num^0 -> 0}> 0, num^0 -> 0}> 0}> 0}> 0}> 0}> Fresh variables: undef49, undef146, undef391, undef406, undef411, undef490, undef504, undef561, undef579, Undef variables: undef49, undef146, undef391, undef406, undef411, undef490, undef504, undef561, undef579, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: 1 + i^0, rest remain the same}> Variables: Pdolen^0, i^0 Graph 2: Transitions: Variables: Precedence: Graph 0 Graph 1 Graph 2 0, num^0 -> 0, rest remain the same}> 0, num^0 -> 0, rest remain the same}> 0, num^0 -> 0, rest remain the same}> 0, num^0 -> 0, rest remain the same}> 0, num^0 -> 0, rest remain the same}> 0, num^0 -> 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> 0, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 6 , 2 ) ( 13 , 1 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.001205 Checking conditional termination of SCC {l13}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000623s Ranking function: -1 + Pdolen^0 - i^0 New Graphs: Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.001712 > No variable changes in termination graph. Checking conditional unfeasibility... Termination failed. Trying to show unreachability... Proving unreachability of entry: 0, num^0 -> 0, rest remain the same}> LOG: CALL check - Post:1 <= 0 - Process 1 * Exit transition: 0, num^0 -> 0, rest remain the same}> * Postcondition : 1 <= 0 Postcodition moved up: 1 <= 0 LOG: Try proving POST Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 2 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000458s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000522s LOG: NarrowEntry size 1 It's unfeasible. Removing transition: 1 + i^0, rest remain the same}> ENTRIES: END ENTRIES: GRAPH: END GRAPH: EXIT: 0, num^0 -> 0, rest remain the same}> POST: 1 <= 0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.001529s Time used: 0.001472 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.003107s Time used: 0.00301 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.004282s Time used: 0.004095 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.013424s Cannot prove unreachability Proving non-termination of subgraph 2 Transitions: Variables: Checking conditional non-termination of SCC {l6}... > No exit transition to close. Calling reachability with... Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: Transition: Conditions: OPEN EXITS: --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, num^0 -> 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: Transition: 0, rest remain the same}> Conditions: OPEN EXITS: 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1) 0, num^0 -> 0, rest remain the same}> (condsUp: undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2) 0, num^0 -> 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1) 0, rest remain the same}> (condsUp: 1 <= ___rho_1_^0) 0, rest remain the same}> (condsUp: ___rho_1_^0 <= 0, undef146 = 1) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef406 <= 0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef406 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, 3 <= undef406, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, undef504 <= 0, 1 <= ___rho_1_^0, undef391 = undef406, undef490 = undef504, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, undef504 <= 0, undef391 = undef406, undef490 = undef504, undef146 = 1, undef411 = 1, undef406 = 2, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, 1 <= ___rho_1_^0, 1 <= undef504, undef490 = undef504, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: 1 + i^0 <= Pdolen^0, ___rho_1_^0 <= 0, 1 <= undef504, undef490 = undef504, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, 1 <= ___rho_1_^0, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, Transition: Conditions: Pdolen^0 <= i^0, ___rho_1_^0 <= 0, undef146 = 1, OPEN EXITS: > Conditions are reachable! Program does NOT terminate