RCS "$Id: GameCheck.str,v 1.84 1998/08/13 11:39:03 pxs Exp $";
(* Model checker based on Stirling games. *)
functor GameCheck ( structure Ag : AGENT_WRAPPER;
structure L : LOGIC2_PROTECTED;
sharing Ag.A = L.M.A) : GAMECHECK =
struct
structure Ag = Ag
structure A = Ag.A
structure AgentHash = HashTable
open L
type index = (int Vector.vector)
(* ints are saying when this decision was added so we can tell when we *)
(* may have invalidated it. 0 means never invalidate this one. *)
(* a decision is Safe if it always applies: no need to check or keep index *)
datatype decision = Safe of int
(* index is the index where we added the decision, obviously *)
| Unsafe of (int * index)
type config = Ag.agent * prop
(* type node represents an annotated node of the game graph, as known so far *)
(* Config uniquely determines node: see function makeNode below. *)
datatype node = DUMMY of
(config * (* where is this node? *)
node list option *
(* successors, if known? *)
(* WARNING: dependency: the A-decision list must be in sync with the *)
(* move node-list. Better way to do this? (O for mutually rec. datatypes.) *)
(decision list * decision list) * (* abelard, eloise: see defn above *)
node list * (* if A-choice with A-dec, what move *)
(* in the strategy justify A-decisions? *)
(index * int * (bool ref * bool ref)) option
(* Is there an occurrence in playList? At what index? What count? *)
(* Has it been used as an assumption for abelard? for eloise? *)
) ref
type position = node * index
type 'a configTable = (prop, (Ag.agent, 'a) HashTable.hash_table)
HashTable.hash_table
exception NotKnownHere
fun getPropEntry l prop = (HashTable.lookup l prop)
handle NotKnownHere => raise (PanicNoisily "GameCheck, getPropEntry")
fun setPropEntry l (key, value) = (HashTable.insert l (key,value); l)
fun noPropEntry _ = HashTable.mkTable (hashval, op =) (126,NotKnownHere)
val applyProp = HashTable.appi
val listPropEntries = HashTable.listItemsi
fun configString (agent, prop) = (Ag.mkstr agent)^"\n"^(L.printString prop)
fun getConfigEntry l (agent,prop) = HashTable.lookup (HashTable.lookup l prop)
agent
fun setConfigEntry l ((agent,prop), value) =
let
(* val _ = UI.debugFn (fn _ => "setConfigEntry for "^(configString (agent, prop))) *)
val agentTable = (HashTable.lookup l prop)
handle NotKnownHere =>
let val emptyAgentTable = HashTable.mkTable (Ag.hashval, Ag.eq)
(1024, NotKnownHere)
in (setPropEntry l (prop, emptyAgentTable); emptyAgentTable)
end
in (AgentHash.insert agentTable (agent, value); value)
end
fun noConfigEntry _ = noPropEntry()
fun deleteConfigEntry l (agent, prop) =
((* UI.debugFn (fn _ => "deleteConfigEntry for "^(configString (agent, prop))); *)
(AgentHash.remove (getPropEntry l prop) agent))
handle NotKnownHere => raise PanicNoisily
"GameCheck, deleteConfigEntry"
fun configTableString eltStr t =
List.foldr
(fn ((prop,agentTable),soFar) => soFar^
"\n\nMoves from "^(L.printString prop)^"\n"^
(List.foldr
(fn ((agent, value),soFar2) => soFar2^"\n"^(Ag.mkstr agent)^" => \n"^
(eltStr value))
"" (AgentHash.listItems agentTable)))
"" (listPropEntries t)
(* We replace fixpoints by their variables. Here's a fun that does that *)
fun variableize p =
case real p of
(Max (X,phi)) => makeProp(Var X)
| (Min (X,phi)) => makeProp(Var X)
| _ => p
(* Let's have a more concise description of a strategy. *)
(* Print it as we go because concatenating this string is slooooooooow *)
fun printStrategyString table =
let val printIt = UI.print
val _ = printIt
("We divide the reachable configurations according to proposition.\n"^
"We omit positions from which there's only one legal move.")
fun f (prop,agentTable) =
let val l = AgentHash.listItems agentTable
val start =
"\n=========================================================================\n"
^(L.printString prop)^"\n"
fun whichOfTwoProps word (p,q) =
let val (pv,qv) = (variableize p, variableize q)
fun separate (left, right) [] = (left, right)
| separate (left, right) ((agent, (_, prop))::t) =
let val propv = variableize prop
in if propv = pv then separate (agent::left, right) t
else if propv = qv then separate (left, agent::right) t
else raise PanicNoisily "GameCheck, strategyString"
end
val (takeLeft, takeRight) = separate ([],[]) l
in if null takeLeft then
if null takeRight then ()
else printIt(start^"always take the right "^word)
else if null takeRight
then printIt(start^"always take the left "^word)
else printIt
(start^"take the left "^word^" from these agents:\n\n"^
(Lib.mkstr Ag.mkstr "\n" takeLeft)^
"\n\nand take the right "^word^" from these agents:\n\n"^
(Lib.mkstr Ag.mkstr "\n" takeRight))
end
(* Really, should filter out cases where there is only one valid successor, *)
(* but that's a bit harder. Worth doing? I dunno. *)
fun whichSuccessor _ =
(printIt (start^"these agents may occur:");
(map (fn (ag1, (ag2, _)) =>
printIt("\nfrom\n"^(Ag.mkstr ag1)^"\nmove to\n"^(Ag.mkstr ag2)))
l);
())
in case real prop of
(And (p,q)) => whichOfTwoProps "conjunct" (p,q)
| (Or (p,q)) => whichOfTwoProps "disjunct" (p,q)
| (Nec (m,p)) => whichSuccessor()
| (Pos (m,p)) => whichSuccessor()
| _ => raise PanicNoisily "GameCheck, strategyString, not a choice point"
end
in (map (fn x => (f x)) (HashTable.listItemsi table); ())
end
(* position and as-yet-unexplored successor nodes *)
type gameListItem = position * node list
fun init _ = ref (HashTable.mkTable (Ag.hashval, Ag.eq) (1024,NotKnownHere))
: (Ag.agent, node) HashTable.hash_table ref
(************************** Players *****************************************)
(* Eloise (Player) is CPS' Player II. Abelard (Opponent) is Player I. *)
(* Abandonned P/O, mostly(!) because it's too confusing with type player *)
(****************************************************************************)
type player = bool
val eloise = true
val abelard = false
fun playerString b = if b then "Eloise"
else "Abelard"
val (pString, oString) = (playerString eloise, playerString abelard)
val other = not (* excessive? historic! *)
datatype mover = Referee | Player of player
(* When we go through a fixpoint we record the fact, so that at each fixpoint*)
(* we can quickly check whether it's a repeat, and who wins. *)
(* When we meet such a repeat won by PlayerA, later decisions for A will be *)
(* vulnerable until/unless we backtrack through the fixpoint checking for A *)
(* If we end up backtracking checking for B we need to recognise that these *)
(* decisions are unusable. We use counters in the assumptions and decisions *)
(* to recognise these ones. This also lets us not *actually* remove them. *)
(* NB same reference, now! *)
val counts as (oCount, pCount) = let val r = ref 0 in (r, r) end
fun pairMember player = if player then snd else fst
(* Segments say which counts mean this decision is invalid. *)
(* Segments are non-overlapping, ordered from high to low. *)
val invalidSegments as (invalidOSegments, invalidPSegments) =
(ref []: (int * int) list ref, ref []: (int * int) list ref)
fun segmentsString l = Lib.mkstr (fn (x,y) : int * int
=> "["^(Int.toString x)^","
^(Int.toString y)^"]") " " l
(* Record the fact that all decisions for player with numbers at least *)
(* leastInvalidNo and at most the current no are invalid. *)
fun invalidate (leastInvalidNo, player) =
let val selector = fn arghValueRestriction =>
pairMember player arghValueRestriction
val topR = selector counts
val top = !topR
val _ = UI.debugFn (fn _ =>
"Invalidating decisions for "^(playerString player)^
" from "^(Int.toString leastInvalidNo)^" to "^
(Int.toString top))
val segments = selector invalidSegments
fun addTo [] = [(top, leastInvalidNo)]
| addTo ((seg as (high,low))::t) =
if low > leastInvalidNo (* seg covered by [top,least...]*)
then addTo t
else if high < leastInvalidNo (* seg doesn't intersect with new bit *)
then (top, leastInvalidNo)::seg::t
else (top, low)::t (* coalesce *)
in (segments := addTo (!segments);
UI.debugFn (fn _ => "New segments: "^(segmentsString (!segments)));
inc topR) (* increment counter! *)
end
fun isValid player no = if no = 0 then true else
let val segments = !(pairMember player invalidSegments)
fun f [] = true
| f ((high,low)::t) = if high < no then true (* gone past no's place *)
else if low > no then f t else false
val answer = f segments
val _ = UI.debugFn (fn _ => let val s = if answer then " valid for "
else " invalid for "
in (Int.toString no)^s^(playerString player)
end)
in answer
end
val (TrueProp, FalseProp) = (makeProp True, makeProp False)
(* relevantSuccessors takes a modality and an agent and returns a list *)
(* of the successor agents which "satisfy" the modality. That is, if *)
(* the modality is a positive act list the state is reached via an *)
(* action in the list; if negative, by an action not in the list *)
fun relevantSuccessors (m, ag) = M.filter (m, (Ag.transitions ag))
(******************** MODEL-CHECKING FUNCTION ******************************)
fun modelCheck definitelyPlay (topLevelAgent, topLevelFormula) =
let
val counter = ref 0
val _ = (oCount := 0; pCount := 0;
invalidOSegments := []; invalidPSegments := [])
(* paranoia: let's avoid checking the debugging flag every time, it won't *)
(* change during model checking of one problem! *)
val debugFn = if UI.debuggingOn() then UI.debugFn else (fn _ => ())
val _ = UI.chat "Examining proposition..."
(************************** Propositions ************************************)
(* Return the no of variables used, and info about the props bound in order *)
(* It's convenient to have maxVar around as well: arrays start from 0 *)
(* Also doublecheck that the variables are in the right order; they should be*)
val (noOfVars, maxVar, propsBound) =
let val current = ref 0
fun check i = if i = (!current) then inc current
else raise PanicNoisily "GameCheck, checkOrder"
fun ex True = []
| ex False = []
| ex (Var v) = []
| ex (And (p,q)) = (examine p)@(examine q)
| ex (Or (p,q)) = (examine p)@(examine q)
| ex (Nec (m,p)) = examine p
| ex (Pos (m,p) )= examine p
| ex (phi as Max (v,p)) = (check v; (true,p))::(examine p)
| ex (phi as Min(v,p)) = (check v; (false,p))::(examine p)
and examine p = ex (real p)
val boundList = examine topLevelFormula
in (!current, (!current) - 1, boundList)
end
val (max, body) =
let val isMax = Array.fromList (map fst propsBound)
val bodies = Array.fromList (map snd propsBound)
in ((fn x => (Array.sub (isMax, x))
handle General.Subscript => raise PanicNoisily "GameCheck, max"),
(fn x => (Array.sub (bodies, x))
handle General.Subscript => raise PanicNoisily "GameCheck, body"))
end
(* A few handy array and vector fns, which assume things have size noOfVars *)
(* Apply a fn to the elements of an array, with index as key, in order. *)
fun applyToArray f i =
let fun g k =
if k > maxVar then ()
else (f (k,Array.sub(i,k)); g (k+1))
in g 0
end handle General.Subscript => raise PanicNoisily "GameCheck, applyToArray"
(* Apply a fn to the elements of an array, with index as key, in order. *)
fun applyToVector f i =
let fun g k =
if k > maxVar then ()
else (f (k,Vector.sub(i,k)); g (k+1))
in g 0
end handle General.Subscript => raise PanicNoisily "GameCheck, applyToVector"
fun arrayList a =
let fun from k = if k > maxVar then []
else (Array.sub (a,k))::(from (k+1))
in from 0
end handle General.Subscript => raise PanicNoisily "GameCheck, arrayList"
(* is there an index s.t. f (index, a[index]) = true? *)
fun arrayExists f a =
let fun from k = if k > maxVar then false
else if f(k,Array.sub (a,k)) then true else (from (k+1))
in from 0
end handle General.Subscript => raise PanicNoisily "GameCheck, arrayExists"
fun arrayString f a =
let fun from k = if k>maxVar then ""
else (f (Array.sub (a,k)))^" "^(from (k+1))
in "["^(from 0)^"]"
end handle General.Subscript => raise PanicNoisily "GameCheck, arrayString"
fun vectorString f a =
let fun from k = if k>maxVar then ""
else (f (Vector.sub (a,k)))^" "^(from (k+1))
in "["^(from 0)^"]"
end handle General.Subscript => raise PanicNoisily "GameCheck, vectorString"
(* Don't include Max or Min, since they don't appear in the game *)
(* In add, below, we rely on the fact that if X = sigma X.phi, *)
(* phi must occur before X! *)
(* A subformula (non-Var) may occur several times: consider this a bug? *)
fun subformulae z =
case real z of
True => [TrueProp]
| False => [FalseProp]
| (Var v) => []
| (And (p,q)) => z::((subformulae p)@(subformulae q))
| (Or (p,q)) => z::((subformulae p)@(subformulae q))
| (Max (Y,q)) => (subformulae q)@[makeProp(Var Y)]
| (Min (Y,q)) => (subformulae q)@[makeProp(Var Y)]
| (Nec (Y,q)) => z::(subformulae q)
| (Pos (Y,q)) => z::(subformulae q)
val subformsWithDuplication = subformulae topLevelFormula (* just for add *)
val subforms = SL.sort le true subformsWithDuplication (* for everywhere *)
(* We need to know, for each subformula phi, whether a given var X may occur*)
(* in a loop X -> phi -> X where X is the winning variable: that is, is X *)
(* active in phi? *)
val activeVarInfo = ref (noPropEntry()) :
(prop, bool Array.array) HashTable.hash_table ref
fun getActiveVars prop = getPropEntry (!activeVarInfo) prop
fun free z = case real z of
True => []
| False => []
| (Var v) => [v]
| (Or (p,q)) => (free p)@(free q)
| (And (p,q)) => (free p)@(free q)
| (Nec (Y,q)) => free q
| (Pos (Y,q)) => free q
| (Max (Y,q)) => filter (fn X => not (X=Y)) (free q)
| (Min (Y,q)) => filter (fn X => not (X=Y)) (free q)
(* Take a prop and list of its free vars. For each var, say X = sigma X.phi,*)
(* look up which vars are active in that phi. Which had better be known!*)
fun add (prop, l) =
let
val a = Array.array (noOfVars, false)
(* We have to be careful not to look up formulae we don't store active info *)
(* for, or to get into a loop *)
val earlierProps =
let val bodies = map body l
fun bodystar p =
if Lib.member (op =) (p, [TrueProp, FalseProp, prop]) then NONE
else case real p of (Max (Y,q)) => bodystar q
| (Min (Y,q)) => bodystar q
| _ => SOME p
in List.foldr (fn (p,ll) => case (bodystar p) of NONE => ll | SOME x => x::ll)
[] bodies
end
val arrays = map getActiveVars earlierProps
fun updateIfNec (k,_) =
(if Lib.member (op =) (k,l) (* k free in prop, so active *)
orelse List.exists (fn x => Array.sub (x,k)) arrays
(* k was active in body of some var which is free in prop, so active in prop *)
then Array.update (a,k,true)
else ())
in (applyToArray updateIfNec a;
activeVarInfo := setPropEntry (!activeVarInfo) (prop, a))
end
val _ = map (fn p => add (p, free p)) subformsWithDuplication
(* Now activeVarInfo really does record what we think it does! *)
(* If no subformula has both min and max variables active in it, then it *)
(* is always safe to use a decision: there is no need to store or compare *)
(* indexes with decisions. So see whether that's the case. *)
val nonAlternating = not (List.exists
(fn (_,a) =>
let fun activeMax (i,active) = active andalso (max i)
fun activeMin (i, active) = active andalso (not (max i))
in (arrayExists activeMax a) andalso (arrayExists activeMin a)
end)
(listPropEntries (!activeVarInfo)))
val _ =
let fun active [] = ""
| active ((prop,activeVars)::t) = (L.printString prop)^" "^
(arrayString Bool.toString activeVars)^"\n"^(active t)
val s = if nonAlternating then " not" else ""
in debugFn (fn _ =>
("The formula is"^s^" alternating\n"^
(active (listPropEntries (!activeVarInfo)))))
end
(* Just for fun, as an experiment, let's try playing with the order in which *)
(* we explore con/disjuncts. Maybe it's a good idea to explore things with *)
(* no or insignificant active variables first? *)
(* POSTPONED: maybe try this later. *)
(*************************** Indexes*****************************************)
(* An index stores in the ith slot, i.e. against the variable i, the number *)
(* of times X has been *)
(* unfolded since any "earlier" variable was unfolded. *)
(****************************************************************************)
fun indexString i = vectorString Int.toString i
(* Initially put 0 against all variables. *)
val initindex = Vector.tabulate (noOfVars, (fn _ => 0))
fun applyToIndex f i = applyToVector f (i)
fun indexSub (i,j) = (Vector.sub (i, j))
handle General.Subscript => raise PanicNoisily "GameCheck, indexSub"
(* find Y, increase its index, zero everything to its right. *)
(* We need a new copy, hence the tabulate call. *)
fun update Y j =
let val i = j
fun newEntry k =
if k < Y then Vector.sub (i, k)
else if k > Y then 0
else Vector.sub (i,Y) + 1
in Vector.tabulate (noOfVars, newEntry)
end handle General.Subscript => raise PanicNoisily "GameCheck, update"
(* index -> index -> player -> bool array -> boolean *)
(* compatindex says whether it is safe to reuse a decision for player b *)
(* which was stored at index old, to avoid exploring from index new *)
fun compatindex new old b safe =
let fun examine k =
if k > maxVar then true (* new and old were identical *)
else let val newVal = Vector.sub(new,k)
val oldVal = Vector.sub(old,k)
in if newVal = oldVal then examine (k+1)
else if Array.sub(safe,k) then true
else if newVal > oldVal then b = max k
else not (b = max k)
end
val answer = examine 0
val _ = debugFn
(fn _ => ((indexString new)^" "^(indexString old)^" "^(playerString b)^
" "^(if answer then " compatible" else " incompatible")))
in answer
end handle General.Subscript => raise PanicNoisily "GameCheck, compatindex"
(* If we have a repeat section with indexes from and to, who wins? The owner *)
(* of the leading difference, i.e. eloise iff most sig. var where to > from *)
(* is maximal. *)
fun winsOn from to =
let val _ = debugFn
(fn _ => "Comparing "^(indexString from)^" with "^(indexString to))
fun g k =
if k > maxVar then raise (PanicNoisily
"GameCheck, winsOn")
else if Vector.sub (to, k) > Vector.sub (from, k) then max k
else g (k+1)
in g 0
end handle General.Subscript => raise PanicNoisily "GameCheck, winsOn(2)"
(***************** Stuff about things we know or assume **********************)
val nodeStore = List.foldr (fn (x,l) => setPropEntry l (x, init()))
(noPropEntry()) subforms
(***************** Functions for manipulating nodes **************************)
fun getRef (DUMMY i) = i
fun getConfig n = let val i = getRef n
val (x,_,_,_,_) = !i
in x
end
fun getAgent n = let val i = getRef n
val ((x,_),_,_,_,_) = !i
in x
end
fun getProp n = let val i = getRef n
val ((_,x),_,_,_,_) = !i
in x
end
fun getNextMove n = let val i = getRef n
val (_,_,_,x,_) = !i
in x
end
fun getDecisionInfo n = let val i = getRef n
val (_,_,x,_,_) = !i
in x
end
fun setDecisionInfo (n, d) = let val i = getRef n
val (x,y,_,z,a) = !i
in i := (x,y,d,z,a)
end
fun getSuccessors n = let val i = getRef n
val (_,x,_,_,_) = !i
in x
end
fun setSuccessors (n, l) = let val i = getRef n
val (x,_,y,z,a) = !i
in i := (x,l,y,z,a)
end
fun pushNextMove (node, next) =
let val i = getRef node
val (x,y,z,w,a) = !i
in i := (x,y,z,next::w,a)
end
fun popNextMove node =
let val i = getRef node
val (x,y,z,w,a) = !i
in case w of
[] => raise PanicNoisily "GameCheck, popNextMove"
| (h::t) => i := (x,y,z,t,a)
end
fun getOccurrence n = let val i = getRef n
val (_,_,_,_,x) = !i
in x
end
fun setOccurrence (n, info) =
let val i = getRef n
val (x,y,z,a,_) = !i
in i := (x,y,z,a,info)
end
(* Notice that an effect of the way we do this is that it's OK to compare *)
(* nodes using = *)
fun makeNode (agent, rawProp) =
let
(* Since we now have to store some decision against True and False, may as *)
(* well be correct!! *)
val (dec,prop) = case real rawProp of
True => (([], [Safe 0]), rawProp)
| False => (([Safe 0], []), rawProp)
| _ => (([], []), variableize rawProp)
val agentTable = !(getPropEntry nodeStore prop )
in
case HashTable.find agentTable agent of
NONE => let val nodeRef = DUMMY (ref ((agent,prop),NONE, dec, [],NONE))
in (AgentHash.insert agentTable (agent, nodeRef); nodeRef)
end
| SOME(x) => x
end
(*****************************************************************************)
(* given a node, whose turn is it next? *)
fun whoseTurnNext node =
let (* Given a prop, whose turn is it next? (Silly q in some cases!)*)
fun wTurnNext True = Player(abelard)
| wTurnNext False = Player(eloise)
| wTurnNext (And _) = Player(abelard)
| wTurnNext (Or _) = Player(eloise)
| wTurnNext (Nec _) = Player(abelard)
| wTurnNext (Pos _) = Player(eloise)
| wTurnNext (Var _) = Referee
| wTurnNext (Min _) = Referee
| wTurnNext (Max _) = Referee
in wTurnNext (real (getProp node))
end
fun nodesConfigString n = configString (getConfig n)
fun positionString (node, index) =
nodesConfigString node^"\n"^(indexString index)
fun forgottenString player j = if isValid player j then "" else "FORGOTTEN "
fun decisionItemStringValid p (Safe j) =
(forgottenString p j)^"Safe "
| decisionItemStringValid p (Unsafe (j,l)) =
(forgottenString p j)^"Unsafe:"^(indexString l)
fun decisionStringValid (a, e) =
"Abelard: \n"^(Lib.mkstr (decisionItemStringValid abelard) " " a)^"\n"^
"Eloise: \n"^(Lib.mkstr (decisionItemStringValid eloise) " " e)^"\n"
fun infoString node =
let val config = nodesConfigString node
fun f [] = ""
| f (h::t) = (nodesConfigString h)^" "^(f t)
val next = f (getNextMove node)
val decisions = decisionStringValid (getDecisionInfo node)
in
"\nRecorded config: \n"^config^
"\nRecorded next move: \n"^next^
"\nRecorded decision: \n"^decisions
end
(* From a choice point, return SOME(node to try next, rest) or NONE if there *)
(* are no possible next nodes. *)
(* If there is a move recorded in the strategy, we try that first, because *)
(* it's the most likely to be right (because of our pessimistic reuse). *)
fun next node =
let val (ag,prop) = getConfig node
fun n (And(p,q)) = [makeNode(ag, p),makeNode(ag,q)]
| n (Or(p,q)) = [makeNode(ag, p),makeNode(ag,q)]
| n (Nec(m,p)) = map (fn x => makeNode(x,p))
(relevantSuccessors (m, ag))
| n (Pos(m,p)) = map (fn x => makeNode(x,p))
(relevantSuccessors (m, ag))
| n _ = raise PanicNoisily "GameCheck, next"
val allChoices = case getSuccessors node of
SOME l => l
| NONE => let val calculated = n (real prop)
in (setSuccessors (node, SOME calculated); calculated)
end
in case getNextMove node of
[] => (case allChoices of
[] => NONE
| (h::t) => SOME(h,t))
| (iNode::t) => SOME(iNode, filter (fn j => not (iNode=j)) allChoices)
end
(* We keep stacks of decisions (and corresponding next moves). Ones other *)
(* than the head are never needed, but may become the head later. *)
(* In fact, there are circumstances where we can discard some decisions, *)
(* saving space -- think about this more, Perdita. *)
val (addKnowledge, getKnowledge) =
if nonAlternating then
(* There's no alternation in the formula, so we don't need to store indexes *)
let fun addKnowledge ((position as (node : node, index : index)), b, m) =
let val _ = (debugFn
(fn _ => ("Adding simple decision for "^(playerString b)^
" at "^
(positionString position))))
val (oldAbD, oldElD) = getDecisionInfo node
val d = if b then (oldAbD, (Safe(!pCount))::oldElD)
else ((Safe(!oCount))::oldAbD, oldElD)
val _ = case m of NONE => () | (SOME next) => pushNextMove (node, next)
in setDecisionInfo (node, d)
end
(* call lookAtEloise only if there is no extant abelard decision. *)
fun lookAtEloise (node, [], w) = NONE
| lookAtEloise (node, ((Safe j)::t), w) =
if isValid eloise j then SOME(eloise)
else (setDecisionInfo (node, ([], t));
(if w = Player(eloise) then popNextMove(node) else ());
lookAtEloise (node, t, w))
| lookAtEloise (node, ((Unsafe _)::t), w) =
raise PanicNoisily "GameCheck, lookAtEloise (safe)"
fun lookAtAbelard (node, ([],d), w) = lookAtEloise (node, d, w)
| lookAtAbelard (node, (((Safe j)::t), d), w) =
if isValid abelard j then SOME(abelard)
else (setDecisionInfo (node, (t, d));
(if w = Player(abelard) then popNextMove(node) else ());
lookAtAbelard (node, (t, d), w))
| lookAtAbelard (node, (((Unsafe _)::t),d), w) =
raise PanicNoisily "GameCheck, lookAtAbelard (safe)"
fun getKnowledge (node, index) =
lookAtAbelard (node, getDecisionInfo node, whoseTurnNext node)
in (addKnowledge, getKnowledge)
end
else
let
(* Return an array to say for each variable whether, if we have indexes *)
(* whose leading difference is that variable, it's always safe to reuse *)
(* a decision for player there -- i.e. there is no "real alternation". *)
fun safetyInfo phi player =
let val other = other player
val active = getActiveVars phi
(* If k is not active in phi, a leading difference of k is safe *)
val safe = Array.tabulate (noOfVars,
(fn k => not(Array.sub (active, k))))
(* If there is no variable less significant than k and belonging to the *)
(* other player which is active in phi, leading diff at k is safe *)
fun noOppVar k =
let fun g i =
if i > maxVar then true (* we got to end without finding problem *)
else if (max i = other) andalso (Array.sub (active, i)) then false
else g (i+1) (* i wasn't a problem, keep looking *)
in g k (* vars more significant than leading diff don't matter *)
end
fun f (k,_) = if (noOppVar k) then Array.update (safe, k, true)
else ()
val _ = applyToArray f safe (* now safe is correct *)
val alwaysSafe = not(arrayExists (fn (_,x) => not x) safe)
val _ = debugFn (fn _ =>
("Safety information for "^L.printString phi^" and "^(playerString player)^
"\nAlways safe: "^
(Bool.toString alwaysSafe)^" Safety array: "^(arrayString Bool.toString safe)))
in (alwaysSafe, safe)
end
fun init x = (safetyInfo x abelard,safetyInfo x eloise)
val safetyKnowledge = List.foldr (fn (x,l) => setPropEntry l (x, init x))
(noPropEntry()) subforms
fun getSafetyInfo node = getPropEntry safetyKnowledge (getProp node)
fun oValid (i,_) = isValid abelard i
fun pValid (i,_) = isValid eloise i
fun addKnowledge ((position as (node, index)), b, m) =
let val _ = debugFn
(fn _ => ("Adding decision for "^(playerString b)^" at "^
(positionString position)))
val selector = fn arghValueRestriction =>
pairMember b arghValueRestriction
val (safeForB,_) = selector (getSafetyInfo node)
val (abDec, elDec) = getDecisionInfo node
val count = selector counts
val newBDecisionInfo = if safeForB then Safe (!count)
else Unsafe (!count, index)
val newDecisionInfo = if b then (abDec, newBDecisionInfo::elDec)
else ((newBDecisionInfo::abDec), elDec)
val _ = case m of
NONE => ()
| (SOME next) => pushNextMove (node, next)
in setDecisionInfo (node, newDecisionInfo)
end
fun canUse (node, index) i player =
let val (always, safe) = pairMember player (getSafetyInfo node)
in always orelse (compatindex index i player safe)
end
(* Answer two questions: does this decision apply here, and do we need to *)
(* forget it? Return boolean (use it) * new decisions. *)
(* p is the player we want a decision for, w is the chooser at this node. *)
fun lookAt (position as (node, index)) p w [] = (false, [])
| lookAt (position as (node, index)) p w (d as ((Safe j)::t)) =
if isValid p j then (true, d)
else ((if w = Player(p) then popNextMove(node) else ());
lookAt position p w t)
| lookAt (position as (node, index)) p w (d as ((Unsafe (j,i))::t)) =
if isValid p j then
if canUse position i p then (true, d)
else (false, d)
(* if we can't use this, then for sure we can't use anything earlier*)
else ((if w = Player(p) then popNextMove(node) else ());
lookAt position p w t)
fun getKnowledge (position as (node, index)) =
let val decs as (abDec, elDec) = getDecisionInfo node
val chooser = whoseTurnNext node
val (canUseAb, newAbDec) = lookAt position abelard chooser abDec
val (answer, newDecs) =
if canUseAb then (SOME(abelard), (newAbDec, elDec))
else
let val (canUseEl, newElDec) = lookAt position eloise chooser elDec
in (if canUseEl then SOME(eloise) else NONE, (newAbDec, newElDec))
end
in (if decs = newDecs then () else setDecisionInfo (node, newDecs);
answer)
end
in (addKnowledge, getKnowledge)
end
(* Return player option to say whether one or other player wins by repeat. *)
fun getWinsByRepeat (position as (node, index)) =
case getOccurrence node of
NONE => NONE
| SOME (i, c, (aUse, eUse)) =>
let val winner = winsOn i index
val select = pairMember winner
val use = select (aUse, eUse)
val _ = use := true
in SOME(winner)
end
(* we're backtracking for winner: if anything used assumptions *)
(* about the other player, we should mark anything that might have done so *)
(* invalid. *)
(* index only passed for sanity checking *)
fun backtrackingThrough ((node, index), winner) =
let val (i,c,use) = case getOccurrence node of
(* If we're backtracking through it we played through it earlier! *)
NONE => raise PanicNoisily "GameCheck, backtrackingThrough (empty)"
| (SOME h) => h
val _ = if i = index then () else
raise PanicNoisily "GameCheck, backtrackingThrough2"
val _ = setOccurrence (node, NONE) (* this occ no longer above us *)
fun maybeInvalidate p u =
if !u then invalidate (c, p) else ()
val loser = other winner
in maybeInvalidate loser (pairMember loser use)
end
fun addOccurrence (position as (node, index)) =
(* remember oCount = pCount *)
setOccurrence (node, SOME (index, (!oCount), (ref false, ref false)))
fun inform b gameList reason =
debugFn (fn _ =>
"Checking for "^(playerString b)^
" on gamelist of length "^
(Int.toString (length gameList))^
" because "^reason)
(* Could make use of the nextMove slot to store this: good or bad?? *)
fun unwind (node, index) =
let val (agent, prop) = getConfig node
val X = case real prop of
Var X => X
| _ => raise PanicNoisily "GameCheck, unwind"
in (makeNode(agent, (body X)), (update X index))
end
datatype interactive = Yes | No
(************************** Playing *****************************************)
(* Order of checking for decision and occurrence: it's easy but tedious to *)
(* show that if you have a decision for A and elsewhere a repeat of the *)
(* same configuration, then if the decision is applicable at the bottom and *)
(* not at the top of the repeat (i.e. there is both an applicable decision *)
(* and an occurrence at the bottom) then A wins on that repeat. That is, we *)
(* may safely check for the decision first: if it's there it gives the same *)
(* answer as we would get from using the occurrence. Phew! *)
fun win interacting fns (position as (node, index)) glist =
let val (getKnowledge, next, nextRef, print, inform) = fns
val _ = inc counter
val _ = inc oCount (* = pCount *)
val _ = print (node, (!counter))
val (backtrack, keepPlaying) = (check interacting fns, win interacting fns)
in case getKnowledge position of
SOME(winner) => backtrack winner glist node
| NONE =>
(* Is this a repeat? If so, see who wins on it, record that we're making *)
(* this assumption, and backtrack for that winner. Otherwise just record *)
(* that we've seen this config, and keep playing. *)
(case getWinsByRepeat (node, index) of
SOME(winner) =>
(inform (winner, "of a repeat");
backtrack winner glist node)
| NONE =>
(debugFn (fn _ =>
((Int.toString (!counter))^
" Exploring "^
(positionString position)));
(case whoseTurnNext node of
Referee => (addOccurrence position;
nextRef();
keepPlaying
(unwind (node, index))
((position,[])::glist))
| (Player chooser) =>
(case next node of
NONE =>
(* the player whose turn it is has no moves, so the other player wins. *)
let val winner = other chooser
in (inform (winner, "there are no moves for loser");
backtrack winner glist node)
end
(* explore some option *)
| SOME(h,t) =>
(addOccurrence position;
keepPlaying (h, index)
((position, t)::glist))))))
end
(* check Someone gamelist assumes that Someone has just won a game whose *)
(* ghost is recorded in gamelist, and checks whether this win extends to *)
(* a winning strategy: i.e. could Someone have coped with all the choices *)
(* the other player could have made? Someone's win may depend on assumptions*)
(* which will get discharged or invalidated as we go *)
(* The node whereWeCameFrom allows us to update the strategy once we know *)
(* which move was successful, as we do here (provisionally). *)
and check No fns winner gameList whereWeCameFrom =
let
val _ = debugFn (fn _ => "Check with: "^(playerString winner))
val play = win No fns
(* The things we must do whenever we decide it's OK to keep backtracking: *)
fun keepBacktracking (position as (node, index), maybeMove, glist) =
(backtrackingThrough ((node, index), winner);
(* invalidate ass. if nec. etc. *)
addKnowledge (position, winner, maybeMove);
(* record the decision *)
chk glist node) (* keep going *)
and chk [] whence = winner
| chk (((position as (node, index)), unexplored)::glist) whence =
case whoseTurnNext node of
Referee => keepBacktracking (position, NONE, glist)
| (Player chooser) =>
if winner = chooser then
(* the choice was made by the player who eventually won the game, so no need *)
(* to examine alternative choices *)
keepBacktracking (position, (SOME whence), glist)
else
(* could the other have chosen differently? *)
(case unexplored of
[] => keepBacktracking (position, NONE, glist)
| (n::l) =>
(debugFn (fn _ =>
("Branching at "^(positionString position)));
play (n, index) ((position, l)::glist)))
in chk gameList whereWeCameFrom
end
(* Version to use when we're playing interactively: *)
(* backtrack simply to remove occurrences, in case we play again. *)
| check Yes fns winner gameList whereWeCameFrom =
let fun chk [] = true
| chk (((position as (node, index)), unexplored)::glist) =
(backtrackingThrough ((node, index), winner);
chk glist)
in chk gameList
end
fun showSize _ = UI.chat
("Total number of nodes visited (counting repetitions) "^
(Int.toString (!counter)))
val winner = (UI.chat ("There are "^(Int.toString (length subforms))^
" relevant subformulae.\nPlaying...");
(win No (getKnowledge, next,
noOp, noOp, (* no printing *)
(fn (r,reason) => UI.debugFn (fn _ => "Got "^
(playerString r)^
" because "^reason)))
(makeNode(topLevelAgent, topLevelFormula),initindex) []))
handle Interrupt => (showSize();
raise Interrupt)
val _ = showSize()
val (winnerString, loserString) = (playerString winner,
playerString (not winner))
val _ = UI.print (Bool.toString winner)
fun interact winner =
let
fun getKnowledgeI (node, index) =
case real (getProp node) of
True => SOME(eloise)
| False => SOME(abelard)
| _ => NONE
fun nextRef _ =
(UI.message "The referee unwinds the fixpoint.";
UI.hitReturnToContinue())
fun nextI node =
let val mover = whoseTurnNext node
in case mover of
Referee =>
(UI.message "The referee unwinds the fixpoint.";
UI.hitReturnToContinue();
next node)
| Player p =>
if p = winner then
(UI.message ("CWB's turn (playing "^(playerString winner)^")");
UI.hitReturnToContinue();
next node)
else (UI.message ("Your turn (playing "^
(playerString (other winner))^")");
case getSuccessors node of
NONE => raise PanicNoisily "GameCheck, interact"
| SOME [] => NONE
| SOME l => let val (befor, chosen, after) =
UI.pickFromListC (fn _ => false) "Which move? "
(fn x => "\n"^(nodesConfigString x)^"\n")
l
in SOME(chosen,befor@after)
end)
end
fun printI (node,c) =
UI.message ((Int.toString c)^": Current position:\n"^
nodesConfigString node)
fun informI (wonHere, reason) =
if winner = wonHere then
UI.message ("The CWB (playing "^(playerString winner)^
") won, because "^reason)
else raise PanicNoisily ("GameCheck, informI2: CWB lost!")
val willPlay = if definitelyPlay then ref true else
if UI.userHatesGames() then ref false else
ref (UI.yOrN false
"Would you like to play (and lose!) a game against the CWB?")
in while (!willPlay) do
(UI.message ("The CWB will choose "^winnerString^
"'s moves.\nYou can choose "^loserString^"'s.");
counter := 0;
(win Yes (getKnowledgeI, nextI, nextRef, printI, informI)
(makeNode(topLevelAgent, topLevelFormula),initindex) []);
willPlay := UI.yOrN false "Another game?")
end
val _ = if UI.interactive() then interact(winner) else ()
in
winner
end
end