------------------------------------------------------------------------
-- This approach is incorrect, but perhaps subtly so
------------------------------------------------------------------------

module NonDeterministic.Incorrect where

open import Data.Colist
open import Coinduction

open import NonDeterministic.Expr

infix 4 _HasTrace_

data _HasTrace_ : Semantics where
  nop  : ∀ {e   ms} (s : ∞ (♭ e HasTrace   ms)) → nop    e HasTrace          ms
  tick : ∀ {e m ms} (s : ∞ (♭ e HasTrace ♭ ms)) → tick m e HasTrace user m ∷ ms
  -- The semantics is non-deterministic; spurious messages (possibly
  -- infinitely many) may be inserted into the message stream.
  tock : ∀ {e m ms} (s : ∞ (e HasTrace ♭ ms)) → e HasTrace ext m ∷ ms

------------------------------------------------------------------------
-- Examples

possible : nops HasTrace []
possible = nop (♯ possible)

-- Should not be allowed, since nops does not emit any messages:

should-be-impossible : ∀ {m ms} → nops HasTrace (user m ∷ ms)
should-be-impossible = nop (♯ should-be-impossible)

ok : ticks HasTrace scissors
ok = tick (♯ ok)