First Commit - As the teacher gave it
This commit is contained in:
commit
7efbcb75cf
GPG Key ID:
DBA23608F23F5A10
23
Makefile
Normal file
23
Makefile
Normal file
@ -0,0 +1,23 @@
|
||||
|
||||
default:
|
||||
@echo 'type `make <target>` where <target> is either ide, replay, test or doc'
|
||||
|
||||
ide:
|
||||
why3 ide min_game.mlw
|
||||
|
||||
replay:
|
||||
why3 replay min_game
|
||||
|
||||
tests:
|
||||
why3 execute min_game.mlw --use MinGame "config0 ()"
|
||||
why3 execute min_game.mlw --use MiniMax "test0 ()"
|
||||
why3 execute min_game.mlw --use AlphaBeta "test_alphabeta ()"
|
||||
|
||||
test_min_game:
|
||||
why3 extract -D ocaml64 min_game.mlw -o minGameExtract.ml
|
||||
ocamlbuild -pkg unix -pkg zarith test_min_game.native
|
||||
./test_min_game.native
|
||||
|
||||
doc:
|
||||
why3 doc min_game.mlw
|
||||
why3 session html min_game
|
||||
BIN
enonce.pdf
Normal file
BIN
enonce.pdf
Normal file
Binary file not shown.
341
min_game.mlw
Normal file
341
min_game.mlw
Normal file
@ -0,0 +1,341 @@
|
||||
|
||||
|
||||
(** {1 Two-Player Games
|
||||
|
||||
MPRI course 2-36-1 Proof of Programs - Project 2023-2024
|
||||
|
||||
*)
|
||||
|
||||
|
||||
(** {2 Dummy symbols to fill holes in the remainder} *)
|
||||
|
||||
module DummySymbols
|
||||
|
||||
predicate __FORMULA_TO_BE_COMPLETED__
|
||||
constant __TERM_TO_BE_COMPLETED__ : 'a
|
||||
constant __VARIANT_TO_BE_COMPLETED__ : int
|
||||
let function __EXPRESSION_TO_BE_COMPLETED__ () : 'a = absurd
|
||||
let constant __CONDITION_TO_BE_COMPLETED__ : bool = False
|
||||
let constant __CODE_TO_BE_COMPLETED__ : unit = ()
|
||||
|
||||
end
|
||||
|
||||
|
||||
(** {2 The "Min" Game} *)
|
||||
|
||||
module MinGame
|
||||
|
||||
use export int.Int
|
||||
use export array.Array
|
||||
use export option.Option
|
||||
use export DummySymbols
|
||||
|
||||
|
||||
(** type for players *)
|
||||
type player = Alice | Bob
|
||||
|
||||
(** type for configurations of the game *)
|
||||
type config = {
|
||||
stack : array int; (* stack of numbers, e.g. [ 20 ; 17 ; 24 ; -30 ; 27 ] *)
|
||||
pos : int; (* position in the stack, i.e. index of the first number
|
||||
to be picked *)
|
||||
turn : player; (* player who will play next move *)
|
||||
score_alice : int; (* current score of Alice *)
|
||||
score_bob : int; (* current score of Bob *)
|
||||
}
|
||||
|
||||
(** initial configuration from a given stack of numbers *)
|
||||
function initial_config (stack: array int) : config =
|
||||
{ stack = stack; pos = 0; turn = Alice; score_alice = 0; score_bob = 0 }
|
||||
|
||||
(** QUESTION 1 *)
|
||||
|
||||
(** invariant on configurations *)
|
||||
predicate inv(c:config) =
|
||||
__FORMULA_TO_BE_COMPLETED__
|
||||
|
||||
(** type for possible moves, here only two choices: pick one or pick
|
||||
two numbers on top of the stack. *)
|
||||
type move = PickOne | PickTwo
|
||||
|
||||
(** QUESTION 2 *)
|
||||
|
||||
(** set of possible moves in a given configuration. It is either empty,
|
||||
represented as `None` or a pair of two moves represented as
|
||||
`Some(m1,m2)` *)
|
||||
let function legal_moves (c:config) : option (move, move) =
|
||||
if __CONDITION_TO_BE_COMPLETED__ then None else __EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
|
||||
(** QUESTION 3 *)
|
||||
|
||||
(** `do_move c m` returns the new configuration obtained from
|
||||
configuration `c` after playing move `m` *)
|
||||
let function do_move (c:config) (m:move) : config
|
||||
requires { inv c }
|
||||
requires { __FORMULA_TO_BE_COMPLETED__ }
|
||||
ensures { inv result }
|
||||
=
|
||||
match m, c.turn with
|
||||
| PickOne, Alice ->
|
||||
let x = c.stack[c.pos] in
|
||||
{ c with turn = Bob; pos = c.pos + 1; score_alice = c.score_alice + x }
|
||||
| PickOne, Bob ->
|
||||
let x = c.stack[c.pos] in
|
||||
__EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
| PickTwo, Alice ->
|
||||
__EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
| PickTwo,Bob ->
|
||||
__EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
end
|
||||
|
||||
(** `config_value c` is an heuristic evaluation of the config `c`,
|
||||
Alice wants to minimize it whereas Bob wants to maximize it *)
|
||||
let function config_value (c:config) : int =
|
||||
c.score_alice - c.score_bob
|
||||
|
||||
use array.Init
|
||||
|
||||
(* QUESTION 4 *)
|
||||
let config0 () : config
|
||||
ensures { result.stack.length = 5 }
|
||||
ensures { result.stack[0] = 20 }
|
||||
ensures { result.stack[1] = 17 }
|
||||
ensures { result.stack[2] = 24 }
|
||||
ensures { result.stack[3] = -30 }
|
||||
ensures { result.stack[4] = 27 }
|
||||
ensures { result.pos = 0 }
|
||||
ensures { result.turn = Alice }
|
||||
ensures { result.score_alice = 0 }
|
||||
ensures { result.score_bob = 0 }
|
||||
ensures { inv result }
|
||||
=
|
||||
let s = init 5 [| 20; 17; 24; -30; 27 |] in
|
||||
{ stack = s;
|
||||
pos = 0;
|
||||
turn = Alice;
|
||||
score_alice = 0;
|
||||
score_bob = 0;
|
||||
}
|
||||
|
||||
(* You can run the test above using:
|
||||
why3 execute min_game.mlw --use MinGame "config0 ()"
|
||||
*)
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
(** {2 The MiniMax value of a tree of moves} *)
|
||||
|
||||
module MiniMax
|
||||
|
||||
use MinGame
|
||||
use int.MinMax
|
||||
|
||||
(* QUESTION 5 *)
|
||||
|
||||
(** [minimax c d] returns the minimax evaluation of config [p]
|
||||
at depth [d]. *)
|
||||
let rec function minimax (c:config) (d:int) : int
|
||||
requires { inv c }
|
||||
variant { __VARIANT_TO_BE_COMPLETED__ }
|
||||
= if d <= 0 then __EXPRESSION_TO_BE_COMPLETED__ () else
|
||||
match legal_moves c with
|
||||
| None -> __EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
| Some(m1,m2) ->
|
||||
match c.turn with
|
||||
| Alice -> (* Alice wants to minimize the config value *)
|
||||
min (minimax (do_move c m1) (d-1)) (minimax (do_move c m2) (d-1))
|
||||
| Bob -> (* Bob wants to maximize the config value *)
|
||||
__EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
end
|
||||
end
|
||||
|
||||
(* QUESTION 6 *)
|
||||
|
||||
(** Testing `minimax` on the sample configuration by concrete execution *)
|
||||
let test0 () =
|
||||
let c0 = config0 () in
|
||||
(minimax c0 0,
|
||||
minimax c0 1,
|
||||
minimax c0 2,
|
||||
minimax c0 3,
|
||||
minimax c0 4,
|
||||
minimax c0 5)
|
||||
|
||||
(* You can run the tests above using:
|
||||
why3 execute min_game.mlw --use MiniMax "test0 ()"
|
||||
*)
|
||||
|
||||
(** Testing `minimax` on the sample configuration with provers *)
|
||||
let test_minimax () =
|
||||
let c0 = config0 () in
|
||||
assert { minimax c0 0 = 0 };
|
||||
assert { minimax c0 1 = 20 };
|
||||
assert { minimax c0 2 = 3 };
|
||||
assert { minimax c0 3 = -3 }
|
||||
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** {2 The alpha-beta algorithm} *)
|
||||
|
||||
module AlphaBeta
|
||||
|
||||
use int.MinMax
|
||||
use MinGame
|
||||
use MiniMax
|
||||
|
||||
(** `lt_alpha_n alpha n` means `alpha < n` *)
|
||||
let predicate lt_alpha_n (alpha: option int) (n:int) =
|
||||
match alpha with
|
||||
| None -> true
|
||||
| Some a -> a < n
|
||||
end
|
||||
|
||||
(** `lt_n_beta n beta` means `n < beta` *)
|
||||
let predicate lt_n_beta (n:int) (beta: option int) =
|
||||
match beta with
|
||||
| None -> true
|
||||
| Some b -> n < b
|
||||
end
|
||||
|
||||
(** `max_alpha alpha n` is the maximum of `alpha` and `n` *)
|
||||
let max_alpha (alpha: option int) (n:int) : option int =
|
||||
match alpha with
|
||||
| None -> Some n
|
||||
| Some a -> Some (max a n)
|
||||
end
|
||||
|
||||
(** `min_beta n beta` is the minimum of `n` and `beta` *)
|
||||
let min_beta (n:int) (beta: option int) : option int =
|
||||
match beta with
|
||||
| None -> Some n
|
||||
| Some b -> Some (min n b)
|
||||
end
|
||||
|
||||
(* QUESTIONS 7 and 8 *)
|
||||
|
||||
let rec alpha_beta (alpha beta:option int) (c:config) (d:int) : int
|
||||
requires { inv c }
|
||||
requires { __FORMULA_TO_BE_COMPLETED__ }
|
||||
variant { __VARIANT_TO_BE_COMPLETED__ }
|
||||
ensures { __FORMULA_TO_BE_COMPLETED__ }
|
||||
= __EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
|
||||
(* QUESTIONS 9 and 10 *)
|
||||
|
||||
exception GameEnded
|
||||
|
||||
let best_move (c:config) (d:int) : move
|
||||
requires { inv c }
|
||||
ensures { __FORMULA_TO_BE_COMPLETED__ }
|
||||
raises { GameEnded -> __FORMULA_TO_BE_COMPLETED__ }
|
||||
= raise GameEnded (* TO BE COMPLETED *)
|
||||
|
||||
let test_alphabeta () =
|
||||
let c0 = config0 () in
|
||||
try
|
||||
(best_move c0 1,
|
||||
best_move c0 2,
|
||||
best_move c0 3,
|
||||
best_move c0 4)
|
||||
with GameEnded -> absurd
|
||||
end
|
||||
|
||||
(* You can run the test above using:
|
||||
why3 execute num_game.mlw --use AlphaBeta "test_alphabeta ()"
|
||||
*)
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** {2 An efficient algorithm for the Min game} *)
|
||||
|
||||
(** Best move found by dynamic programming *)
|
||||
|
||||
|
||||
|
||||
module Dynamic
|
||||
|
||||
|
||||
|
||||
use int.Int
|
||||
use int.MinMax
|
||||
use array.Array
|
||||
|
||||
use MinGame
|
||||
use MiniMax
|
||||
|
||||
|
||||
(** QUESTION 13 *)
|
||||
|
||||
(* Lemma relating the minimax value of a configuration to the minimax
|
||||
value of the same configuration with score set to zero. *)
|
||||
|
||||
let rec lemma minimax_independence (c:config) (d:int) : unit
|
||||
requires { inv c }
|
||||
requires { __FORMULA_TO_BE_COMPLETED__ }
|
||||
variant { __VARIANT_TO_BE_COMPLETED__ }
|
||||
ensures { minimax c d =
|
||||
minimax { c with score_alice = 0 ; score_bob = 0 } d +
|
||||
__TERM_TO_BE_COMPLETED__ }
|
||||
= __EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
|
||||
|
||||
|
||||
|
||||
(* QUESTION 16 *)
|
||||
|
||||
predicate dynamic_inv_at_index (stack:array int) (i:int) (a:array int) =
|
||||
forall t:player, sa sb : int, d:int.
|
||||
let c =
|
||||
{ stack = stack; pos = i; turn = t; score_alice = sa; score_bob = sb }
|
||||
in
|
||||
(* relating `minimax c d` to a[i] *)
|
||||
__FORMULA_TO_BE_COMPLETED__
|
||||
|
||||
(* QUESTION 15 and 17 *)
|
||||
|
||||
let dynamic (stack : array int) : int
|
||||
requires { __FORMULA_TO_BE_COMPLETED__ }
|
||||
ensures { forall d:int. __FORMULA_TO_BE_COMPLETED__ }
|
||||
(* relating the result to minimax *)
|
||||
=
|
||||
let l = stack.length in
|
||||
let a = Array.make (l+1) 0 in
|
||||
for n = l-2 downto 0 do
|
||||
invariant { __FORMULA_TO_BE_COMPLETED__ }
|
||||
a[n] <- __EXPRESSION_TO_BE_COMPLETED__ ();
|
||||
done;
|
||||
a[0]
|
||||
|
||||
let test () =
|
||||
let c0 = config0 () in
|
||||
dynamic c0.stack
|
||||
(* You can run the test above using:
|
||||
why3 execute min_game.mlw --use Dynamic "test ()"
|
||||
*)
|
||||
|
||||
|
||||
|
||||
(* QUESTION 18 *)
|
||||
|
||||
let dynamic_opt (stack : array int) : int
|
||||
requires { __FORMULA_TO_BE_COMPLETED__ }
|
||||
ensures { __FORMULA_TO_BE_COMPLETED__ }
|
||||
= __EXPRESSION_TO_BE_COMPLETED__ ()
|
||||
|
||||
|
||||
end
|
||||
82
test_min_game.ml
Normal file
82
test_min_game.ml
Normal file
@ -0,0 +1,82 @@
|
||||
|
||||
open Format
|
||||
|
||||
let run msg f d =
|
||||
let t = Unix.gettimeofday () in
|
||||
let x = f d in
|
||||
let t = Unix.gettimeofday () -. t in
|
||||
printf "@[[%2.2f] %s(%d): %a@]@." t msg d Z.pp_print x
|
||||
|
||||
let z = Z.of_int
|
||||
|
||||
(* pseudo-random arrays as test *)
|
||||
let random_array size =
|
||||
let () = Random.init 2024 in
|
||||
Array.init size (fun _ -> z (Random.int 2024 - 1000))
|
||||
|
||||
open MinGameExtract
|
||||
|
||||
let random_config size : config = {
|
||||
stack = random_array size;
|
||||
pos = z 0;
|
||||
turn = Alice;
|
||||
score_alice = z 0;
|
||||
score_bob = z 0;
|
||||
}
|
||||
|
||||
let () =
|
||||
(* testing alpha-beta *)
|
||||
let f d = MinGameExtract.alpha_beta None None (random_config d) (z d) in
|
||||
run "alpha_beta" f 0;
|
||||
run "alpha_beta" f 1;
|
||||
run "alpha_beta" f 2;
|
||||
run "alpha_beta" f 3;
|
||||
run "alpha_beta" f 5;
|
||||
run "alpha_beta" f 10;
|
||||
run "alpha_beta" f 15;
|
||||
run "alpha_beta" f 20;
|
||||
run "alpha_beta" f 25;
|
||||
run "alpha_beta" f 30;
|
||||
run "alpha_beta" f 35;
|
||||
(* comment some of the tests below if it takes too long time *)
|
||||
run "alpha_beta" f 40;
|
||||
run "alpha_beta" f 41;
|
||||
run "alpha_beta" f 42;
|
||||
run "alpha_beta" f 43;
|
||||
run "alpha_beta" f 44;
|
||||
run "alpha_beta" f 45;
|
||||
run "alpha_beta" f 46;
|
||||
run "alpha_beta" f 47;
|
||||
run "alpha_beta" f 48;
|
||||
run "alpha_beta" f 49;
|
||||
run "alpha_beta" f 50;
|
||||
run "alpha_beta" f 51;
|
||||
(* testing dynamic programming *)
|
||||
let h d = MinGameExtract.dynamic (random_array d) in
|
||||
run "dynamic" h 0;
|
||||
run "dynamic" h 1;
|
||||
run "dynamic" h 2;
|
||||
run "dynamic" h 3;
|
||||
run "dynamic" h 5;
|
||||
run "dynamic" h 10;
|
||||
run "dynamic" h 15;
|
||||
run "dynamic" h 20;
|
||||
run "dynamic" h 25;
|
||||
run "dynamic" h 30;
|
||||
run "dynamic" h 35;
|
||||
run "dynamic" h 40;
|
||||
run "dynamic" h 41;
|
||||
run "dynamic" h 42;
|
||||
run "dynamic" h 43;
|
||||
run "dynamic" h 44;
|
||||
run "dynamic" h 45;
|
||||
run "dynamic" h 46;
|
||||
run "dynamic" h 47;
|
||||
run "dynamic" h 48;
|
||||
run "dynamic" h 49;
|
||||
run "dynamic" h 50;
|
||||
run "dynamic" h 51;
|
||||
run "dynamic" h 100;
|
||||
run "dynamic" h 1024;
|
||||
run "dynamic" h 2024;
|
||||
()
|
||||
Loading…
x
Reference in New Issue
Block a user