From a5b23f7d5de0fda6f12a2622d6065c4ae1bff9c1 Mon Sep 17 00:00:00 2001 From: Changlin Li Date: Mon, 29 Jul 2019 13:37:01 -0400 Subject: [PATCH] Fix theorem statement I was missing a temporal quantification in the theorem statement of TypeOK --- Peterson.tla | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Peterson.tla b/Peterson.tla index 4be320c..d7a28af 100644 --- a/Peterson.tla +++ b/Peterson.tla @@ -255,9 +255,9 @@ CanOnlyBeCriticalIfTurn == \A p \in {0, 1} : processState[p] = "critical" => tur (* Finally we note simply that our variables should always stay within the *) (* bounds we enumerated earlier. *) (***************************************************************************) -THEOREM Spec => TypeOK +THEOREM Spec => []TypeOK ============================================================================= \* Modification History -\* Last modified Thu Jul 25 11:05:46 EDT 2019 by changlin +\* Last modified Mon Jul 29 13:36:49 EDT 2019 by changlin \* Created Wed Jul 24 18:56:50 EDT 2019 by changlin