Remove no longer necessary comments & assumes

examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl

@@ -19,7 +19,6 @@ choreography Main() {
   ensures (\endpoint p2; state(p2, false));
   requires (\endpoint p1; p1.turn ==> turnInvariant(p1, p2));
   requires (\endpoint p2; p2.turn ==> turnInvariant(p2, p1));
-  // Endpoint annotations using "\endpoint" will be removed after switching to the lightweight encoding.
   requires (\chor p1.turn != p2.turn);
   requires p1.emptyBoard() ** p2.emptyBoard();
   ensures (\endpoint p1;
@@ -59,11 +58,7 @@ choreography Main() {
       }
       p1.turn := !p1.turn;
       p2.turn := !p2.turn;
-
-      // Assumption required for shortcoming in one of the backends. The the other backend can verify it just fine. Can be removed after implementing the lightweight encoding.
-      assume (\chor p1.gameFinished() == p2.gameFinished());
     }
-    assume (\chor p1.gameFinished() == p2.gameFinished());
 
     if (p1.turn && !p2.turn) {
       // Send "true" from p1 to p2. p2 discards the value immediately.