@@ -4,35 +4,49 @@ open Lin
44module Spec =
55 struct
66 type t = int Stack .t
7- let m = Mutex. create ()
87
98 type cmd =
10- | Push of int '
11- | Pop
12- | Pop_opt
13- | Top
14- | Top_opt
15- | Clear
16- | Is_empty
17- | Fold of fct * int '
18- | Length [@@ deriving qcheck , show { with_path = false }]
19- and int' = int [@ gen Gen .nat ]
20- and fct = (int -> int -> int ) fun_ [@ printer fun fmt f -> fprintf fmt " %s" (Fn. print f)] [@ gen (fun2 Observable. int Observable. int small_int).gen]
9+ | Push of Var .t * int
10+ | Pop of Var .t
11+ | Pop_opt of Var .t
12+ | Top of Var .t
13+ | Top_opt of Var .t
14+ | Clear of Var .t
15+ | Is_empty of Var .t
16+ | Fold of Var .t * fct * int
17+ | Length of Var .t [@@ deriving show { with_path = false }]
18+ and fct = (int -> int -> int ) fun_ [@ printer fun fmt f -> fprintf fmt " %s" (Fn. print f)]
19+
20+ let gen_int = Gen. nat
21+ let gen_fct = (fun2 Observable. int Observable. int small_int).gen
22+
23+ let gen_cmd gen_var =
24+ Gen. (oneof [
25+ map2 (fun t i -> None ,Push (t,i)) gen_var gen_int;
26+ map (fun t -> None , Pop t) gen_var;
27+ map (fun t -> None , Pop_opt t) gen_var;
28+ map (fun t -> None , Top t) gen_var;
29+ map (fun t -> None , Top_opt t) gen_var;
30+ map (fun t -> None , Clear t) gen_var;
31+ map (fun t -> None , Is_empty t) gen_var;
32+ map3 (fun t f i -> None ,Fold (t,f,i)) gen_var gen_fct gen_int;
33+ map (fun t -> None , Length t) gen_var;
34+ ])
2135
2236 let shrink_cmd c = match c with
23- | Pop
24- | Pop_opt
25- | Top
26- | Top_opt
27- | Clear
28- | Is_empty
29- | Length -> Iter. empty
30- | Push i -> Iter. map (fun i -> Push i ) (Shrink. int i)
31- | Fold (f ,i ) ->
37+ | Pop _
38+ | Pop_opt _
39+ | Top _
40+ | Top_opt _
41+ | Clear _
42+ | Is_empty _
43+ | Length _ -> Iter. empty
44+ | Push ( t , i ) -> Iter. map (fun i -> Push (t,i) ) (Shrink. int i)
45+ | Fold (t , f ,i ) ->
3246 Iter. (
33- (map (fun f -> Fold (f,i)) (Fn. shrink f))
47+ (map (fun f -> Fold (t, f,i)) (Fn. shrink f))
3448 < +>
35- (map (fun i -> Fold (f,i)) (Shrink. int i)))
49+ (map (fun i -> Fold (t, f,i)) (Shrink. int i)))
3650
3751 type res =
3852 | RPush
@@ -53,56 +67,59 @@ module SConf =
5367 struct
5468 include Spec
5569 let run c s = match c with
56- | Push i -> Stack. push i s; RPush
57- | Pop -> RPop (Util. protect Stack. pop s)
58- | Pop_opt -> RPop_opt (Stack. pop_opt s)
59- | Top -> RTop (Util. protect Stack. top s)
60- | Top_opt -> RTop_opt (Stack. top_opt s)
61- | Clear -> Stack. clear s; RClear
62- | Is_empty -> RIs_empty (Stack. is_empty s)
63- | Fold (f , a ) -> RFold (Stack. fold (Fn. apply f) a s)
64- | Length -> RLength (Stack. length s)
70+ | None ,Push (t ,i ) -> Stack. push i s.(t); RPush
71+ | None ,Pop t -> RPop (Util. protect Stack. pop s.(t))
72+ | None ,Pop_opt t -> RPop_opt (Stack. pop_opt s.(t))
73+ | None ,Top t -> RTop (Util. protect Stack. top s.(t))
74+ | None ,Top_opt t -> RTop_opt (Stack. top_opt s.(t))
75+ | None ,Clear t -> Stack. clear s.(t); RClear
76+ | None ,Is_empty t -> RIs_empty (Stack. is_empty s.(t))
77+ | None ,Fold (t ,f ,a ) -> RFold (Stack. fold (Fn. apply f) a s.(t))
78+ | None ,Length t -> RLength (Stack. length s.(t))
79+ | _ , _ -> failwith (Printf. sprintf " unexpected command: %s" (show_cmd (snd c)))
6580 end
6681
6782module SMutexConf =
6883 struct
6984 include Spec
85+ let m = Mutex. create ()
7086 let run c s = match c with
71- | Push i -> Mutex. lock m;
72- Stack. push i s;
73- Mutex. unlock m; RPush
74- | Pop -> Mutex. lock m;
75- let r = Util. protect Stack. pop s in
76- Mutex. unlock m;
77- RPop r
78- | Pop_opt -> Mutex. lock m;
79- let r = Stack. pop_opt s in
80- Mutex. unlock m;
81- RPop_opt r
82- | Top -> Mutex. lock m;
83- let r = Util. protect Stack. top s in
84- Mutex. unlock m;
85- RTop r
86- | Top_opt -> Mutex. lock m;
87- let r = Stack. top_opt s in
88- Mutex. unlock m;
89- RTop_opt r
90- | Clear -> Mutex. lock m;
91- Stack. clear s;
92- Mutex. unlock m;
93- RClear
94- | Is_empty -> Mutex. lock m;
95- let b = Stack. is_empty s in
96- Mutex. unlock m;
97- RIs_empty b
98- | Fold (f , a ) -> Mutex. lock m;
99- let r = Stack. fold (Fn. apply f) a s in
100- Mutex. unlock m;
101- RFold r
102- | Length -> Mutex. lock m;
103- let l = Stack. length s in
104- Mutex. unlock m;
105- RLength l
87+ | None ,Push (t ,i ) -> Mutex. lock m;
88+ Stack. push i s.(t);
89+ Mutex. unlock m; RPush
90+ | None ,Pop t -> Mutex. lock m;
91+ let r = Util. protect Stack. pop s.(t) in
92+ Mutex. unlock m;
93+ RPop r
94+ | None ,Pop_opt t -> Mutex. lock m;
95+ let r = Stack. pop_opt s.(t) in
96+ Mutex. unlock m;
97+ RPop_opt r
98+ | None ,Top t -> Mutex. lock m;
99+ let r = Util. protect Stack. top s.(t) in
100+ Mutex. unlock m;
101+ RTop r
102+ | None ,Top_opt t -> Mutex. lock m;
103+ let r = Stack. top_opt s.(t) in
104+ Mutex. unlock m;
105+ RTop_opt r
106+ | None ,Clear t -> Mutex. lock m;
107+ Stack. clear s.(t);
108+ Mutex. unlock m;
109+ RClear
110+ | None ,Is_empty t -> Mutex. lock m;
111+ let b = Stack. is_empty s.(t) in
112+ Mutex. unlock m;
113+ RIs_empty b
114+ | None ,Fold (t ,f ,a ) -> Mutex. lock m;
115+ let r = Stack. fold (Fn. apply f) a s.(t) in
116+ Mutex. unlock m;
117+ RFold r
118+ | None ,Length t -> Mutex. lock m;
119+ let l = Stack. length s.(t) in
120+ Mutex. unlock m;
121+ RLength l
122+ | _ , _ -> failwith (Printf. sprintf " unexpected command: %s" (show_cmd (snd c)))
106123 end
107124
108125module ST = Lin. Make (SConf )
0 commit comments