[Termtools] Conflict in ITS

[Albert Rubio]

Samir is right. There is a subtle bug in VeryMax due to the use of the 
graph resulting form the conditional termination proof to then prove 
non-termination. This problem appears rarely and it disappears when the 
use of this graph is disabled adding the flag "-nt-graph original" to 
the call.

Best,

Albert


On 23/3/19 15:48, Akihisa Yamada wrote:
> Thanks a lot Genaim! Any comment, Albert?
>
> Best,
> Akihisa
>
> On Mar 23, 2019, at 21:46, Samir Genaim <genaim at gmail.com 
> <mailto: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.
>>
>>
>
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20190325/c94fcdfc/attachment.html>