content: {-# LANGUAGE OverloadedLabels #-}
  
  module Specifications.BitClock where
  
  import Data.Word (Word8)
  
  import Language.Spectacle
    ( Action,
      ActionType (ActionWF),
      Fairness (WeakFair),
      Modality (Always),
      Specification (Specification),
      Temporal,
      TemporalType (PropG),
      interaction,
      plain,
      specInit,
      specNext,
      specProp,
      (.=),
      pattern ConF,
      pattern NilF,
      type (#),
    )
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  check :: IO ()
  check = interaction bitClockSpec
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  type BitClockSpec =
    Specification
      '["clock" # Word8]
      '["tick" # 'WeakFair]
      '["times" # 'Always]
  
  bitClockNext :: Action '["clock" # Word8] Bool
  bitClockNext = do
    clock <- plain #clock
    if clock == 0
      then #clock .= pure 1
      else #clock .= pure 0
    return True
  
  bitClockTimes :: Temporal '["clock" # Word8] Bool
  bitClockTimes = do
    clock <- plain #clock
    pure (clock == 0 || clock == 1)
  
  bitClockSpec :: BitClockSpec
  bitClockSpec =
    Specification
      { specInit = ConF #clock (pure 0) NilF
      , specNext = ConF #tick (ActionWF bitClockNext) NilF
      , specProp = ConF #times (PropG bitClockTimes) NilF
      }
  