module Strat

: sig

Strategies

Implementation of a winning strategy of a graph: the graph represents a two players game, each vertex belongs to either player (whose turn it is to play) and describes a configuration of the game. The algorithm computes the winning strategy of a player, if any; i.e. the moves to play (which vertex to go to) so that for all possible moves of the other player, the game goes through a final state.

Author Nicolas Ayache

module type G = sig

Signature for graphs

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

module type PLAYER = sig

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

type t

type vertex

val get_initial : t -> vertex

val is_final : t -> vertex -> bool

val turn : t -> vertex -> bool

end

module type STRAT = sig

Signature for strategies: for a given state, the strategy tells which state to go to

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

module Algo : functor (G : G) -> functor (P : PLAYER with type vertex = G.vertex) -> functor (S : STRAT with type vertex = G.vertex) -> sig

Implements strategy algorithms on graphs

val coherent_player : G.t -> P.t -> bool

coherent_player g p returns true iff the completion p is coherent w.r.t. the graph g

val coherent_strat : G.t -> S.t -> bool

coherent_strat g s returns true iff the strategy s is coherent w.r.t. the graph g

val game : G.t -> P.t -> S.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 strategy : G.t -> P.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 strategyA : G.t -> P.t -> bool * S.t

strategyA g p returns true iff there exists a winning stragegy for the true player. In this case, the winning strategy is provided.

end