Liveness property checked incorrectly about spectacle HOT 1 CLOSED

module Specs.SimpleCounterSpec where

import Data.Either qualified as Either
import Data.Hashable (Hashable)
import GHC.Generics (Generic)
import Language.Spectacle (
  ActionType (ActionWF),
  Fairness (WeakFair),
  Modality (Eventually, Stays),
  Specification (..),
  Temporal,
  TemporalType (PropF, PropFG),
  modelcheck,
  plain,
  (.=),
  pattern ConF,
  pattern NilF,
  type (#),
 )
import Test.Hspec (Spec, describe, hspec, it, shouldSatisfy)

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  describe "SimpleCounter spec" $ do
    describe "eventually is maxCounter" $ do
      specification <- pure $ specification @Eventually PropF
      it "passes when initialCounter < maxCounter" $ do
        result <- modelcheck (specification (1, 4))
        result `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        result <- modelcheck (specification (4, 4))
        result `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        result <- modelcheck (specification (4, 2))
        result `shouldSatisfy` Either.isLeft
    describe "eventually always is maxCounter" $ do
      specification <- pure $ specification @Stays PropFG
      it "passes when initialCounter < maxCounter" $ do
        result <- modelcheck (specification (1, 4))
        result `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        result <- modelcheck (specification (4, 4))
        result `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        result <- modelcheck (specification (4, 2))
        result `shouldSatisfy` Either.isLeft

data Counter = Counting Word | Done Word
  deriving stock (Eq, Show, Generic)
  deriving anyclass (Hashable)

type CounterSpec modality =
  Specification CounterState CounterActions (CounterProperty modality)

type CounterState =
  '[ "goal" # Word
   , "counter" # Counter
   ]

type CounterActions =
  '[ "counterInc" # 'WeakFair
   ]

type CounterProperty modality =
  '["counterEqualsMax" # modality]

specification ::
  (forall s. Temporal s Bool -> TemporalType s modality) ->
  (Word, Word) ->
  CounterSpec modality
specification toProp (initialCounter, maxCounter) =
  Specification
    { specInit =
        ConF #goal (pure maxCounter)
          . ConF #counter (pure (Counting initialCounter))
          $ NilF
    , specNext =
        ConF #counterInc (ActionWF counterInc) NilF
    , specProp =
        ConF #counterEqualsMax (toProp counterEqualsMax) NilF
    }
 where
  counterInc =
    plain #counter >>= \case
      Done _ -> pure False
      Counting counter -> do
        goal <- plain #goal
        let counter' =
              if counter < goal
                then Counting $ counter + 1
                else Done counter
        #counter .= pure counter'
        pure True
  counterEqualsMax = do
    goal <- plain #goal
    counter <- plain #counter
    pure
      case counter of
        Done c -> c == goal
        _ -> False