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