Warning: Only the first three correct solutions of
this alternative final assignment will be accepted. If your solution arrives
as fourth or later, you have to do the "regular" final assignment!
Flipping glasses
Suppose we are given a table with a square platform on it. The platform
can be rotated for 90, 180, 270 or 360 (or 0, if you prefer) degrees. At
each corner of the platform there is a glass which can be set in a normal
position up, or it can be set upside-down. Two players, A and B, are playing
a game, with each turn consisting of the following steps:
-
First, player A rotates the platform for 90, 180, 270 or 360 (or 0, if
you prefer) degrees;
-
Then player B, who is blindfolded, i.e., it cannot see the platform, tells
player A to flip an arbitrary nonnegative number (1, 2, 3, or 4) of glasses
(i.e., if the glass is up, then it is turned upside-down, and vice versa).
In fact, B tells A the corners of the platform for which the glasses should
be flipped. To this end, we assume that there are labels on the table the
platform resides on: UL(uuper-left), UR(upper-right), LL(lower-left) and
LR(lower-right). (The labels, of course, do not move with the platform,
so there is no way to "stick" a label to a particular glass);
-
Player A flips the glasses and it reports player B only in case all glasses
are up, which also means that B wins the game;
Find (manually) a winning strategy for B, provided that before the first
turn at least one glass on the platform is set upside-down. Program the
game and the strategy for B in Promela and prove the correctness of your
solution, i.e., prove that for any initial configuration of glasses (with
at least one glass upside-down) player B wins the game.
Your report should consist of a short description of the strategy. It
can be given in a form of comments in the Promela program.