This is an Alloy module for the prisoners puzzle
The warden of a prison gives his prisoners the following problem. There is a room in the prison with two switches, labeled A and B. Every so often, the warden will select a prisoner at random and take him into the room, where he must flip (change the position of) exactly one of the switches. The only guarantee he makes is that every prisoner will eventually be brought into the room multiple times.
At any time, any prisoner may declare that all the prisoners have
been in the room at least once. If that prisoner is right, then
all the prisoners go free. If he is wrong, all the prisoners are
immediately executed.
The prisoners are allowed to decide upon a strategy, after which
they will not be allowed to communicate with one another. And, of
course, they cannot see the room or who is being brought into it.
What do they do?
The solution presented by the Car Guys and checked in Alloy by Shiran Zada