11open QCheck
2- open STM_base
2+ open STM
33
44module SConf =
55struct
@@ -28,66 +28,66 @@ struct
2828 let arb_cmd _s =
2929 let name_gen = Gen. (oneofl [" aaa" ; " bbb" ; " ccc" ; " ddd" ; " eee" ]) in
3030 let path_gen = Gen. map (fun path -> path) (Gen. list_size (Gen. int_bound 5 ) name_gen) in (* can be empty *)
31- let perm_gen = Gen. (oneofl [ 0o777 ]) in
31+ let perm_gen = Gen. return 0o777 in
3232 QCheck. make ~print: show_cmd
3333 Gen. (oneof
3434 [
35- map (fun path -> File_exists ( path) ) path_gen ;
35+ map (fun path -> File_exists path) path_gen ;
3636 map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen;
3737 map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen;
38- map (fun path -> Readdir ( path) ) path_gen;
38+ map (fun path -> Readdir path) path_gen;
3939 map3 (fun path new_file_name perm -> Touch (path, new_file_name, perm)) path_gen name_gen perm_gen;
4040 ])
4141
4242 let static_path = Sys. getcwd ()
4343
4444 let init_state = Directory {perm = 0o777 ; fs_map = Map_names. empty}
4545
46- let rec find_opt fs path =
46+ let rec find_opt_model fs path =
4747 match fs with
4848 | File f ->
4949 if path = []
5050 then Some (File f)
5151 else None
5252 | Directory d ->
53- (match path with
54- | [] -> Some (Directory d)
55- | hd :: tl ->
56- (match Map_names. find_opt hd d.fs_map with
57- | None -> None
58- | Some fs -> find_opt fs tl))
53+ (match path with
54+ | [] -> Some (Directory d)
55+ | hd :: tl ->
56+ (match Map_names. find_opt hd d.fs_map with
57+ | None -> None
58+ | Some fs -> find_opt_model fs tl))
5959
60- let mem fs path = find_opt fs path <> None
60+ let mem_model fs path = find_opt_model fs path <> None
6161
62- let rec mkdir fs path new_dir_name perm =
62+ let rec mkdir_model fs path new_dir_name perm =
6363 match fs with
64- | File _ -> fs
64+ | File _ -> fs
6565 | Directory d ->
6666 (match path with
6767 | [] ->
6868 let new_dir = Directory {perm; fs_map = Map_names. empty} in
6969 Directory {d with fs_map = Map_names. add new_dir_name new_dir d.fs_map}
7070 | next_in_path :: tl_path ->
7171 (match Map_names. find_opt next_in_path d.fs_map with
72- | None -> fs
72+ | None -> fs
7373 | Some sub_fs ->
74- let nfs = mkdir sub_fs tl_path new_dir_name perm in
74+ let nfs = mkdir_model sub_fs tl_path new_dir_name perm in
7575 if nfs = sub_fs
7676 then fs
7777 else
7878 let new_map = Map_names. remove next_in_path d.fs_map in
7979 let new_map = Map_names. add next_in_path nfs new_map in
8080 Directory {d with fs_map = new_map}))
8181
82- let readdir fs path =
83- match find_opt fs path with
82+ let readdir_model fs path =
83+ match find_opt_model fs path with
8484 | None -> None
8585 | Some fs ->
86- match fs with
86+ ( match fs with
8787 | File _ -> None
88- | Directory d -> Some (Map_names. fold (fun k _ l -> l @ [k] ) d.fs_map [] )
88+ | Directory d -> Some (Map_names. fold (fun k _ l -> k::l ) d.fs_map [] ) )
8989
90- let rec rmdir fs path delete_dir_name =
90+ let rec rmdir_model fs path delete_dir_name =
9191 match fs with
9292 | File _ -> fs
9393 | Directory d ->
@@ -101,13 +101,12 @@ struct
101101 (match Map_names. find_opt next_in_path d.fs_map with
102102 | None -> fs
103103 | Some sub_fs ->
104- let nfs = rmdir sub_fs tl_path delete_dir_name in
104+ let nfs = rmdir_model sub_fs tl_path delete_dir_name in
105105 if nfs = sub_fs
106106 then fs
107- else
108- Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)}))
107+ else Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)}))
109108
110- let rec touch fs path new_file_name perm =
109+ let rec touch_model fs path new_file_name perm =
111110 match fs with
112111 | File _ -> fs
113112 | Directory d ->
@@ -119,36 +118,32 @@ struct
119118 (match Map_names. find_opt next_in_path d.fs_map with
120119 | None -> fs
121120 | Some sub_fs ->
122- let nfs = touch sub_fs tl_path new_file_name perm in
121+ let nfs = touch_model sub_fs tl_path new_file_name perm in
123122 if nfs = sub_fs
124123 then fs
125- else
126- Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs}))
124+ else Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs}))
127125
128126 let next_state c fs =
129127 match c with
130- | File_exists ( _path ) -> fs
128+ | File_exists _path -> fs
131129 | Mkdir (path , new_dir_name , perm ) ->
132- if mem fs (path @ [new_dir_name])
130+ if mem_model fs (path @ [new_dir_name])
133131 then fs
134- else mkdir fs path new_dir_name perm
132+ else mkdir_model fs path new_dir_name perm
135133 | Rmdir (path ,delete_dir_name ) ->
136- if mem fs (path @ [delete_dir_name])
137- then rmdir fs path delete_dir_name
134+ if mem_model fs (path @ [delete_dir_name])
135+ then rmdir_model fs path delete_dir_name
138136 else fs
139137 | Readdir _path -> fs
140138 | Touch (path , new_file_name , perm ) ->
141- if mem fs (path @ [new_file_name])
139+ if mem_model fs (path @ [new_file_name])
142140 then fs
143- else touch fs path new_file_name perm
141+ else touch_model fs path new_file_name perm
144142
145143 let init_sut () =
146144 match Sys. os_type with
147- | "Unix" -> ignore (Sys. command (" rm -rf " ^ (static_path / " sandbox_root" ) ^ " && mkdir " ^ (static_path / " sandbox_root" )))
148- | "Win32" ->
149- ignore (Sys. command (
150- " powershell -Command \" Remove-Item -Path " ^ (static_path / " sandbox_root" ) ^ " -Recurse -Force -ErrorAction Ignore \"
151- & mkdir " ^ (static_path / " sandbox_root" )))
145+ | "Unix" -> ignore (Sys. command (" mkdir " ^ (static_path / " sandbox_root" )))
146+ | "Win32" -> ignore (Sys. command (" mkdir " ^ (static_path / " sandbox_root" )))
152147 | v -> failwith (" Sys tests not working with " ^ v)
153148
154149 let cleanup _ =
@@ -163,71 +158,73 @@ struct
163158
164159 let run c _file_name =
165160 match c with
166- | File_exists ( path ) -> Res (bool , Sys. file_exists (p path))
161+ | File_exists path -> Res (bool , Sys. file_exists (p path))
167162 | Mkdir (path , new_dir_name , perm ) ->
168163 Res (result unit exn , protect (Sys. mkdir ((p path) / new_dir_name)) perm)
169164 | Rmdir (path , delete_dir_name ) ->
170165 Res (result unit exn , protect (Sys. rmdir) ((p path) / delete_dir_name))
171- | Readdir ( path ) ->
166+ | Readdir path ->
172167 Res (result (array string ) exn , protect (Sys. readdir) (p path))
173168 | Touch (path , new_file_name , _perm ) ->
174- (match Sys. os_type with
175- | "Unix" -> Res (unit , ignore( Sys. command (" touch " ^ (p path) / new_file_name ^ " 2>/dev/null" ) ))
176- | "Win32" -> Res (unit , ignore( Sys. command (" type nul >> \" " ^ (p path / new_file_name) ^ " \" " ) ))
177- | v -> failwith (" Sys tests not working with " ^ v))
169+ (match Sys. os_type with
170+ | "Unix" -> Res (int , Sys. command (" touch " ^ (p path) / new_file_name ^ " 2>/dev/null" ))
171+ | "Win32" -> Res (int , Sys. command (" type nul >> \" " ^ (p path / new_file_name) ^ " \" " ))
172+ | v -> failwith (" Sys tests not working with " ^ v))
178173
179174 let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false
180175
181176 let path_is_a_dir fs path =
182- match find_opt fs path with
177+ match find_opt_model fs path with
183178 | None -> false
184179 | Some target_fs -> fs_is_a_dir target_fs
185180
186181 let postcond c (fs : filesys ) res =
187182 match c, res with
188- | File_exists ( path ) , Res ((Bool,_ ),b ) -> b = mem fs path
183+ | File_exists path , Res ((Bool,_ ),b ) -> b = mem_model fs path
189184 | Mkdir (path , new_dir_name , _perm ), Res ((Result (Unit,Exn),_ ), res ) ->
190185 let complete_path = (path @ [new_dir_name]) in
191186 (match res with
192- | Error err ->
193- (match err with
194- | Sys_error s ->
195- (s = (p complete_path) ^ " : Permission denied" ) ||
196- (s = (p complete_path) ^ " : File exists" && mem fs complete_path) ||
197- (s = (p complete_path) ^ " : No such file or directory" && not (mem fs path)) ||
198- (s = (p complete_path) ^ " : Not a directory" && not (path_is_a_dir fs complete_path))
199- | _ -> false )
200- | Ok () -> not (mem fs complete_path) && mem fs path && path_is_a_dir fs path )
187+ | Error err ->
188+ (match err with
189+ | Sys_error s ->
190+ (s = (p complete_path) ^ " : Permission denied" ) ||
191+ (s = (p complete_path) ^ " : File exists" && mem_model fs complete_path) ||
192+ (s = (p complete_path) ^ " : No such file or directory" && not (mem_model fs path)) ||
193+ (s = (p complete_path) ^ " : Not a directory" && not (path_is_a_dir fs complete_path))
194+ | _ -> false )
195+ | Ok () -> mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path) )
201196 | Rmdir (path , delete_dir_name ), Res ((Result (Unit,Exn),_ ), res ) ->
202197 let complete_path = (path @ [delete_dir_name]) in
203198 (match res with
204- | Error err ->
205- (match err with
206- | Sys_error s ->
207- (s = (p complete_path) ^ " : Directory not empty" && not (readdir fs complete_path = Some [] )) ||
208- (s = (p complete_path) ^ " : No such file or directory" && not (mem fs complete_path)) ||
209- (s = (p complete_path) ^ " : Not a directory" && not (path_is_a_dir fs complete_path))
210- | _ -> false )
211- | Ok () ->
212- let is_empty = readdir fs complete_path = Some [] in
213- mem fs complete_path && is_empty && path_is_a_dir fs complete_path)
214- | Readdir (path ), Res ((Result (Array String,Exn),_ ), res ) ->
199+ | Error err ->
200+ (match err with
201+ | Sys_error s ->
202+ (s = (p complete_path) ^ " : Directory not empty" && not (readdir_model fs complete_path = Some [] )) ||
203+ (s = (p complete_path) ^ " : No such file or directory" && not (mem_model fs complete_path)) ||
204+ (s = (p complete_path) ^ " : Not a directory" && not (path_is_a_dir fs complete_path))
205+ | _ -> false )
206+ | Ok () ->
207+ mem_model fs complete_path && path_is_a_dir fs complete_path && readdir_model fs complete_path = Some [] )
208+ | Readdir path , Res ((Result (Array String,Exn),_ ), res ) ->
215209 (match res with
216- | Error err ->
217- (match err with
218- | Sys_error s ->
219- (s = (p path) ^ " : Permission denied" ) ||
220- (s = (p path) ^ " : No such file or directory" && not (mem fs path)) ||
221- (s = (p path) ^ " : Not a directory" && not (path_is_a_dir fs path))
222- | _ -> false )
223- | Ok array_of_subdir ->
224- let sut = List. sort (fun a b -> - (String. compare a b)) (Array. to_list array_of_subdir) in
225- let same_result =
226- (match readdir fs path with
227- | None -> false
228- | Some l -> List. sort (fun a b -> - (String. compare a b)) l = sut) in
229- same_result && mem fs path && path_is_a_dir fs path)
230- | Touch (_path , _new_dir_name , _perm ), Res ((Unit,_ ),_ ) -> true
210+ | Error err ->
211+ (match err with
212+ | Sys_error s ->
213+ (s = (p path) ^ " : Permission denied" ) ||
214+ (s = (p path) ^ " : No such file or directory" && not (mem_model fs path)) ||
215+ (s = (p path) ^ " : Not a directory" && not (path_is_a_dir fs path))
216+ | _ -> false )
217+ | Ok array_of_subdir ->
218+ mem_model fs path && path_is_a_dir fs path &&
219+ (match readdir_model fs path with
220+ | None -> false
221+ | Some l ->
222+ List. sort String. compare l
223+ = List. sort String. compare (Array. to_list array_of_subdir)))
224+ | Touch (path , _new_file_name , _perm ), Res ((Int,_ ),n ) ->
225+ if n = 0
226+ then (mem_model fs path && path_is_a_dir fs path)
227+ else (not (mem_model fs path) || not (path_is_a_dir fs path))
231228 | _ ,_ -> false
232229end
233230
@@ -236,6 +233,6 @@ module Sys_dom = STM_domain.Make(SConf)
236233
237234;;
238235QCheck_base_runner. run_tests_main [
239- Sys_seq. agree_test ~count: 1000 ~name: " STM Sys test sequential" ;
240- Sys_dom. agree_test_par ~count: 100 ~name: " STM Sys test parallel"
236+ Sys_seq. agree_test ~count: 1000 ~name: " STM Sys test sequential" ;
237+ Sys_dom. agree_test_par ~count: 200 ~name: " STM Sys test parallel"
241238 ]
0 commit comments