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.
paulmckrcu 
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.
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.
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.
Re: Alternative implmentation
Good point! Fifty-four factorial is not exactly a small number…