search

awakesecurity / spectacle

Embedded specification language & model checker in Haskell
Apache License 2.0
175 stars 12 forks source link

Liveness property checked incorrectly #39

Closed gusbicalho closed 2 years ago

gusbicalho commented 2 years ago

Hello! First of all, impressive work with his library. Thanks for releasing it.

I was trying to port some stuff from TLA+ to Spectacle and run into some weird behaviour with eventually and eventually . always properties.

The test file below reproduces the issues.

The expected behaviour of the model is that a Right counter value will be incremented until it gets to the maxCounter constant, and then it shifts to the final state Left counter. Thus, it should hold that #counter is eventually equal to Left maxCounter, and it is also the case that it eventually is always equal to Left counter. However, this property should be violated if the initialCounter value is larger than maxCounter.

What I see, though, is that eventually seems to reject cases where the model gets stuck forever in a state, even though that state matches the formula. On the other hand, it looks like eventually . always accepts possibilities that actually never achieve the desired state.

Of course it may be that I'm making a mistake using the library. If that's the case I would be very thankful if you could point me in the right direction.

Versions:

Test module

{-# LANGUAGE DataKinds, ImportQualifiedPost, OverloadedLabels, TypeOperators #-}

module Specs.SimpleCounterSpec where

import Data.Either qualified as Either
import Language.Spectacle (Action, Initial, Invariant, always, define, eventually, modelCheck, plain, weakFair, (.=), type (#))
import Language.Spectacle.Specification (Specification (..))
import Test.Hspec (Spec, describe, hspec, it, shouldSatisfy)

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  describe "Counter spec" $ do
    describe "eventually is maxCounter" $ do
      let specification constants =
            Specification
              { initialAction = initSpec constants
              , nextAction = next
              , temporalFormula = eventually $ formula constants
              , terminationFormula = Nothing
              , fairnessConstraint = weakFair
              }
      it "passes when initialCounter < maxCounter" $ do
        modelCheck (specification (1, 4)) `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        modelCheck (specification (4, 4)) `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        modelCheck (specification (4, 2)) `shouldSatisfy` Either.isLeft
    describe "eventually always is maxCounter" $ do
      let specification constants =
            Specification
              { initialAction = initSpec constants
              , nextAction = next
              , temporalFormula = eventually . always $ formula constants
              , terminationFormula = Nothing
              , fairnessConstraint = weakFair
              }
      it "passes when initialCounter < maxCounter" $ do
        modelCheck (specification (1, 4)) `shouldSatisfy` Either.isRight
      it "passes when initialCounter = maxCounter" $ do
        modelCheck (specification (4, 4)) `shouldSatisfy` Either.isRight
      it "fails when initialCounter > maxCounter" $ do
        modelCheck (specification (4, 2)) `shouldSatisfy` Either.isLeft

type CounterSpec = '["goal" # Word, "counter" # Either Word Word]

initSpec :: (Word, Word) -> Initial CounterSpec ()
initSpec (initialCounter, maxCounter) = do
  #goal `define` pure maxCounter
  #counter `define` pure (Right initialCounter)

next :: Action CounterSpec Bool
next = do
  goal <- plain #goal
  counter <- plain #counter
  case counter of
    Right c
      | c < goal -> do
        #counter .= pure (Right $ c + 1)
        pure True
      | otherwise -> do
        #counter .= pure (Left c)
        pure True
    Left _ -> pure True

formula :: (Word, Word) -> Invariant CounterSpec Bool
formula (_, maxCounter) = do
  counter <- plain #counter
  pure $ counter == Left maxCounter

Output of test run:

Counter spec
  eventually is maxCounter
    passes when initialCounter < maxCounter [✘]
    passes when initialCounter = maxCounter [✘]
    fails when initialCounter > maxCounter [✔]
  eventually always is maxCounter
    passes when initialCounter < maxCounter [✔]
    passes when initialCounter = maxCounter [✔]
    fails when initialCounter > maxCounter [✘]

Failures:

  test/Specs/SimpleCounterSpec.hs:24:9: 
  1) Counter spec, eventually is maxCounter, passes when initialCounter < maxCounter
       predicate failed on: Left [MCFormulaError <<0x86c03a317:goal=4 counter=Left 4 RNil>> --> <<0x86c03a317:goal=4 counter=Left 4 RNil>> (Just (SrcLoc {srcLocPackage = "main", srcLocModule = "Specs.SimpleCounterSpec", srcLocFile = "test/Specs/SimpleCounterSpec.hs", srcLocStartLine = 19, srcLocStartCol = 35, srcLocEndLine = 19, srcLocEndCol = 65})) EventuallyPropK]

  To rerun use: --match "/Counter spec/eventually is maxCounter/passes when initialCounter < maxCounter/"

  test/Specs/SimpleCounterSpec.hs:26:9: 
  2) Counter spec, eventually is maxCounter, passes when initialCounter = maxCounter
       predicate failed on: Left [MCFormulaError <<0x86c03a317:goal=4 counter=Left 4 RNil>> --> <<0x86c03a317:goal=4 counter=Left 4 RNil>> (Just (SrcLoc {srcLocPackage = "main", srcLocModule = "Specs.SimpleCounterSpec", srcLocFile = "test/Specs/SimpleCounterSpec.hs", srcLocStartLine = 19, srcLocStartCol = 35, srcLocEndLine = 19, srcLocEndCol = 65})) EventuallyPropK]

  To rerun use: --match "/Counter spec/eventually is maxCounter/passes when initialCounter = maxCounter/"

  test/Specs/SimpleCounterSpec.hs:43:9: 
  3) Counter spec, eventually always is maxCounter, fails when initialCounter > maxCounter
       predicate failed on: Right (ModelMetrics {_distinctStates = 2, _treeDepth = 2, _treeWidth = 0})

  To rerun use: --match "/Counter spec/eventually always is maxCounter/fails when initialCounter > maxCounter/"

Randomized with seed 1147279803

Finished in 0.0219 seconds
6 examples, 3 failures
*** Exception: ExitFailure 1
gusbicalho commented 2 years ago

I just adapted my example to use the current version from main (commit 21337e45f710a88de7760e3d4b51458969d6eb63), and everything seem to be working now! New code below:

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