[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Mathematical puzzle modeling

Hi,

In case you are interested, we have posted a compact TLA+ version for the N=4 and W=40 stone puzzle as an example of our Logic Calculator:
  http://www.stups.uni-duesseldorf.de/ProB/index.php5/ProB_Logic_Calculator
(1. Click on the Formalism Menu on the right and choose TLA+. 2. Now click on the Examples Menu and choose the StonesPuzzle entry.)

We also have a generic B solution for arbitrary weight and number of pieces. We will try and translate it to TLA+ and post it as another example on the site.

Greetings,
Michael Leuschel

On 5 Feb 2015, at 01:56, TLA Plus <tlapl...@xxxxxxxxx> wrote:

I just posted in the CodePlex repository a TLA+/TLC solution to this problem for arbitrary weight of stone and number of pieces.  The repository is at


Click on Source Code > examples > Stones.  However, I recommend trying to write such a solution yourself before looking at mine.

On Wed, Feb 4, 2015 at 1:48 PM, TLA Plus <tlapl...@xxxxxxxxx> wrote:
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. 

On Wed, Feb 4, 2015 at 1:15 PM, stepha...@xxxxxxxxx <guys...@xxxxxxxxx> wrote:

A farmer has a 40 pound stone and a balance scale. How can he break the stone into 4 pieces so that, using those pieces and the balance scale, he can weigh out any integral number of pounds of corn from 1 pound through 40 pounds.
Who to use TLA+ to specify the problem and use TLC to find the solution?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.



--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.