diff --git a/AB.tla b/AB.tla index d8948f4..b6fc1fa 100644 --- a/AB.tla +++ b/AB.tla @@ -94,7 +94,9 @@ THEOREM Spec => ABS!Spec (***************************************************************************) FairSpec == Spec /\ SF_vars(ARcv) /\ SF_vars(BRcv) /\ WF_vars(ASnd) /\ WF_vars(BSnd) + +THEOREM FairSpec => ABS!FairSpec ============================================================================= \* Modification History -\* Last modified Mon Jan 14 18:42:09 CET 2019 by veitheller +\* Last modified Mon Jan 14 18:57:03 CET 2019 by veitheller \* Created Wed Mar 25 11:53:40 PDT 2015 by lamport