From 0dcb2adcc2c7d944fe0e08928cce8bff7214dd35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Aug 2016 11:15:39 +0200
Subject: [PATCH] explain how the ghost state for the counter example can be
 implemented

---
 program_logic/counter_examples.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3b1751aa9..540d3fa02 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -87,6 +87,12 @@ Module inv. Section inv.
   (* We have tokens for a little "two-state STS": [start] -> [finish].
      state. [start] also asserts the exact state; it is only ever owned by the
      invariant.  [finished] is duplicable. *)
+  (* Posssible implementations of these axioms:
+     * Using the STS monoid of a two-state STS, where [start] is the
+       authoritative saying the state is exactly [start], and [finish]
+       is the "we are at least in state [finish]" typically owned by threads.
+     * Ex () +_⊥ ()
+  *)
   Context (gname : Type).
   Context (start finished : gname → iProp).
 
-- 
GitLab