*************************************************************************
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: 'noemptyprg.pl'.
Program loaded.
>> loadspe.
Write the name of the program: 'noemptyspe.pl'.
Specification loaded.
>> listspe.
********************************************
*** DISPLAY SPECIFICATION. ***
********************************************
noemptyapp([_4539|_4540],[_4537|_4538]) = append([_4539|_4540],[_4537|_4538]).
append([],_4557) = _4557.
append([_4568|_4569],_4572) = [_4568|append(_4569,_4572)].
********************************************
********************************************
>> listprg.
**********************************************
*** DISPLAY PROGRAM. ***
**********************************************
noemptyapp([],[_5239|_5240]) = [_5239|_5240].
noemptyapp([_5261|_5262],[_5259|_5260]) = [_5261|noemptyapp(_5262,[_5259|_5260])].
**********************************************
**********************************************
>> 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+ ***
************************************************
noemptyapp([_10416|_10417],[_10424|_10425]) = [_10416|_10435].
append([_10396|_10387],_10400) = [_10396|_10397].
append([],_10376) = _10376.
noemptyapp([_10343|_10344],[_10341|_10342]) = append([_10343|_10344],[_10341|_10342]).
[] = [].
noemptyapp(_10299,_10300) = noemptyapp(_10299,_10300).
[_10283|_10284] = [_10283|_10284].
append(_10270,_10271) = append(_10270,_10271).
************************************************
************************************************
The Over Approximation I(+) has been computed with 3 iterations.
Enter the number K of iterations for computing I(-) : 1.
************************************************
*** UNDER APPROXIMATION I- ***
************************************************
append([_16267|_16265],_16271) = [_16267|append(_16265,_16271)].
append([],_16234) = _16234.
noemptyapp([_16201|_16202],[_16199|_16200]) = append([_16201|_16202],[_16199|_16200]).
[] = [].
noemptyapp(_16157,_16158) = noemptyapp(_16157,_16158).
[_16141|_16142] = [_16141|_16142].
append(_16128,_16129) = append(_16128,_16129).
************************************************
************************************************
************************************************
*** TR(I-) ***
************************************************
[] = [].
noemptyapp(_21648,_21649) = noemptyapp(_21648,_21649).
[_21632|_21633] = [_21632|_21633].
noemptyapp([_21616|_21614],[_21611|_21612]) = [_21616|noemptyapp(_21614,[_21611|_21612])].
noemptyapp([],[_21575|_21576]) = [_21575|_21576].
************************************************
************************************************
************************************************
*** ERRORS ***
************************************************
Incorrect equation: noemptyapp([],[_23801|_23802]) = [_23801|_23802].
Incorrect rule: noemptyapp([],[_23801|_23802]) = [_23801|_23802].
CORRECTION OPTIONS
************************************************
1. Automatic correction.
2. Manual correction.
Enter option: 1.
************************************************
*** EXAMPLE GENERATION ***
************************************************
Enter a list of ground constructors
|: [[a],[a,a]].
************************************************
*** Positive Examples ***
************************************************
noemptyapp([[a,a],a,a],[[a,a],a,a]) = [[a,a],a,a,[a,a],a,a].
noemptyapp([[a,a],a,a],[[a,a],a]) = [[a,a],a,a,[a,a],a].
noemptyapp([[a,a],a,a],[[a],a,a]) = [[a,a],a,a,[a],a,a].
noemptyapp([[a,a],a,a],[[a],a]) = [[a,a],a,a,[a],a].
noemptyapp([[a],a,a],[[a,a],a,a]) = [[a],a,a,[a,a],a,a].
noemptyapp([[a],a,a],[[a,a],a]) = [[a],a,a,[a,a],a].
noemptyapp([[a],a,a],[[a],a,a]) = [[a],a,a,[a],a,a].
noemptyapp([[a],a,a],[[a],a]) = [[a],a,a,[a],a].
append([a,a],[a]) = [a,a,a].
append([a,a],[a,a]) = [a,a,a,a].
noemptyapp([[a],a],[[a],a]) = [[a],a,[a],a].
noemptyapp([[a],a],[[a],a,a]) = [[a],a,[a],a,a].
noemptyapp([[a],a],[[a,a],a]) = [[a],a,[a,a],a].
noemptyapp([[a],a],[[a,a],a,a]) = [[a],a,[a,a],a,a].
noemptyapp([[a,a],a],[[a],a]) = [[a,a],a,[a],a].
noemptyapp([[a,a],a],[[a],a,a]) = [[a,a],a,[a],a,a].
noemptyapp([[a,a],a],[[a,a],a]) = [[a,a],a,[a,a],a].
noemptyapp([[a,a],a],[[a,a],a,a]) = [[a,a],a,[a,a],a,a].
append([[a],a,a],[a]) = [[a],a,a,a].
append([[a],a,a],[a,a]) = [[a],a,a,a,a].
append([[a,a],a,a],[a]) = [[a,a],a,a,a].
append([[a,a],a,a],[a,a]) = [[a,a],a,a,a,a].
append([[a,a],a],[a,a]) = [[a,a],a,a,a].
append([[a,a],a],[a]) = [[a,a],a,a].
append([[a],a],[a,a]) = [[a],a,a,a].
append([[a],a],[a]) = [[a],a,a].
append([a],[a,a]) = [a,a,a].
append([a],[a]) = [a,a].
append([],[a,a]) = [a,a].
append([],[a]) = [a].
************************************************
************************************************
************************************************
*** Negative Examples ***
************************************************
noemptyapp([],[[a],a]) = [[a],a].
noemptyapp([],[[a],a,a]) = [[a],a,a].
noemptyapp([],[[a,a],a]) = [[a,a],a].
noemptyapp([],[[a,a],a,a]) = [[a,a],a,a].
************************************************
************************************************
........
The positive example append([],[a]) = [a] 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 append([],[a,a]) = [a,a] 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 append([a],[a]) = [a,a] 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 append([a],[a,a]) = [a,a,a] 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 append([[a],a],[a]) = [[a],a,a] 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 append([[a],a],[a,a]) = [[a],a,a,a] 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 append([[a,a],a],[a]) = [[a,a],a,a] 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 append([[a,a],a],[a,a]) = [[a,a],a,a,a] 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 append([[a,a],a,a],[a,a]) = [[a,a],a,a,a,a] 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 append([[a,a],a,a],[a]) = [[a,a],a,a,a] 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 append([[a],a,a],[a,a]) = [[a],a,a,a,a] 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 append([[a],a,a],[a]) = [[a],a,a,a] 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 append([a,a],[a,a]) = [a,a,a,a] 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 append([a,a],[a]) = [a,a,a] 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 ***
************************************************
noemptyapp([[a,a],a],[[a,a],a,a]) = [[a,a],a,[a,a],a,a].
noemptyapp([[a,a],a],[[a,a],a]) = [[a,a],a,[a,a],a].
noemptyapp([[a,a],a],[[a],a,a]) = [[a,a],a,[a],a,a].
noemptyapp([[a,a],a],[[a],a]) = [[a,a],a,[a],a].
noemptyapp([[a],a],[[a,a],a,a]) = [[a],a,[a,a],a,a].
noemptyapp([[a],a],[[a,a],a]) = [[a],a,[a,a],a].
noemptyapp([[a],a],[[a],a,a]) = [[a],a,[a],a,a].
noemptyapp([[a],a],[[a],a]) = [[a],a,[a],a].
noemptyapp([[a],a,a],[[a],a]) = [[a],a,a,[a],a].
noemptyapp([[a],a,a],[[a],a,a]) = [[a],a,a,[a],a,a].
noemptyapp([[a],a,a],[[a,a],a]) = [[a],a,a,[a,a],a].
noemptyapp([[a],a,a],[[a,a],a,a]) = [[a],a,a,[a,a],a,a].
noemptyapp([[a,a],a,a],[[a],a]) = [[a,a],a,a,[a],a].
noemptyapp([[a,a],a,a],[[a],a,a]) = [[a,a],a,a,[a],a,a].
noemptyapp([[a,a],a,a],[[a,a],a]) = [[a,a],a,a,[a,a],a].
noemptyapp([[a,a],a,a],[[a,a],a,a]) = [[a,a],a,a,[a,a],a,a].
************************************************
************************************************
The correction is
noemptyapp([_87043,_87041],[_87039|_87040]) = [_87043,_87041,_87039|_87040].
noemptyapp([_87019,_87017,_87015,_87013|_87014],[_87011|_87012]) = [_87019,_87017,_87015,_87013|noemptyapp(_87014,[_87011|_87012])].
noemptyapp([_86984,_86982,_86980],[_86978|_86979]) = [_86984,_86982,_86980,_86978|_86979].
noemptyapp([_86956],[_86954|_86955]) = [_86956,_86954|_86955].