content: {-# LANGUAGE OverloadedLabels #-}
  
  module Specifications.SimpleClock where
  
  import Language.Spectacle
    ( Action,
      ActionType (ActionWF),
      Fairness (WeakFair),
      Modality (Always, Infinitely),
      Specification (Specification),
      Temporal,
      TemporalType (PropG, PropGF),
      interaction,
      modelcheck,
      plain,
      prime,
      specInit,
      specNext,
      specProp,
      (.=),
      pattern ConF,
      pattern NilF,
      type (#),
    )
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  interactClockSpec :: IO ()
  interactClockSpec = interaction clockSpec
  
  clockSpecCheck :: IO ()
  clockSpecCheck = do
    modelcheck clockSpec >>= \case
      Left err -> print err
      Right xs -> print xs
  
  -- ---------------------------------------------------------------------------------------------------------------------
  
  type ClockSpec =
    Specification
      '["hour" # Int]
      '["next" # 'WeakFair]
      '["ticks" # 'Infinitely, "times" # 'Always]
  
  clockNext :: Action '["hour" # Int] Bool
  clockNext = do
    hour <- plain #hour
    if hour == 12
      then #hour .= pure 1
      else #hour .= pure (1 + hour)
    pure True
  
  clockTicks :: Temporal '["hour" # Int] Bool
  clockTicks = do
    hour <- plain #hour
    hour' <- prime #hour
    pure (1 + hour == hour')
  
  clockTimes :: Temporal '["hour" # Int] Bool
  clockTimes = do
    hour <- plain #hour
    pure (1 <= hour && hour <= 12)
  
  clockSpec :: ClockSpec
  clockSpec =
    Specification
      { specInit = ConF #hour (pure 1) NilF
      , specNext = ConF #next (ActionWF clockNext) NilF
      , specProp =
          ConF #ticks (PropGF clockTicks)
            . ConF #times (PropG clockTimes)
            $ NilF
      }
  