Up

# moduleStrat

: 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.

#
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
end