/
hanoi.ml
66 lines (54 loc) · 1.86 KB
/
hanoi.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
open QCheck
module HanoiConf =
struct
type peg = Peg1 | Peg2 | Peg3 [@@deriving show { with_path = false }]
type cmd = Move of peg * peg [@@deriving show { with_path = false }]
type state = { peg1: int list;
peg2: int list;
peg3: int list; }
type sut = unit
let contents s peg = match peg with
| Peg1 -> s.peg1
| Peg2 -> s.peg2
| Peg3 -> s.peg3
let pop src s = match src with
| Peg1 -> List.hd s.peg1, { s with peg1 = List.tl s.peg1 }
| Peg2 -> List.hd s.peg2, { s with peg2 = List.tl s.peg2 }
| Peg3 -> List.hd s.peg3, { s with peg3 = List.tl s.peg3 }
let push dst s v = match dst with
| Peg1 -> { s with peg1 = v::s.peg1 }
| Peg2 -> { s with peg2 = v::s.peg2 }
| Peg3 -> { s with peg3 = v::s.peg3 }
let precond (Move (src,dst)) s =
src <> dst &&
match contents s src, contents s dst with
| [], _ -> false
| _, [] -> true
| x::_, y::_ -> x<y
let gen_cmd s =
let pegs = [Peg1;Peg2;Peg3] in
let moves =
List.fold_right (fun src ->
List.fold_right (fun dst acc ->
let m = Move(src,dst) in
if precond m s then m::acc else acc) pegs) pegs [] in
Gen.oneofl moves
let arb_cmd s = QCheck.make ~print:show_cmd (gen_cmd s)
let init_state = { peg1 = [1;2;3;4];
peg2 = [];
peg3 = []; }
let next_state (Move (src,dst)) s =
if src = dst
then failwith ("illegal move: " ^ show_cmd (Move (src,dst)))
else
let hd,s = pop src s in
push dst s hd
let init_sut _ = ()
let cleanup _ = ()
let run_cmd c s sut = (* "we never hit a state with first two pegs empty" *)
let next = next_state c s in
not (next.peg1 = [] && next.peg2 = [])
end
module HT = QCSTM.Make(HanoiConf)
;;
QCheck_runner.run_tests ~verbose:true [HT.agree_test ~count:100 ~name:"towers of Hanoi"]