[Toss-devel-svn] SF.net SVN: toss:[1641] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1641] trunk/Toss
|
From: <luk...@us...> - 2012-01-17 00:38:24
|
Revision: 1641
http://toss.svn.sourceforge.net/toss/?rev=1641&view=rev
Author: lukaszkaiser
Date: 2012-01-17 00:38:17 +0000 (Tue, 17 Jan 2012)
Log Message:
-----------
Cleanups and improvements in Learn, adding tc-atoms distinguishing.
Modified Paths:
--------------
trunk/Toss/Formula/FormulaSubst.ml
trunk/Toss/Formula/FormulaSubst.mli
trunk/Toss/Learn/Distinguish.ml
trunk/Toss/Learn/Distinguish.mli
trunk/Toss/Learn/DistinguishTest.ml
trunk/Toss/Learn/LearnGame.ml
trunk/Toss/Learn/LearnGameTest.ml
trunk/Toss/Learn/Makefile
Modified: trunk/Toss/Formula/FormulaSubst.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubst.ml 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Formula/FormulaSubst.ml 2012-01-17 00:38:17 UTC (rev 1641)
@@ -370,20 +370,22 @@
let inphi = And [In (xv, frX); All (([nxv; nyv] :> var list), impphi)] in
All ([(frX :> var)], Or [Not inphi; In (yv, frX)])
-(* First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
-let rec make_fo_tc_conj k x y phi =
+(* First-order [k]-step [?refl] transitive closure of [phi] over [x] and [y]. *)
+let rec make_fo_tc_conj ?(reflexive=true) k x y phi =
let (xv, yv) = (fo_var_of_string x, fo_var_of_string y) in
- if k = 0 then Eq (xv, yv) else if k = 1 then Or [Eq (xv, yv); phi] else
+ if k = 0 then Eq (xv, yv) else if k = 1 then
+ if reflexive then Or [Eq (xv, yv); phi] else phi
+ else
let (fv, k1, k2) = (free_vars phi, k / 2, k - (k / 2)) in
let (_, t) = subst_name_avoiding fv (var_of_string "t") in
- let (phi1, phi2) =
- (make_fo_tc_conj k1 x y phi, make_fo_tc_conj k2 x y phi) in
+ let (phi1, phi2) = (make_fo_tc_conj ~reflexive k1 x y phi,
+ make_fo_tc_conj ~reflexive k2 x y phi) in
let (phi1s, phi2s) =
(subst_vars [(y,t)] phi1, subst_vars [(x,t)] phi2) in
Ex ([var_of_string t], And [phi1s; phi2s])
(* First-order [k]-step refl. transitive closure of [phi], disjunctive form. *)
-let make_fo_tc_disj k x y phi =
+let make_fo_tc_disj ?(reflexive=true) k x y phi =
let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
let (_, t) = subst_name_avoiding fv (var_of_string "t") in
let phi_t = subst_vars [(y,t)] phi in
@@ -392,4 +394,4 @@
let lst = k_step (i-1) in
let psi = subst_vars [(x,t)] (List.hd lst) in
Ex ([var_of_string t], And [phi_t; psi]) :: lst in
- Or (List.rev (k_step k))
+ if reflexive then Or (List.rev (k_step k)) else List.hd (k_step k)
Modified: trunk/Toss/Formula/FormulaSubst.mli
===================================================================
--- trunk/Toss/Formula/FormulaSubst.mli 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Formula/FormulaSubst.mli 2012-01-17 00:38:17 UTC (rev 1641)
@@ -65,8 +65,10 @@
val make_mso_tc : string -> string -> formula -> formula
(** First-order [k]-step refl. transitive closure of [phi] over [x] and [y]. *)
-val make_fo_tc_conj : int -> string -> string -> formula -> formula
-val make_fo_tc_disj : int -> string -> string -> formula -> formula
+val make_fo_tc_conj : ?reflexive: bool ->
+ int -> string -> string -> formula -> formula
+val make_fo_tc_disj : ?reflexive: bool ->
+ int -> string -> string -> formula -> formula
(** {2 Debugging} *)
Modified: trunk/Toss/Learn/Distinguish.ml
===================================================================
--- trunk/Toss/Learn/Distinguish.ml 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/Distinguish.ml 2012-01-17 00:38:17 UTC (rev 1641)
@@ -3,7 +3,7 @@
let debug_level = ref 0
let set_debug_level i = (debug_level := i)
-type logic = FO | GuardedFO
+type logic = FO | ExFO | GuardedFO | ExGuardedFO
(* Helper functions to construct variables for indices. *)
@@ -22,6 +22,7 @@
Assignments.assignments_of_list elems vars [tuple] in
eval structure formula assignment <> AssignmentSet.Empty
+
(* - Atoms and FO Types - *)
(* The list of literals which hold for a tuple on a structure. *)
@@ -36,9 +37,9 @@
) (atoms @ (equalities (varnames k)))
-(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc].
- In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
-let rec ntype_memo struc mem qr tuple =
+(* The [?existential] [qr]-type in [length of tuple]-variables of [tuple] in
+ [struc]. We memorize [mem] results for [qr] and [tuple], *not* [struc]. *)
+let rec ntype_memo existential struc mem qr tuple =
try Hashtbl.find mem (qr, tuple) with Not_found ->
if qr = 0 then (
let res = Formula.flatten_sort (And (atoms struc tuple)) in
@@ -46,30 +47,34 @@
res
) else (
let prevtp i e =
- ntype_memo struc mem (qr-1) (Aux.array_replace tuple i e) in
+ ntype_memo existential struc mem (qr-1) (Aux.array_replace tuple i e) in
let elems = Structure.elements struc in
let conj_prev_ex i =
And (List.map (fun e -> Ex ([var i], prevtp i e)) elems) in
let all_prev_disj i =
All ([var i], Or (List.map (prevtp i) elems)) in
- let next_ntype i = And [conj_prev_ex i; all_prev_disj i] in
+ let next_ntype i =
+ if existential then conj_prev_ex i else
+ And [conj_prev_ex i; all_prev_disj i] in
let nexttp = And (List.map next_ntype (Aux.range (Array.length tuple))) in
let res = Formula.flatten_sort (
- And [ntype_memo struc mem (qr-1) tuple; nexttp]) in
+ And [ntype_memo existential struc mem (qr-1) tuple; nexttp]) in
Hashtbl.add mem (qr, tuple) res;
res
)
-(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
-let ntype struc qr tuple = ntype_memo struc (Hashtbl.create 7) qr tuple
+(* The [?existential] [qr]-type in [length of tuple]-variables
+ of [tuple] in [struc]. *)
+let ntype ?(existential=false) struc qr tuple =
+ ntype_memo existential struc (Hashtbl.create 7) qr tuple
-(* All types of rank [qr] of all [k]-tuples in [struc]. *)
-let ntypes struc ~qr ~k =
+(* All [?existential] types of rank [qr] of all [k]-tuples in [struc]. *)
+let ntypes ?(existential=false) struc ~qr ~k =
let elems = Structure.elements struc in
let tups = List.map Array.of_list (Aux.all_ntuples elems k) in
let mem = Hashtbl.create 63 in
- Aux.unique_sorted (List.rev_map (ntype_memo struc mem qr) tups)
+ Aux.unique_sorted (List.rev_map (ntype_memo existential struc mem qr) tups)
(* - Guards and Guarded Types - *)
@@ -120,23 +125,24 @@
(Formula.str atom) ^ " >"
-(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc].
- In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
-let rec guarded_type_memo struc mem qr tuple =
+(* Guarded [?existential] [qr]-type in [length of tuple]-variables of [tuple] in
+ [struc]. We memorize [mem] results for [qr] and [tuple], *not* [struc]. *)
+let rec guarded_type_memo existential struc mem qr tuple =
try Hashtbl.find mem (qr, tuple) with Not_found ->
if qr = 0 then (
let res = Formula.flatten_sort (And (atoms struc tuple)) in
Hashtbl.add mem (qr, tuple) res;
res
) else (
- let prevtp tup = guarded_type_memo struc mem (qr-1) tup in
+ let prevtp tup = guarded_type_memo existential struc mem (qr-1) tup in
let conj_prev_ex vars guard subst_tuples =
let subst_tuples = List.filter (fun tup -> tup <> tuple) subst_tuples in
And (List.map (fun tup -> Ex (vars, prevtp tup)) subst_tuples) in
let all_prev_disj vars guard subst_tuples =
All (vars, Or ((Not guard) :: (List.map prevtp subst_tuples))) in
let next_gtype vs (g, ts) =
- And [conj_prev_ex vs g ts; all_prev_disj vs g ts] in
+ if existential then conj_prev_ex vs g ts else
+ And [conj_prev_ex vs g ts; all_prev_disj vs g ts] in
let subst_tuples =
List.rev_map (fun (_,vs,t,_,_) -> (vs, t)) (guards struc tuple) in
let subst_tuples = Aux.unique_sorted (([], tuple) :: subst_tuples) in
@@ -161,18 +167,20 @@
let next_gtype_vs (vs, gtups) = And (List.map (next_gtype vs) gtups) in
let nextf = And (List.map next_gtype_vs tups_with_guards) in
let res = Formula.flatten_sort (
- And [guarded_type_memo struc mem (qr-1) tuple; nextf]) in
+ And [guarded_type_memo existential struc mem (qr-1) tuple; nextf]) in
Hashtbl.add mem (qr, tuple) res;
res
)
-(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
-let guarded_type struc qr tuple =
- guarded_type_memo struc (Hashtbl.create 7) qr tuple
+(* Guarded [?existential] [qr]-type in [length of tuple]-variables
+ of [tuple] in [struc]. *)
+let guarded_type ?(existential=false) struc qr tuple =
+ guarded_type_memo existential struc (Hashtbl.create 7) qr tuple
-(* All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
-let guarded_types struc ~qr ~k =
+(* All guarded [?existential] types of rank [qr] of
+ guarded [k]-tuples in [struc]. *)
+let guarded_types ?(existential=false) struc ~qr ~k =
let tups = List.map (Structure.incident struc) (Structure.elements struc) in
let tups = List.concat (List.map snd (List.concat tups)) in
let tups = List.filter (fun tup -> Array.length tup >= k) tups in
@@ -181,13 +189,62 @@
let ktups = List.rev_map k_subtuples (Aux.unique_sorted tups) in
let ktups = Aux.unique_sorted (List.concat ktups) in
let mem = Hashtbl.create 63 in
- Aux.unique_sorted (List.rev_map (guarded_type_memo struc mem qr) ktups)
+ Aux.unique_sorted (List.rev_map
+ (guarded_type_memo existential struc mem qr) ktups)
+(* - Transitive Closure Formulas - *)
+(* Maximum n between [from] and [upto] such that n-step TC of phi holds. *)
+let tc_max struc phi ?(from=1) upto =
+ let from, upto = max from 1, max (max upto 1) from in
+ let tc n = FormulaSubst.make_fo_tc_disj ~reflexive:false n "x0" "x1" phi in
+ if not (check struc [||] (tc from)) then None else
+ let rec ok i =
+ if i > upto || not (check struc [||] (tc i)) then i-1 else ok (i+1) in
+ Some (ok (from+1))
+
+(* Pairs (n, phi) such that phi is a two-variable [?positive] atomic formula
+ and the n-step transitive closure of phi holds somewhere on [struc].
+ The n is between [?from] and [upto], at least 1, phi has 2 free variables. *)
+let tc_atomic ?(positive=false) ?(repeat_vars=true) struc ?(from=1) upto =
+ let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in
+ let atoms = Array.of_list (FormulaOps.atoms ~repetitions:repeat_vars
+ (Structure.rel_signature struc) (varnames 2)) in
+ let choices = List.rev_map Array.of_list
+ (if positive then Aux.product (rept (Array.length atoms) [0; 1]) else
+ Aux.product (rept (Array.length atoms) [0; 1; -1])) in
+ let atom_chosen i = function
+ | c when c < 0 -> Not (atoms.(i))
+ | c when c = 0 -> And []
+ | c -> atoms.(i) in
+ let max_n_chosen l =
+ let f = Formula.flatten (And (Array.to_list (Array.mapi atom_chosen l))) in
+ if List.length (FormulaSubst.free_vars f) < 2 then None else
+ match tc_max struc f ~from upto with None -> None
+ | Some n -> Some (n, f) in
+ Aux.map_some max_n_chosen choices
+
+(* Find a upto-[n]-step transitive closures of two-variable [?positive] atomic
+ formulas that hold on all [pos_strucs] and on no [neg_strucs]. *)
+let tc_atomic_distinguish ?(positive=false) ?(repeat_vars=true) pos neg n =
+ if pos = [] then failwith "tc_atomic_distinguish: no pos" else
+ let tc n f= FormulaSubst.make_fo_tc_disj ~reflexive:false n "x0" "x1" f in
+ let is_ok (m, phi) negstruc = not (check negstruc [||] (tc m phi)) in
+ let ok_all (m, phi) = List.for_all (is_ok (m, phi)) neg in
+ let tcs s = List.filter ok_all (tc_atomic ~positive ~repeat_vars s n) in
+ let choose l =
+ if l = [] then raise Not_found else
+ let cmp (n1, f1) (n2, f2) =
+ if n1 <> n2 then n1-n2 else Formula.compare f1 f2 in
+ let (k, phi) = List.hd (List.sort cmp l) in
+ tc k phi in
+ try Some (Or (List.rev_map (fun s -> choose (tcs s)) pos)) with
+ Not_found -> None
+
+
(* - Distinguishing Structure Sets - *)
-
(* Helper function: remove atoms from a formula if [cond] is still satisfied.
Note that this is just a greedy heuristic, only And/Or and into Ex/All. *)
let rec greedy_remove ?(pos=false) cond phi =
@@ -218,20 +275,24 @@
(* Find the minimal [logic]-type of [struc] not included in [neg_types]
and with at most [qr] quantifiers and [k] variables. *)
-let min_type_omitting ?(logic = GuardedFO) ~qr ~k neg_types struc =
+let min_type_omitting ?(logic=ExGuardedFO) ~qr ~k neg_types struc =
let pos_types = match logic with
| GuardedFO -> guarded_types struc ~qr ~k
- | FO -> ntypes struc ~qr ~k in
+ | ExGuardedFO -> guarded_types ~existential:true struc ~qr ~k
+ | FO -> ntypes struc ~qr ~k
+ | ExFO -> ntypes ~existential:true struc ~qr ~k in
let ok_types = List.filter (fun f -> not (List.mem f neg_types)) pos_types in
let ok_types = List.sort !compare_types ok_types in
if ok_types = [] then None else Some (List.hd ok_types)
(* Find a [logic]-formula with at most [qr] quantifiers and [k] variables
which holds on all [pos_strucs] and on no [neg_strucs]. *)
-let distinguish_upto ?(logic = GuardedFO) ~qr ~k pos_strucs neg_strucs =
+let distinguish_upto ?(logic=ExGuardedFO) ~qr ~k pos_strucs neg_strucs =
let types s = match logic with
- | GuardedFO -> guarded_types s ~qr ~k
- | FO -> ntypes s ~qr ~k in
+ | GuardedFO -> guarded_types s ~qr ~k
+ | ExGuardedFO -> guarded_types ~existential:true s ~qr ~k
+ | FO -> ntypes s ~qr ~k
+ | ExFO -> ntypes ~existential:true s ~qr ~k in
let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
let fails_on_negs f = not (List.exists (fun s-> check s [||] f) neg_strucs) in
let extend_by_pos acc struc =
@@ -250,20 +311,29 @@
Some (FormulaOps.rename_quant_avoiding fv minimized)
-(* Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+(* Find a formula holding on all [pos_strucs] and on no [neg_strucs].
Leaves free variables (existential) if [skip_outer_exists] is set. *)
-let distinguish ?(how=GuardedFO) ?(skip_outer_exists=false) strucs1 strucs2 =
+let distinguish ?(skip_outer_exists=false) s1 s2 =
if !debug_level > 0 then
Printf.printf "distinguishing:\n\n%s\n\n and\n\n %s\n%!"
- (String.concat "\n" (List.map Structure.str strucs1))
- (String.concat "\n" (List.map Structure.str strucs2));
+ (String.concat "\n" (List.map Structure.str s1))
+ (String.concat "\n" (List.map Structure.str s2));
let rec diff qr k =
if qr > k then diff 0 (k+1) else (
if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
- match distinguish_upto ~logic:how ~qr ~k strucs1 strucs2 with
- | Some f ->
- if skip_outer_exists then Some f else
- Some (Ex (FormulaSubst.free_vars f, f))
- | None -> diff (qr+1) k
+ if qr = 0 then
+ match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
+ | Some f -> f | None ->
+ match tc_atomic_distinguish ~positive:true
+ ~repeat_vars:false s1 s2 (3*k) with
+ | Some f -> Formula.flatten_sort f | None -> diff (qr+1) k
+ else
+ match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
+ | Some f ->
+ (match distinguish_upto ~logic:ExGuardedFO ~qr ~k s1 s2 with
+ | Some g-> if 2*(Formula.size f) < Formula.size g then f else g
+ | None -> f)
+ | None -> diff (qr+1) k
) in
- diff 0 1
+ let res = diff 0 1 in
+ if skip_outer_exists then res else Ex (FormulaSubst.free_vars res, res)
Modified: trunk/Toss/Learn/Distinguish.mli
===================================================================
--- trunk/Toss/Learn/Distinguish.mli 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/Distinguish.mli 2012-01-17 00:38:17 UTC (rev 1641)
@@ -1,6 +1,6 @@
(** Distinguish sets of structures by formulas. *)
-type logic = FO | GuardedFO
+type logic = FO | ExFO | GuardedFO | ExGuardedFO
(** {2 Atoms and FO Types} *)
@@ -9,11 +9,14 @@
i.e. the atomic type of this tuple. *)
val atoms: Structure.structure -> int array -> Formula.formula list
-(** The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
-val ntype: Structure.structure -> int -> int array -> Formula.formula
+(** The [?existential] [qr]-type in [length of tuple]-variables
+ of [tuple] in [struc]. *)
+val ntype: ?existential: bool ->
+ Structure.structure -> int -> int array -> Formula.formula
-(** All types of rank [qr] of all [k]-tuples in [struc]. *)
-val ntypes: Structure.structure -> qr: int -> k:int -> Formula.formula list
+(** All [?existential] types of rank [qr] of all [k]-tuples in [struc]. *)
+val ntypes: ?existential: bool ->
+ Structure.structure -> qr: int -> k:int -> Formula.formula list
(** {2 Guards and Guarded Types} *)
@@ -36,14 +39,36 @@
(int list * Formula.var list * int array * int array * Formula.formula) ->
string
-(** Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
-val guarded_type: Structure.structure -> int -> int array -> Formula.formula
+(** Guarded [?existential] [qr]-type in [length of tuple]-variables
+ of [tuple] in [struc]. *)
+val guarded_type: ?existential: bool ->
+ Structure.structure -> int -> int array -> Formula.formula
-(** All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
-val guarded_types: Structure.structure -> qr: int -> k:int ->
- Formula.formula list
+(** All guarded [?existential] types of rank [qr] of
+ guarded [k]-tuples in [struc]. *)
+val guarded_types: ?existential: bool ->
+ Structure.structure -> qr: int -> k:int -> Formula.formula list
+(** {2 Transitive Closure Formulas} *)
+
+(** Maximum n between [from] and [upto] such that n-step TC of phi holds. **)
+val tc_max:
+ Structure.structure -> Formula.formula -> ?from: int -> int -> int option
+
+(** Pairs (n, phi) such that phi is a two-variable [?positive] atomic formula
+ and the n-step transitive closure of phi holds somewhere on [struc].
+ The n is between [?from] - [upto], at least 1, phi has 2 free variables. **)
+val tc_atomic: ?positive: bool -> ?repeat_vars: bool ->
+ Structure.structure -> ?from: int -> int -> (int * Formula.formula) list
+
+(** Find a upto-[n]-step transitive closures of two-variable [?positive] atomic
+ formulas that hold on all [pos_strucs] and on no [neg_strucs]. **)
+val tc_atomic_distinguish: ?positive: bool -> ?repeat_vars: bool ->
+ Structure.structure list -> Structure.structure list -> int ->
+ Formula.formula option
+
+
(** {2 Distinguishing Structure Sets} *)
(** Order on types that we use to select the minimal ones. *)
@@ -60,10 +85,10 @@
val distinguish_upto: ?logic: logic -> qr: int -> k: int ->
Structure.structure list -> Structure.structure list -> Formula.formula option
-(** Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+(** Find a formula holding on all [pos_strucs] and on no [neg_strucs].
Leaves free variables (existential) if [skip_outer_exists] is set. *)
-val distinguish: ?how: logic -> ?skip_outer_exists: bool ->
- Structure.structure list -> Structure.structure list -> Formula.formula option
+val distinguish: ?skip_outer_exists: bool ->
+ Structure.structure list -> Structure.structure list -> Formula.formula
(** {2 Debugging} *)
Modified: trunk/Toss/Learn/DistinguishTest.ml
===================================================================
--- trunk/Toss/Learn/DistinguishTest.ml 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/DistinguishTest.ml 2012-01-17 00:38:17 UTC (rev 1641)
@@ -208,6 +208,27 @@
(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
);
+ "tc_atomic" >::
+ (fun () ->
+ let struc = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+ formula_list_eq [ "R(x1, x0)"; "R(x0, x1)" ]
+ (List.rev_map snd (tc_atomic ~positive:true struc 1));
+ formula_list_eq [ "R(x1, x0)"; "R(x0, x1)" ]
+ (List.rev_map snd (tc_atomic ~positive:true struc 2));
+ formula_list_eq [ "R(x1, x0)"; "R(x0, x1)" ]
+ (List.rev_map snd (tc_atomic ~positive:true struc ~from:2 2));
+ formula_list_eq []
+ (List.rev_map snd (tc_atomic ~positive:true struc ~from:3 3));
+ );
+
+ "tc_atomic_distinguish" >::
+ (fun () ->
+ let s1 = (struc_of_string "[ | P { 1; 2; 3 }; R { (1,2); (2,3) } | ]") in
+ let s2 = (struc_of_string "[ | P { 1; 2 }; R { (1,2); (2,3) } | ]") in
+ formula_option_eq "ex t (P(t) and P(x1) and R(t, x1) and R(x0, t))"
+ (tc_atomic_distinguish ~positive:true [s1] [s2] 2);
+ );
+
"distinguish_upto" >::
(fun () ->
let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
@@ -220,7 +241,7 @@
(Distinguish.distinguish_upto ~logic:FO ~qr:0 ~k:2 [struc1] [struc2]);
formula_option_eq "None" (* we use guarded types - so None here *)
(Distinguish.distinguish_upto ~qr:0 ~k:3 [struc1] [struc2]);
- formula_option_eq "R(x0, x1) and ex x2 R(x2, x0)"
+ formula_option_eq "R(x0, x1) and ex x2 R(x1, x2)"
(Distinguish.distinguish_upto ~qr:1 ~k:2 [struc1] [struc2]);
let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
@@ -233,13 +254,12 @@
(fun () ->
let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
- formula_option_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x2, x0))"
+ formula_eq "ex x0, x1, t (R(t, x1) and R(x0, t))"
(Distinguish.distinguish [struc1] [struc2]);
let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
- formula_option_eq "ex x0 P(x0)"
- (Distinguish.distinguish [struc1] [struc2]);
+ formula_eq "ex x0 P(x0)" (Distinguish.distinguish [struc1] [struc2]);
let struc1 = struc_of_string "[ | | ] \"
...
@@ -253,7 +273,7 @@
...
...
\"" in
- formula_option_eq "ex x0, x1 (P(x0) and C(x0, x1))"
+ formula_eq "ex x0, x1 (P(x0) and C(x0, x1))"
(Distinguish.distinguish [struc1] [struc2]);
);
]
@@ -292,8 +312,8 @@
P..
... ...
...P ...
-\"" in formula_option_eq
- "P(x0) and P(x1) and C(x0, x1) and ex x2 (P(x2) and C(x2, x0))"
+\"" in formula_eq
+ "ex t (P(t) and P(x0) and P(x1) and C(t, x1) and C(x0, t))"
(Distinguish.distinguish ~skip_outer_exists:true
[strucP] [strucN1; strucN2; strucN3]);
);
@@ -336,7 +356,7 @@
... ... ... ...
...W ... ... ...
\"" in (* Distinguish.set_debug_level 1; *)
- formula_option_eq "W(x1) and all x0 not C(x1, x0)"
+ formula_eq "W(x1) and all x0 not C(x1, x0)"
(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
);
]
Modified: trunk/Toss/Learn/LearnGame.ml
===================================================================
--- trunk/Toss/Learn/LearnGame.ml 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/LearnGame.ml 2012-01-17 00:38:17 UTC (rev 1641)
@@ -19,8 +19,7 @@
"Searching WIN:\n" ^
(String.concat "\n" (List.map Structure.str winningStates)) ^ "\nNOT\n"^
(String.concat "\n" (List.map Structure.str notWinningStates)));
- FormulaOps.tnf_fv
- (Aux.unsome (Distinguish.distinguish winningStates notWinningStates))
+ FormulaOps.tnf_fv (Distinguish.distinguish winningStates notWinningStates)
let cleanStructure struc =
let funs = ref [] in
@@ -73,11 +72,11 @@
let win0f = winFormula
(List.map (fun x -> List.hd (List.rev x)) win0)
(List.flatten ((List.map (fun x-> List.tl (List.rev x))
- win0) @ win1)) in
+ win0) @ win1 @ tie)) in
let win1f = winFormula
(List.map (fun x -> List.hd (List.rev x)) win1)
(List.flatten ((List.map (fun x-> List.tl (List.rev x))
- win1) @ win0)) in
+ win1) @ win0 @ tie)) in
let moves0 = movesi 0 (win0 @ win1) in
let moves1 = movesi 1 (win0 @ win1) in
Modified: trunk/Toss/Learn/LearnGameTest.ml
===================================================================
--- trunk/Toss/Learn/LearnGameTest.ml 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/LearnGameTest.ml 2012-01-17 00:38:17 UTC (rev 1641)
@@ -3,8 +3,15 @@
let formula_of_string s =
FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-let struc_of_string s =
- StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
+let struc_of_string ?(diag=false) s =
+ if diag then
+ let s = "MODEL " ^ s ^ " with Da (x, y) = ex u (R(x, u) and C(u, y));" ^
+ " Db (x, y) = ex u (R(x, u) and C(y, u))" in
+ match ArenaParser.parse_game_defs Lexer.lex (Lexing.from_string s) with
+ | Arena.StateStruc struc -> struc
+ | _ -> failwith "LearnGameTest:struc_of_string: not a structure"
+ else
+ StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
let tests = "LearnGame" >::: [
"simple test game" >::
@@ -39,7 +46,7 @@
\"" ;]] in
let res_game =
"PLAYERS 1, 2
-REL Win1() = ex x1 (Q(x1) and ex x0 R(x1, x0))
+REL Win1() = ex x0 (Q(x0) and ex x1 R(x0, x1))
REL Win2() = ex x1 (Q(x1) and ex x0 R(x0, x1))
RULE Mv1:
[1 | P:1 {}; Q:1 {}; R:2 {} | ] -> [1 | P (1); Q:1 {}; R:2 {} | ]
@@ -73,7 +80,7 @@
(fun () ->
Distinguish.set_debug_level 0; (* set to 1 to get some info printed out *)
let partylist0 = [
- List.map struc_of_string [
+ List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . .
@@ -122,7 +129,7 @@
. . .
. . .
\"";
- ]; List.map struc_of_string [
+ ]; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . .
@@ -170,17 +177,41 @@
. . .
Q . .
. . .
-\"";]
- ] in
-let partylist1 = [
- List.map struc_of_string [
+\"";]; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . .
. . .
. . .
. . .
+Q Q Q
+\"";]; List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
. . .
+. Q .
+. . .
+. Q .
+. . .
+. Q .
+\"";]; List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
+. . .
+. . Q
+. . .
+. Q .
+. . .
+Q . .
+\"";]
+] in
+ let partylist1 = [
+ List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
+. . .
+. . .
+. . .
+. . .
+. . .
+. . .
\"" ;
"[ | P:1 {}; Q:1 {} | ] \"
Q . .
@@ -246,7 +277,7 @@
. . .
P P P
\"";
- ]; List.map struc_of_string [
+ ]; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . .
@@ -304,7 +335,7 @@
P P P
\"";
]
- ; List.map struc_of_string [
+ ; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . .
@@ -313,7 +344,7 @@
. . .
P P P
\"";]
- ; List.map struc_of_string [
+ ; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. P .
@@ -322,7 +353,7 @@
. . .
. P .
\"";]
- ; List.map struc_of_string [
+ ; List.map (struc_of_string ~diag:true) [
"[ | P:1 {}; Q:1 {} | ] \"
. . .
. . P
@@ -331,10 +362,39 @@
. . .
P . .
\"";]
- ] in
+] in
+let tie = [
+ List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
+. . .
+. P .
+. . .
+. Q .
+. . .
+. P .
+\"";]
+ ; List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
+. . .
+. . Q
+. . .
+. P .
+. . .
+P . .
+\"";]
+ ; List.map (struc_of_string ~diag:true) [
+"[ | P:1 {}; Q:1 {} | ] \"
+. . .
+. . P
+. . .
+. P .
+. . .
+Q . .
+\"";]
+] in
assert_equal ~printer:(fun x -> x) ""
((LearnGame.learnFromParties ~win0:partylist0 ~win1:partylist1
- ~tie:[] ~wrong:[]));
+ ~tie ~wrong:[]));
);
]
Modified: trunk/Toss/Learn/Makefile
===================================================================
--- trunk/Toss/Learn/Makefile 2012-01-16 14:23:37 UTC (rev 1640)
+++ trunk/Toss/Learn/Makefile 2012-01-17 00:38:17 UTC (rev 1641)
@@ -1,4 +1,4 @@
-all: reco
+all: tests reco
shapes.o: shapes.c shapes.h
gcc -c shapes.c
@@ -6,5 +6,18 @@
reco: reco.cpp shapes.o
g++ shapes.o reco.cpp -o reco `pkg-config opencv --cflags --libs`
+%Test:
+ make -C .. Learn/$@Verbose
+
+DistinguishTest:
+LearnGameTest:
+
+
+tests:
+ make -C .. LearnTestsVerbose
+
+
+.PHONY: clean
+
clean:
rm -rf reco log*.ppm *.o *~
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
