[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Mathematical puzzle modeling
Thanks for the puzzle. It took me just a little more time to write a spec that allows TLC to solve the problem than to solve it myself. (However, I had heard it before and so recreating the solution was easy.) TLC found the solution in a few seconds. I will leave this as a puzzle for readers to solve, and I hope others will do the same. I therefore rejected an email someone just sent that reveals the solution, although not the TLA+ spec that allows TLC to solve it. After TLC shows you the answer, the reasoning behind it becomes fairly obvious.