Problem in understanding mutable state in Alloy 6

I tried to model a puzzle in Alloy 6 to get familiar with the new notation of mutable states and temporal logic in Alloy 6.
Usually, I use B and Event-B for modeling and ProB for animation and verification.

The puzzle:
45 chameleons live on an island, 13 of which are blue, 15 green and 17 yellow.
If two chameleons of different colors meet, they change their color to the third color.
Show that this doesn’t make it possible for all chameleons to be yellow at some point.

My attempt in Alloy 6 which does not seem to be correct:

enum colors {blue,green,yellow}

var sig population {
  var chameleons: colors -> one Int

fact init {
  (population.chameleons)[blue] = 13 and 
  (population.chameleons)[green] = 15 and 
  (population.chameleons)[yellow] = 17

pred meet[c1: colors, c2: colors] {
  c1 != c2 and (population.chameleons)[c1] > 0 and (population.chameleons)[c2] > 0 and  // guard
  after (let c3 = ((colors - c1) - c2) |                                             // action
         population'.chameleons' =                      
            (((population.chameleons ++ (c1->(minus[(population.chameleons)[c1],1]))) 
               ++ (c2->(minus[(population.chameleons)[c2],1]))) 
               ++ (c3->(plus[(population.chameleons)[c3],2]))

pred skip { 
  after population'.chameleons' = population.chameleons

fact step {
  always ((some c1,c2: colors | meet[c1,c2]) or skip)

assert invariant {
  always (not ((population.chameleons)[blue] = 0 and (population.chameleons)[green] = 0))

check invariant for 7 Int, 100 steps

When checking the invariant, I receive the counterexample (population.chameleons)[blue] = 0 and (population.chameleons)[green] = 0 and (population.chameleons)[yellow] = -63.
I don’t know how this state can be reached. The predicate skip does not change anything, and the predicate meet[c1,c2] decrements the amount of chameleons with colors c1 or c2 by one and increments the amount of chameleons with the third color by two.

If I change the “action” of the predicate meet[c1,c2] to be population'.chameleons' = population.chameleons there should only be skip actions.
Yet, I receive the counterexample (population.chameleons)[blue] = 0 and (population.chameleons)[green] = 0 and (population.chameleons)[yellow] = 62.
Again, I don’t understand how this state can be reached when only skip actions are available.

I am obviously missing an important aspect of mutable states in Alloy 6.

Any help is appreciated.


Edit: a more detailed description of the puzzle can be found here

After a very quick glance, it seems your events lack frame conditions. These conditions are constraints that state what does not change when an event happens. In B/Event-B, you don’t have to state these as the language is operational (you specify a state machine: you only need to say what changes and the rest is inferred so to speak); but Alloy is more “declarative”: you specify behaviors quite liberally, but there’s a price to pay (writing frame conditions).

(Notice also that prime already means “the value at the next instant”, so you don’t need to use after; in fact using after and primes makes you specify the value at instant i + 2.)

Thanks a lot! When removing the two after keywords, I receive reasonable state changes as expected.
This seems to be the only error in the model.
I think we don’t need a frame condition in this specific model since there is only one mutable state, which is assigned in both predicates for state changes.

I also noticed that the signature population does not have to be variable. Using one sig population improves performance for checking the invariant by several orders of magnitude.

It wasn’t the case because population was var. Now that you changed it to a static one sig, yes!

1 Like

I love these puzzles so I did a go at it. However, with the given numbers it takes forever to solve. Did you actually wait for step 100 to be resolved?

This is my model, I think it is a bit closer to your spec and simpler. I get some traces with fewer chameleons but have not waited 100 steps so no guarantees :slight_smile:

enum Color { blue, green, yellow }

sig Chameleon { var color: Color }

-- If two chameleons of different colors meet, 
-- they change their color to the third color.
pred meet[ a, b : Chameleon ] {
	a.color != b.color implies { 
		let thirdColor = Color - a.color - b.color {
			color' = color ++ (a->thirdColor + b->thirdColor)
	} else {
		color' = color
run {
	-- 45 chameleons live on an island
    # Chameleon    = 45
	#   = 13
	#  = 15
	# color.yellow = 17

	always ( some a, b : Chameleon | meet[a,b] )

	-- Show that this doesn’t make it possible for all 
    -- chameleons to be yellow at some point.
	eventually Chameleon.color = yellow
} for 45 but 7 int, 100 steps

Very nice :slight_smile: Your solution is indeed simpler (although the visualization becomes harder to read, but that’s not a problem).
I also haven’t checked the model for all 100 steps due to the long runtime.
I thought the low performance of the solvers is caused by the use of integers (at least in my model), but that does not seem to be the case.

We also modeled the puzzle in classical B:

MACHINE Chamelon
 Colors = {blau,gruen,gelb}
  cham : Colors --> NATURAL &
  not(cham(blau) = 0 & cham(gruen)=0)
INITIALISATION cham := {blau |-> 13, gruen |-> 15,  gelb |-> 17 }
  meet(c1,c2,c3) = PRE [c1,c2,c3]:perm(Colors) &
                    c1:Colors & cham(c1)>0 & cham(c2)>0 THEN
    cham := {c1|-> cham(c1)-1, c2|-> cham(c2)-1, c3 |-> cham(c3)+2}

ProB’s explicit state model checker is able to check all 361 states in around 2 seconds.

361 states sounds awfully low for 45 chameleons?

I agree the 7 int is a lot for Alloy. Maybe Daniel will kick in with a faster solution.

I thought so too at first, but I think the state space is correct.
There are 1982 transitions when checking above B model completely, many of which lead to the same state. In total, this results in 361 distinct states.

There are 1081 states in total, many of which are not reachable due to the initialization.

>>> {a,b,c| {a,b,c} <: 0..n & a+b+c=n}=res & n=45 & c=card(res)
Existentially Quantified Predicate over n,res,c is TRUE
       n = 45 &
       res = #1081:{(0|->0|->45),(0|->1|->44),...,(44|->1|->0),(45|->0|->0)} &
       c = 1081