You are viewing paulmck

Previous Entry | Next Entry

Abusing Promela to solve CACM puzzle

BookAndGlasses
The May issue of Communications of the ACM has a page of puzzles at the end, the first of which involves a colony of 54 chameleons, of which 20 are red, 18 are blue, and 16 are green. Should a pair of chameleons of different colors meet, they both turn to the other color, so that if a red and a blue chameleon meet, both will turn green. Assuming no births or deaths, is there a sequence of meetings that results in all the chameleons being the same color?

It turns out that you can abuse Promela to solve this problem, although I am sure that the puzzle creator had something else in mind! See here for the Promela code and here for the output.

The way that the model is set up, zero “errors” indicates that the goal cannot be reached. You can of course tweak the initial values of the r, b, and g variables to see if other colonies could go monochrome.

Tags:

Comments

( 4 comments )
jldugger
May. 10th, 2009 12:38 am (UTC)
Clever. I would have tried to model each chameleon as a process and used rendezvous channels to model the color change and a never claim regarding monochromicity.
paulmck
Jun. 8th, 2009 05:43 pm (UTC)
Alternative implmentation
Interesting point! Your approach is more natural in some sense. I would be interested in hearing whether it is simpler or more complex.
jldugger
Jun. 8th, 2009 07:13 pm (UTC)
Re: Alternative implmentation
Probably, yours has a smaller search space. Mine would have a branching factor related to the number of chameleons, even though they're indistinguishable. And the interleavings would be massive.
paulmck
Jun. 8th, 2009 07:58 pm (UTC)
Re: Alternative implmentation
Good point! Fifty-four factorial is not exactly a small number...
( 4 comments )