[Toss-devel-svn] SF.net SVN: toss:[1424] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1424] trunk/Toss
|
From: <luk...@us...> - 2011-04-28 22:09:13
|
Revision: 1424
http://toss.svn.sourceforge.net/toss/?rev=1424&view=rev
Author: lukaszkaiser
Date: 2011-04-28 22:09:04 +0000 (Thu, 28 Apr 2011)
Log Message:
-----------
Create structures from pictures, add SO variable variant, monadic and full least and greatest fixed-point variants, move (part of) ClassTest to OUnit.
Modified Paths:
--------------
trunk/Toss/Formula/BoolFunctionTest.ml
trunk/Toss/Formula/FFTNF.ml
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/Formula.mli
trunk/Toss/Formula/FormulaTest.ml
trunk/Toss/Server/Makefile
trunk/Toss/Solver/Class.ml
trunk/Toss/Solver/ClassTest.ml
trunk/Toss/Solver/PresbTest.ml
trunk/Toss/TossTest.ml
Added Paths:
-----------
trunk/Toss/Server/Picture.ml
trunk/Toss/Server/Picture.mli
trunk/Toss/Server/PictureTest.ml
trunk/Toss/www/img/Breakthrough.ppm
Modified: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Formula/BoolFunctionTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -14,7 +14,7 @@
let assert_eq_string arg msg x_in y_in =
let full_msg = msg ^ " (argument: " ^ arg ^ ")" in
- let ws = Str.regexp "[ ,\n,\t]+" in
+ let ws = Str.regexp "[ \n\t]+" in
let x = Str.global_replace ws " " (" " ^ x_in ^ " ") in
let y = Str.global_replace ws " " (" " ^ y_in ^ " ") in
assert_equal ~printer:(fun x -> x) ~msg:full_msg
Modified: trunk/Toss/Formula/FFTNF.ml
===================================================================
--- trunk/Toss/Formula/FFTNF.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Formula/FFTNF.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -172,6 +172,7 @@
List.map2 (fun v -> function
| `FO _ -> `FO v
| `MSO _ -> `MSO v
+ | `SO _ -> `SO v
| `Real _ -> `Real v) vs xs in
let update_sb vs vars sb =
Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Formula/Formula.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -1,16 +1,17 @@
(* Represent formulas with first-order, mso, and real variables - basic defs.*)
let debug_level = ref 0
-let set_debug_level i = Sat.set_debug_level (i-1); (debug_level := i)
+let set_debug_level i = ( Sat.set_debug_level (i-1); debug_level := i; )
(* ----------------------- BASIC TYPE DEFINITIONS -------------------------- *)
(* Our variables can be first-order, monadic second-order or reals. *)
-type var = [ `FO of string | `MSO of string | `Real of string ] ;;
-type fo_var = [ `FO of string ];;
-type mso_var = [ `MSO of string ];;
-type real_var = [ `Real of string ];;
+type var = [ `FO of string | `MSO of string | `SO of string | `Real of string ]
+type fo_var = [ `FO of string ]
+type mso_var = [ `MSO of string ]
+type so_var = [ `SO of string ]
+type real_var = [ `Real of string ]
(* We recognize if the variable is FO (x, y) or MSO (X, Y) or Real (r1, r2). *)
let var_of_string s : var =
@@ -18,27 +19,34 @@
failwith "empty strings not allowed as vars"
else if s.[0] = ':' then
`Real s
+ else if s.[0] = '|' then
+ `SO s
else if ((Char.uppercase s.[0]) = s.[0]) && (not (Aux.is_digit s.[0])) then
`MSO s
else `FO s
let fo_var_of_string s : fo_var =
match var_of_string s with
- `FO s -> `FO s
+ | `FO s -> `FO s
| _ -> failwith ("non first-order variable: " ^ s)
let mso_var_of_string s : mso_var =
match var_of_string s with
- `MSO s -> `MSO s
+ | `MSO s -> `MSO s
| _ -> failwith ("non MSO variable: " ^ s)
+let so_var_of_string s : so_var =
+ match var_of_string s with
+ | `SO s -> `SO s
+ | _ -> failwith ("non SO variable: " ^ s)
+
let real_var_of_string s : real_var =
match var_of_string s with
- `Real s -> `Real s
+ | `Real s -> `Real s
| _ -> failwith ("non real variable: " ^ s)
(* Print a variable as a string. *)
-let var_str = function `FO s -> s | `MSO s -> s | `Real s -> s
+let var_str = function `FO s -> s | `MSO s -> s | `SO s -> s | `Real s -> s
let print_var v = Format.print_string (var_str v)
(* Print a variable list/array as a string. *)
@@ -58,23 +66,24 @@
(* Check variable type. *)
let is_fo (v : var) = match v with `FO _ -> true | _ -> false
let is_mso (v : var) = match v with `MSO _ -> true | _ -> false
+let is_so (v : var) = match v with `SO _ -> true | _ -> false
let is_real (v : var) = match v with `Real _ -> true | _ -> false
(* Casts to particular variable types. *)
let to_fo (v : var) : fo_var = fo_var_of_string (var_str v)
let to_mso (v : var) : mso_var = mso_var_of_string (var_str v)
+let to_so (v : var) : so_var = so_var_of_string (var_str v)
let to_real (v : var) : real_var = real_var_of_string (var_str v)
(* Cast that is safe provided that tuples are not modified in-place. *)
-let var_tup (vs : [< var ] array) =
- (Obj.magic vs : var array)
+let var_tup (vs : [< var ] array) = (Obj.magic vs : var array)
(* Sign operands. *)
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
(* Print a sign_op as string. *)
let sign_op_str = function
- EQZero -> " = 0"
+ | EQZero -> " = 0"
| GZero -> " > 0"
| LZero -> " < 0"
| GEQZero -> " >= 0"
@@ -85,7 +94,7 @@
(* This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type formula =
- Rel of string * fo_var array
+ | Rel of string * fo_var array
| Eq of fo_var * fo_var
| In of fo_var * mso_var
| RealExpr of real_expr * sign_op
@@ -94,22 +103,26 @@
| Or of formula list
| Ex of var list * formula
| All of var list * formula
+ | MLfp of mso_var * fo_var * formula
+ | MGfp of mso_var * fo_var * formula
+ | Lfp of so_var * fo_var list * formula
+ | Gfp of so_var * fo_var list * formula
and real_expr =
- RVar of string
+ | RVar of string
| Const of float
| Times of real_expr * real_expr
| Plus of real_expr * real_expr
| Fun of string * fo_var
| Char of formula
| Sum of fo_var list * formula * real_expr
-;;
let is_atom = function
- Rel _ | Eq _ | In _ | RealExpr _ -> true
+ | Rel _ | Eq _ | In _ | RealExpr _ -> true
| _ -> false
+
(* Helper power function, used in parser. *)
let rec pow p n =
if n = 0 then Const 1. else if n = 1 then p else Times (p, pow p (n-1))
@@ -242,26 +255,28 @@
(* ------------------------ ORDER ON FORMULAS ------------------------------- *)
-(* Compare two variables. We assume that FO < MSO < Real. *)
+(* Compare two variables. We assume that FO < MSO < SO < Real. *)
let compare_vars x y =
- if x == y then 0 else
- match (x, y) with
- (`FO x, `FO y) -> String.compare x y
- | (`FO _, _) -> 1
- | (_, `FO _) -> -1
- | (`MSO x, `MSO y) -> String.compare x y
- | (`MSO _, _) -> 1
- | (_, `MSO _) -> -1
- | (`Real x, `Real y) -> String.compare x y
+ if x == y then 0 else match (x, y) with
+ | (`FO x, `FO y) -> String.compare x y
+ | (`FO _, _) -> 1
+ | (_, `FO _) -> -1
+ | (`MSO x, `MSO y) -> String.compare x y
+ | (`MSO _, _) -> 1
+ | (_, `MSO _) -> -1
+ | (`SO x, `SO y) -> String.compare x y
+ | (`SO _, _) -> 1
+ | (_, `SO _) -> -1
+ | (`Real x, `Real y) -> String.compare x y
(* Helper function: compare lists/arrays lexicographically by [cmp]. *)
let rec compare_lists_lex cmp = function
- ([], []) -> 0
+ | ([], []) -> 0
| ([], _) -> -1
| (_, []) -> 1
| (x :: xs, y :: ys) ->
- let c = cmp x y in
- if c <> 0 then c else compare_lists_lex cmp (xs, ys)
+ let c = cmp x y in
+ if c <> 0 then c else compare_lists_lex cmp (xs, ys)
let compare_arrays_lex cmp a b =
let res = ref (Array.length a - Array.length b) in
@@ -285,19 +300,18 @@
| Rel _ | Eq _ | In _ | RealExpr _ -> acc + 1
| Not phi | Ex (_, phi) | All (_, phi) -> size ~acc:(acc + 1) phi
| And flist | Or flist ->
- List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
+ List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
let rec rec_compare phi1 phi2 =
let cmp_lists = compare_lists_lex rec_compare in
match (phi1, phi2) with
- (Rel (r1, vs1), Rel (r2, vs2)) ->
- let c = compare_var_tups vs1
- vs2 in
- if c <> 0 then c else String.compare r1 r2
+ | (Rel (r1, vs1), Rel (r2, vs2)) ->
+ let c = compare_var_tups vs1 vs2 in
+ if c <> 0 then c else String.compare r1 r2
| (Rel (r, vs), Eq (x, y)) ->
- let c = compare_var_tups vs [|x; y|] in if c = 0 then -1 else c
+ let c = compare_var_tups vs [|x; y|] in if c = 0 then -1 else c
| (Eq (x, y), Rel (r, vs)) ->
- let c = compare_var_tups [|x; y|] vs in if c = 0 then 1 else c
+ let c = compare_var_tups [|x; y|] vs in if c = 0 then 1 else c
| (Eq (x1, y1), Eq (x2, y2)) -> compare_var_tups [|x1; y1|] [|x2; y2|]
| (Rel _, _) | (Eq _, _) -> -1
| (_, Rel _) | (_, Eq _) -> 1
@@ -307,8 +321,8 @@
| (In _, _) -> -1
| (_, In _) -> 1
| (RealExpr (re1, s1), RealExpr (re2, s2)) ->
- let c = rec_compare_re re1 re2 in
- if c <> 0 then c else Pervasives.compare s1 s2
+ let c = rec_compare_re re1 re2 in
+ if c <> 0 then c else Pervasives.compare s1 s2
| (RealExpr _, _) -> -1
| (_, RealExpr _) -> 1
| (Not psi1, Not psi2) -> rec_compare psi1 psi2
@@ -320,21 +334,21 @@
| (Or _, _) -> -1
| (_, Or _) -> 1
| (All (vs1, psi1), All (vs2, psi2)) | (Ex (vs1, psi1), Ex (vs2, psi2)) ->
- let c = compare_var_lists vs1 vs2 in
- if c <> 0 then c else rec_compare psi1 psi2
+ let c = compare_var_lists vs1 vs2 in
+ if c <> 0 then c else rec_compare psi1 psi2
| (All _, _) -> -1
| (_, All _) -> 1
and rec_compare_re re1 re2 =
match (re1, re2) with
- (Char phi1, Char phi2) -> rec_compare phi1 phi2
+ | (Char phi1, Char phi2) -> rec_compare phi1 phi2
| (Const x, Const y) -> Pervasives.compare x y
| _ -> Pervasives.compare re1 re2 (* TODO: improve this *)
let compare phi1 phi2 =
if phi1 == phi2 then 0 else
let (s1, s2) = (size phi1, size phi2) in
- if s1 <> s2 then s1 - s2 else rec_compare phi1 phi2
+ if s1 <> s2 then s1 - s2 else rec_compare phi1 phi2
(* --------------- BASIC HELPER FUNCTIONS USED IN PARSER ------------------- *)
Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Formula/Formula.mli 2011-04-28 22:09:04 UTC (rev 1424)
@@ -3,35 +3,38 @@
(** {2 Basic Type Definitions.} *)
(** Our variables can be first-order, monadic second-order or reals. *)
-type var = [ `FO of string | `MSO of string | `Real of string ] ;;
-type fo_var = [ `FO of string ];;
-type mso_var = [ `MSO of string ];;
-type real_var = [ `Real of string ];;
+type var = [ `FO of string | `MSO of string | `SO of string | `Real of string ]
+type fo_var = [ `FO of string ]
+type mso_var = [ `MSO of string ]
+type so_var = [ `SO of string ]
+type real_var = [ `Real of string ]
-(** We recognize if the variable is FO (x, y) or MSO (X, Y) or Real (r1, r2). *)
+(** We recognize if the variable is FO (x), MSO (X), SO (|x) or Real (:x). *)
val var_of_string : string -> var
val fo_var_of_string : string -> fo_var
val mso_var_of_string : string -> mso_var
+val so_var_of_string : string -> so_var
val real_var_of_string : string -> real_var
(** Check variable type. *)
val is_fo : var -> bool
val is_mso : var -> bool
+val is_so : var -> bool
val is_real : var -> bool
(** Casts to particular variable types. *)
val to_fo : var -> fo_var
val to_mso : var -> mso_var
+val to_so : var -> so_var
val to_real : var -> real_var
val var_tup : [< var] array -> var array
-(** Compare two variables. We assume FO < MSO < Real. *)
+(** Compare two variables. We assume FO < MSO < SO < Real. *)
val compare_vars : ([< var ] as 'a) -> 'a -> int
val compare_var_lists : ([< var ] as 'a) list -> 'a list -> int
-val compare_var_tups :
- ([< var ] as 'a) array -> 'a array -> int
+val compare_var_tups : ([< var ] as 'a) array -> 'a array -> int
(** Sign operands. *)
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
@@ -43,7 +46,7 @@
(** This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type formula =
- Rel of string * fo_var array
+ | Rel of string * fo_var array
| Eq of fo_var * fo_var
| In of fo_var * mso_var
| RealExpr of real_expr * sign_op
@@ -52,10 +55,14 @@
| Or of formula list
| Ex of var list * formula
| All of var list * formula
+ | MLfp of mso_var * fo_var * formula
+ | MGfp of mso_var * fo_var * formula
+ | Lfp of so_var * fo_var list * formula
+ | Gfp of so_var * fo_var list * formula
-(** Real-valued terms allow counting, characteristic functions and arithmetic. *)
+(** Real-valued terms allow counting, characteristic functions, arithmetic. *)
and real_expr =
- RVar of string
+ | RVar of string
| Const of float
| Times of real_expr * real_expr
| Plus of real_expr * real_expr
@@ -75,11 +82,10 @@
(** {2 Printing Functions} *)
(** Print a variable as a string. *)
-val var_str : [< `FO of string | `MSO of string | `Real of string ] -> string
+val var_str : [< var] -> string
(** Print a variable list as a string. *)
-val var_list_str: [< `FO of string | `MSO of string | `Real of string ] list ->
- string
+val var_list_str: [< var] list -> string
(** Print a formula as a string. *)
val str : formula -> string
Modified: trunk/Toss/Formula/FormulaTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaTest.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Formula/FormulaTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -1,7 +1,7 @@
open OUnit
-FormulaOps.set_debug_level 0 ;;
-BoolFormula.set_debug_level 0 ;;
+FormulaOps.set_debug_level 0;
+BoolFormula.set_debug_level 0
let tests = "Formula" >::: [
"basic flatten" >::
@@ -16,8 +16,7 @@
Formula.And [Formula.And [r "P"; r "Q"]; Formula.And [r "S"]]))
(Formula.And [r "P"; r "Q"; r "S"]);
);
-] ;;
+]
-let a =
- Aux.run_test_if_target "FormulaTest" tests
-;;
+
+let exec = Aux.run_test_if_target "FormulaTest" tests
Modified: trunk/Toss/Server/Makefile
===================================================================
--- trunk/Toss/Server/Makefile 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Server/Makefile 2011-04-28 22:09:04 UTC (rev 1424)
@@ -9,10 +9,12 @@
%TestDebug:
make -C .. Server/$@
+PictureTest:
+PictureTestProfile:
+PictureTestDebug:
+
ServerTest:
-
ServerTestProfile:
-
ServerTestDebug:
tests:
Added: trunk/Toss/Server/Picture.ml
===================================================================
--- trunk/Toss/Server/Picture.ml (rev 0)
+++ trunk/Toss/Server/Picture.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -0,0 +1,235 @@
+(* Processing Pictures to create Structures *)
+
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i;)
+
+
+(* --------- Basic Picture Functions --------- *)
+
+type picture = (int * int * int) array array
+
+(* Read a picture from a scanning buffer. *)
+let read_pic buf =
+ let (width, height) = Scanf.bscanf buf "P3 %d %d 255" (fun x y -> (x, y)) in
+ let pic = Array.make_matrix width height (0, 0, 0) in
+ for j = 0 to height-1 do
+ for i = 0 to width-1 do
+ pic.(i).(j) <- Scanf.bscanf buf " %d %d %d" (fun x y z -> (x, y, z))
+ done
+ done;
+ pic
+
+(* Print a matrix to the formatter [f], use [elem_f] for elements. *)
+let fprint_matrix f elem_f start mid m =
+ let (width, height) = (Array.length m, Array.length (m.(0))) in
+ Format.fprintf f "%s %d %d %s\n%!" start width height mid;
+ for j = 0 to height-1 do
+ for i = 0 to width-1 do
+ Format.fprintf f "%a" elem_f m.(i).(j);
+ done;
+ Format.fprintf f "\n%!";
+ done
+
+(* Print a picture in the simple PPM format to a formatter. *)
+let fprint_pic f pic =
+ let pr fmt (a, b, c) = Format.fprintf fmt " %d %d %d\n" a b c in
+ fprint_matrix f pr "P3" "255" pic
+
+(* Print a picture in the simple PPM format to standard output. *)
+let print_pic pic = fprint_pic Format.std_formatter pic
+
+
+(* Flip a picture. *)
+let flip pic =
+ let (width, height) = (Array.length pic, Array.length (pic.(0))) in
+ let flpic = Array.make_matrix height width (0, 0, 0) in
+ for i = 0 to width-1 do
+ for j = 0 to height-1 do
+ flpic.(j).(i) <- pic.(i).(j)
+ done
+ done;
+ flpic
+
+
+(* Cut a picture to the given rectangle. *)
+let cut (x1, y1) (x2, y2) pic =
+ let (orig_w, orig_h) = (Array.length pic, Array.length (pic.(0))) in
+ let x2 = if x2 <= 0 then orig_w + x2 - 1 else x2 in
+ let y2 = if y2 <= 0 then orig_h + y2 - 1 else y2 in
+ if x2 < x1+1 || y2 < y1+1 || orig_w<x2+1 || orig_h<y2+1 || x1<0 || y1<0 then
+ failwith (Printf.sprintf "cut: wrong dimensions %i %i %i %i" x1 x2 y1 y2);
+ let cutpic = Array.make_matrix (x2-x1+1) (y2-y1+1) (0, 0, 0) in
+ for i = 0 to x2-x1 do
+ for j = 0 to y2-y1 do
+ cutpic.(i).(j) <- pic.(i+x1).(j+y1)
+ done
+ done;
+ cutpic
+
+
+(* Apply the filter function [f] to each pixel in a picture. *)
+let apply_filter f pic =
+ let (width, height) = (Array.length pic, Array.length (pic.(0))) in
+ let fpic = Array.make_matrix width height (0, 0, 0) in
+ for i = 0 to width-1 do
+ for j = 0 to height-1 do
+ fpic.(i).(j) <- f i j width height pic
+ done
+ done;
+ fpic
+
+
+(* ------------ Change Detection ------------ *)
+
+let diff_filter maxdiff (distx, disty) x y w h pic =
+ let res = ref false in
+ for i = -distx to distx do
+ for j = -disty to disty do
+ if x+i >= 0 && x+i < w && y+j >= 0 && y+j < h then
+ let (r1, g1, b1) = pic.(x).(y) in
+ let (r2, g2, b2) = pic.(x+i).(y+j) in
+ let (rd, gd, bd) = maxdiff in
+ if rd >= abs (r1-r2) && gd >= abs (g1-g2) && bd >= abs (b1-b2) then
+ res := false
+ else res := true
+ done
+ done;
+ if !res then (255, 255, 255) else (0, 0, 0)
+
+(* Calculate color difference, accept maxdiff differences up to dist. *)
+let diff ?(maxdiff=(1,1,1)) ?(dist=(1,1)) =
+ apply_filter (diff_filter maxdiff dist)
+
+
+(* ------------ Simple Segmentation ------------ *)
+
+let all_in_color cl ((x1, y1), (x2, y2)) pic =
+ let (w, h) = (Array.length pic, Array.length (pic.(0))) in
+ if x2 < x1 || y2 < y1 || w < x2+1 || h < y2+1 || x1 < 0 || y1 < 0 then
+ failwith (Printf.sprintf "all_in_color: wrong dim %i %i %i %i" x1 y1 x2 y2);
+ let res = ref true in
+ for i = x1 to x2 do
+ for j = y1 to y2 do
+ if pic.(i).(j) <> cl then res := false
+ done
+ done;
+ !res
+
+let rec next_x cl i j w h pic =
+ if pic.(i).(j) = cl then (i, j) else
+ if i+1 < w then next_x cl (i+1) j w h pic else raise Not_found
+
+let rec next_y cl i j w h pic =
+ if pic.(i).(j) = cl then (i, j) else
+ if j+1 < h then next_y cl i (j+1) w h pic else raise Not_found
+
+let next_color cl i j w h pic =
+ try
+ let (i1, _) = next_x cl i j w h pic in
+ if i1+1 < w && pic.(i1+1).(j) = cl then (i1, j) else raise Not_found
+ with Not_found ->
+ let (_, j1) = next_y cl 0 (j+1) w h pic in
+ if j1+1 < h && pic.(i).(j1+1) = cl then (0, j1) else raise Not_found
+
+(* Make a row-first column-next black-white tour of a picture. *)
+let bw_tour pic =
+ let (width, height) = (Array.length pic, Array.length (pic.(0))) in
+ let (i, j, newi, newj) = (ref 0, ref 0, ref 0, ref 0) in
+ let (rects, intv) = (ref [], ref []) in
+ try
+ while true do
+ intv := [];
+ while !j = !newj do
+ let (ni, nj) = next_color (0, 0, 0) !i !j width height pic in
+ newi := ni;
+ let (nni, nnj) = next_color (255, 255, 255) ni nj width height pic in
+ if nnj = !j then intv := (ni, nni-1) :: !intv;
+ i := nni; j := !newj; newj := nnj;
+ done;
+ if !intv != [] then intv := (!newi, width-1) :: !intv;
+ rects := (List.map (fun v-> v, (!j,!newj-1)) !intv) @ !rects;
+ j := !newj; i := 0
+ done;
+ failwith "bw_tour: unreachable"
+ with Not_found ->
+ if !intv != [] then intv := (!newi, width-1) :: !intv;
+ rects := (List.map (fun v-> v, (!j,height-1)) !intv) @ !rects;
+ List.rev_map (fun ((a, b), (c, d)) -> (a, c), (b, d)) !rects
+
+let rect_dist ((x1, y1), (x2, y2)) ((a1, b1), (a2, b2)) pic =
+ let (w, h, d) = (min (x2-x1) (a2-a1), min (y2-y1) (b2-b1), ref 0) in
+ for i = 0 to w-1 do
+ for j = 0 to h-1 do
+ let (x, y, z), (a, b, c) = pic.(x1+i).(y1+j), pic.(a1+i).(b1+j) in
+ d := !d + (abs (x-a)) + (abs (y-b)) + (abs (z-c))
+ done
+ done;
+ (float !d) /. (float (w*h))
+
+let rect_dist_offset (x, y) ((x1, y1), (x2, y2)) ((a1, b1), (a2, b2)) pic =
+ rect_dist ((x1+x, y1+y), (x2+x, y2+y)) ((a1+x, b1+y), (a2+x, b2+y)) pic
+
+(* Very basic picture segmentation, should work for grids. *)
+let segment offset threshold pic =
+ let df = diff (cut (offset, offset) (-offset, -offset) pic) in
+ let rects = bw_tour df in
+ let assign_name (dict, i, bi) rect =
+ let (a, b), (c, d) = rect in
+ try
+ let (r, n) =
+ List.find (fun (r,_) ->
+ rect_dist_offset (offset, offset) r rect pic < threshold) dict in
+ if !debug_level > 0 then
+ Printf.printf " (%i, %i) - (%i, %i) %s found \n%!" a b c d n;
+ ((rect, n) :: dict, i, bi)
+ with Not_found ->
+ if all_in_color (0, 0, 0) rect df then (
+ let n = Printf.sprintf "B%i" bi in
+ if !debug_level > 0 then
+ Printf.printf " (%i, %i) - (%i, %i) %s assigned \n%!" a b c d n;
+ ((rect, n) :: dict, i, bi+1)
+ ) else (
+ let n = Printf.sprintf "P%i" i in
+ if !debug_level > 0 then
+ Printf.printf " (%i, %i) - (%i, %i) %s assigned \n%!" a b c d n;
+ ((rect, n) :: dict, i+1, bi)
+ ) in
+ let (res, _, _) = List.fold_left assign_name ([], 1, 0) rects in
+ List.rev res
+
+
+(* ------------- Structure from Segmented Data ------------ *)
+
+(* Create a structure from segmented data. *)
+let make_struc dict =
+ let (prev_ys, prev_xs, maxdx, maxdy) =
+ (ref (0, 0), ref (0, 0), ref 0, ref 0) in
+ let add_el (struc, i, j) (((x1, y1), (x2, y2)), pred) =
+ let (ni, nj) =
+ if (y1, y2) = !prev_ys then (
+ maxdx := max !maxdx (abs ((fst !prev_xs) - x1));
+ prev_xs := (x1, x2);
+ (i+1, j)
+ ) else (
+ maxdy := max !maxdy (abs ((fst !prev_ys) - y1));
+ prev_xs := (x1, x2);
+ prev_ys := (y1, y2);
+ (1, j+1)
+ ) in
+ let name = try Structure.board_coords_name (ni, nj) with Not_found ->
+ Printf.sprintf "e%i,%i" ni nj in
+ let (s1, elem) = Structure.add_new_elem struc ~name () in
+ let s2 = Structure.add_fun s1 "x" (elem, float (x1+x2) /. 2.) in
+ let s3 = Structure.add_fun s2 "y" (elem, float (y1+y2) /. (-2.)) in
+ let s4 = Structure.add_fun s3 "x1" (elem, float x1) in
+ let s5 = Structure.add_fun s4 "y1" (elem, float y1) in
+ let s6 = Structure.add_fun s5 "x2" (elem, float x2) in
+ let s7 = Structure.add_fun s6 "y2" (elem, float y2) in
+ let s8 = Structure.add_fun s7 "vx" (elem, 0.) in
+ let new_s = Structure.add_fun s8 "vy" (elem, 0.) in
+ if pred = "B0" then (new_s, ni, nj) else
+ (Structure.add_rel new_s pred [|elem|], ni, nj) in
+ let (s, _, _) =
+ List.fold_left add_el (Structure.empty_structure (), 1, 0) dict in
+ (s, !maxdx, !maxdy)
+
Added: trunk/Toss/Server/Picture.mli
===================================================================
--- trunk/Toss/Server/Picture.mli (rev 0)
+++ trunk/Toss/Server/Picture.mli 2011-04-28 22:09:04 UTC (rev 1424)
@@ -0,0 +1,50 @@
+(** Processing Pictures to create Structures *)
+
+(** {2 Debugging} *)
+
+val set_debug_level : int -> unit
+
+
+(** {2 Basic Picture Functions} *)
+
+type picture = (int * int * int) array array
+
+
+(** Read a picture from a scanning buffer. *)
+val read_pic : Scanf.Scanning.scanbuf -> picture
+
+(** Print a picture in the simple PPM format to a formatter. *)
+val fprint_pic : Format.formatter -> picture -> unit
+
+(** Print a picture in the simple PPM format to standard output. *)
+val print_pic : picture -> unit
+
+(** Flip a picture. *)
+val flip : picture -> picture
+
+(** Cut a picture to the given rectangle. *)
+val cut : int * int -> int * int -> picture -> picture
+
+(** Apply the filter function [f] to each pixel in a picture. *)
+val apply_filter : (int -> int -> int -> int -> picture -> int * int * int) ->
+ picture -> picture
+
+
+(** {2 Change Detection} *)
+
+(** Calculate color difference, accept maxdiff differences up to dist. *)
+val diff : ?maxdiff: int * int * int -> ?dist: int * int -> picture -> picture
+
+
+(** {2 Simple Segmentation} *)
+
+(** Very basic picture segmentation, should work for grids. *)
+val segment : int -> float -> picture ->
+ (((int * int) * (int * int)) * string) list
+
+
+(** {2 Structure from Segmented Data} *)
+
+(** Create a structure from segmented data. *)
+val make_struc : (((int * int) * (int * int)) * string) list ->
+ Structure.structure * int * int
Added: trunk/Toss/Server/PictureTest.ml
===================================================================
--- trunk/Toss/Server/PictureTest.ml (rev 0)
+++ trunk/Toss/Server/PictureTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -0,0 +1,50 @@
+open OUnit
+
+Picture.set_debug_level 0
+
+let tests = "Picture" >::: [
+ "segmentation size for breakthrough" >::
+ (fun () ->
+ let fname = "./www/img/Breakthrough.ppm" in
+ let pic = Picture.read_pic (Scanf.Scanning.from_file fname) in
+ let seg = Picture.segment 2 40. pic in
+ assert_equal ~printer:string_of_int 64 (List.length seg)
+ );
+
+ "breakthrough structure P1 size" >::
+ (fun () ->
+ let fname = "./www/img/Breakthrough.ppm" in
+ let pic = Picture.read_pic (Scanf.Scanning.from_file fname) in
+ let seg = Picture.segment 2 40. pic in
+ let (struc, _, _) = Picture.make_struc seg in
+ assert_equal ~printer:string_of_int 16 (Structure.rel_size struc "P1")
+ );
+]
+
+
+let main () =
+ Gc.set { (Gc.get()) with
+ Gc.space_overhead = 300; (* 300% instead of 80% std *)
+ Gc.minor_heap_size = 160*1024; (* 4*std, opt ~= L2 cache/proc *)
+ Gc.major_heap_increment = 8*124*1024 (* 8*std ok *) };
+ let (file) = (ref "") in
+ let dbg_level i = (Picture.set_debug_level i) in
+ let opts = [
+ ("-v", Arg.Unit (fun () -> dbg_level 1), "be verbose");
+ ("-d", Arg.Int (fun i -> dbg_level i), "set debug level");
+ ("-f", Arg.String (fun s -> file := s), "process file");
+ ] in
+ Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
+ if !file = "" then ignore (OUnit.run_test_tt tests) else (
+ let pic = Picture.read_pic (Scanf.Scanning.from_file !file) in
+ let (struc, dx, dy) = Picture.make_struc (Picture.segment 2 40. pic) in
+ let formula_r = Printf.sprintf
+ ":y(a) = :y(b) and :x(a) < :x(b) and :x(b) < :x(a) + %i.8" dx in
+ let formula_c = Printf.sprintf
+ ":x(a) = :x(b) and :y(b) < :y(a) and :y(a) < :y(b) + %i.8" dy in
+ Printf.printf "MODEL \n %s \n with \n R(a, b) = %s;\n C(a, b) = %s\n\n%!"
+ (Structure.sprint struc) formula_r formula_c;
+ )
+
+
+let _ = Aux.run_if_target "PictureTest" main
Modified: trunk/Toss/Solver/Class.ml
===================================================================
--- trunk/Toss/Solver/Class.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Solver/Class.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -37,19 +37,19 @@
let struct_sum_str = function
Struct s -> Structure.str s
| Sum (comps, rdefs) ->
- let comps_s =
- String.concat " + " (List.map (fun (s, t) -> s ^ ": " ^ t) comps) in
- let defstr (rel, (vars, def)) =
- Formula.str (Rel (rel, Array.of_list vars)) ^
- " <- " ^ (Formula.str def)
- in
- if rdefs = [] then comps_s else
- comps_s ^ " with\n " ^
- (String.concat ";\n " (List.map defstr rdefs))
+ let pstr (s, t) = if s = "_" then t else s ^ ": " ^ t in
+ let comps_s = String.concat " + " (List.map pstr comps) in
+ let defstr (rel, (vars, def)) =
+ Formula.str (Rel (rel, Array.of_list vars)) ^
+ " <- " ^ (Formula.sprint def)
+ in
+ if rdefs = [] then comps_s else
+ comps_s ^ " with\n " ^
+ (String.concat ";\n " (List.map defstr rdefs)) ^ ";"
(* Print an inductive structure class as a string, using its definition. *)
let str cdefs =
- let cdef_s (id, alternatives) = "class " ^ id ^ " =\n " ^
+ let cdef_s (id, alternatives) = (* "class " ^ *) id ^ " =\n " ^
(String.concat "\n | " (List.map struct_sum_str alternatives))
in
String.concat "\nand " (List.map cdef_s cdefs)
@@ -69,36 +69,36 @@
| Sum (ids_l, rels_l) ->
let prefixes s = List.map (fun (i, _) -> s ^ ":" ^ i) ids_l in
let replace_in s = function
- In (fo_v, `MSO w) when w = s ->
- Or (List.map (fun ps -> In (fo_v, `MSO ps)) (prefixes s))
+ | In (fo_v, `MSO w) when w = s ->
+ Or (List.map (fun ps -> In (fo_v, `MSO ps)) (prefixes s))
| x -> x in
let rec split_formula = function
- Ex ([], phi) | All ([], phi) -> split_formula phi
+ | Ex ([], phi) | All ([], phi) -> split_formula phi
| Ex ([v], phi) -> (
- match v with
- `Real _ -> failwith "splitting reals not supported in ex"
- | `MSO s ->
- Ex (List.map (fun x -> `MSO x) (prefixes s),
- split_formula (map_to_atoms (replace_in s) phi))
- | `FO s ->
- let new_phi ps =
- Ex ([`FO ps], split_formula (subst_vars [(s, ps)] phi))
- in
- Or (List.map new_phi (prefixes s))
- )
+ match v with
+ | `Real _ -> failwith "splitting reals not supported (ex)"
+ | `SO _ -> failwith "splitting non-monadic SO not supported (ex)"
+ | `MSO s ->
+ Ex (List.map (fun x -> `MSO x) (prefixes s),
+ split_formula (map_to_atoms (replace_in s) phi))
+ | `FO s ->
+ let new_phi ps =
+ Ex ([`FO ps], split_formula (subst_vars [(s, ps)] phi)) in
+ Or (List.map new_phi (prefixes s))
+ )
| Ex (v::vs, phi) -> split_formula (Ex ([v], Ex (vs, phi)))
| All ([v], phi) -> (
- match v with
- `Real _ -> failwith "splitting reals not supported in forall"
- | `MSO s ->
- All (List.map (fun x -> `MSO x) (prefixes s),
- split_formula (map_to_atoms (replace_in s) phi))
- | `FO s ->
- let new_phi ps =
- All ([`FO ps], split_formula (subst_vars [(s, ps)] phi))
- in
- And (List.map new_phi (prefixes s))
- )
+ match v with
+ | `Real _ -> failwith "splitting reals not supported (all)"
+ | `SO _ -> failwith "splitting non-monadic SO not supported (all)"
+ | `MSO s ->
+ All (List.map (fun x -> `MSO x) (prefixes s),
+ split_formula (map_to_atoms (replace_in s) phi))
+ | `FO s ->
+ let new_phi ps =
+ All ([`FO ps], split_formula (subst_vars [(s, ps)] phi)) in
+ And (List.map new_phi (prefixes s))
+ )
| All (v::vs, phi) -> split_formula (All ([v], All (vs, phi)))
| Or (flist) -> Or (List.rev_map split_formula flist)
| And (flist) -> And (List.rev_map split_formula flist)
@@ -207,37 +207,44 @@
(* Compute a decomposition of a formula on a given class definition. *)
let decompose ?(get_ids=false) phi_in = function
- Struct s as cdef ->
- if !debug_level > 0 then print_endline ("Deciding " ^ (Formula.str phi_in) ^ " on struct");
- [[("", split phi_in cdef)]]
+ | Struct s as cdef ->
+ if !debug_level > 0 then
+ print_endline ("Deciding " ^ (Formula.str phi_in) ^ " on struct");
+ [[("", split phi_in cdef)]]
| Sum (ids_l, rels_r) as cdef ->
- let phi = class_tnf (simplify phi_in) in
- if !debug_level > 0 then
- print_endline ("Decomposing " ^ (Formula.str phi) ^ " on " ^ (struct_sum_str cdef));
- let phi_fv = free_vars phi in
- let split_phi = split (Ex (phi_fv, phi)) cdef in
- let (summand_ids, _) = List.split ids_l in
- let simp_split_phi = map_to_atoms (simplify_atom summand_ids) split_phi in
- match List.rev_map simplify (to_dnf (class_tnf (simplify (simp_split_phi)))) with
- [] -> [[("", Or [])]]
- | fl when List.mem (And []) fl -> [[("", And [])]]
- | fl ->
- let rec del_quant = (function
- Ex (vs, psi) ->
- let was_free v = List.mem v phi_fv in
- let ws= List.filter (fun x -> not (was_free x)) vs in
- if ws = [] then del_quant psi else Ex (ws, psi)
- | And flist -> And (List.map del_quant flist)
- | psi -> psi (* del_quant is applied to conjucts of DNF*) ) in
- let del_quants = List.rev_map (fun (s, f) -> (s, del_quant f)) in
- let process f = rename_extract_conjunction get_ids ids_l f in
- let decomp_lit_str (cid, phi) = "\nsome " ^ cid ^ " |= " ^ (Formula.str phi) in
- let decomp_tuple_str cj =
- "(" ^ String.concat " and " (List.map decomp_lit_str cj) ^ ")" in
- let decomp_str df = String.concat " or " (List.map decomp_tuple_str df) in
- let res = List.rev_map (fun f -> del_quants (process f)) fl in
- if (!debug_level > 1) then print_endline ("DECOMP: " ^ (decomp_str res));
- res
+ let phi = class_tnf (simplify phi_in) in
+ if !debug_level > 0 then
+ print_endline ("Decomposing " ^ (Formula.str phi) ^ " on " ^
+ (struct_sum_str cdef));
+ let phi_fv = free_vars phi in
+ let split_phi = split (Ex (phi_fv, phi)) cdef in
+ let (summand_ids, _) = List.split ids_l in
+ let simp_split_phi = map_to_atoms (simplify_atom summand_ids) split_phi in
+ match List.rev_map simplify
+ (to_dnf (class_tnf (simplify (simp_split_phi)))) with
+ | [] -> [[("", Or [])]]
+ | fl when List.mem (And []) fl -> [[("", And [])]]
+ | fl ->
+ let rec del_quant = (function
+ Ex (vs, psi) ->
+ let was_free v = List.mem v phi_fv in
+ let ws= List.filter (fun x -> not (was_free x)) vs in
+ if ws = [] then del_quant psi else Ex (ws, psi)
+ | And flist -> And (List.map del_quant flist)
+ | psi -> psi (* del_quant is applied to conjucts of DNF*) ) in
+ let del_quants = List.rev_map (fun (s, f) -> (s, del_quant f)) in
+ let process f = rename_extract_conjunction get_ids ids_l f in
+ let decomp_lit_str (cid, phi) =
+ "\nsome " ^ cid ^ " |= " ^ (Formula.str phi) in
+ let decomp_tuple_str cj =
+ "(" ^ String.concat " and " (List.map decomp_lit_str cj) ^ ")" in
+ let decomp_str df =
+ String.concat " or " (List.map decomp_tuple_str df) in
+ let fflat l = List.map (fun (s, f) -> (s, flatten f)) l in
+ let res = List.rev_map (fun f -> fflat (del_quants (process f))) fl in
+ if !debug_level > 1 then
+ print_endline ("DECOMP: " ^ (decomp_str res));
+ res
Modified: trunk/Toss/Solver/ClassTest.ml
===================================================================
--- trunk/Toss/Solver/ClassTest.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Solver/ClassTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -1,184 +1,251 @@
-Class.set_debug_level 0 ;;
+open OUnit
+Class.set_debug_level 0
+
let class_of_string s =
ClassParser.parse_class Lexer.lex (Lexing.from_string s)
-;;
+
let formula_of_string s =
FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-;;
-let test_sum name f print_f class_str =
- let (_, suml) = List.hd (class_of_string class_str) in
- let sum = List.hd suml in
- print_endline (name ^ " on:\n" ^ (Class.struct_sum_str sum) ^ "\nis:");
- print_endline ((print_f (f sum)) ^"\n");
-;;
+let assert_eq_string arg msg x_in y_in =
+ let full_msg = msg ^ " (argument: " ^ arg ^ ")" in
+ let ws = Str.regexp "[ \n\t]+" in
+ let x = Str.global_replace ws " " (" " ^ x_in ^ " ") in
+ let y = Str.global_replace ws " " (" " ^ y_in ^ " ") in
+ assert_equal ~printer:(fun x -> x) ~msg:full_msg
+ ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
-let test name f print_f class_str =
- let cl = class_of_string class_str in
- print_endline (name ^ " on:\n" ^ (Class.str cl) ^ "\nis:");
- print_endline ((print_f (f cl)) ^"\n");
-;;
-(* ----------------- VARIOUS TREE CLASSES AND PARSING TESTS ----------------- *)
+(* ----------------- VARIOUS CLASSES ----------------- *)
let fin_tree_class =
"point =
- [x | Left:2 {} ; Right:2 {} ; Root { x } | ]
+ [x | Left:2 {}; Right:2 {}; Root (x) | ]
and tree =
point
| L: tree + N: point + R: tree with
- Left (x, y) <- Left (x, y) or (N (x) and L (y) and Root (y)) ;
- Right (x, y) <- Right (x, y) or (N(x) and R (y) and Root (y)) ;
- Root (x) <- N (x);"
-;;
+ Left(x, y) <- Left(x, y) or (N(x) and L(y) and Root(y));
+ Right(x, y) <- Right(x, y) or (N(x) and R(y) and Root(y));
+ Root(x) <- N(x);"
-test "Id" (fun x -> x) Class.str "point = [ x | | ]" ;;
-test "Id" (fun x -> x) Class.str fin_tree_class ;;
-
let inf_tree =
"tree =
L: tree + N: point + R: tree with
- Left (x, y) <- Left (x, y) or (N (x) and L (y) and Root (y)) ;
- Right (x, y) <- Right (x, y) or (N(x) and R (y) and Root (y)) ;
- Root (x) <- N (x);
+ Left(x, y) <- Left(x, y) or (N(x) and L(y) and Root(y));
+ Right(x, y) <- Right(x, y) or (N(x) and R(y) and Root(y));
+ Root(x) <- N(x);
and point =
- [x | Left:2 {} ; Right:2 {} ; Root { x } | ]"
-;;
+ [x | Left:2 {}; Right:2 {}; Root (x) | ]"
-test "Id" (fun x -> x) Class.str inf_tree ;;
-let omega =
- "omega =
- Z: point + S: omega with
- LessEq (x, y) <- LessEq (x, y) or Z (x) ;
- Succ (x, y) <- Succ (x, y) or (Z(x) and S (y) and Zero (y)) ;
- Zero (x) <- Z (x) ;
- and point =
- [x | LessEq { (x, x) } ; Succ:2 {} ; Zero { x } | ]"
-;;
-
-test "Id" (fun x -> x) Class.str inf_tree ;;
-test "Id" (fun x -> x) Class.str omega ;;
-
let inf_tree_lr =
"Ttree =
L: Ltree + N: point + R: Rtree with
- Pref (x, y) <- Pref (x, y) or (N(x) and (L(y) or R(y)));
- Left (x) <- Left (x);
- Right (x) <- Right (x);
- Root (x) <- N(x);
+ Pref(x, y) <- Pref(x, y) or (N(x) and (L(y) or R(y)));
+ Left(x) <- Left(x);
+ Right(x) <- Right(x);
+ Root(x) <- N(x);
and Ltree =
L: Ltree + N: point + R: Rtree with
- Pref (x, y) <- Pref (x, y) or (N(x) and (L(y) or R(y)));
- Left (x) <- Left (x) or N(x);
- Right (x) <- Right (x);
- Root (x) <- Root (x);
+ Pref(x, y) <- Pref(x, y) or (N(x) and (L(y) or R(y)));
+ Left(x) <- Left(x) or N(x);
+ Right(x) <- Right(x);
+ Root(x) <- Root(x);
and Rtree =
L: Ltree + N: point + R: Rtree with
- Pref (x, y) <- Pref (x, y) or (N(x) and (L(y) or R(y)));
- Left (x) <- Left (x);
- Right (x) <- Right (x) or N(x);
- Root (x) <- Root (x);
+ Pref(x, y) <- Pref(x, y) or (N(x) and (L(y) or R(y)));
+ Left(x) <- Left(x);
+ Right(x) <- Right(x) or N(x);
+ Root(x) <- Root(x);
and point =
- [x | Left:1 {} ; Right:1 {} ; Pref:2 {} ; Root:1 {} | ]"
-;;
+ [x | Left:1 {}; Pref:2 {}; Right:1 {}; Root:1 {} | ]"
-test "Id" (fun x -> x) Class.str inf_tree_lr ;;
+let omega =
+ "omega =
+ Z: point + S: omega with
+ LessEq(x, y) <- LessEq(x, y) or Z(x);
+ Succ(x, y) <- Succ(x, y) or (Z(x) and S(y) and Zero(y));
+ Zero(x) <- Z(x);
+ and point =
+ [x | LessEq (x, x); Succ:2 {}; Zero (x) | ]"
-(* ----------------------------- SPLIT TESTS -------------------------------- *)
-let test_split phi_s cs =
- let f = formula_of_string phi_s in
- let split_f s = Class.split f s in
- test_sum ("Split of " ^ phi_s) split_f Formula.str cs
-;;
-let test_split_simplify phi_s cs =
- let f = formula_of_string phi_s in
- let split_f s = Class.split_simplify f s in
- test_sum ("Simplified Split of " ^ phi_s) split_f Formula.str cs
-;;
+(* ------------------- UNIT TESTS ------------------- *)
-(* Splits on inf_tree. *)
+let test_sum name f print_f class_str res_str =
+ let (_, suml) = List.hd (class_of_string class_str) in
+ let sum = List.hd suml in
+ let sum_str = Class.struct_sum_str sum in
+ assert_eq_string sum_str name res_str (print_f (f sum))
-test_split "ex x Root (x)" inf_tree ;;
-test_split "ex x, y Left (x, y)" inf_tree ;;
+let tests = "Class" >::: [
+ "parsing and printing" >::
+ (fun () ->
+ let test name f print_f class_str res_str =
+ let cl = class_of_string class_str in
+ assert_eq_string class_str name res_str (print_f (f cl)) in
+ test "Id" (fun x -> x) Class.str "point = [ x | | ]" "point = [x | | ]";
+ test "Id" (fun x -> x) Class.str fin_tree_class fin_tree_class;
+ test "Id" (fun x -> x) Class.str inf_tree inf_tree;
+ test "Id" (fun x -> x) Class.str inf_tree_lr inf_tree_lr;
+ test "Id" (fun x -> x) Class.str omega omega;
+ );
-(* Y is contains all left-successors of X *)
-test_split "all X ex Y all x, y (x in X and Left (x, y) -> y in Y)" inf_tree ;;
+ "split" >::
+ (fun () ->
+ let test_split ?(do_simp=false) phi_s cs res =
+ let f = formula_of_string phi_s in
+ let split_f s =
+ if do_simp then Class.split_simplify f s else Class.split f s in
+ let name = if do_simp then "Simplified Split of " else "Split of " in
+ test_sum (name ^ phi_s) split_f Formula.str cs res in
+ test_split "ex x Root (x)" inf_tree
+ "(ex x:L (N(x:L)) or ex x:N (N(x:N)) or ex x:R (N(x:R)))";
+ test_split "ex x, y Left (x, y)" inf_tree
+ ("(ex x:L ((ex y:L ((Left(x:L, y:L) or ((N(x:L) and L(y:L)) and " ^
+ "Root(y:L)))) or ex y:N ((Left(x:L, y:N) or ((N(x:L) and L(y:N))" ^
+ " and Root(y:N)))) or ex y:R ((Left(x:L, y:R) or ((N(x:L) and " ^
+ "L(y:R)) and Root(y:R)))))) or ex x:N ((ex y:L ((Left(x:N, y:L) " ^
+ "or ((N(x:N) and L(y:L)) and Root(y:L)))) or ex y:N " ^
+ "((Left(x:N, y:N) or ((N(x:N) and L(y:N)) and Root(y:N)))) " ^
+ "or ex y:R ((Left(x:N, y:R) or ((N(x:N) and L(y:R)) and " ^
+ "Root(y:R)))))) or ex x:R ((ex y:L ((Left(x:R, y:L) or ((N(x:R) " ^
+ "and L(y:L)) and Root(y:L)))) or ex y:N ((Left(x:R, y:N) or " ^
+ "((N(x:R) and L(y:N)) and Root(y:N)))) or ex y:R ((Left(x:R, y:R)" ^
+ " or ((N(x:R) and L(y:R)) and Root(y:R)))))))");
+ test_split ~do_simp:true (* Y is contains all left-successors of X *)
+ "all X ex Y all x, y (x in X and Left (x, y) -> y in Y)" inf_tree
+ ("all X:L, X:N, X:R (ex Y:L, Y:N, Y:R ((all x:L (all y:L" ^
+ " (((y:L in Y:L) or (not (Left(x:L, y:L) and (x:L in X:L))))))" ^
+ " and all x:R (all y:R (((y:R in Y:R) or (not (Left(x:R, y:R) " ^
+ "and (x:R in X:R)))))) and all x:N ((all y:N (((y:N in Y:N) or" ^
+ " (not (Left(x:N, y:N) and (x:N in X:N))))) and all y:L " ^
+ "(((y:L in Y:L) or (not ((x:N in X:N) and Root(y:L))))))))))");
-(* Splits on inf_tree_lr. *)
+ test_split "ex x, y Pref (x, y)" inf_tree_lr
+ ("(ex x:L ((ex y:L ((Pref(x:L, y:L) or (N(x:L) and (L(y:L) or " ^
+ "R(y:L))))) or ex y:N ((Pref(x:L, y:N) or (N(x:L) and (L(y:N)" ^
+ " or R(y:N))))) or ex y:R ((Pref(x:L, y:R) or (N(x:L) and " ^
+ "(L(y:R) or R(y:R))))))) or ex x:N ((ex y:L ((Pref(x:N, y:L) or" ^
+ " (N(x:N) and (L(y:L) or R(y:L))))) or ex y:N ((Pref(x:N, y:N)" ^
+ " or (N(x:N) and (L(y:N) or R(y:N))))) or " ^
+ "ex y:R ((Pref(x:N, y:R) or (N(x:N) and (L(y:R) or R(y:R)))))))" ^
+ " or ex x:R ((ex y:L ((Pref(x:R, y:L) or (N(x:R) and (L(y:L) " ^
+ "or R(y:L))))) or ex y:N ((Pref(x:R, y:N) or (N(x:R) and " ^
+ "(L(y:N) or R(y:N))))) or ex y:R ((Pref(x:R, y:R) or (N(x:R) " ^
+ "and (L(y:R) or R(y:R))))))))");
+ test_split ~do_simp:true
+ ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) -> " ^
+ "(Root(y) or Right(y))))))") inf_tree_lr
+ ("ex X:L, X:N, X:R ((all x:N ((Left(x:N) or (not (x:N in X:N)))) " ^
+ "and all x:L (((not (x:L in X:L)) or (Left(x:L) and all y:L " ^
+ "((Right(y:L) or (not Pref(y:L, x:L))))))) and all x:R (((not" ^
+ " (x:R in X:R)) or (Left(x:R) and all y:R ((Right(y:R) or " ^
+ "(not Pref(y:R, x:R)))))))))");
+ test_split ~do_simp:true
+ ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) -> " ^
+ "(Root(y) or Right(y))))))") inf_tree_lr
+ ("ex X:L, X:N, X:R ((all x:N ((Left(x:N) or (not (x:N in X:N)))) " ^
+ "and all x:L (((not (x:L in X:L)) or (Left(x:L) and all y:L " ^
+ "((Right(y:L) or (not Pref(y:L, x:L))))))) and all x:R (((not" ^
+ " (x:R in X:R)) or (Left(x:R) and all y:R ((Right(y:R) " ^
+ "or (not Pref(y:R, x:R)))))))))");
+ );
-test_split "ex x, y Pref (x, y)" inf_tree_lr ;;
+ "decompose" >::
+ (fun () ->
+ let test_decompose ?(ids=true) phi_s cs res =
+ let f = formula_of_string phi_s in
+ let decompose_f s = Class.decompose ~get_ids:ids f s in
+ let decomp_lit_str (cid, phi) =
+ "Ex " ^ cid ^ " |= " ^ (Formula.sprint phi) in
+ let decomp_tuple_str cj =
+ "(" ^ String.concat " and " (List.map decomp_lit_str cj) ^ ")" in
+ let decomp_str df =
+ String.concat " or " (List.map decomp_tuple_str df) in
+ test_sum ("Decomposition of " ^ phi_s) decompose_f decomp_str cs res in
-test_split ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) -> " ^
- "(Root(y) or Right(y))))))") inf_tree_lr ;;
+ (* On omega *)
+ test_decompose "ex x, y LessEq (x, y)" omega "(Ex |= true)";
+ test_decompose
+ ("ex Z (((not all s ((Zero(s) or (not (s in Z))))) and " ^
+ "ex C ((all s (((s in C) or (not Zero(s)))) and " ^
+ "all t (((t in C) or (not (t in Z)))) and " ^
+ "all t (((t in Z) or (not (t in C)))) and " ^
+ "all s (((not (s in C)) or all t ((not Succ(t, s))))) and all s " ^
+ "(((not (s in C)) or all t (((t in C) or (not Succ(t, s))))))))))")
+ omega
+ ("(Ex Z |= (all s, t not Succ(t, s) and ex Z, C (all s s in C and " ^
+ "all t t in C and all t t in Z)) and Ex S |= ex Z (not all s " ^
+ "not s in Z and ex C (all t (t in C or not t in Z) and all t " ^
+ "(t in Z or not t in C) and all s (not s in C or all t (t in C " ^
+ "or not Succ(t, s))) and all s (not s in C or (not Zero(s) and " ^
+ "all t not Succ(t, s)))))) or (Ex Z |= (all s, t not Succ(t, s) " ^
+ "and ex Z, C (all s s in C and all t t in Z)) and Ex S |= ex Z " ^
+ "(not all s not s in Z and ex C (all t (t in C or not t in Z) and" ^
+ " all t (t in Z or not t in C) and all s (not Zero(s) or " ^
+ "not s in C) and all s (not s in C or all t (t in C or not " ^
+ "Succ(t, s))) and all s (not s in C or (not Zero(s) and " ^
+ "all t not Succ(t, s))))))");
-test_split_simplify ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) -> " ^
- "(Root(y) or Right(y))))))") inf_tree_lr ;;
+ (* On inf_tree *)
+ test_decompose "ex x Root (x)" inf_tree "(Ex |= true)";
+ test_decompose "x in X" inf_tree
+ "(Ex L |= x in X) or (Ex N |= x in X) or (Ex R |= x in X)";
+ test_decompose "ex x, y Left (x, y)" inf_tree
+ ("(Ex L |= ex x, y Left(x, y)) or (Ex N |= ex x, y Left(x, y))" ^
+ " or (Ex R |= ex x, y Left(x, y)) or (Ex L |= ex y Root(y))");
+ (* On inf_tree_lr *)
+ test_decompose ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) " ^
+ "-> (Root(y) or Right(y))))))") inf_tree_lr
+ ("(Ex R |= ex X all x (not x in X or (Left(x) and all y (Right(y) or " ^
+ "not Pref(y, x)))) and Ex N |= ex X all x (Left(x) or not x in X)" ^
+ " and Ex L |= ex X all x (not x in X or (Left(x) and " ^
+ "all y (Right(y) or not Pref(y, x)))))");
+ test_decompose "Left(x) and Right(y)" inf_tree_lr
+ ("(Ex L |= (Left(x) and Right(y))) or (Ex N |= Right(y) and " ^
+ "Ex L |= Left(x)) or (Ex R |= Right(y) and Ex L |= Left(x)) or " ^
+ "(Ex N |= Left(x) and Ex L |= Right(y)) or (Ex N |= (Left(x) " ^
+ "and Right(y))) or (Ex R |= Right(y) and Ex N |= Left(x)) or " ^
+ "(Ex R |= Left(x) and Ex L |= Right(y)) or (Ex R |= Left(x) and " ^
+ "Ex N |= Right(y)) or (Ex R |= (Left(x) and Right(y)))");
+ test_decompose "ex x Left(x)" inf_tree_lr
+ ("(Ex L |= ex x Left(x)) or (Ex N |= ex x Left(x)) or" ^
+ " (Ex R |= ex x Left(x))");
+ test_decompose "Left(x)" inf_tree_lr
+ "(Ex L |= Left(x)) or (Ex N |= Left(x)) or (Ex R |= Left(x))";
+ test_decompose "all y (x=y or Pref(x,y))" inf_tree_lr
+ "(Ex N |= all y (Pref(x, y) or x = y))";
+ test_decompose "Left(x) and Right(y) and all z (Pref(z,x) and Pref(z,y))"
+ inf_tree_lr "(Ex |= false)";
+ test_decompose
+ "ex X ex y( y in X and all z( Pref(y,z) or z in X))" inf_tree_lr
+ ("(Ex N |= ex X, y (y in X and all z (Pref(y, z) or z in X))) or " ^
+ "(Ex R |= ex X, y (y in X and all z (Pref(y, z) or z in X)) and" ^
+ " Ex N |= ex X all z z in X and Ex L |= ex X all z z in X) or " ^
+ "(Ex R |= ex X all z z in X and Ex N |= ex X all z z in X and " ^
+ "Ex L |= ex X, y (y in X and all z (Pref(y, z) or z in X)))");
+ test_decompose
+ "all X ex y( y in X and all z( Pref(y,z) or z in X))" inf_tree_lr
+ ("(Ex N |= all X ex y (y in X and all z (Pref(y, z) or z in X))) or" ^
+ " (Ex L |= all X, z z in X) or (Ex R |= true and Ex L |= " ^
+ "all X, z z in X) or (Ex R |= all X, z z in X and Ex L |= true) " ^
+ "or (Ex R |= all X, z z in X)");
+ );
+]
-(* --------------------------- DECOMPOSE TESTS ------------------------------ *)
-let test_decompose ids phi_s cs =
- let f = formula_of_string phi_s in
- let decompose_f s = Class.decompose ~get_ids:ids f s in
- let decomp_lit_str (cid, phi) = "some " ^ cid ^ " |= " ^ (Formula.str phi) in
- let decomp_tuple_str cj =
- "(" ^ String.concat " and " (List.map decomp_lit_str cj) ^ ")" in
- let decomp_str df = String.concat " or " (List.map decomp_tuple_str df) in
- test_sum ("Decomposition of " ^ phi_s) decompose_f decomp_str cs
-;;
-
-
-(* Decompositions on omega. *)
-
-test_decompose true "ex x, y LessEq (x, y)" omega ;;
-
-
-(* Decompositions on inf_tree. *)
-
-test_decompose true "ex x Root (x)" inf_tree ;;
-
-test_decompose true "x in X" inf_tree ;;
-
-test_decompose true "ex x, y Left (x, y)" inf_tree ;;
-
-test_decompose true ("ex X (all x (x in X -> (Left(x) and all y (Pref(y,x) -> "^
- "(Root(y) or Right(y))))))") inf_tree_lr ;;
-
-test_decompose true "Left(x) and Right(y)" inf_tree_lr ;;
-
-test_decompose true "ex x Left(x)" inf_tree_lr ;;
-
-test_decompose true "Left(x)" inf_tree_lr ;;
-
-test_decompose true "all y (x=y or Pref(x,y))" inf_tree_lr ;;
-
-test_decompose true "Left(x) and Right(y) and all z (Pref(z,x) and Pref(z,y))" inf_tree_lr ;;
-
-
-(* ------------ There is some bug... --------------- *)
-
-(* "ex X ..." works *)
-test_decompose true "ex X ex y( y in X and all z( Pref(y,z) or z in X))" inf_tree_lr ;;
-
-(* but "all X ..." does not *)
-Class.set_debug_level 2 ;;
-test_decompose true "all X ex y( y in X and all z( Pref(y,z) or z in X))" inf_tree_lr ;;
-
-
-
-
(* ------------------------- MODEL CHECKING TESTS -------------------------- *)
let test_check phi_s id cs =
@@ -188,7 +255,6 @@
print_endline "";
;;
-Class.set_debug_level 0 ;;
test_check "all x, y LessEq (x, y)" "omega" omega ;;
@@ -334,16 +400,6 @@
;;
-test_decompose true
- "ex Z (((not all s ((Zero(s) or (not (s in Z))))) and
- ex C ((all s (((s in C) or (not Zero(s)))) and
- all t (((t in C) or (not (t in Z)))) and
- all t (((t in Z) or (not (t in C)))) and
- all s (((not (s in C)) or all t ((not Succ(t, s)))))
- and all s (((not (s in C)) or all t (((t in C) or (not Succ(t, s))))))))))"
- omega ;;
-
-
(* ------------ HORN FORMULA TESTS ------------------ *)
@@ -358,10 +414,6 @@
"ex X (" ^ quant ^ "(" ^ clauses ^ "))"
;;
-FormulaOps.set_debug_level 0 ;;
-Sat.set_debug_level 0;;
-Class.set_debug_level 1 ;;
-
let horn_f = horn 10 ;;
print_endline ("Horn: " ^ horn_f);
@@ -372,7 +424,6 @@
-BoolFormula.set_simplification 6 ;;
(*
print_endline ("Checking non-TNF Horn...");;
@@ -385,9 +436,4 @@
print_endline ("Checking TNF Horn...");;
test_check horn_tnf "omega" omega ;;
-
-let s = Gc.stat () in
-let alloc_w = s.Gc.minor_words +. s.Gc.major_words -. s.Gc.promoted_words in
-print_endline ("Alloc B: " ^ (string_of_float (4. *. alloc_w)));
-print_endline ("Alloc KB: " ^ (string_of_float (alloc_w /. 256. )));
-print_endline ("Alloc MB: " ^ (string_of_float (alloc_w /. (1024. *. 256.))));
+let exec = Aux.run_test_if_target "ClassTest" tests ;;
Modified: trunk/Toss/Solver/PresbTest.ml
===================================================================
--- trunk/Toss/Solver/PresbTest.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/Solver/PresbTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -129,7 +129,7 @@
BoolFormula.set_debug_level 0 ;;
BoolFormula.set_simplification 6 ;;
-Class.set_debug_level 1;;
+Class.set_debug_level 0;;
test_check eq "omega" omega ;;
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2011-04-27 17:44:35 UTC (rev 1423)
+++ trunk/Toss/TossTest.ml 2011-04-28 22:09:04 UTC (rev 1424)
@@ -14,6 +14,7 @@
StructureTest.tests;
AssignmentsTest.tests;
SolverTest.tests;
+ ClassTest.tests;
]
let arena_tests = "Arena" >::: [
@@ -36,6 +37,7 @@
]
let server_tests = "Server" >::: [
+ PictureTest.tests;
ServerTest.tests;
]
Added: trunk/Toss/www/img/Breakthrough.ppm
===================================================================
--- trunk/Toss/www/img/Breakthrough.ppm (rev 0)
+++ trunk/Toss/www/img/Breakthrough.ppm 2011-04-28 22:09:04 UTC (rev 1424)
@@ -0,0 +1,120003 @@
+P3
+200 200
+255
+0
+0
+0
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+43
+0
+21
+47
+0
+19
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+44
+0
+18
+49
+0
+12
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+40
+0
+13
+41
+0
+16
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+41
+0
+20
+41
+0
+20
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+41
+0
+16
+40
+0
+13
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+49
+0
+12
+44
+0
+18
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+47
+0
+19
+43
+0
+21
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+45
+0
+15
+0
+0
+0
+26
+0
+26
+38
+3
+20
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+40
+6
+21
+43
+8
+24
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+52
+17
+30
+44
+9
+24
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+9
+25
+39
+4
+21
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+40
+5
+21
+41
+7
+22
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+48
+13
+27
+45
+10
+25
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+43
+8
+23
+40
+6
+22
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+49
+14
+27
+44
+8
+23
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+45
+11
+26
+38
+3
+20
+26
+0
+26
+26
+0
+26
+39
+4
+21
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+113
+82
+73
+112
+80
+71
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+57
+22
+33
+200
+171
+132
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+197
+167
+130
+54
+20
+31
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+228
+170
+255
+22...
[truncated message content] |
