[Termtools] Conflict in ITS

[Akihisa Yamada]

Thanks a lot Genaim! Any comment, Albert?

Best,
Akihisa

> On Mar 23, 2019, at 21:46, Samir Genaim <genaim at gmail.com> wrote:
> 
> 
> As far I can see this ITS is terminating. It is easier to explain using the following equivalent program. The symbol * means non-deterministic integer choice, and the variables are: walker_0 is w, seq_0 is s, i_0 is i, choice_0 is c and z_0 is z (N_0 was removed since it is the constant 2, and pos_0 was removed since it is not used)
> 
> 
> w=1; s=1; i=1; z=*; assert(z >= 0); // edge 14->13
> while ( 1 =< w && w =< 2 ) { // nodes 13, 17, 18 
>    c = *; assert(0 <= c && c <= 1) // edge 17->16
>    if ( z >= 1 ) { 
>       z--;   // edge 16->12
>    } else { // z <= 0, edge 16->15
>       if ( i <= 0 ) {
>          s++; i=s; z=*; assert(z >= 0); // one of edges 15->12
>       } else if ( i >= 1 and c <= 0 ) {
>          i--; // one of edges 15->12
>       } else {
>          break; // implicit exit at node 15 (blocking behaviour)
>       }
>    }
>    if ( c <= 0 ) {
>       w--; // one of edges 12->13
>    } else {
>       w++; // one of edges 12->13
>    }
> }
> 
> 
> First, instructions w-- and w++ must alternate in consecutive iterations, otherwise, the loop terminates since w will become either 0 or 3.
> 
> If the loop does not terminate, eventually we reach a state in which i=2 and z=0, which means that the following instruction has to execute in two consecutive iterations
>  
>    else if ( i >= 1 and c <= 0 ) {
>       i--;
>    } else {
>       break;
>    }
> 
> if it does not 'break' out of the loop, then c=0 in these two iterations and thus w-- is executed twice in a row and the program terminates with w=0.
> 
> 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20190323/f0df2558/attachment.html>