From fce43eeb7b41710b180f5532dfe4b9ab3f953c5e Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Fri, 10 Nov 2017 20:19:00 +0100
Subject: [PATCH] Use non-local solver from pgsolver
Looks like we misinterpreted the meaning of "local" in pgsolver. It
only calculates the correct solution for the root node, but we
need information about other nodes for intermediate
propagation (on-the-fly game solving).
Now we use a non-local solver, which works but is very slow at the
moment because the game has to be constructed anew every time we
propagate. => We should try to keep the game up-to-date as we expand
nodes, if possible.
---
src/lib/CoAlgReasoner.ml | 45 ++++++++++++++++++++++++++--------------
src/lib/CoolGraph.ml | 24 +++++++++++++--------
src/lib/CoolGraph.mli | 3 +++
3 files changed, 48 insertions(+), 24 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index e3a43de..b942a40 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -230,41 +230,56 @@ let solveGame () =
in
let root_idx1 = coreGetIdxOr1 (graphGetRoot ()) in
- let game1 = (root_idx1, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors1, nodeData, fun _ -> None) in
let root_idx2 = coreGetIdxOr (Some PG_Map.sat_node) (graphGetRoot ()) in
- let game2 = (root_idx2, CU.compose Tcsbasedata.Enumerators.of_list nodeSucessors2, nodeData, fun _ -> None) in
- (* Basics.verbosity := 3; *)
+
+ (* Generate data as required by PG.pg_init *)
+ let game1 = PG.pg_create (PG_Map.size ()) in
+ let game2 = PG.pg_create (PG_Map.size ()) in
+
+ let rec populate game succ node =
+ if PG.pg_get_owner game node <> PG.plr_undef then () else begin
+ let (prio, player) = nodeData node in
+ let children = succ node in
+ PG.pg_set_owner game node player;
+ PG.pg_set_priority game node prio;
+ List.iter (fun child -> begin
+ populate game succ child;
+ PG.pg_add_edge game node child
+ end) children
+ end
+ in
+ populate game1 nodeSucessors1 root_idx1;
+ populate game2 nodeSucessors2 root_idx2;
let seenmap = Hashtbl.create 10 in
let rec printGame game node =
if Hashtbl.mem seenmap node then () else
begin
Hashtbl.add seenmap node ();
- let (_, suc, _, _) = game in
- let children = Tcsbasedata.Enumerators.to_list (suc node) in
+ let children = PG.ns_nodes (PG.pg_get_successors game node) in
let formatList l = "[" ^ String.concat "; " (List.map string_of_int l) ^ "]" in
Printf.printf "%d -> %s\n" node (formatList children);
List.iter (printGame game) children
end
in
- (* print_endline "GAME 1 ####################"; *)
- (* printGame game1 root_idx1; *)
- (* print_endline "GAME 2 ####################"; *)
- (* Hashtbl.clear seenmap; *)
- (* printGame game2 root_idx2; *)
-
- let solution1 = Stratimprlocal2.partially_solve game1 in
- let solution2 = Stratimprlocal2.partially_solve game2 in
+ (* print_endline "GAME 1 ####################";
+ * printGame game1 root_idx1;
+ * print_endline "GAME 2 ####################";
+ * Hashtbl.clear seenmap;
+ * printGame game2 root_idx2; *)
+ let (solution1, _) = Recursive.solve game1 in
+ let (solution2, _) = Recursive.solve game2 in
+
let nodeSetStatus node status = match PG_Map.find node with
| PG_Map.State state -> stateSetStatus state status
| PG_Map.Core core -> coreSetStatus core status
| _ -> assert false
in
let applySolution node =
- let (sol1_player,_) = solution1 node in
- let (sol2_player,_) = solution2 node in
+ let sol1_player = solution1.(node) in
+ let sol2_player = solution2.(node) in
if sol1_player = eloise then begin
nodeSetStatus node Sat
end
diff --git a/src/lib/CoolGraph.ml b/src/lib/CoolGraph.ml
index c715f03..0ad18f4 100644
--- a/src/lib/CoolGraph.ml
+++ b/src/lib/CoolGraph.ml
@@ -102,6 +102,8 @@ module type S = sig
val sat_node : Paritygame.node
val unsat_node : Paritygame.node
+ val size : unit -> int
+
val reset : unit -> unit
end
@@ -363,6 +365,15 @@ let doSatPropagation () = match !prop_rate with
(* "Module type" and a specific implementation of the graph *)
(*****************************************************************************)
+(* Counter begins at 2 to have two reserved values 0 and 1
+ This is needed for special nodes in parity games *)
+let nodeCounter = ref 2
+let nextNodeIdx () : int =
+ let oldVal = !nodeCounter in
+ nodeCounter := oldVal + 1;
+ oldVal
+let nodeCounterReset () = nodeCounter := 2
+
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
@@ -373,7 +384,8 @@ let graphInit () =
graphStates := Array.init size (fun _ -> GHt.create 128);
graphCores := Array.init size (fun _ -> GHt.create 128);
graphCnstrs := GHtS.create 128;
- graphRoot := None
+ graphRoot := None;
+ nodeCounterReset ()
let graphIterStates fkt =
Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
@@ -461,6 +473,8 @@ module ParityGameMapping = struct
let sat_node = 0
let unsat_node = 1
+ let size () = Hashtbl.length node_table
+
let reset () =
Hashtbl.reset node_table;
Hashtbl.add node_table sat_node Sat;
@@ -471,14 +485,6 @@ end
(* "Module type" and a specific implementation of state nodes *)
(*****************************************************************************)
-(* Counter begins at 2 to have two reserved values 0 and 1
- This is needed for special nodes in parity games *)
-let nodeCounter = ref 2
-let nextNodeIdx () : int =
- let oldVal = !nodeCounter in
- nodeCounter := oldVal + 1;
- oldVal
-
let stateMake sort bs focus exp =
let res = { sortS = sort; bsS = bs; focusS = focus; statusS = Expandable;
parentsS = []; childrenS = []; constraintsS = cssEmpty;
diff --git a/src/lib/CoolGraph.mli b/src/lib/CoolGraph.mli
index aae81f2..984f578 100644
--- a/src/lib/CoolGraph.mli
+++ b/src/lib/CoolGraph.mli
@@ -97,6 +97,9 @@ module type S = sig
val sat_node : Paritygame.node
val unsat_node : Paritygame.node
+ (** Return the number of nodes in the game *)
+ val size : unit -> int
+
val reset : unit -> unit
end
--
GitLab