content: {-# LANGUAGE OverloadedLabels #-}
  
  module Specifications.Diehard where
  
  import Language.Spectacle
    ( Action,
      ActionType (ActionUF),
      Fairness (Unfair),
      Modality (Always),
      Specification (Specification),
      Temporal,
      TemporalType (PropG),
      interaction,
      plain,
      prime,
      specInit,
      specNext,
      specProp,
      (.=),
      pattern ConF,
      pattern NilF,
      type (#),
    )
  
  -- -------------------------------------------------------------------------------------------------
  
  interactDiehardSpec :: IO ()
  interactDiehardSpec = interaction diehardSpec
  
  -- -------------------------------------------------------------------------------------------------
  
  type DiehardSpec =
    Specification
      DiehardVars
      '[ "emptySmall" # 'Unfair
       , "emptyBig" # 'Unfair
       , "fillSmall" # 'Unfair
       , "fillBig" # 'Unfair
       , "smallToBig" # 'Unfair
       , "bigToSmall" # 'Unfair
       ]
      '[ "isSolved" # 'Always
       ]
  
  type DiehardVars =
    '[ "smallJug" # Int
     , "bigJug" # Int
     ]
  
  emptySmall :: Action DiehardVars Bool
  emptySmall = do
    #smallJug .= pure 0
    return True
  
  emptyBig :: Action DiehardVars Bool
  emptyBig = do
    #bigJug .= pure 0
    pure True
  
  fillSmall :: Action DiehardVars Bool
  fillSmall = do
    #smallJug .= pure 3
    return True
  
  fillBig :: Action DiehardVars Bool
  fillBig = do
    #bigJug .= pure 5
    pure True
  
  bigToSmall :: Action DiehardVars Bool
  bigToSmall = do
    bigJug <- plain #bigJug
    smallJug <- plain #smallJug
  
    #smallJug .= pure (min (bigJug + smallJug) 3)
    #bigJug .= do
      smallJug' <- prime #smallJug
      pure (bigJug - (smallJug' - smallJug))
  
    pure True
  
  smallToBig :: Action DiehardVars Bool
  smallToBig = do
    bigJug <- plain #bigJug
    smallJug <- plain #smallJug
  
    #bigJug .= pure (min (bigJug + smallJug) 5)
    #smallJug .= do
      bigJug' <- prime #bigJug
      pure (smallJug - (bigJug' - bigJug))
  
    pure True
  
  isSolved :: Temporal DiehardVars Bool
  isSolved = do
    bigJug <- plain #bigJug
    pure (bigJug /= 4)
  
  diehardSpec :: DiehardSpec
  diehardSpec =
    Specification
      { specInit =
          ConF #smallJug (pure 0)
            . ConF #bigJug (pure 0)
            $ NilF
      , specNext =
          ConF #emptySmall (ActionUF emptySmall)
            . ConF #emptyBig (ActionUF emptyBig)
            . ConF #fillSmall (ActionUF fillSmall)
            . ConF #fillBig (ActionUF fillBig)
            . ConF #smallToBig (ActionUF smallToBig)
            . ConF #bigToSmall (ActionUF bigToSmall)
            $ NilF
      , specProp =
          ConF #isSolved (PropG isSolved) NilF
      }
  