[Termtools] Bug in TTTbox

Martin Johann Korp Martin.Korp at uibk.ac.at
Wed Aug 23 11:40:53 CEST 2006


Dear all,

Johannes Waldman and Jörg Endrullis found out that the proof of TTTbox at the
competition for the SRS "Waldmann/z086-variant.srs" was not correct. When
TTTbox searches for open paths, it consider only a special subset of states.
The reason for the failure was now that I have forgotten to take the transitive
closure of that subset. With the correct program version the SRSs
"secret05/jambox5.srs", "secret2006/aprove05.srs" and
"Waldmann/z086-variant.srs" and the TRS "secret2006/jambox10.trs" can not be
proved terminating any longer.

Best regards,
            Martin Korp

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



More information about the Termtools mailing list