strat.ml

(**************************************************************************)
(*                                                                        *)
(*  Ocamlgraph: a generic graph library for OCaml                         *)
(*  Copyright (C) 2004-2007                                               *)
(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2, with the special exception on linking              *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* $Id:$ *)

(* Signature for graphs *)
module type G = sig

  type t

  module V : Sig.ORDERED_TYPE

  type vertex = V.t

  val mem_vertex : t -> vertex -> bool

  val succ : t -> vertex -> vertex list

  val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a
  val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
end


(* Signature for graph add-ons: an initial vertex, final vertices
   and membership of vertices to either true or false,
   i.e. first or second player *)
module type PLAYER = sig

  type t
  type vertex

  val get_initial : t -> vertex
  val is_final : t -> vertex -> bool

  val turn : t -> vertex -> bool

end


(* Signature for strategies : for a given state, the strategy tells
   which state to go to *)
module type STRAT = sig

  type t
  type vertex

  val empty : t
  val add : t -> vertex -> vertex -> t

  val next : t -> vertex -> vertex
    (* Raises Invalid_argument if vertex's image is not defined *)

end


(* Implements strategy algorithms on graphs *)
module Algo (G : G) (P : PLAYER with type vertex = G.vertex)
  (S : STRAT with type vertex = G.vertex) :
sig

  (* coherent_player g p returns true iff
     the completion p is coherent w.r.t.
     the graph g *)
  val coherent_player : G.t -> P.t -> bool

  (* coherent_strat g s returns true iff
     the strategy s is coherent w.r.t.
     the graph g *)
  val coherent_strat : G.t -> S.t -> bool

  (* game g p a b returns true iff a wins in g
     given the completion p (i.e. the game
     goes through a final state). *)
  val game : G.t -> P.t -> S.t -> S.t -> bool

  (* strategy g p s returns true iff s wins in g
     given the completion p, whatever strategy
     plays the other player. *)
  val strategy : G.t -> P.t -> S.t -> bool

  (* strategyA g p returns true iff there
     exists a winning stragegy for the true
     player. In this case, the winning
     strategy is provided. *)
  val strategyA : G.t -> P.t -> (bool * S.t)
end = struct

    module SetV = Set.Make (G.V)


    let rec eq l1 l2 = match l1, l2 with
	[], [] -> true
      | e1 :: l1', e2 :: l2' ->
	  (e1 = e2) && (eq l1' l2')
      | _ -> false

    let rec eq_mem i l1 l2 = match l1, l2 with
	[], [] -> (true, false)
      | e1 :: l1', e2 :: l2' ->
	  if e1 = e2 then
	    if e1 = i then (eq l1' l2', true)
	    else eq_mem i l1' l2'
	  else (false, false)
      | _ -> (false, false)

    let puit g v = match G.succ g v with
	[] -> true
      | _ -> false


    let get_finals g p =
      let f a l =
	if P.is_final p a then a :: l
	else l
      in G.fold_vertex f g []


    let coherent_player g p =
      G.mem_vertex g (P.get_initial p)


    let coherent_strat g s =
      let f v b =
	try
	  let v' = S.next s v in
	    b && (G.mem_vertex g v')
	with Invalid_argument _ -> true
      in
	G.fold_vertex f g true


    let game g p a b =

      let rec game_aux l pi =
	let continue x =
	  try
	    game_aux (SetV.add pi l) (S.next x pi)
	  with Invalid_argument _ -> false
	in
	  (P.is_final p pi) ||
	    (if SetV.mem pi l then false
	     else
	       if P.turn p pi then continue a
	       else continue b)

      in
	game_aux SetV.empty (P.get_initial p)


    let rec attract1 g p s l =
      let f v l1 =
	if not (List.mem v l1) then
	  if P.turn p v then
	    try
	      if List.mem (S.next s v) l1 then v :: l1
	      else l1
	    with Invalid_argument _ -> l1
	  else
	    if puit g v then l1
	    else
	      if G.fold_succ (fun v' b -> b && (List.mem v' l1)) g v true
	      then v :: l1
	      else l1
	else l1
      in
	G.fold_vertex f g l


    let rec strategy g p s =

      let rec strategy_aux l1 l2 =
	let (b1, b2) = eq_mem (P.get_initial p) l1 l2 in
	  if b1 then b2
	  else strategy_aux (attract1 g p s l1) l1

      in
      let finaux = get_finals g p in
	strategy_aux (attract1 g p s finaux) finaux
	  

    let rec attract g p (l, l') =
      let f v (l1, l1') =
	if not (List.mem v l1) then
	  if P.turn p v then
	    let f' v' l2 =
	      (match l2 with
		   [] ->
		     if List.mem v' l1 then [v']
		     else []
		 | _ -> l2) in
	      (match G.fold_succ f' g v [] with
		   [] -> (l1, l1')
		 | v' :: _ -> (v :: l1, S.add l1' v v' ))
	  else
	    if puit g v then (l1, l1')
	    else
	      if G.fold_succ (fun v' b -> b && (List.mem v' l1)) g v true
	      then (v :: l1, l1')
	      else (l1, l1')
	else (l1, l1')
      in
	G.fold_vertex f g (l, l')


    let rec strategyA g p =

      let rec strategyA_aux l1 l2 f =
	let (b1, b2) = eq_mem (P.get_initial p) l1 l2 in
	  if b1 then (b2, f)
	  else
	    let (new_l1, new_f) = attract g p (l1, f) in
	      strategyA_aux new_l1 l1 new_f

      in
      let finaux = get_finals g p in
      let (l, r) = attract g p (finaux, S.empty) in
	strategyA_aux l finaux r;;

  end