*************************************************************************
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: 'playdiceprg.pl'.
Program loaded.
>> loadspe.
Write the name of the program: 'playdicespe.pl'.
Specification loaded.
>> listspe.
********************************************
*** DISPLAY SPECIFICATION. ***
********************************************
playdice(_4535) = double(winningface(_4535)).
winningface(s(0)) = s(0).
winningface(s(s(0))) = s(s(0)).
double(_4580) = sum(_4580,_4580).
sum(_4594,0) = _4594.
sum(_4608,s(_4606)) = s(sum(_4608,_4606)).
********************************************
********************************************
>> listprg.
**********************************************
*** DISPLAY PROGRAM. ***
**********************************************
playdice(_5686) = double(winningface(_5686)).
double(0) = 0.
double(s(_5712)) = s(s(double(_5712))).
winningface(s(_5728)) = s(winningface(_5728)).
winningface(0) = 0.
**********************************************
**********************************************
>> 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+ ***
************************************************
playdice(s(s(0))) = s(_12629).
playdice(s(0)) = s(_12604).
playdice(s(0)) = sum(s(0),s(0)).
playdice(s(s(0))) = sum(s(s(0)),s(s(0))).
double(s(_12499)) = s(_12509).
double(0) = 0.
playdice(s(s(0))) = double(s(s(0))).
playdice(s(0)) = double(s(0)).
sum(_12404,s(_12392)) = s(_12402).
sum(_12380,0) = _12380.
double(_12355) = sum(_12355,_12355).
winningface(s(s(0))) = s(s(0)).
winningface(s(0)) = s(0).
playdice(_12281) = double(winningface(_12281)).
sum(_12251,_12252) = sum(_12251,_12252).
0 = 0.
s(_12225) = s(_12225).
playdice(_12212) = playdice(_12212).
winningface(_12197) = winningface(_12197).
double(_12182) = double(_12182).
************************************************
************************************************
The Over Approximation I(+) has been computed with 5 iterations.
Enter the number K of iterations for computing I(-) : 2.
************************************************
*** UNDER APPROXIMATION I- ***
************************************************
double(s(_34813)) = s(sum(s(_34813),_34813)).
sum(_34780,s(s(_34772))) = s(s(sum(_34780,_34772))).
double(0) = 0.
sum(_34712,s(0)) = s(_34712).
playdice(s(s(0))) = double(s(s(0))).
playdice(s(0)) = double(s(0)).
sum(_34624,s(_34620)) = s(sum(_34624,_34620)).
sum(_34587,0) = _34587.
double(_34562) = sum(_34562,_34562).
winningface(s(s(0))) = s(s(0)).
winningface(s(0)) = s(0).
playdice(_34488) = double(winningface(_34488)).
sum(_34458,_34459) = sum(_34458,_34459).
0 = 0.
s(_34432) = s(_34432).
playdice(_34419) = playdice(_34419).
winningface(_34404) = winningface(_34404).
double(_34389) = double(_34389).
************************************************
************************************************
************************************************
*** TR(I-) ***
************************************************
s(_47295) = s(_47295).
0 = 0.
playdice(_47271) = playdice(_47271).
winningface(_47256) = winningface(_47256).
double(_47241) = double(_47241).
winningface(0) = 0.
playdice(0) = double(0).
winningface(s(_47180)) = s(winningface(_47180)).
playdice(s(_47149)) = double(s(winningface(_47149))).
double(s(_47114)) = s(s(double(_47114))).
playdice(s(0)) = s(s(double(0))).
playdice(s(s(0))) = s(s(double(s(0)))).
double(0) = 0.
playdice(_46986) = double(winningface(_46986)).
************************************************
************************************************
************************************************
*** ERRORS ***
************************************************
Incorrect equation: playdice(s(_53301)) = double(s(winningface(_53301))).
Incorrect rule: winningface(s(_53301)) = s(winningface(_53301)).
Incorrect equation: winningface(s(_53329)) = s(winningface(_53329)).
Incorrect rule: winningface(s(_53329)) = s(winningface(_53329)).
Incorrect equation: playdice(0) = double(0).
Incorrect rule: winningface(0) = 0.
Incorrect equation: winningface(0) = 0.
Incorrect rule: winningface(0) = 0.
CORRECTION OPTIONS
************************************************
1. Automatic correction.
2. Manual correction.
Enter option: 1.
************************************************
*** EXAMPLE GENERATION ***
************************************************
Enter a list of ground constructors
|: [0,s(0),s(s(0)),s(s(s(0)))].
************************************************
*** Positive Examples ***
************************************************
playdice(s(s(0))) = s(s(s(s(0)))).
double(s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))).
sum(s(s(s(0))),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(s(0)))))))).
sum(s(s(0)),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(0))))))).
sum(s(0),s(s(s(s(s(0)))))) = s(s(s(s(s(s(0)))))).
sum(0,s(s(s(s(s(0)))))) = s(s(s(s(s(0))))).
sum(0,s(s(s(s(0))))) = s(s(s(s(0)))).
sum(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))).
sum(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(0)))))).
sum(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(0))))))).
double(s(s(s(0)))) = s(s(s(s(s(s(0)))))).
playdice(s(0)) = s(s(0)).
double(s(s(0))) = s(s(s(s(0)))).
sum(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(0)))))).
sum(s(s(0)),s(s(s(0)))) = s(s(s(s(s(0))))).
sum(s(0),s(s(s(0)))) = s(s(s(s(0)))).
sum(0,s(s(s(0)))) = s(s(s(0))).
double(0) = 0.
sum(0,s(s(0))) = s(s(0)).
sum(s(0),s(s(0))) = s(s(s(0))).
sum(s(s(0)),s(s(0))) = s(s(s(s(0)))).
sum(s(s(s(0))),s(s(0))) = s(s(s(s(s(0))))).
double(s(0)) = s(s(0)).
sum(s(s(s(0))),s(0)) = s(s(s(s(0)))).
sum(s(s(0)),s(0)) = s(s(s(0))).
sum(s(0),s(0)) = s(s(0)).
sum(0,s(0)) = s(0).
sum(s(s(s(0))),0) = s(s(s(0))).
sum(s(s(0)),0) = s(s(0)).
sum(s(0),0) = s(0).
sum(0,0) = 0.
winningface(s(s(0))) = s(s(0)).
winningface(s(0)) = s(0).
************************************************
************************************************
************************************************
*** Negative Examples ***
************************************************
winningface(0) = 0.
playdice(0) = 0.
winningface(s(s(s(0)))) = s(s(s(0))).
winningface(s(s(s(s(0))))) = s(s(s(s(0)))).
playdice(s(s(s(0)))) = s(s(s(s(s(s(0)))))).
playdice(s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))).
************************************************
************************************************
........
The positive example sum(0,0) = 0 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 sum(s(0),0) = s(0) 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 sum(s(s(0)),0) = s(s(0)) 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 sum(s(s(s(0))),0) = s(s(s(0))) 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 sum(0,s(0)) = s(0) 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 sum(s(0),s(0)) = s(s(0)) 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 sum(s(s(0)),s(0)) = s(s(s(0))) 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 sum(s(s(s(0))),s(0)) = s(s(s(s(0)))) 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 sum(s(s(s(0))),s(s(0))) = s(s(s(s(s(0))))) 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 sum(s(s(0)),s(s(0))) = s(s(s(s(0)))) 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 sum(s(0),s(s(0))) = s(s(s(0))) 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 sum(0,s(s(0))) = s(s(0)) 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 sum(0,s(s(s(0)))) = s(s(s(0))) 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 sum(s(0),s(s(s(0)))) = s(s(s(s(0)))) 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 sum(s(s(0)),s(s(s(0)))) = s(s(s(s(s(0))))) 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 sum(s(s(s(0))),s(s(s(0)))) = s(s(s(s(s(s(0)))))) 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 sum(s(s(s(0))),s(s(s(s(0))))) = s(s(s(s(s(s(s(0))))))) 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 sum(s(s(0)),s(s(s(s(0))))) = s(s(s(s(s(s(0)))))) 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 sum(s(0),s(s(s(s(0))))) = s(s(s(s(s(0))))) 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 sum(0,s(s(s(s(0))))) = s(s(s(s(0)))) 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 sum(0,s(s(s(s(s(0)))))) = s(s(s(s(s(0))))) 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 sum(s(0),s(s(s(s(s(0)))))) = s(s(s(s(s(s(0)))))) 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 sum(s(s(0)),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(0))))))) 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 sum(s(s(s(0))),s(s(s(s(s(0)))))) = s(s(s(s(s(s(s(s(0)))))))) 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 ***
************************************************
winningface(s(0)) = s(0).
winningface(s(s(0))) = s(s(0)).
double(s(0)) = s(s(0)).
double(0) = 0.
double(s(s(0))) = s(s(s(s(0)))).
playdice(s(0)) = s(s(0)).
double(s(s(s(0)))) = s(s(s(s(s(s(0)))))).
double(s(s(s(s(0))))) = s(s(s(s(s(s(s(s(0)))))))).
playdice(s(s(0))) = s(s(s(s(0)))).
************************************************
************************************************
The correction is
winningface(s(s(0))) = s(s(0)).
double(s(_269830)) = s(s(double(_269830))).
double(0) = 0.
playdice(_269802) = double(winningface(_269802)).
winningface(s(0)) = s(0).