Skip to content

Commit

Permalink
Adapt tests to Postcondition
Browse files Browse the repository at this point in the history
  • Loading branch information
jasagredo committed Apr 25, 2024
1 parent 81626ac commit a107509
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 11 deletions.
6 changes: 3 additions & 3 deletions quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
ref <- ask
lift $ atomicModifyIORef' ref (\count -> (succ count, count))

postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
postcondition (_, FailingCounter{failingCount}) _ _ _ = PostBool $ failingCount < 4

-- A generic but simple counter model
data Counter = Counter Int
Expand Down Expand Up @@ -93,5 +93,5 @@ instance RunModel Counter (ReaderT (IORef Int) IO) where
writeIORef ref 0
pure n

postcondition (Counter n, _) Reset _ res = pure $ n == res
postcondition _ _ _ _ = pure True
postcondition (Counter n, _) Reset _ res = PostBool $ n == res
postcondition _ _ _ _ = PostBool True
14 changes: 6 additions & 8 deletions quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -129,16 +129,14 @@ instance RunModel RegState RegM where
pure $ Right ()

postcondition (s, _) (WhereIs name) env mtid = do
pure $ (env <$> Map.lookup name (regs s)) == mtid
postcondition _ _ _ _ = pure True
PostBool $ (env <$> Map.lookup name (regs s)) == mtid
postcondition _ _ _ _ = PostBool True

postconditionOnFailure (s, _) act@Register{} _ res = do
monitorPost $
tabulate
"Reason for -Register"
[why s act]
pure $ isLeft res
postconditionOnFailure _s _ _ _ = pure True
PostMonitor
(tabulate "Reason for -Register" [why s act])
(PostBool $ isLeft res)
postconditionOnFailure _s _ _ _ = PostBool True

monitoring (_s, s') act@(showDictAction -> ShowDict) _ res =
counterexample (show res ++ " <- " ++ show act ++ "\n -- State: " ++ show s')
Expand Down

0 comments on commit a107509

Please sign in to comment.