From 86bc5be1956c23ded7cc7f9c4f73ba464b9c96f6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 14:44:28 +0100
Subject: [PATCH] remark on AlwaysStable assertions
---
algebra/upred.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/algebra/upred.v b/algebra/upred.v
index 0477b715c..306906368 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -301,6 +301,8 @@ Infix "↔" := uPred_iff : uPred_scope.
Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
Arguments timelessP {_} _ {_}.
+(* TODO: Derek suggested to call such assertions "persistent", which we now
+ do in the paper. *)
Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
Arguments always_stable {_} _ {_}.
--
GitLab