*************************************************************************



         DECLARATIVE DEBUGGER FOR FUNCTIONAL LOGIC PROGRAMS .



*************************************************************************

*************************************************************************
*** help.      -> display menu                                        ***
*** clean.     -> clean program and specification                     ***
*** loadprg.   -> read in program to be corrected from file           ***
*** loadspe.   -> load specification of the semantics from file       ***
*** listprg.   -> display program                                     ***
*** listspe.   -> display specification                               ***
*** debugger.  -> run debugger                                        ***
*** save.      -> save program to file                                ***
*** exit.      -> leave program                                       ***
*************************************************************************

>> loadprg.

Write the name of the program: 'oddprg2.pl'.
Program loaded.

>> loadspe.

Write the name of the program: 'oddspe2.pl'.

Specification loaded.

>> listprg.


**********************************************
***            DISPLAY PROGRAM.            ***
**********************************************

odd(0) = true.

odd(s(_4543)) = odd(_4543).


**********************************************
**********************************************


>> listspe.


********************************************
***         DISPLAY SPECIFICATION.       ***
********************************************

even(0) = true.

even(s(s(_5086))) = even(_5086).

odd(s(_5107)) = true :- even(_5107) = true.
.


********************************************
********************************************


>> debugger.



************************************************
       NARROWING STRATEGY  OPTION
************************************************

1. Basic Narrowing.
2. Leftmost-Innermost Narrowing.
3. Leftmost-Outermost Narrowing.
4. Needed Narrowing.

Introduce the option: 2.



************************************************
***          OVER APPROXIMATION I+           ***
************************************************

odd(s(0)) = true.
odd(s(s(s(_10482)))) = true.
even(s(s(_10459))) = _10474.
even(0) = true.
odd(_10429) = odd(_10429).
s(_10414) = s(_10414).
0 = 0.
even(_10390) = even(_10390).
true = true.

************************************************
************************************************


The Over Approximation I(+) has been computed with 3 iterations.

Enter the number K of iterations for computing I(-) : 3.


************************************************
***          UNDER APPROXIMATION I-          ***
************************************************

odd(s(s(s(s(s(0)))))) = true.
odd(s(s(s(s(s(s(s(0)))))))) = true.
even(s(s(s(s(s(s(_26929))))))) = even(_26929).
even(s(s(s(s(0))))) = true.
odd(s(0)) = true.
odd(s(s(s(0)))) = true.
even(s(s(s(s(_26825))))) = even(_26825).
even(s(s(0))) = true.
even(s(s(_26775))) = even(_26775).
even(0) = true.
odd(_26731) = odd(_26731).
s(_26716) = s(_26716).
0 = 0.
even(_26692) = even(_26692).
true = true.

************************************************
************************************************



************************************************
***                TR(I-)                    ***
************************************************

s(_35872) = s(_35872).
0 = 0.
odd(_35848) = odd(_35848).
true = true.
odd(s(_35820)) = odd(_35820).
odd(0) = true.

************************************************
************************************************


************************************************
***                  ERRORS                  ***
************************************************

Incorrect equation: odd(0) = true.
Incorrect rule: odd(0) = true.


Incorrect equation: odd(s(_37368)) = odd(_37368).
Incorrect rule: odd(s(_37368)) = odd(_37368).


                 CORRECTION OPTIONS              
************************************************
1.   Automatic correction. 
2.   Manual correction. 
     Enter option: 1.

************************************************
***           EXAMPLE GENERATION             ***
************************************************

Enter a list of ground constructors 
|: [0,s(0)].

************************************************
***             Positive Examples            ***
************************************************
even(s(s(s(s(s(s(0))))))) = true.
odd(s(s(s(s(s(0)))))) = true.
odd(s(s(s(s(s(s(s(0)))))))) = true.
even(s(s(s(s(0))))) = true.
odd(s(0)) = true.
odd(s(s(s(0)))) = true.
even(s(s(0))) = true.
even(0) = true.

************************************************
************************************************

************************************************
***            Negative Examples             ***
************************************************

odd(0) = true.
odd(s(s(0))) = true.

************************************************
************************************************
........ 
The positive example even(0) = true is not covered by the program R 
1.   Eliminate
2.   Recompute I(-)
3.   Calculate new set of positive examples
     Enter option: 1.
The positive example even(s(s(0))) = true is not covered by the program R 
1.   Eliminate
2.   Recompute I(-)
3.   Calculate new set of positive examples
     Enter option: 1.
The positive example even(s(s(s(s(0))))) = true is not covered by the program R 1.   Eliminate
2.   Recompute I(-)
3.   Calculate new set of positive examples
     Enter option: 1.
The positive example even(s(s(s(s(s(s(0))))))) = true is not covered by the program R 
1.   Eliminate
2.   Recompute I(-)
3.   Calculate new set of positive examples
     Enter option: 1.
************************************************
***      Positive Examples covered by R      ***
************************************************

odd(s(s(s(0)))) = true.
odd(s(0)) = true.
odd(s(s(s(s(s(s(s(0)))))))) = true.
odd(s(s(s(s(s(0)))))) = true.

************************************************
************************************************

The correction is 

odd(s(0)) = true.
odd(s(s(_151706))) = odd(_151706).