@@ -676,7 +676,7 @@ generator Model{..} = oneof $ concat [
676676 (rf, wf) = if fileExists then (10 ,3 ) else (1 ,3 )
677677
678678 genAllowExisting :: Gen AllowExisting
679- genAllowExisting = elements [AllowExisting , MustBeNew ]
679+ genAllowExisting = elements [AllowExisting , MustBeNew , MustExist ]
680680
681681 genSeekMode :: Gen SeekMode
682682 genSeekMode = elements [
@@ -1004,84 +1004,107 @@ data Tag =
10041004 -- > Get ..
10051005 | TagPutTruncateGet
10061006
1007- -- Close a handle 2 times
1007+ -- | Close a handle 2 times
10081008 --
10091009 -- > h <- Open ..
10101010 -- > close h
10111011 -- > close h
10121012 | TagClosedTwice
10131013
1014- -- Open an existing file with ReadMode and then with WriteMode
1014+ -- | Open an existing file with ReadMode and then with WriteMode
10151015 --
10161016 -- > open fp ReadMode
10171017 -- > open fp Write
10181018 | TagOpenReadThenWrite
10191019
1020- -- Open 2 Readers of a file.
1020+ -- | Open 2 Readers of a file.
10211021 --
10221022 -- > open fp ReadMode
10231023 -- > open fp ReadMode
10241024 | TagOpenReadThenRead
10251025
1026- -- ListDir on a non empty dirextory.
1026+ -- | ListDir on a non empty dirextory.
10271027 --
10281028 -- > CreateDirIfMissing True a/b
10291029 -- > ListDirectory a
10301030 | TagCreateDirWithParentsThenListDirNotNull
10311031
1032- -- Read from an AppendMode file
1032+ -- | Read from an AppendMode file
10331033 --
10341034 -- > h <- Open fp AppendMode
10351035 -- > Read h ..
10361036 | TagReadInvalid
10371037
1038- -- Write to a read only file
1038+ -- | Write to a read only file
10391039 --
10401040 -- > h <- Open fp ReadMode
10411041 -- > Put h ..
10421042 | TagWriteInvalid
10431043
1044- -- Put Seek and Get
1044+ -- | Put Seek and Get
10451045 --
10461046 -- > Put ..
10471047 -- > Seek ..
10481048 -- > Get ..
10491049 | TagPutSeekGet
10501050
1051- -- Put Seek (negative) and Get
1051+ -- | Put Seek (negative) and Get
10521052 --
10531053 -- > Put ..
10541054 -- > Seek .. (negative)
10551055 -- > Get ..
10561056 | TagPutSeekNegGet
10571057
1058- -- Open with MustBeNew (O_EXCL flag), but the file already existed.
1058+ -- | Open with MustBeNew (O_EXCL flag), but the file already existed.
10591059 --
10601060 -- > h <- Open fp (AppendMode _)
10611061 -- > Close h
10621062 -- > Open fp (AppendMode MustBeNew)
10631063 | TagExclusiveFail
10641064
1065+ -- | Open a file in read mode successfully
1066+ --
1067+ -- > h <- Open fp (WriteMode _)
1068+ -- > Close h
1069+ -- > h <- Open fp ReadMode
1070+ | TagReadModeMustExist
1071+
1072+ -- | Open a file in read mode, but it fails because the file does not exist.
1073+ --
1074+ -- > h <- Open fp ReadMode
1075+ | TagReadModeMustExistFail
1076+
1077+ -- | Open a file in non-read mode with 'MustExist' successfully.
1078+ --
1079+ -- > h <- Open fp (_ MustBeNew)
1080+ -- > Close h
1081+ -- > h <- Open fp (_ MustExist)
1082+ | TagFileMustExist
1083+
1084+ -- | Open a file in non-read mode with 'MustExist', but it fails because the
1085+ -- files does not exist.
1086+ --
1087+ -- > h <- Open fp (_ MustExist)
1088+ | TagFileMustExistFail
10651089
1066- -- Reading returns an empty bytestring when EOF
1090+ -- | Reading returns an empty bytestring when EOF
10671091 --
10681092 -- > h <- open fp ReadMode
10691093 -- > Get h 1 == ""
10701094 | TagReadEOF
10711095
1072-
1073- -- GetAt
1096+ -- | GetAt
10741097 --
10751098 -- > GetAt ...
10761099 | TagPread
10771100
1078- -- Roundtrip for I/O with user-supplied buffers
1101+ -- | Roundtrip for I/O with user-supplied buffers
10791102 --
10801103 -- > PutBuf h bs c
10811104 -- > GetBuf h c (==bs)
10821105 | TagPutGetBuf
10831106
1084- -- Roundtrip for I/O with user-supplied buffers
1107+ -- | Roundtrip for I/O with user-supplied buffers
10851108 --
10861109 -- > PutBufAt h bs c o
10871110 -- > GetBufAt h c o (==bs)
@@ -1136,6 +1159,10 @@ tag = C.classify [
11361159 , tagPutSeekGet Set. empty Set. empty
11371160 , tagPutSeekNegGet Set. empty Set. empty
11381161 , tagExclusiveFail
1162+ , tagReadModeMustExist
1163+ , tagReadModeMustExistFail
1164+ , tagFileMustExist
1165+ , tagFileMustExistFail
11391166 , tagReadEOF
11401167 , tagPread
11411168 , tagPutGetBuf Set. empty
@@ -1481,6 +1508,39 @@ tag = C.classify [
14811508 Left TagExclusiveFail
14821509 _otherwise -> Right tagExclusiveFail
14831510
1511+ tagReadModeMustExist :: EventPred
1512+ tagReadModeMustExist = C. predicate $ \ ev ->
1513+ case (eventMockCmd ev, eventMockResp ev) of
1514+ (Open _ ReadMode , Resp (Right (RHandle _))) -> Left TagReadModeMustExist
1515+ _otherwise -> Right tagReadModeMustExist
1516+
1517+ tagReadModeMustExistFail :: EventPred
1518+ tagReadModeMustExistFail = C. predicate $ \ ev ->
1519+ case (eventMockCmd ev, eventMockResp ev) of
1520+ (Open _ ReadMode , Resp (Left fsError))
1521+ | fsErrorType fsError == FsResourceDoesNotExist ->
1522+ Left TagReadModeMustExistFail
1523+ _otherwise -> Right tagReadModeMustExistFail
1524+
1525+ tagFileMustExist :: EventPred
1526+ tagFileMustExist = C. predicate $ \ ev ->
1527+ case (eventMockCmd ev, eventMockResp ev) of
1528+ (Open _ mode, Resp (Right (WHandle _ _)))
1529+ | MustExist <- allowExisting mode
1530+ , mode /= ReadMode
1531+ -> Left TagFileMustExist
1532+ _otherwise -> Right tagFileMustExist
1533+
1534+ tagFileMustExistFail :: EventPred
1535+ tagFileMustExistFail = C. predicate $ \ ev ->
1536+ case (eventMockCmd ev, eventMockResp ev) of
1537+ (Open _ mode, Resp (Left fsError))
1538+ | MustExist <- allowExisting mode
1539+ , mode /= ReadMode
1540+ , fsErrorType fsError == FsResourceDoesNotExist ->
1541+ Left TagFileMustExistFail
1542+ _otherwise -> Right tagFileMustExistFail
1543+
14841544 tagReadEOF :: EventPred
14851545 tagReadEOF = successful $ \ ev suc ->
14861546 case (eventMockCmd ev, suc) of
0 commit comments