Problem in understanding mutable state in Alloy 6

Alloy 6
1

Hi,
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.

Greetings,
Joshua

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

2

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.)

3

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.

Edit:
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.

4

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

1 Like
5

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
	# color.blue   = 13
	# color.green  = 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
1 Like
6

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
SETS
 Colors = {blau,gruen,gelb}
VARIABLES cham
INVARIANT
  cham : Colors --> NATURAL &
  not(cham(blau) = 0 & cham(gruen)=0)
INITIALISATION cham := {blau |-> 13, gruen |-> 15,  gelb |-> 17 }
OPERATIONS
  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}
  END
END

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

7

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.

8

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
Solution:
       n = 45 &
       res = #1081:{(0|->0|->45),(0|->1|->44),...,(44|->1|->0),(45|->0|->0)} &
       c = 1081
9

Where do you find puzzles like this? This sounds like a great idea to send check my actual competency against my believed competency. Also asking @JoshuaSchmidt or anyone here the same question.

10

My solution:

enum Person { Alice, Bob, Claire, Desmond, Elena, Fernando, Gary, Horace, Ingrid }

one sig World {
	people	 : set Person,
	knights  : set people,
	knaves   : set people
} { 
	knights = people - knaves
}

let says[p,e] 	= (p) in World.knights => (e) else not (e)
let isKnave[p] 	= (p) in World.knaves
let isKnight[p] = (p) in World.knights

-- Problem 1: There are two native islanders, named Alice and Bob, 
-- standing next to each other. You do not know what type either of 
-- them is. Suddenly, Alice says “At least one of us is a Knave.”	
run BobAlice {
	World.people = Bob+Alice	

	-- Alice says: At least one of us is a Knave
	Alice.says[ some p : Bob+Alice | p.isKnave ]
}

-- Problem 2: Again, there are two native islanders standing next 
-- to each other. One is named Claire and the other is named Desmond. 
-- You do not know what type either of them are. Claire suddenly says, 
-- “We are both Knights”. After this, Desmond says “Either Claire is a 
-- Knight or I am a Knight, but we are not both Knights.

run ClaireDesmond {
	World.people = Claire+Desmond

	-- Claire says “We are both Knights”
	Claire.says[ (Claire+Desmond).isKnight ]

	-- Desmond says “Either Claire is a 
	-- Knight or I am a Knight, but we are not both Knights.
	Desmond.says[ (Claire.isKnight or Desmond.isKnight) and not ( Claire.isKnight and Desmond.isKnight ) ]
}

-- Problem 3: There are three native islanders, named Elena, Fernando, and Gary, 
-- standing together. You ask Elena, “How many knights are among you?”, and Elena 
-- answered but you couldn’t quite hear what she said. You then ask Fernando, “What 
-- did Elena say?”, and Fernando replies, “Elena said there is one knight among us.”
-- At this point, Gary says “Don’t believe Fernando; he is lying.”

run ElenaFernandoGary {
	World.people = Elena + Fernando + Gary

	Gary.says[ not Fernando.says[ 	Claire.says[ one World.knights ] ] ]
	
}
1 Like
11

@DanielJackson’s book contains some classic puzzle statements, among other forms of exercises. @alcino and @nmacedo may have some exercise available on Alloy4Fun too.

12

We have a few Alloy4Fun challenges to practice relational logic here:
https://haslab.github.io/formal-software-design/structural-design/index.html#exercises

And a couple more to practice the temporal logic connectives here:
https://haslab.github.io/formal-software-design/protocol-design/index.html#exercises

Have fun!
Alcino