[Termtools] TORPA nondeterminism

[Zantema, H.]

Indeed at several points TORPA tries several attempts of interpretations
and labellings guided by a random generator. As a consequence it is
nondeterministic: at one run it can give another proof than at another
run, if the random generator generates other values. Also it occurs that
at one run it finds a solution and at another run it does not, as seems
to be the case for SRS/Trafo-un17.

Further I did not do any tuning towards computation time, by which
computation time is not a parameter of TORPA. 

I agree that for repeatability of tests nondeterministic behaviour is
undesirable. So I agree with adding the requirement of being
deterministic for all tools for the next competition.

This year's competition is really exciting, with the biggest surprise
the impressive power of Jambox. Joerg: congratulations!

            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749
 

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools