# Problem in understanding mutable state in Alloy 6

**URL:** <https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268>\
**Category:** Alloy 6\
**Created:** [June 13, 2022, 9:15am UTC](https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268 "2022-06-13T09:15:50Z")\
**Posts on this page:** 1\
**Showing post:** 10

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [May 31, 2023, 7:52am UTC](https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268/10 "2023-05-31T07:52:28Z")

</div>

> **[Solving Knights and Knaves with Alloy](https://www.hillelwayne.com/post/knights-knaves/)**
>
> There’s a famous logic puzzle, originally from Raymond Smullyan, called a “Knights and Knaves” puzzle. We have a set of people, all of whom are either a Knight or a Knave. Knights only make true statements, and Knaves only make false statements....

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] ] ]
	
}

```

* * *

> <https://stackoverflow.com/questions/47969967/alloy-model-of-the-einstein-puzzle>

> <https://github.com/AlloyTools/models/blob/master/puzzles/farmer-chicken-fox/farmer.als>

---

_[View the full topic](https://alloytools.discourse.group/t/problem-in-understanding-mutable-state-in-alloy-6/268)._