{-# OPTIONS --safe --cubical #-}

module Spartan6.Semantics.System where

open import Spartan6.Prelude

-- Carriers are parameters rather than fields.  This keeps simulations between
-- different state types free of equalities between unrelated projections.

record System
  (Input Output Event State : Type₀) : Type₁ where
  field
    Initial : State → Type₀
    ObservationAllowed : Input → State → Output → Type₀
    TransitionAllowed : Event → Input → State → State → Type₀

open System public

record StepEvidence
  {Input Output Event State : Type₀}
  (system : System Input Output Event State)
  (input : Input) (event : Event) (before after : State)
  (observation : Output) : Type₀ where
  field
    observed : ObservationAllowed system input before observation
    transitioned : TransitionAllowed system event input before after

open StepEvidence public