Synthesising a Game Solver in Imandra

In this notebook we introduce a simple game called "Les Bâtonnets Géants", and show how imandra can be exploited to synthesise a strategy which always wins. The game itself consists of 16 pegs, and opponents take turns in taking 1,2 or 3 pegs from the end. The loser is the player with 1 remaining peg a their turn. Imandrabot

Game specific rules

Let us first set up a very simple representation of this game consisting of a state which is either in play with n pieces or ended with a winner:

In [1]:
type choice = int
;;

type player = 
  | Imandra
  | Opponent 
;;

type state = 
  | Inplay of int
  | Terminal of player
;;

let create_initial_state n = 
  Inplay n;;

let final_state n = 
  n=1
;;

let remove_pins num_pins state = 
 match state with 
 | Terminal p -> Terminal p 
 | Inplay n -> if n-num_pins >= 1 then Inplay (n - num_pins) else Inplay n
;;
Out[1]:
type choice = int
type player = Imandra | Opponent
type state = Inplay of int | Terminal of player
val create_initial_state : int -> state = <fun>
val final_state : Z.t -> bool = <fun>
val remove_pins : Z.t -> state -> state = <fun>

Now let us also set up simple functions which describe a "move" in the game, given by the function step, and two functions which find all the valid choices for a given state, and determine if a move is valid for a given state.

In [2]:
let step choice state = 
  if choice <=0 || choice >3 then state else remove_pins choice state
;;

let find_all_available_choices state = 
 match state with 
 | Inplay n -> 
  if n>3 then [1;2;3] else if n>2 then [2;1] else if n>1 then [1]
 else []
 | Terminal _ -> [];;

let is_valid_choice choice state =
  choice <=3 && choice >=1 && match state with 
  | Inplay s -> s > choice 
  | Terminal _ -> false;;
Out[2]:
val step : int -> state -> state = <fun>
val find_all_available_choices : state -> Z.t list = <fun>
val is_valid_choice : int -> state -> bool = <fun>

Above are the specific functions we need for this game. In what follows a generalised architecture for solving adversarial games is given - this could be viewed as similar to a Functor structure in OCaml where the specific functions given for game of Batonnets Géants are those given above.

General solver synthesis functions

We introduce first a function called one_step which assumes the player of the game is Imandra. The function takes a list of possible states as well as a map between states and choices. For each list of states the choice is played, resulting in a new list of states. If any of these states are in a final state they become "annealed" to the Terminal variant of state declaring Imandra as the winner. For any non-terminal states, every possible opponent play is calcuated using the function find_all_available_choices to calculate all the next possible states.

In [3]:
let one_step (choice_map: (state*choice) list) (states:state list): state list = 
  let new_states = 
    List.fold_left (fun acc el -> 
        match List.find (fun (x,_) -> x=el) choice_map with 
        | None -> el::acc
        | Some (_,choice) -> 
          let a = step choice el in if List.mem a acc then acc else
            (step choice el)::acc) [] states in
  let annealed_states = List.map (fun x -> 
      match x with 
      | Inplay l -> 
        if final_state l then Terminal Imandra else Inplay l 
      | Terminal p -> Terminal p
    ) new_states in 
  List.fold_left (fun acc el -> 
      match el with 
      | Terminal p -> (Terminal p)::acc
      | Inplay l -> 
        let next_states = List.fold_left (fun acc el -> 
            (step el (Inplay l))::acc
          ) [] (find_all_available_choices (Inplay l)) in 
        List.fold_left (fun acc el -> if List.mem el acc then acc else el::acc) acc next_states
    ) [] annealed_states
;;
Out[3]:
val one_step : (state * choice) list -> state list -> state list = <fun>

Using Imandra to synthesise a solver

We now introduce a function which takes an initial state and a set of steps and returns true if every resulting list of states is a winning state for Imandra.

In [4]:
let init_state = create_initial_state 16;;

let instance_function init_state steps =   
  let states,validity_cond = List.fold_left (fun acc el -> 
      match acc with 
      | first,second -> 
        (one_step el first,
         second && (
           let fsts = List.map fst el in 
           fsts=first && 
           List.for_all (
             fun (s,c) -> 
               match List.find (fun (x,_) -> x = s) el with 
               | None -> false 
               | Some (s,c) -> is_valid_choice c s 
           ) el
         )
        )) ([init_state],true) steps in 
  validity_cond &&
  List.for_all (fun x ->
      match x with 
      | Terminal Imandra -> true 
      | _ -> false) states;;
Out[4]:
val init_state : state = Inplay 16
val instance_function : state -> (state * choice) list list -> bool = <fun>

Now we can exploit Imandra's technology to find a solution for the game - in this case using [@@blast] to find the solution:

In [5]:
instance (fun steps -> 
    instance_function init_state steps) [@@blast];;
Out[5]:
- : (state * choice) list list -> bool = <fun>
module CX : sig val steps : (state * Z.t) list list end
Instance (after 497 steps, 27.286s):
  let steps =
    [[(Inplay 16, 3)]; [(Inplay 12, 3); (Inplay 11, 2); (Inplay 10, 1)];
     [(Inplay 8, 3); (Inplay 7, 2); (Inplay 6, 1)];
     [(Inplay 4, 3); (Inplay 3, 2); (Inplay 2, 1)]]
Instance

Playing against Imandra

Now this is a strategy for the game, we can write a simple game player to play against.

In [6]:
[@@@program]
let rec gather_inputs max = 
    let user_input = read_line () in
    if user_input = "" then gather_inputs max else
      let n = String.to_nat user_input in
      match n with 
      | None -> gather_inputs max 
      | Some n -> 
      if n <=0 || n >max then gather_inputs max else 
      n;;
      

let winner_message p =
  match p with Imandra -> "imandra wins " | Opponent -> "you win";;

let print_state state = 
  let rec print_state_aux l = 
    if l <=0 then "\n"
    else "|"^(print_state_aux (l-1)) in
  match state with 
  | Terminal p -> 
    winner_message p
  | Inplay l -> 
    print_state_aux l;;

let print_choice choice = 
  String.of_int choice;;

let rec play_against_imandra state solver  = 
  match state with 
  | Terminal p -> 
    print_endline (winner_message p)
  | Inplay l -> 
    if final_state l then 
      print_endline (winner_message Imandra)
    else
      begin
        match solver with 
        | [] -> ()
        | h::t -> 
          begin
            match List.find (fun (x,_) -> x = state) h with 
            | None -> print_endline "Solver error"; ()
            | Some (_,choice) -> 
              begin 
                let next_state = step choice state in 
                print_endline ("Imandra plays: "^ (print_choice choice)^"\n");
                print_endline (print_state next_state);
                if (match next_state with |Inplay l -> final_state l | _ -> false)then
                  print_endline "Imandra wins\n"else
                  print_endline "Enter your choices";
                let user_choice = gather_inputs (match next_state with Terminal _ -> 0 | Inplay n -> n-1 ) in
                if is_valid_choice user_choice next_state
                then 
                  let next_state = step user_choice next_state in 
                  print_endline ("You played: "^ (print_choice user_choice)^"\n");
                  print_endline (print_state next_state);
                  if (match next_state with |Inplay l -> final_state l | _ -> false)then
                    print_endline "You win\n"else
                    play_against_imandra next_state t
                else 
                  print_endline "invalid choices - replaying...";
                play_against_imandra state solver 
              end
          end
      end
;;
Out[6]:
val gather_inputs : int -> int = <fun>
val winner_message : player -> string = <fun>
val print_state : state -> String.t = <fun>
val print_choice : int -> String.t = <fun>
val play_against_imandra : state -> (state * int) list list -> unit = <fun>

By invoking the following code in program mode it is possible to play against imandra, but never win:

let play () = 
  print_endline (print_state init_state);
  play_against_imandra init_state CX.steps
;;

play ();;

An example trace is:

  play ();;
||||||||||||||||

Imandra plays: [3]

|||||||||||||

Enter your choices
1
You played: [1]

||||||||||||

Imandra plays: [3]

|||||||||

Enter your choices
2
You played: [2]

|||||||

Imandra plays: [2]

|||||

Enter your choices
1
You played: [1]

||||

Imandra plays: [3]

|

Imandra wins