program torpa(input,output); { This is the source of the Pascal version of the program TORPA for proving termination of string rewriting. This code has been written by Hans Zantema in 2003/2004. This version accepts the TPDB format and follows the guidelines of the competition of termination tools of WST04. This is version 1.3 from May 14, 2004 For documentation see http://www.win.tue.nl/~hzantema/torpa.html } const maxrule = 1000; maxnaam = 100; maxresult = 1000; maxlen = 20; maxautom = 1000; maxloop = 100; var l,lw,r,rw,lbu,rbu,lq,rq,lorig,rorig : array[1..maxrule,1..maxlen] of byte; strict, strictq,strictw,strbu,strictorig : array[1..maxrule] of boolean; stappen,hib,whib,qhib,naamhib,nwhib,nqhib,norighib,orighib ,nror : integer; naam,naamw,naamq,naamorig : array[1..maxnaam] of string; unlab : array[1..maxrule] of integer; verbose, sn, stoplab, remrules, qm, revers, rev2, remov, allstrict, loopfound : boolean; c,preced : string; resul : array[1..maxresult] of string; rtel,rtbu,i : integer; function inttostr(i : integer): string; var n : integer; s : string; procedure schr(j : integer); begin if j = 0 then s := s + '0'; if j = 1 then s := s + '1'; if j = 2 then s := s + '2'; if j = 3 then s := s + '3'; if j = 4 then s := s + '4'; if j = 5 then s := s + '5'; if j = 6 then s := s + '6'; if j = 7 then s := s + '7'; if j = 8 then s := s + '8'; if j = 9 then s := s + '9'; end; begin s := ''; n := i; if n > 99 then begin schr(n div 100); n := n mod 100; end; if (s <> '') or ((n div 10) > 0) then schr(n div 10); schr(n mod 10); inttostr := s; end; function nr(c : string) : integer; var i,r : integer; begin i := 0; while i < naamhib do begin i := i + 1; if naam[i] = c then begin r := i; i := naamhib + 1 end; end; if i = naamhib then begin naamhib := naamhib + 1; naam[naamhib] := c; r := naamhib; end; nr := r; end; procedure srstoq; begin lq := l; rq := r; qhib := hib; strictq := strict; naamq := naam; nqhib := naamhib; end; procedure qtosrs; begin l := lq; r := rq; hib := qhib; strict := strictq; naam := naamq; naamhib := nqhib; end; procedure srstoorig; begin lorig := l; rorig := r; orighib := hib; strictorig := strict; naamorig := naam; norighib := naamhib; end; procedure origtosrs; begin l := lorig; r := rorig; hib := orighib; strict := strictorig; naam := naamorig; naamhib := norighib; end; procedure srstow; begin lw := l; rw := r; whib := hib; strictw := strict; naamw := naam; nwhib := naamhib; end; procedure wtosrs; begin l := lw; r := rw; hib := whib; strict := strictw; naam := naamw; naamhib := nwhib; end; function schrijfregel(i:integer):string; var s : string; j : integer; begin s := ''; j := 1; while lw[i,j] <> 0 do begin s := s+naamw[lw[i,j]]+' '; j := j+1 end; if strictw[i] then s := s + ' -> ' else s := s + ' ->= '; j := 1; while rw[i,j] <> 0 do begin s := s+naamw[rw[i,j]]+' '; j := j+1 end; if j = 1 then s := s + 'e'; schrijfregel := s; end; procedure schrijf(s : string); begin rtel := rtel + 1; if rtel < maxresult then resul[rtel] := s; end; procedure lees; var c : char; symt,j,t : integer; s,nm : string; function nextsym : char; begin if symt < length(s) then symt := symt + 1 else begin readln(s); symt := 1; end; nextsym := s[symt]; if length(s) = 0 then nextsym := ' '; end; {nextsym} procedure leesnaam; begin c := nextsym; while c = ' ' do c := nextsym; if not(c in [',','-',')']) then begin nm := c; c := nextsym; while not(c in [' ',',','-',')']) do begin nm := nm + c; c := nextsym end; if c <> ' ' then begin c := ' '; symt := symt -1 end; end; end; {leesnaam} begin {lees} readln(s); symt := 0; allstrict := true; rtel := 0; naamhib := 0; hib := 0; while nextsym <> 'S' do; c := ' '; while c <> ')' do begin leesnaam; if not (c in [',',')']) then begin hib := hib + 1; strict[hib] := true; t := 0; while c <> '-' do begin t := t + 1; l[hib,t] := nr(nm); leesnaam; end; c := nextsym; l[hib,t+1] := 0; t := 0; leesnaam; while not(c in [',',')']) do begin t := t + 1; r[hib,t] := nr(nm); leesnaam; end; r[hib,t+1] := 0; end; end; srstoorig; schrijf('TORPA 1.3 is applied to the string rewriting system'); srstow; for j := 1 to whib do schrijf(schrijfregel(j)); nror := hib; end; {lees} procedure rev; var i,j,k,t : integer; begin for i := 1 to whib do begin j := 1; while lw[i,j] > 0 do j := j+1; j := j-1; k := 1; while j > k do begin t := lw[i,j]; lw[i,j] := lw[i,k]; lw[i,k] := t; j := j-1; k := k+ 1; end; j := 1; while rw[i,j] > 0 do j := j+1; j := j-1; k := 1; while j > k do begin t := rw[i,j]; rw[i,j] := rw[i,k]; rw[i,k] := t; j := j-1; k := k+ 1; end; end; end; procedure depp; var i,j,k,hibor : integer; def : array[1..maxnaam] of boolean; cap : array[1..maxnaam] of integer; begin for i := 1 to naamhib do def[i] := false; for i := 1 to hib do def[l[i,1]] := true; hibor := hib; for i := 1 to naamhib do if def[i] then begin naamhib := naamhib +1; cap[i] := naamhib; if (length(naam[i]) = 1) and (naam[i][1] in ['a'..'z']) then naam[naamhib] := chr(ord(naam[i][1]) + ord('A') - ord('a')) else naam[naamhib] := '#'+naam[i]; end; for i := 1 to hibor do begin j := 1; while r[i,j] > 0 do begin if def[r[i,j]] then begin hib := hib +1; strict[hib] := true{was: strict[i], maar dat is niet correct}; l[hib,1] := cap[l[i,1]]; k := 2; while l[i,k] >0 do begin l[hib,k] := l[i,k]; k := k+1; end; l[hib,k] := 0; k := j; r[hib,1] := cap[r[i,k]]; k := k+1; while r[i,k] >0 do begin r[hib,k-j+1] := r[i,k]; k := k+1; end; r[hib,k-j+1] := 0; end; j := j+1; end; end; for i := 1 to hibor do strict[i] := false; end; {depp} procedure rpo; var t,i,j,k : integer; procedure rpo2; var doetmee : array [1..maxnaam] of boolean; gr : array [1..maxnaam,1..maxnaam] of boolean; i,j,n,m,mbu: integer; uitg : boolean; function recpo : boolean; var i,li,ri : integer; ok : boolean; function emb : boolean; var lj,rj:integer; begin lj := li+1; rj := ri; while (lw[i,lj] > 0) and (rw[i,rj] > 0) do if lw[i,lj] = rw[i,rj] then begin lj:=lj+1; rj:=rj+1 end else lj := lj+1; emb := (rw[i,rj] = 0); end; function neq(i : integer):boolean; var p : integer; begin p := 1; while (lw[i,p]>0) and (lw[i,p] = rw[i,p]) do p := p+1; neq := (lw[i,p] <> rw[i,p]); end; begin {recpo2} ok := true; for i := 1 to whib do begin li := 1; ri := 1; if lw[i,li] = 0 then if strictw[i] or (rw[i,ri] > 0) then ok := false; if strictw[i] or neq(i) then while ok and (rw[i,ri] > 0) and not emb do if lw[i,li] = rw[i,ri] then begin li:=li+1;ri:=ri+1; if lw[i,li] = 0 then ok := false; end else begin if not gr[lw[i,li],rw[i,ri]] then preced := preced + ' ' + naamw[lw[i,li]]+'>'+ naamw[rw[i,ri]]; gr[lw[i,li],rw[i,ri]] := true; ri := ri +1; end; end; recpo := ok; end; begin {rpo2} preced := ''; n := nwhib; for i := 1 to n do for j := 1 to n do gr[i,j] := false; if recpo then begin for i := 1 to n do doetmee[i] := true; m := n; mbu := n+1; while m < mbu do begin mbu := m; m := 0; for i := 1 to n do if doetmee[i] then begin uitg := false; for j := 1 to n do if doetmee[j] and gr[i,j] then uitg := true; if uitg then m := m+1 else doetmee[i] := false; end; end; {if m > 0 then canvas.textout(0,0,'niet SN');} if m = 0 then sn := true; end {else canvas.textout(0,0,'loop')}; end; procedure rpo3; begin revers := false; rpo2; if not sn then begin revers := true; rev; rpo2; rev; end; end; begin{rpo} rpo3; t := 0; lbu := lw; rbu := rw; strbu := strictw; while (not sn) and (t < nwhib) do begin t := t + 1; for k := 1 to whib do begin i := 1; j := 1; while lbu[k,i] >0 do if lbu[k,i] = t then i := i+1 else begin lw[k,j] := lbu[k,i]; i := i+1; j := j+1; end; lw[k,j] := 0; i := 1; j := 1; while rbu[k,i] >0 do if rbu[k,i] = t then i := i+1 else begin rw[k,j] := rbu[k,i]; i := i+1; j := j+1; end; rw[k,j] := 0; end; rpo3; preced := preced + ', after removing '+ naamw[t]; end; lw := lbu; rw := rbu; strictw := strbu; end; function rrr : boolean; var doetmee,tien,decr : array[1..maxrule] of boolean; doetmeeran : array[1..maxrule] of integer; tel,n,i : integer; fd,r : boolean; s : string; function ok : boolean; var i,j : integer; found : boolean; begin found := false; j := 1; while j <= whib do begin i := 1; tel := 0; while lw[j,i] > 0 do begin if doetmee[lw[j,i]] then tel := tel+1; i := i+1 end; i := 1; while rw[j,i] > 0 do begin if doetmee[rw[j,i]] then tel := tel-1; i := i+1 end; if tel < 0 then j := whib + 2; if tel = 0 then decr[j] := false; if tel > 0 then begin decr[j] := true; found := true; end; j := j+1; end; ok := (j = whib + 1) and found; end; {ok} function okran : boolean; var i,j,tel : integer; found : boolean; begin found := false; j := 1; while j <= whib do begin i := 1; tel := 0; while lw[j,i] > 0 do begin tel := tel + doetmeeran[lw[j,i]]; i := i+1 end; i := 1; while rw[j,i] > 0 do begin tel := tel - doetmeeran[rw[j,i]]; i := i+1 end; if tel < 0 then j := whib + 2; if tel = 0 then decr[j] := false; if tel > 0 then begin decr[j] := true; found := true; end; j := j+1; end; okran:= (j = whib + 1) and found; end; {okran} function ok2 : boolean; var i,j,l0,l1,r0,r1,dir : integer; ovflow,found : boolean; begin found := false; ovflow := false; j := 1; while j <= whib do begin i := 1; l1 := 1; l0 := 0; {polynoom: l1*X + l0} if r then dir := 1 else begin while lw[j,i] > 0 do i := i+1; i := i-1; dir := -1; end; while (i >0) and (lw[j,i] > 0) do begin if doetmee[lw[j,i]] then l0 := l0 + 1; if tien[lw[j,i]] then begin if l1>10000 then ovflow := true; l0 := 10*l0; l1 := 10* l1; end; i := i + dir; end; i := 1; r1 := 1; r0 := 0; if not r then begin while rw[j,i] > 0 do i := i+1; i := i-1; end; while (i >0) and (rw[j,i] > 0) do begin if doetmee[rw[j,i]] then r0 := r0 + 1; if tien[rw[j,i]] then begin if r1>10000 then ovflow := true; r0 := 10*r0; r1 := 10* r1; end; i := i + dir; end; if ovflow then j := whib + 2 else if r1 > l1 then j := whib + 2 else if r1 < l1 then begin decr[j] := true; found := true; end else if r0 > l0 then j := whib + 2 else if r0 < l0 then begin decr[j] := true; found := true; end else decr[j] := false; j := j+1; end; ok2 := (j = whib + 1) and found; end; {ok2} begin {rrr} fd := false; for tel := 1 to nwhib do doetmee[tel] := true; if ok then fd := true; for n := 1 to nwhib do if not fd then begin for tel := 1 to nwhib + 1 do doetmee[tel] := false; doetmee[n] := true; if ok then fd := true; end; if not fd then for n := 1 to nwhib -1 do for i := n+1 to nwhib do if not fd then begin for tel := 1 to nwhib + 1 do doetmee[tel] := false; doetmee[i] := true; doetmee[n] := true; if ok then fd := true; end; for n := 1 to nwhib do if not fd then begin for tel := 1 to nwhib do doetmee[tel] := true; doetmee[n] := false; if ok then fd := true; end; if not fd then for n := 1 to nwhib -1 do for i := n+1 to nwhib do if not fd then begin for tel := 1 to nwhib + 1 do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; if ok then fd := true; end; if fd then if verbose then begin s := 'Choose polynomial interpretation '; for tel := 1 to nwhib do if doetmee[tel] then s := s + ' ' + naamw[tel]; s := s + ': lambda x.x+1'; tel := 1; while tel <= nwhib do if doetmee[tel] then tel := tel+1 else begin tel := nwhib + 1; s := s + ', rest identity'; end; schrijf(s); end; if not fd then if nwhib < 4 then begin for i := 1 to nwhib + 1 do doetmeeran[nwhib+1] := 0; while (not fd) and (doetmeeran[nwhib+1] = 0) do begin i := 1; doetmeeran[i] := doetmeeran[i] + 1; while doetmeeran[i] = 4 do begin doetmeeran[i] := 0; i := i + 1; doetmeeran[i] := doetmeeran[i] + 1; end; if okran then fd := true; end; if fd and verbose then begin schrijf('Choose polynomial interpretation '); for tel := 1 to nwhib do if doetmeeran[tel] = 0 then schrijf(naamw[tel] + ': identity') else schrijf(naamw[tel] + ': lambda x.x+' + inttostr(doetmeeran[tel])); end; end; for r := false to true do if not fd then begin for n := 1 to nwhib do if not fd then begin for tel := 1 to nwhib do doetmee[tel] := true; doetmee[n] := false; for tel := 1 to nwhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ': lambda x.10x, rest lambda x.x+1'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib do for i := 1 to nwhib do if not fd then if i <> n then begin for tel := 1 to nwhib do doetmee[tel] := false; doetmee[i] := true; for tel := 1 to nwhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ': lambda x.10x, ' + naamw[i] + ': lambda x.x+1'; if nwhib >2 then s := s + ', rest identity'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib do for i := 1 to nwhib do if not fd then if i <> n then begin for tel := 1 to nwhib do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; for tel := 1 to nwhib do tien[tel] := false; tien[n] := true; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ': lambda x.10x, ' + naamw[i] + ': identity, rest lambda x.x+1'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib - 1 do for i := n+1 to nwhib do if not fd then begin for tel := 1 to nwhib do doetmee[tel] := true; doetmee[i] := false; doetmee[n] := false; for tel := 1 to nwhib do tien[tel] := false; tien[n] := true; tien[i] := true; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ' and ' + naamw[i] + ': lambda x.10x, rest lambda x.x+1'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib do if not fd then begin for tel := 1 to nwhib do doetmee[tel] := false; doetmee[n] := true; for tel := 1 to nwhib do tien[tel] := true; tien[n] := false; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib - 1 do for i := n+1 to nwhib do if not fd then begin for tel := 1 to nwhib do doetmee[tel] := false; doetmee[n] := true; doetmee[i] := true; for tel := 1 to nwhib do tien[tel] := true; tien[i] := false; tien[n] := false; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ' and ' + naamw[i] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; end; for r := false to true do if not fd then begin for n := 1 to nwhib do for i := 1 to nwhib do if not fd then if n <> i then begin for tel := 1 to nwhib do doetmee[tel] := false; doetmee[i] := true; for tel := 1 to nwhib do tien[tel] := true; tien[i] := false; tien[n] := false; if ok2 then begin fd := true; if verbose then begin if r then schrijf('Reverse every lhs and rhs of the system and choose polynomial interpretation:') else schrijf('Choose polynomial interpretation:'); s := naamw[n] + ': identity, ' + naamw[i] + ': lambda x.x+1, rest lambda x.10x'; schrijf(s); end; end; end; end; {end of all rrr cases} if fd then begin if verbose then for i := 1 to whib do if decr[i] then schrijf('remove: ' + schrijfregel(i)); n := 0; for tel := 1 to whib do if not decr[tel] then begin n := n+1; lw[n] := lw[tel]; rw[n] := rw[tel]; unlab[n] := unlab[tel]; strictw[n] := strictw[tel]; end; whib := n; end; rrr := fd; end; {rrr} procedure dptekst; var i : integer; begin schrijf('Dependency pair transformation:'); for i := 1 to whib do schrijf(' ' + schrijfregel(i)); end; procedure remredr; var i : integer; term : boolean; begin while rrr do; term := true; for i := 1 to whib do if strictw[i] then term := false; if term then begin sn := true; remrules := false; if verbose then if whib = 0 then schrijf('Terminating since no rules remain.') else schrijf('Relatively terminating since no strict rules remain.'); end else if verbose then begin if whib = 1 then schrijf('Remaining rule:') else {schrijf('Remaining '+inttostr(whib)+' rules:');} schrijf('Remaining rules:'); for i := 1 to whib do begin schrijf(' '+schrijfregel(i)); end; end; end; procedure printrpo; begin schrijf(''); if revers then begin schrijf('Terminating since rev(l) > rev(r) for all rules l -> r'); schrijf('where > is the recursive path order with precedence:'); end else schrijf('Terminating by recursive path order with precedence:'); schrijf(preced); end; procedure semlab; var intp : array[1..maxnaam] of byte; ok,rl,rr,rulesrem,b : boolean; i,j,n,hibs : integer; lbs,rbs : array[1..maxrule,1..maxlen] of byte; unlabs : array[1..maxrule] of integer; strbs,doetmee : array[1..maxrule] of boolean; s : string; function res(k : byte;c : boolean):boolean; begin if k = 0 then res := c else if k = 1 then res := false else if k = 2 then res := true else res := not(c); end;{res} begin {semlab} ok := false; while not ok do begin for i := 1 to naamhib do if qm then intp[i] := random(3) else intp[i] := random(4); ok := true; whib := 0; for i := 1 to hib do for b := false to true do begin whib := whib + 1; strictw[whib] := strict[i]; unlab[whib] := i; rl := b; j := 1; while l[i,j] > 0 do j := j+1; lw[whib,j] := 0; while j > 1 do begin j := j-1; if rl then lw[whib,j] := l[i,j] else lw[whib,j] := l[i,j]+naamhib; rl := res(intp[l[i,j]],rl); end; rr := b; j := 1; while r[i,j] > 0 do j := j+1; rw[whib,j] := 0; while j > 1 do begin j := j-1; if rr then rw[whib,j] := r[i,j] else rw[whib,j] := r[i,j]+naamhib; rr := res(intp[r[i,j]],rr); end; if qm then ok := ok and (rl or (not rr)) else ok := ok and (rl = rr); end; end; {while not ok} if qm then for i := 1 to naamhib do begin whib := whib +1; strictw[whib] := false; unlab[whib] := 0; lw[whib,1] := i; rw[whib,1] := i + naamhib; lw[whib,2] := 0; rw[whib,2] := 0; end; hibs := whib; for i := 1 to whib do for j := 1 to maxlen do begin lbs[i,j] := lw[i,j]; rbs[i,j] := rw[i,j]; strbs[i] := strictw[i]; unlabs[i] := unlab[i]; end; remredr; rpo; stoplab := sn; if remov then if ((not sn) and (whib >0)) then begin for i := 1 to hib do doetmee[i] := false; for i := 1 to whib do if unlab[i] > 0 then doetmee[unlab[i]] := true; stoplab := false; for i := 1 to hib do if not doetmee[i] then stoplab := true; end; if stoplab then begin if whib <> hibs then rulesrem := true else rulesrem := false; whib := hibs; for i := 1 to whib do begin for j := 1 to maxlen do begin lw[i,j] := lbs[i,j]; rw[i,j] := rbs[i,j]; end; strictw[i] := strbs[i]; unlab[i] := unlabs[i]; end; schrijf(''); if rev2 then begin schrijf('Reverse every lhs and rhs of the system.'); schrijf(''); end; schrijf('Apply labelling with the following interpretation in {0,1}:'); for i := 1 to naamhib do if intp[i] = 0 then schrijf(' '+ naam[i] + ': identity') else if intp[i] = 3 then schrijf(' '+ naam[i] + ': lambda x.1-x') else if intp[i] = 2 then schrijf(' '+ naam[i] + ': constant 1') else if intp[i] = 1 then schrijf(' '+ naam[i] + ': constant 0'); schrijf('and label every symbol by the value of its argument.'); schrijf(''); {schrijf('found after '+inttostr(n)+' attempts');} if qm then schrijf('This is a quasi-model for 1 > 0.') else schrijf('This interpretation is a model.'); schrijf(''); schrijf('Labelled system:'); for i := 1 to whib do schrijf(' '+schrijfregel(i)); schrijf(''); if rulesrem then begin verbose := true; remredr; verbose := false; end; if remrules and sn then printrpo; end; end; procedure semlab2; var n : integer; begin if not stoplab then begin qm := false; n := 0; while (n < stappen) and (not stoplab) do begin n := n+1; semlab; end; end; if not stoplab then begin qm := true; n := 0; while (n < stappen) and not stoplab do begin n := n+1; semlab; end; end; end; procedure semlab3; var i : integer; begin for i := 1 to naamhib do {naam[naamhib+i] := chr(ord(naam[i]) + ord('A') - ord('a'));} begin naamw[i] := naam[i]+'1 '; naamw[naamhib+i] := naam[i]+'0 '; end; nwhib := 2* naamhib; rev2 := false; semlab2; if not stoplab then begin lw := l; rw := r; whib := hib; rev; l := lw; r := rw; rev2 := true; semlab2; end; if not stoplab then begin lw := l; rw := r; whib := hib; rev; l := lw; r := rw; end; end; procedure total; var i,n : integer; doetmee : array [1..maxrule] of boolean; begin stoplab := true; while (stoplab and (not sn)) do begin stoplab := false; remrules := true; whib := hib; for n := 1 to hib do begin lw[n] := l[n]; rw[n] := r[n]; strictw[n] := strict[n]; end; nwhib := naamhib; for i := 1 to nwhib do naamw[i] := naam[i]; remredr; if whib < hib then begin whib := hib; for n := 1 to hib do begin lw[n] := l[n]; rw[n] := r[n]; strictw[n] := strict[n]; end; nwhib := naamhib; verbose := true; remredr; verbose := false; hib := whib; for n := 1 to hib do begin l[n] := lw[n]; r[n] := rw[n]; strict[n] := strictw[n]; end; end; if not sn then begin rpo; if sn then begin printrpo; end; end; write(''); {MIRACLE: without this dummy it does not work} if not sn then semlab3; if not sn then if stoplab then begin schrijf(''); schrijf('Remove all labels, remaining unlabelled system:'); for i := 1 to hib do doetmee[i] := false; for i := 1 to whib do if unlab[i] > 0 then doetmee[unlab[i]] := true; n := 0; for i := 1 to hib do if doetmee[i] then begin n := n+1; l[n] := l[i]; r[n] := r[i]; strict[n] := strict[i]; end; hib := n; srstow; for i := 1 to whib do schrijf(' '+schrijfregel(i)); end; end; end;{total} procedure matchb; var le,buur,goal,sym,lab : array[1..maxautom] of integer; mb, i, j, ehib, ehibbu, nhib, lijsthib, rulenr,startnode, maxe : integer; lijst : array[1..50,1..maxlen] of integer; templijst : array[1..maxlen] of integer; ovflow : boolean; { le : nodes -> edges (leftmost edge) buur : edges -> edges goal : edges -> nodes sym, lab : edges -> nr } procedure maaklijst(node,symnr: integer); {maakt lijst van alle manieren om lw[rulenr] te doorlopen} var edge,i: integer; begin if lw[rulenr,symnr] = 0 then begin lijsthib := lijsthib + 1; if lijsthib >50 then ovflow := true else begin for i := 1 to symnr do lijst[lijsthib,i] := templijst[i]; lijst[lijsthib,symnr] := 0; {s := 'lijst: '; for i := 1 to symnr-1 do s := s + inttostr(goal[templijst[i]]); schrijf(s); } end end else begin edge := le[node]; while edge > 0 do if sym[edge] = lw[rulenr,symnr] then begin templijst[symnr] := edge; maaklijst(goal[edge],symnr+1); edge := buur[edge]; end else edge := buur[edge]; end; end; {maaklijst} procedure maakpad(lijsti:integer); var minl,endnode,i, maxok,bestj,j,innode, e : integer; procedure zoek(j,node:integer); { zoeknode(j,n) wordt alleen aangeroepen als er een goed pad is van startnode naar n van lengte j-startj} var edge: integer; begin if j > maxok then begin maxok := j; innode := node; end; if rw[rulenr,j] > 0 then begin edge := le[node]; while edge > 0 do begin if (sym[edge] = rw[rulenr,j]) and (lab[edge] = minl) then if (rw[rulenr,j+1] > 0) or (goal[edge] = endnode) then zoek(j+1,goal[edge]); edge := buur[edge]; end; end; end; {zoek} begin {maakpad} minl := 1000; i := 1; while lijst[lijsti,i] > 0 do begin if lab[lijst[lijsti,i]] < minl then minl := lab[lijst[lijsti,i]]; endnode := goal[lijst[lijsti,i]]; i := i+1; end; minl := minl + 1; if minl > mb then mb := minl; maxok := 0; zoek(1,startnode); if rw[rulenr,maxok] > 0 then begin bestj := 0; if rw[rulenr,2] > 0 then for j := 1 to nhib do begin maxok := 0; zoek(2,j); if rw[rulenr,maxok] = 0 then bestj := j; end; if bestj = 0 then {maak pad van startnode naar endnode} begin maxok := 1; e := le[startnode]; while buur[e] > 0 do e := buur[e]; ehib := ehib + 1; if ehib > maxe then ovflow := true; buur[e] := ehib; e := ehib; buur[e] := 0; lab[e] := minl; sym[e] := rw[rulenr,maxok]; while rw[rulenr,maxok+1] > 0 do begin maxok := maxok + 1; nhib := nhib + 1; goal[e] := nhib; ehib := ehib +1; e := ehib; le[nhib] := e; buur[e] := 0; lab[e] := minl; sym[e] := rw[rulenr,maxok]; end; goal[e] := endnode end else {maak edge van startnode naar bestj} begin e := le[startnode]; while buur[e] > 0 do e := buur[e]; ehib := ehib + 1; if ehib > maxe then ovflow := true; buur[e] := ehib; e := ehib; buur[e] := 0; lab[e] := minl; sym[e] := rw[rulenr,1]; goal[e] := bestj; end; end; end; {maakpad} procedure initrfc; var i,j,k,ebu : integer; begin nwhib := nwhib + 1; naamw[nwhib] := '#'; for i := 1 to hib do begin j := 1; while l[i,j+1] > 0 do begin whib := whib + 1; rw[whib] := r[i]; for k := 1 to j do lw[whib,k] := l[i,k]; lw[whib,j+1] := nwhib; lw[whib,j+2] := 0; j := j+1; end; end; nhib := 2; ehib := 1; le[2] := 1; goal[1] := 2; lab[1] := 0; sym[1] := nwhib; buur[1] := 0; le[1] := 2; for i := 1 to hib do begin j := 1; while r[i,j] > 0 do begin ehib := ehib + 1; sym[ehib] := r[i,j]; lab[ehib] := 0; if j = 1 then ebu := ehib; buur[ehib] := 0; if r[i,j+1] = 0 then goal[ehib] := 2 else begin nhib := nhib + 1; goal[ehib] := nhib; le[nhib] := ehib + 1; end; j := j+1; end; if i < hib then buur[ebu] := ehib + 1; end; end; {initrfc} begin {matchb} srstow; ovflow := false; mb := 0; initrfc; { versie voor Sigma* ipv RFC nhib := 1; ehib := nwhib; le[1] := 1; for i := 1 to nwhib do begin if i < nwhib then buur[i] := i+1 else buur[i] := 0; goal[i] := 1; sym[i] := i; lab[i] := 0; end; } maxe := 800; ehibbu := 0; while (not ovflow) and (ehibbu < ehib) do begin ehibbu := ehib; for rulenr := 1 to whib do for startnode := 1 to nhib do begin lijsthib := 0; maaklijst(startnode,1); for i := 1 to lijsthib do if not ovflow then maakpad(i); end; end; if not ovflow then begin sn := true; schrijf(''); schrijf('Terminating due to RFC match bound '+inttostr(mb)+','); schrijf('proved by the automaton defined by'); schrijf('initial state = 1, final state = 2, transitions:'); for j := 1 to nhib do begin i := le[j]; while i > 0 do begin schrijf('from '+inttostr(j)+' to '+inttostr(goal[i])+ ', label: '+naamw[sym[i]]+inttostr(lab[i])); i := buur[i]; end; end; end; end; {matchb} procedure experhs; {expand empty rhs, from q to srs} var erhs : boolean; i,j,k : integer; begin erhs := false; for i := 1 to qhib do if rq[i][1] = 0 then erhs := true; if erhs then begin schrijf('Expand empty rhs:'); hib := 0; for i := 1 to qhib do if rq[i][1] > 0 then begin hib := hib + 1; l[hib] := lq[i]; r[hib] := rq[i]; strict[hib] := true; end else for j := 1 to nqhib do begin hib := hib + 1; k := 1; while lq[i][k] > 0 do begin l[hib][k] := lq[i][k]; k := k+1 end; l[hib][k] := j; l[hib][k+1] := 0; r[hib][1] := j; r[hib][2] := 0; strict[hib] := true; end; srstow; for j := 1 to whib do schrijf(' '+schrijfregel(j)); rtbu := rtel; srstoq; end else qtosrs; end; {experhs} function strip : boolean; var i,j : integer; begin if hib > 1 then strip := false else if l[1,2] = 0 then strip := false else if r[1,2] = 0 then strip := false else if l[1,1] = r[1,1] then begin schrijf('Strip first symbol, yielding the rule'); i := 1; while l[1,i] > 0 do begin l[1,i] := l[1,i+1]; i := i+1; end; i := 1; while r[1,i] > 0 do begin r[1,i] := r[1,i+1]; i := i+1; end; srstow; schrijf(' '+schrijfregel(1)); strip := true; end else begin i := 1; while l[1,i+1] > 0 do i := i+1; j := 1; while r[1,j+1] > 0 do j := j+1; if l[1,i] <> r[1,j] then strip := false else begin l[1,i] := 0; r[1,j] := 0; srstow; schrijf('Strip last symbol, yielding the rule'); schrijf(' '+schrijfregel(1)); strip := true; end; end; end; procedure loopch; var v : array[1..maxloop,1..20] of integer; nieuw : array[1..40] of integer; e : array[0..maxloop,1..maxloop] of boolean; vhib,vhibu, i,j,k,vi,ri : integer; s : string; procedure testloop; var i,j,m,mbu : integer; doetmee : array[1..maxloop] of boolean; uitg : boolean; begin for i := 1 to vhib do doetmee[i] := true; m := vhib; mbu := vhib+1; while m < mbu do begin mbu := m; m := 0; for i := 1 to vhib do if doetmee[i] then begin uitg := false; for j := 1 to vhib do if doetmee[j] and e[i,j] then uitg := true; if uitg then m := m+1 else doetmee[i] := false; end; end; if m >0 then begin i := 1; while not doetmee[i] do i := i+1; loopfound := true; rtel := nror + 2; s := 'Non-terminating; looping derivation starting in: '; { for i := 1 to vhib do begin if doetmee[i] then s := '* ' else s := ' '; } j:= 1; while v[i,j] > 0 do begin s := s+naam[v[i,j]]; j := j+1; end; schrijf(s); end; end; {testloop} function zoek : integer; var i,j,k : integer; begin i := 1; while i <= vhib do begin j := 1; while (v[i,j] = nieuw[j]) and (nieuw[j] > 0) do j := j+1; if v[i,j] = nieuw[j] then begin k := i; i := vhib + 10; end else i := i+1; end; if i < vhib + 10 then if vhib < maxloop then begin vhib := vhib + 1; j := 1; while nieuw[j] > 0 do begin v[vhib,j] := nieuw[j]; j := j+1; end; v[vhib,j] := 0; k := vhib; end else k := 0; zoek := k; end;{zoek} procedure prob1; {if ri = rule l -> r1 r2, v[vi] = v r1, #v = k, then add (vl,v r1) } var i : integer; begin i := 1; while (v[vi,k+i] = r[ri,i]) and (v[vi,k+i] > 0) do i := i + 1; if v[vi,k+i] = 0 then begin for i := 1 to k do nieuw[i] := v[vi,i]; i := 1; while l[ri,i] > 0 do begin nieuw[k+i] := l[ri,i]; i := i+1; end; nieuw[k+i] := 0; if k+i <= 20 then e[zoek,vi] := true; end; end;{prob1} procedure prob4; {if ri = rule l -> r, v[vi] = w r w', #w = k, then add (wlw',wrw') } var i,j : integer; begin i := 1; while (v[vi,k+i] = r[ri,i]) and (v[vi,k+i] > 0) do i := i + 1; if r[ri,i] = 0 then begin j := k+i; for i := 1 to k do nieuw[i] := v[vi,i]; i := 1; while l[ri,i] > 0 do begin nieuw[k+i] := l[ri,i]; i := i+1; end; while v[vi,j] > 0 do begin nieuw[k+i] := v[vi,j]; i := i+1; j := j+1; end; nieuw[k+i] := 0; if k+i <= 20 then e[zoek,vi] := true; end; end;{prob4} procedure prob2; {if ri = rule l -> r1 r2, v[vi] = r2 v, #r1 = k, then add (lv,r2 v) } var i,j : integer; begin i := 1; while (r[ri,k+i] = v[vi,i]) and (r[ri,k+i] > 0) do i := i + 1; if r[ri,k+i] = 0 then begin j := i; i := 1; while l[ri,i] > 0 do begin nieuw[i] := l[ri,i]; i := i+1; end; while v[vi,j] > 0 do begin nieuw[i] := v[vi,j]; i:=i+1; j:=j+1; end; nieuw[i] := 0; if i <= 20 then e[zoek,vi] := true; end; end;{prob2} procedure prob3; {if ri = rule l -> r1 r2 r3, v[vi] = r2, then add (l,r2) } var i : integer; begin i := 1; while (r[ri,k+i] = v[vi,i]) and (r[ri,k+i] > 0) do i := i + 1; if v[vi,i] = 0 then begin i := 1; while l[ri,i] > 0 do begin nieuw[i] := l[ri,i]; i := i+1; end; nieuw[i] := 0; if i <= 20 then e[zoek,vi] := true; end; end;{prob3} begin {loopch} for i := 1 to hib do for j := 1 to 20 do v[i,j] := l[i,j]; vhib := hib; for i := 1 to maxloop do for j := 1 to maxloop do e[i,j] := false; vhibu := 0; while vhibu < vhib do begin vhibu := vhib; for vi := 1 to vhibu do for ri := 1 to hib do begin k := 0; while v[vi,k+1] > 0 do begin prob1; prob4; k := k + 1; end; k := 0; while r[ri,k+1] > 0 do begin prob2; prob3; k := k + 1; end; end; end; testloop; end;{loopch} procedure total2; begin verbose := false; rtbu := rtel; total; rtbu := rtel; if allstrict and not sn then begin srstoq; depp; srstow; dptekst; total; end; if allstrict and not sn then begin rtel := rtbu; qtosrs; schrijf(''); schrijf('Reverse every lhs and rhs of the system.'); schrijf(''); srstow; rev; wtosrs; depp; srstow; dptekst; total; end; end; {total2} procedure main; begin schrijf(''); sn := false; loopfound := false; stappen := 0; total2; if allstrict and not sn then begin rtel := rtbu; experhs; matchb; end; if allstrict and not sn then begin rtel := rtbu; qtosrs; schrijf(''); schrijf('Reverse every lhs and rhs of the system.'); schrijf(''); srstow; rev; wtosrs; matchb; end; if allstrict and not sn then begin rtel := rtbu; qtosrs; if strip then matchb; end; if allstrict and not sn then begin rtel := rtbu; qtosrs; schrijf(''); schrijf('Reverse every lhs and rhs of the system.'); schrijf(''); srstow; rev; wtosrs; if strip then matchb; end; if not sn then begin qtosrs; loopch; end; if not sn then if not loopfound then begin origtosrs; {writeln('arrived, hib =',hib,' naamhib = ',naamhib); rtel := rtbu;} rtel := nror + 2; stappen := 100; total2; end; if sn then writeln('YES') else if loopfound then writeln('NO') else begin rtel := nror + 2; schrijf('no termination proof found'); end; for i := 1 to rtel do writeln(resul[i]); end; {main} {main program} begin lees; remov := true; main; end.