I had to extend his solution a bit to allow for an internal validation function of any constructed tree, but besides from that my only comment to his solution is that he treats error conditions by silently ignore them – that is the following actions generate no errors/exceptions:A) Deleting an element that does not exist in the tree.
B) Inserting an element twice into the tree.
Patching these up in his code, my model generated test cases all passed, so his implementation is rock-solid! Kudos for that!
References: Application of Model Based Testing to a Binary Search Tree - Part I
 Application of Model Based Testing to a Binary Search Tree - Part II