[Termtools] Conflict in ITS

[Akihisa Yamada]

Dear Albert,

are you going to fix this? Probably you only need to add a 
configuration. If it's done, please let me know.

Best,
Akihisa

On 2019/03/25 17:54, Albert Rubio wrote:
> 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
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>