From 7747d8fb0145172a033c148b18ab537cbd27a17d Mon Sep 17 00:00:00 2001 From: Bob Rubbens Date: Wed, 25 Sep 2024 10:08:24 +0200 Subject: [PATCH] Remove no longer necessary comments & assumes --- .../2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl | 5 ----- 1 file changed, 5 deletions(-) diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl index 75b160c60..6238416ff 100644 --- a/examples/publications/2024/IFM2024VeyMontPermissions/1-TTTmsg/1-TTTmsg.pvl +++ b/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.