[Toss-devel-svn] SF.net SVN: toss:[1683] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1683] trunk/Toss
|
From: <luk...@us...> - 2012-03-07 03:56:23
|
Revision: 1683
http://toss.svn.sourceforge.net/toss/?rev=1683&view=rev
Author: lukaszkaiser
Date: 2012-03-07 03:56:13 +0000 (Wed, 07 Mar 2012)
Log Message:
-----------
Correcting loging, printing and old tests; adding bitvector.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/ContinuousRuleTest.ml
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Arena/Term.ml
trunk/Toss/Arena/TermTest.ml
trunk/Toss/Client/clientTest.js
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/AuxIO.ml
trunk/Toss/Formula/AuxIO.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormulaTest.ml
trunk/Toss/Formula/BoolFunction.ml
trunk/Toss/Formula/BoolFunction.mli
trunk/Toss/Formula/BoolFunctionTest.ml
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Sat/MiniSAT.ml
trunk/Toss/GGP/GameSimplTest.ml
trunk/Toss/GGP/KIFLexer.mll
trunk/Toss/GGP/TranslateGame.ml
trunk/Toss/GGP/TranslateGameTest.ml
trunk/Toss/Learn/LearnGameTest.ml
trunk/Toss/Makefile
trunk/Toss/MenhirLib/tableInterpreter.ml
trunk/Toss/Play/GameTree.ml
trunk/Toss/Play/Play.ml
trunk/Toss/Server/ReqHandler.ml
trunk/Toss/Server/Server.ml
trunk/Toss/Server/Tests.ml
trunk/Toss/Solver/ClassTest.ml
trunk/Toss/Solver/Structure.ml
trunk/Toss/Solver/StructureTest.ml
Added Paths:
-----------
trunk/Toss/Solver/Num/Bitvector.ml
trunk/Toss/Solver/Num/Bitvector.mli
trunk/Toss/Solver/Num/BitvectorTest.ml
Removed Paths:
-------------
trunk/Toss/Client/MissingFunctions.js
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/Arena.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -93,7 +93,7 @@
List.map (fun (lhs_v, m_e) ->
lhs_v,
(try Structure.find_elem state.struc m_e
- with Not_found -> Printf.printf "NF m_e=%s\n%!" m_e;
+ with Not_found -> AuxIO.print (Printf.sprintf "NF m_e=%s\n%!" m_e);
raise Not_found))
match_str
with Not_found ->
@@ -360,10 +360,7 @@
Format.fprintf f "@[<1>[%s@ %F,@ %s@ ->@ %i@ emb@ %s]%s@]" rn t p_s l m_s rt
)
-let sprint_game_move gm =
- ignore (Format.flush_str_formatter ());
- fprint_game_move Format.str_formatter gm;
- Format.flush_str_formatter ()
+let sprint_game_move gm = AuxIO.sprint_of_fprint fprint_game_move gm
let fprint_state_full print_compiled_rules ppf
({rules = rules;
@@ -416,18 +413,9 @@
Format.fprintf ppf "@]"
let fprint_state = fprint_state_full false
-
-let print_state r = fprint_state Format.std_formatter r
-let sprint_state r =
- ignore (Format.flush_str_formatter ());
- fprint_state Format.str_formatter r;
- Format.flush_str_formatter ()
-
-let sprint_state_full r =
- ignore (Format.flush_str_formatter ());
- fprint_state_full true Format.str_formatter r;
- Format.flush_str_formatter ()
-
+let print_state r = AuxIO.print_of_fprint (fprint_state_full false) r
+let sprint_state r = AuxIO.sprint_of_fprint (fprint_state_full false) r
+let sprint_state_full r = AuxIO.sprint_of_fprint (fprint_state_full true) r
let str game = sprint_state (game, snd empty_state)
let state_str state = sprint_state state
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/ContinuousRule.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -253,11 +253,8 @@
let fprint = fprint_full false
-let print r = fprint Format.std_formatter r
-let sprint r =
- ignore (Format.flush_str_formatter ());
- fprint Format.str_formatter r;
- Format.flush_str_formatter ()
+let print r = AuxIO.print_of_fprint fprint r
+let sprint r = AuxIO.sprint_of_fprint fprint r
let matching_str struc emb =
let name (lhs_v,rhs_e) =
Modified: trunk/Toss/Arena/ContinuousRuleTest.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRuleTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/ContinuousRuleTest.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -42,12 +42,12 @@
let r = rule_of_str s signat [] "rule2" in
assert_equal ~msg:"2. update" ~printer:(fun x->x) s (str r);
- let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
+ let dyn_eq = ":f(a)' = 2. * :f(a) + t; :f(b)' = :f(b)" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ " inv true post true" in
let r = rule_of_str s signat [] "rule3" in
assert_equal ~msg:"3. dynamics" ~printer:(fun x->x) s (str r);
- let dyn_eq = " :f(a)' = (2. * :f(a)) + t;\n :f(b)' = :f(b)" in
+ let dyn_eq = ":f(a)' = 2. * :f(a) + t; :f(b)' = :f(b)" in
let upd_eq = " :f(c) = 2. * :f(a);\n :f(d) = :f(b)\n" in
let s = discr ^ "\ndynamics\n" ^ dyn_eq ^ "\nupdate\n" ^ upd_eq ^
" inv true post true" in
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/DiscreteRule.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -1347,11 +1347,8 @@
(Aux.fprint_sep_list ";" matched) matching
-let print_rule r = fprint_rule Format.std_formatter r
-let sprint_rule r =
- ignore (Format.flush_str_formatter ());
- fprint_rule Format.str_formatter r;
- Format.flush_str_formatter ()
+let print_rule r = AuxIO.print_of_fprint fprint_rule r
+let sprint_rule r = AuxIO.sprint_of_fprint fprint_rule r
(* Either build a default correspondence for a rule, where RHS
Modified: trunk/Toss/Arena/Term.ml
===================================================================
--- trunk/Toss/Arena/Term.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/Term.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -19,36 +19,6 @@
(* ------------------------ PRINTING FUNCTION ------------------------------- *)
-(* Print a term as a string. *)
-let rec str = function
- | Var s -> s
- | FVar (f, a) -> ":" ^ f ^ "(" ^ a ^ ")"
- | Const n -> string_of_float n
- | Times (p, q) -> term_pair_str " * " p q
- | Plus (p, Times (Const c, q)) when c = -1. -> term_pair_str " - " p q
- | Plus (p, Const c) when c < 0. -> term_pair_str " - " p (Const (-. c))
- | Plus (p, q) -> term_pair_str " + " p q
- | Div (p, q) -> term_pair_str " / " p q
-
-and term_pair_str sep p q =
- let brack s = if String.length s < 2 then s else "(" ^ s ^ ")" in
- match (p, q) with
- | (Const _, Const _) | (FVar _, Const _) | (Const _, FVar _)
- | (FVar _, FVar _) -> (str p) ^ sep ^ (str q)
- | (Const _, _) | (FVar _, _) -> (str p) ^ sep ^ (brack (str q))
- | (_, Const _) | (_, FVar _) -> (brack (str p)) ^ sep ^ (str q)
- | _ -> (brack (str p)) ^ sep ^ (brack (str q))
-
-
-(* Print an equation system as a string. *)
-let eq_str ?(diff=true) eqs =
- let sing_str ((f, a), t) =
- let mid_str = if diff then "' = " else " = " in
- let l_str = str (FVar (f, a)) in
- let r_str = str t in
- l_str ^ mid_str ^ r_str in
- " " ^ (String.concat ";\n " (List.map sing_str eqs))
-
(* Bracket-savvy precedences: + 0, - 1, * 2, / 3 *)
let rec fprint ?(prec=0) ppf = function
| Var s -> Format.pp_print_string ppf s
@@ -77,11 +47,9 @@
Format.fprintf ppf "@[<1>%s%a@ /@ %a%s@]" lb
(fprint ~prec:2) p (fprint ~prec:3) q rb
-let print r = fprint Format.std_formatter r
-let sprint r =
- ignore (Format.flush_str_formatter ());
- fprint Format.str_formatter r;
- Format.flush_str_formatter ()
+let print r = AuxIO.print_of_fprint fprint r
+let sprint r = AuxIO.sprint_of_fprint fprint r
+let str = sprint
(* Print an equation system. *)
let fprint_eqs ?(diff=false) ppf eqs =
@@ -91,11 +59,9 @@
f a mid_str (fprint ~prec:0) t in
Format.fprintf ppf "@[<hv>%a@]" (Aux.fprint_sep_list ";" sing) eqs
-let print_eqs ?diff r = fprint_eqs ?diff Format.std_formatter r
-let sprint_eqs ?diff r =
- ignore (Format.flush_str_formatter ());
- fprint_eqs ?diff Format.str_formatter r;
- Format.flush_str_formatter ()
+let print_eqs ?diff r = AuxIO.print_of_fprint (fprint_eqs ?diff) r
+let sprint_eqs ?diff r = AuxIO.sprint_of_fprint (fprint_eqs ?diff) r
+let eq_str = sprint_eqs
(* -------------------- SIMPLIFICATION OF CONSTANTS ------------------------- *)
Modified: trunk/Toss/Arena/TermTest.ml
===================================================================
--- trunk/Toss/Arena/TermTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Arena/TermTest.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -13,13 +13,13 @@
let tests = "Term" >::: [
"parse" >::
(fun () ->
- let s = "(x - 0.2) / ((z * y) - 3.)" in
+ let s = "(x - 0.2) / (z * y - 3.)" in
assert_equal ~printer:(fun x->x) s (str (term_of_string s));
let t0s = ":f(a) + t" in
assert_equal ~printer:(fun x->x) t0s (str (term_of_string t0s));
- let eqs = " :f(a)' = :f(a) + t" in
+ let eqs = ":f(a)' = :f(a) + t" in
assert_equal ~printer:(fun x->x) eqs
(eq_str ~diff:true (eqs_of_string eqs));
Deleted: trunk/Toss/Client/MissingFunctions.js
===================================================================
--- trunk/Toss/Client/MissingFunctions.js 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Client/MissingFunctions.js 2012-03-07 03:56:13 UTC (rev 1683)
@@ -1,54 +0,0 @@
-// A bug in js_of_ocaml: it sometimes omits the functions below, which
-// belong to its runtmie.
-
-// Applies to code below this line:
-// Js_of_ocaml runtime support
-// http://www.ocsigen.org/js_of_ocaml/
-// Copyright (C) 2010 Jérôme Vouillon
-// Laboratoire PPS - CNRS Université Paris Diderot
-//
-// This program is free software; you can redistribute it and/or modify
-// it under the terms of the GNU Lesser General Public License as published by
-// the Free Software Foundation, with linking exception;
-// either version 2.1 of the License, or (at your option) any later version.
-//
-// This program is distributed in the hope that it will be useful,
-// but WITHOUT ANY WARRANTY; without even the implied warranty of
-// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-// GNU Lesser General Public License for more details.
-//
-// You should have received a copy of the GNU Lesser General Public License
-// along with this program; if not, write to the Free Software
-// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
-
-// Provides: caml_int64_bits_of_float const
-function caml_int64_bits_of_float (x) {
- if (!isFinite(x)) {
- if (isNaN(x)) return [255, 1, 0, 0xfff0];
- return (x > 0)?[255,0,0,0x7ff0]:[255,0,0,0xfff0];
- }
- var sign = (x>=0)?0:0x8000;
- if (sign) x = -x;
- var exp = Math.floor(Math.LOG2E*Math.log(x)) + 1023;
- if (exp <= 0) {
- exp = 0;
- x /= Math.pow(2,-1026);
- } else {
- x /= Math.pow(2,exp-1027);
- if (x < 16) { x *= 2; exp -=1; }
- if (exp == 0) { x /= 2; }
- }
- var k = Math.pow(2,24);
- var r3 = x|0;
- x = (x - r3) * k;
- var r2 = x|0;
- x = (x - r2) * k;
- var r1 = x|0;
- r3 = (r3 &0xf) | sign | exp << 4;
- return [255, r1, r2, r3];
-}
-//Provides: caml_int64_to_bytes
-function caml_int64_to_bytes(x) {
- return [x[3] >> 8, x[3] & 0xff, x[2] >> 16, (x[2] >> 8) & 0xff, x[2] & 0xff,
- x[1] >> 16, (x[1] >> 8) & 0xff, x[1] & 0xff];
-}
Modified: trunk/Toss/Client/clientTest.js
===================================================================
--- trunk/Toss/Client/clientTest.js 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Client/clientTest.js 2012-03-07 03:56:13 UTC (rev 1683)
@@ -88,7 +88,7 @@
return (existsId ("pred_b2_P"));
});
doAtTime (page, 4100, function () {
- ASYNCH ("run_tests_big", [""], function () {});
+ ASYNCH ("run_tests_small", [""], function () {});
});
doAtTime (undefined, 30000000, function () {
//console.log ("rendering");
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/Aux.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -49,37 +49,94 @@
(c = '0') || (c = '1') || (c = '2') || (c = '3') || (c = '4') ||
(c = '5') || (c = '6') || (c = '7') || (c = '8') || (c = '9')
-let is_space c =
- c = '\n' || c = '\r' || c = ' ' || c = '\t'
+let is_space c = c = ' ' || c = '\n' || c = '\r' || c = '\t'
-let strip_spaces s =
+let strip_charprop f s =
let (b, e) = (ref 0, ref ((String.length s) - 1)) in
- while !b < !e && is_space (s.[!b]) do incr b done;
- while !b <= !e && is_space (s.[!e]) do decr e done;
+ while !b < !e && f (s.[!b]) do incr b done;
+ while !b <= !e && f (s.[!e]) do decr e done;
if !e < !b then "" else String.sub s !b (!e - !b + 1)
-let split_charprop s f =
+let strip_spaces s = strip_charprop is_space s
+
+let split_charprop ?(keep_split_chars=false) f s =
let l, i = String.length s, ref 0 in
let rec split_charprop_rec acc =
- while !i < l && f s.[!i] do i := !i+1 done;
- if !i = l then acc else (
+ while !i < l && f s.[!i] do
+ if keep_split_chars then acc := (String.make 1 s.[!i]) :: !acc;
+ i := !i+1;
+ done;
+ if !i = l then !acc else (
let start = !i in
while !i < l && not (f s.[!i]) do i := !i+1 done;
- split_charprop_rec ((String.sub s start (!i - start)) :: acc)
+ acc := (String.sub s start (!i - start)) :: !acc;
+ split_charprop_rec acc
) in
- List.rev (split_charprop_rec [])
+ List.rev (split_charprop_rec (ref []))
-let split_spaces s = split_charprop s is_space
+let split_spaces s = split_charprop is_space s
+let split_newlines s = split_charprop (fun c -> c = '\n' || c = '\r') s
+
+let split_empty_lines s = (* Split a string on empty lines. *)
+ let lstr accs = if accs = "" then [] else [accs] in
+ let rec concat_nonempty accs = function
+ | [] -> lstr accs
+ | [x] -> if x = "\n" then lstr accs else lstr (accs ^ x)
+ | x :: y :: rs when x = "\n" && y = "\n" -> accs :: (concat_nonempty "" rs)
+ | x :: y :: rs -> concat_nonempty (accs ^ x) (y :: rs) in
+ concat_nonempty "" (split_charprop ~keep_split_chars:true (fun c-> c='\n') s)
+
let normalize_spaces s = String.concat " " (split_spaces s)
-let replace_charprop s f repl =
- let split, l = split_charprop s f, String.length s in
+let replace_charprop f repl s =
+ let split, l = split_charprop f s, String.length s in
let res = ref (String.concat repl split) in
if (l > 0 && f s.[0]) then res := repl ^ !res;
if (l > 1 && f s.[l-1]) then res := !res ^ repl;
!res
+let str_index ?(from=0) pattern s =
+ let l, pl = String.length s, String.length pattern in
+ let eq i =
+ let res = ref true in
+ for j = 0 to pl-1 do if pattern.[j] <> s.[i+j] then res := false; done;
+ !res in
+ let rec solve i = if i + pl > l then raise Not_found else
+ if eq i then i else solve (i+1) in
+ if pl = 0 then 0 else solve from
+
+let str_contains s pat = try str_index pat s >= 0 with Not_found -> false
+
+let str_subst_once_report pat res s =
+ if pat = "" then failwith "str_subst_once: empty pattern" else
+ try
+ let i, l, pl = str_index pat s, String.length s, String.length pat in
+ ((String.sub s 0 i) ^ res ^ (String.sub s (i+pl) (l-i-pl)), true)
+ with Not_found -> (s, false)
+
+let str_subst_once pat res s = fst (str_subst_once_report pat res s)
+
+let rec str_subst_all pat res s =
+ let (new_s, didsth) = str_subst_once_report pat res s in
+ if didsth then str_subst_all pat res new_s else s
+
+let str_subst_once_from_to_report sfrom sto res s =
+ if sfrom = "" || sto = "" then failwith "str_subst_once_from_to: empty" else
+ try
+ let i, lfrom,l = str_index sfrom s, String.length sfrom,String.length s in
+ let j, lto = str_index ~from:(i+lfrom) sto s, String.length sto in
+ ((String.sub s 0 i) ^ res ^ (String.sub s (j+lto) (l-j-lto)), true)
+ with Not_found -> (s, false)
+
+let str_subst_once_from_to f t res s =
+ fst (str_subst_once_from_to_report f t res s)
+
+let rec str_subst_all_from_to f t res s =
+ let (new_s, didsth) = str_subst_once_from_to_report f t res s in
+ if didsth then str_subst_all_from_to f t res new_s else s
+
+
let fst3 (a,_,_) = a
let snd3 (_,a,_) = a
let trd3 (_,_,a) = a
@@ -738,36 +795,3 @@
Format.fprintf f "%s@\n@\n%a" sep f_el hd;
pr_tail f tl in
Format.fprintf f "%a%a" f_el hd pr_tail tl
-
-
-
-(* Replacements for basic Str functions. *)
-
-(* [split_regexp ~regexp:r s] splits [s] into substrings, taking as
- delimiters the substrings that match [r], and returns the list of
- substrings. For instance, [split ~regexp:"[ \t]+" s] splits [s]
- into blank-separated words. An occurrence of the delimiter at the
- beginning and at the end of the string is ignored. *)
-let split_regexp ~regexp s =
- IFDEF JAVASCRIPT THEN (
- let js_s = Js.string s in
- let js_regex = jsnew Js.regExp (Js.string regexp) in
- let res = js_s##split_regExp (js_regex) in
- let res = Js.to_array (Js.str_array res) in
- Array.to_list (Array.map Js.to_string res)
- ) ELSE (
- Str.split (Str.regexp regexp) s
- ) ENDIF
-
-(* [replace_regexp ~regexp ~templ s] returns a string identical to
- [s], except that all substrings of [s] that match [regexp] have
- been replaced by [templ]. *)
-let replace_regexp ~regexp ~templ s =
- IFDEF JAVASCRIPT THEN (
- let js_s = Js.string s in
- let js_regex = jsnew Js.regExp (Js.string regexp) in
- let res = js_s##replace (js_regex, Js.string templ) in
- Js.to_string res
- ) ELSE (
- Str.global_replace (Str.regexp regexp) templ s
- ) ENDIF
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/Aux.mli 2012-03-07 03:56:13 UTC (rev 1683)
@@ -46,18 +46,6 @@
(** {2 Helper functions on lists and other functions lacking from the
standard library.} *)
-(** Split a string on characters satisfying [f]. *)
-val split_charprop : string -> (char -> bool) -> string list
-
-(** Split a string on spaces. *)
-val split_spaces : string -> string list
-
-(** Replace all white space sequences by a simple space, strip on both ends. *)
-val normalize_spaces : string -> string
-
-(** Replace characters satisfying [f] by [repl]. *)
-val replace_charprop : string -> (char -> bool) -> string -> string
-
(** Random element of a list. *)
val random_elem : 'a list -> 'a
@@ -329,10 +317,23 @@
val not_conflicting_name : ?truncate:bool -> Strings.t -> string -> string
(** Returns [n] strings proloning [s] and not appearing in [names]. *)
-val not_conflicting_names :
- ?truncate:bool ->
+val not_conflicting_names : ?truncate:bool ->
string -> Strings.t -> 'a list -> string list
+(** Printf helper functions. *)
+val list_fprint :
+ (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
+val array_fprint :
+ (out_channel -> 'a -> unit) -> out_channel -> 'a array -> unit
+
+(** Print an unboxed separated list, with breaks after the separator. *)
+val fprint_sep_list :
+ ?newline : int -> string -> (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a list -> unit
+
+
+(** Replacements for basic Str functions. *)
+
(** Character classes. *)
val is_uppercase : char -> bool
val is_lowercase : char -> bool
@@ -345,31 +346,49 @@
and to start with a lowercase letter. **)
val clean_name : string -> string
+(** Strip characters satisfying [f] from left and right of a string. *)
+val strip_charprop : (char -> bool) -> string -> string
+
(** Strip spaces from left and right of a string. *)
val strip_spaces : string -> string
-(** Printf helper functions. *)
-val list_fprint :
- (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
-val array_fprint :
- (out_channel -> 'a -> unit) -> out_channel -> 'a array -> unit
+(** Split a string on characters satisfying [f]. *)
+val split_charprop : ?keep_split_chars: bool ->
+ (char -> bool) -> string -> string list
+
+(** Split a string on spaces. *)
+val split_spaces : string -> string list
-(** Print an unboxed separated list, with breaks after the separator. *)
-val fprint_sep_list :
- ?newline : int -> string -> (Format.formatter -> 'a -> unit) ->
- Format.formatter -> 'a list -> unit
+(** Split a string on newlines (\n or \r). *)
+val split_newlines : string -> string list
+(** Split a string on empty lines (\n\n). *)
+val split_empty_lines : string -> string list
-(** Replacements for basic Str functions. *)
+(** Replace all white space sequences by a simple space, strip on both ends. *)
+val normalize_spaces : string -> string
-(** [split_regexp ~regexp:r s] splits [s] into substrings, taking as
- delimiters the substrings that match [r], and returns the list of
- substrings. For instance, [split ~regexp:"[ \t]+" s] splits [s]
- into blank-separated words. An occurrence of the delimiter at the
- beginning and at the end of the string is ignored. *)
-val split_regexp : regexp:string -> string -> string list
+(** Replace characters satisfying [f] by [repl]. *)
+val replace_charprop : (char -> bool) -> string -> string -> string
-(** [replace_regexp ~regexp ~templ s] returns a string identical to [s],
- except that all substrings of [s] that match [regexp] have been
- replaced by [templ]. *)
-val replace_regexp : regexp:string -> templ:string -> string -> string
+(** Index of the first occurence of the first argument in the second one.
+ Only positions after [from] count. If it does not occur, raise Not_found. *)
+val str_index : ?from : int -> string -> string -> int
+
+(** Checks whether the first argument contains in the second one. *)
+val str_contains : string -> string -> bool
+
+(** Substitute the first ocurrence of the first argument by the second one. *)
+val str_subst_once : string -> string -> string -> string
+
+(** Substitute all ocurrences of the first argument by the second one. *)
+val str_subst_all : string -> string -> string -> string
+
+(** Substitute the first ocurrence of the interval between
+ the first argument and the second one by the third one. *)
+val str_subst_once_from_to : string -> string -> string -> string -> string
+
+(** Substitute all ocurrences of the interval between
+ the first argument and the second one by the third one.
+ E.g. (str_subst_all_from_to "/*" "*/" "") removes C-style comments. *)
+val str_subst_all_from_to : string -> string -> string -> string -> string
Modified: trunk/Toss/Formula/AuxIO.ml
===================================================================
--- trunk/Toss/Formula/AuxIO.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/AuxIO.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -220,6 +220,15 @@
print_string s; flush stdout
) ENDIF
+let printf fmt = Printf.ksprintf print fmt
+
+let print_err s =
+ IFDEF JAVASCRIPT THEN (
+ if is_worker then worker_log ("ERROR: "^ s) else console_log ("ERROR: "^ s)
+ ) ELSE (
+ prerr_string s; flush stderr
+ ) ENDIF
+
let sprint_of_fprint fprint_fun x =
ignore (Format.flush_str_formatter ());
Format.fprintf Format.str_formatter "@[%a@]" fprint_fun x;
@@ -229,7 +238,7 @@
IFDEF JAVASCRIPT THEN (
print (sprint_of_fprint fprint_fun x)
) ELSE (
- fprint_fun Format.std_formatter x
+ fprint_fun Format.std_formatter x; Format.print_flush ()
) ENDIF
let log module_name debug_lev s =
Modified: trunk/Toss/Formula/AuxIO.mli
===================================================================
--- trunk/Toss/Formula/AuxIO.mli 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/AuxIO.mli 2012-03-07 03:56:13 UTC (rev 1683)
@@ -66,6 +66,12 @@
(** Printing for JS and native. *)
val print : string -> unit
+(** Printf.printf for JS and native. *)
+val printf : ('a, unit, string, unit) format4 -> 'a
+
+(** Printing to stderr for JS and native. *)
+val print_err : string -> unit
+
(** Given formatter printing function, creates a to-string printing function. *)
val sprint_of_fprint : (Format.formatter -> 'a -> unit) -> 'a -> string
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/BoolFormula.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -476,7 +476,7 @@
(fun clause ->
(* actually these clauses do not necessarily contain only
literals but maybe also more complex subformulas! *)
- let lits = (*print_endline("checking clause: " ^ str clause); *)
+ let lits =
match clause with
| BOr lits -> lits
| BVar v as lit -> [lit]
@@ -696,12 +696,12 @@
let try_dnf ?(disc_vars=[]) tm phi =
match to_dnf ~disc_vars ~tm phi with None -> phi | Some psi -> psi
-let univ ?(dbg=0) v phi =
- if dbg > 0 then Printf.printf "Univ subst in %s\n%!" (str phi);
+let univ ?(dbg=0) v phi =
+ if dbg > 0 then AuxIO.printf "Univ subst in %s\n%!" (str phi);
let simp1 = subst_simp [v] phi in
- if dbg > 0 then Printf.printf "Univ subst POS: %s\n%!" (str simp1);
+ if dbg > 0 then AuxIO.printf "Univ subst POS: %s\n%!" (str simp1);
let simp2 = subst_simp [-v] phi in
- if dbg > 0 then Printf.printf "Univ subst NEG: %s\n%!" (str simp2);
+ if dbg > 0 then AuxIO.printf "Univ subst NEG: %s\n%!" (str simp2);
BAnd [simp1; simp2]
Modified: trunk/Toss/Formula/BoolFormulaTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFormulaTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/BoolFormulaTest.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -417,7 +417,7 @@
Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";
if !file = "" then ( exec (); execbig (); ) else (
let qbf = read_qdimacs (AuxIO.input_file !file) in
- print_endline (BoolFormula.str (elim_quant qbf))
+ AuxIO.print ((BoolFormula.str (elim_quant qbf)) ^ "\n")
)
let _ = AuxIO.run_if_target "BoolFormulaTest" main
Modified: trunk/Toss/Formula/BoolFunction.ml
===================================================================
--- trunk/Toss/Formula/BoolFunction.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/BoolFunction.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -51,24 +51,8 @@
Format.fprintf f "@[<1>(exists@ %a.@ %a)@]"
fprint_mod_var_list mod_vars fprint phi
-(* Print to stdout, template from formatter printing. *)
-let make_print fprint_fun x = (
- Format.print_flush();
- fprint_fun Format.std_formatter x;
- Format.print_flush();
-)
-
-(* Print to string, template from formatter printing. *)
-let make_sprint fprint_fun x =
- ignore (Format.flush_str_formatter ());
- Format.fprintf Format.str_formatter "@[%a@]" fprint_fun x;
- Format.flush_str_formatter ()
-
-(* Print to stdout. *)
-let print = make_print fprint
-(* Print to string. *)
-let sprint = make_sprint fprint
-(* Another name for sprint. *)
+let print x = AuxIO.print_of_fprint fprint x
+let sprint x = AuxIO.sprint_of_fprint fprint x
let str = sprint
(* Print definition to formatter. *)
@@ -88,11 +72,10 @@
Format.fprintf f "@[<1>%s(%a)@ (%a)@]" name
fprint_mod_var_list mod_vars fprint def
-(* Print definition to stdout. *)
-let print_def ?(print_bool=false) = make_print (fprint_def ~print_bool)
-(* Print definition to string. *)
-let sprint_def ?(print_bool=false) = make_sprint (fprint_def ~print_bool)
-(* Another name for sprint_def. *)
+let print_def ?(print_bool=false) x =
+ AuxIO.print_of_fprint (fprint_def ~print_bool) x
+let sprint_def ?(print_bool=false) x =
+ AuxIO.sprint_of_fprint (fprint_def ~print_bool) x
let str_def = sprint_def
(* Print class and definition list to formatter. *)
@@ -115,11 +98,10 @@
Format.fprintf f "@[<1> %a;@]"
(Aux.fprint_sep_list ~newline:2 ";" (fprint_def ~print_bool)) dl
-(* Print definitions to stdout. *)
-let print_defs ?(print_bool=false) = make_print (fprint_defs ~print_bool)
-(* Print definitions to string. *)
-let sprint_defs ?(print_bool=false) = make_sprint (fprint_defs ~print_bool)
-(* Another name for sprint_defs. *)
+let print_defs ?(print_bool=false) x =
+ AuxIO.print_of_fprint (fprint_defs ~print_bool) x
+let sprint_defs ?(print_bool=false) x =
+ AuxIO.sprint_of_fprint (fprint_defs ~print_bool) x
let str_defs = sprint_defs
@@ -319,7 +301,7 @@
let nonf ?(tm=1200.) = apply_bool_elim (fun x -> Some (simplify x)) "ELIM"
(* Solve fixed-points in the definitions. *)
-let solve_lfp ?(nf=0) cls all_defs =
+let solve_lfp ?(nf=2) cls all_defs =
let (deffp, defsimp) =
List.partition (fun (_, fp, _, _) -> fp) (inline_defs all_defs) in
let defs = List.map (fun (_, _, _, f) -> f) deffp in
Modified: trunk/Toss/Formula/BoolFunction.mli
===================================================================
--- trunk/Toss/Formula/BoolFunction.mli 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/BoolFunction.mli 2012-03-07 03:56:13 UTC (rev 1683)
@@ -19,7 +19,7 @@
(** {2 Printing Functions} *)
-(** Print to stdout. *)
+(** Print. *)
val print : bool_function -> unit
(** Print to string. *)
val sprint : bool_function -> string
@@ -28,7 +28,7 @@
(** Print to formatter. *)
val fprint : Format.formatter -> bool_function -> unit
-(** Print definition to stdout. *)
+(** Print definition. *)
val print_def : ?print_bool : bool -> bool_def -> unit
(** Print definition to string. *)
val sprint_def : ?print_bool : bool -> bool_def -> string
@@ -38,7 +38,7 @@
val fprint_def : ?print_bool : bool -> Format.formatter -> bool_def -> unit
-(** Print definitions to stdout. *)
+(** Print definitions. *)
val print_defs : ?print_bool : bool ->
(string * string list) list * bool_def list -> unit
(** Print definitions to string. *)
Modified: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml 2012-03-05 23:24:41 UTC (rev 1682)
+++ trunk/Toss/Formula/BoolFunctionTest.ml 2012-03-07 03:56:13 UTC (rev 1683)
@@ -17,6 +17,34 @@
assert_equal ~printer:(fun x -> x) ~msg:full_msg
("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
+let solve_mu_file ?(only_inline=false) ?(prbools=false) ?(debug=0) ?(nf=2) fs =
+ let lines = List.map Aux.strip_spaces (Aux.split_newlines fs) in
+ let ignore_line l =
+ let ll = String.length l in
+ (ll = 0) || l.[0] = '#' || (ll > 2 && (l.[0] = '/' && l.[1] = '/')) ||
+ (Aux.str_contains l "~+") || (Aux.str_contains l "<") in
+ let lines = List.filter (fun l -> not (ignore_line l)) lines in
+ let clean_line l =
+ Aux.str_subst_all_from_to "/*" "*/" "" (Aux.str_subst_all "bool" "" l) in
+ let res_s = String.concat "\n" (List.map clean_line lines) in
+ try
+ let (cl, dl, goal) = defs_goal_of_string res_s in
+ let new_defs = if only_inline then (cl, inline_defs dl) else
+ (cl, solve_lfp ~nf cl dl) in
+ let inline_goal = triv_simp (apply_defs (snd new_defs) goal) in
+ if only_inline || debug > 0 then print_defs ~print_bool:prbools new_defs;
+ if only_inline then inline_goal else Aux.unsome (dnf cl inline_goal)
+ with Lexer.Parsing_error err -> (
+ AuxIO.print (res_s ^ "\n");
+ let msg_raw = String.sub err 9 ((String.length err)-9) in
+ let msg = String.concat "\n// " (Aux.split_newlines msg_raw) in
+ failwith ("// ERROR: NOT PARSED\n//\n// " ^ msg ^ "\n\n")
+ )
+
+let test_mu_file s res =
+ assert_equal ~printer:(fun x -> x) (str (solve_mu_file s)) res
+
+
let tests = "BoolFunction" >::: [
"parsing and printing" >::
(fun () ->
@@ -100,58 +128,2717 @@
test_inline_defs "R(M m) (m.a1=0); Q(M m) (m.a0=0 & R(m))"
"R(M m) (m.a1=0); Q(M m) ((m.a0=0 & m.a1=0));"
);
+
+ "mu files solving" >::
+ (fun () ->
+ let p_one_mu = "
+class Module {
+bool a1;
+bool a2;
+bool a3;
+};
+
+class PrCount {
+bool b1;
+bool b2;
+bool b3;
+bool b4;
+};
+
+class Global { bool fake; };
+
+class Local { bool fake; };
+
+bool CopyLocals(
+Module m,
+Local c,
+Local d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+);
+#size CopyLocals;
+
+
+
+bool CopyGlobals(
+Module m,
+Global c,
+Global d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+);
+
+#size CopyGlobals;
+
+
+
+bool initPC( PrCount pc)(
+true
+& !pc.b1
+& !pc.b2
+& !pc.b3
+& !pc.b4
+);
+
+bool initMOD( Module mod)(
+true
+& !mod.a1
+& !mod.a2
+& !mod.a3
+);
+
+bool programInt1(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt1;
+
+
+bool programInt2(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Global G
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L < G
+(false
+| ((cm.a1=0 & cm.a2=0 & cm.a3=0)&
+((false
+|( /* IF */
+ (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0) & ((dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0)|(dp.b1=1 & dp.b2=0 & dp.b3=1 & dp.b4=0))
+)|(
+ /* SKIP */
+ (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0)
+&(dp.b1=0 & dp.b2=0 & dp.b3=1 & dp.b4=0))|(
+ /* ASSUME ASSERT 1 */
+(cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0)
+&(dp.b1=1 & dp.b2=1 & dp.b3=0 & dp.b4=0)&false
+
+))))
+);
+
+#size programInt2;
+
+
+bool programInt3(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt3;
+
+
+bool CopyVariables_ProgramInt(
+ Module m,
+ PrCount p,
+ Local cL,
+ Local dL,
+ Global cG,
+ Global dG
+)
+ m < p,
+ p < cL,
+ cL ~+ dL,
+ cL < cG,
+ cG ~+ dG
+(false
+| (true
+));
+
+#size CopyVariables_ProgramInt;
+
+
+bool programCall(
+ Module cm,
+ Module dm,
+ PrCount cp,
+ Local cL,
+ Local dL,
+ Global cG
+)
+ cm ~+ dm,
+ cm < cp,
+ cp < cL,
+ cL ~+ dL,
+ cL < cG
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)&(dm.a1=0 & dm.a2=1 & dm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)
+);
+
+#size programCall;
+
+
+
+bool Calling(Module m, PrCount p)
+(false
+| ((m.a1=0 & m.a2=0 & m.a3=0) & (p.b1=0 & p.b2=0 & p.b3=0 & p.b4=0))
+);
+
+#size Calling;
+
+
+
+ bool Exit( Module cm, PrCount cp )
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|((cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=1 & cp.b4=0))
+|((cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=1 & cp.b4=0))
+);
+
+#size Exit;
+
+
+
+bool SetReturnUS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local uL,
+ Local sL,
+ Global uG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < uL,
+ uL ~+ sL,
+ uL < uG,
+ uG ~+ sG
+((false
+|(
+ (um.a1=0 & um.a2=1 & um.a3=0)& (up.b1=0 & up.b2=0 & up.b3=0 & up.b4=0)
+ & (false
+ |((tm.a1=0 & tm.a2=0 & tm.a3=0)& (tp.b1=0 & tp.b2=0 & tp.b3=0 & tp.b4=0)
+ )
+ )
+)
+));
+
+
+
+#size SetReturnUS;
+
+
+
+bool SetReturnTS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local tL,
+ Local sL,
+ Global tG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < tL,
+ tL ~+ sL,
+ tL < tG,
+ tG ~+ sG
+(false
+| (true
+));
+
+#size SetReturnTS;
+
+
+
+bool enforce(
+ Module m,
+ Local L,
+ Global G
+)
+ m < L,
+ L < G
+(false
+ | ( (m.a1=0 & m.a2=0 & m.a3=0) & ( true ) )
+ | ( (m.a1=0 & m.a2=1 & m.a3=0) & ( true ) )
+
+);
+
+
+#size enforce;
+
+
+
+bool SkipCall(
+ Module cm,
+ PrCount cp,
+ PrCount dp
+)
+cm < cp,
+dp ~+ dp
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)&(dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0))
+
+);
+
+
+#size SkipCall;
+
+
+
+bool target(Module cm, PrCount cp) ( (cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0));mu bool Reachable(
+ Module s_mod,
+ PrCount s_pc,
+ Local s_CL,
+ Global s_CG,
+ Local s_ENTRY_CL,
+ Global s_ENTRY_CG
+)
+s_mod < s_pc,
+s_pc < s_CL,
+s_CL ~+ s_ENTRY_CL,
+s_CL < s_CG,
+s_CG ~+ s_ENTRY_CG
+(
+ false
+
+ // early termination
+
+ | ( exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( target(t_mod,t_pc) &
+ Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG)
+ )
+ )
+
+|(enforce(s_mod, s_CL, s_CG) &
+
+ (
+ // initial conf
+ ( initMOD(s_mod) & initPC(s_pc) )
+
+
+ // forward propagation on call transitions
+ | ( initPC(s_pc) & CopyLocals(s_mod,s_ENTRY_CL,s_CL)
+ & (exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( (Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG) & CopyGlobals(s_mod,t_CG,s_CG) )
+ & CopyGlobals(s_mod, t_CG, s_ENTRY_CG)
+ & programCall(t_mod,s_mod,t_pc,t_CL,s_CL,t_CG)
+ ) ) )
+
+
+ // forward propagation on internal transitions on current set (not just the frontier from prev round)
+ | (exists PrCount t_pc, Local t_CL, Global t_CG.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ &(
+ ( programInt1(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ & CopyVariables_ProgramInt(s_mod,t_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ | programInt3(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ )
+ )
+
+ | (exists PrCount t_pc.
+ ( (Reachable(s_mod,t_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ & programInt2(s_mod,t_pc,s_pc,s_CL,s_CG)
+ )
+ )
+
+
+
+
+
+ // forward propagation on SkipCall (jump from exit to return)
+ | (exists PrCount t_pc, Global t_CG, Module u_mod, PrCount u_pc, Local u_ENTRY_CL.
+ ( exists Local t_CL.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) // t is reachable
+ & SkipCall(s_mod,t_pc,s_pc))
+ & programCall(s_mod,u_mod,t_pc,t_CL,u_ENTRY_CL,t_CG)
+ & SetReturnTS(s_mod,u_mod,t_pc,u_pc,t_CL,s_CL,t_CG,s_CG)
+ ))
+ &
+ ( exists Local u_CL, Global u_CG.
+ (
+ (Reachable(u_mod,u_pc,u_CL,u_CG,u_ENTRY_CL,t_CG) // u is reachable
+ & Exit(u_mod,u_pc)) // u is an exit
+ & SetReturnUS(s_mod,u_mod,t_pc,u_pc,u_CL,s_CL,u_CG,s_CG)
+ )
+ )
+ )
+
+
+ ))
+);
+
+/****************************************************************************/
+// Reachableability formula
+/***************************************************************************/
+
+( exists Module s_mod, PrCount s_pc, Local s_CL, Global s_CG, Local s_ENTRY_CL, Global s_ENTRY_CG.
+ ( target(s_mod,s_pc) &
+ Reachable(s_mod,s_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG)
+ )
+);" in
+ test_mu_file p_one_mu "false";
+
+ let p_ntest61_mu =
+"
+class Module {
+bool a1;
+bool a2;
+bool a3;
+};
+
+class PrCount {
+bool b1;
+bool b2;
+bool b3;
+bool b4;
+};
+
+class Global { bool fake; };
+
+class Local { bool fake; };
+
+bool CopyLocals(
+Module m,
+Local c,
+Local d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+);
+#size CopyLocals;
+
+
+
+bool CopyGlobals(
+Module m,
+Global c,
+Global d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+);
+
+#size CopyGlobals;
+
+
+
+bool initPC( PrCount pc)(
+true
+& !pc.b1
+& !pc.b2
+& !pc.b3
+& !pc.b4
+);
+
+bool initMOD( Module mod)(
+true
+& !mod.a1
+& !mod.a2
+& !mod.a3
+);
+
+bool programInt1(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt1;
+
+
+bool programInt2(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Global G
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L < G
+(false
+| ((cm.a1=0 & cm.a2=0 & cm.a3=0)&
+((false
+|( /* IF */
+ (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0) & ((dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0)|(dp.b1=1 & dp.b2=1 & dp.b3=0 & dp.b4=0))
+)|(
+ /* SKIP */
+ (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0)
+&(dp.b1=1 & dp.b2=1 & dp.b3=0 & dp.b4=0)))))
+);
+
+#size programInt2;
+
+
+bool programInt3(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt3;
+
+
+bool CopyVariables_ProgramInt(
+ Module m,
+ PrCount p,
+ Local cL,
+ Local dL,
+ Global cG,
+ Global dG
+)
+ m < p,
+ p < cL,
+ cL ~+ dL,
+ cL < cG,
+ cG ~+ dG
+(false
+| (true
+));
+
+#size CopyVariables_ProgramInt;
+
+
+bool programCall(
+ Module cm,
+ Module dm,
+ PrCount cp,
+ Local cL,
+ Local dL,
+ Global cG
+)
+ cm ~+ dm,
+ cm < cp,
+ cp < cL,
+ cL ~+ dL,
+ cL < cG
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)&(dm.a1=0 & dm.a2=1 & dm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)
+);
+
+#size programCall;
+
+
+
+bool Calling(Module m, PrCount p)
+(false
+| ((m.a1=0 & m.a2=0 & m.a3=0) & (p.b1=0 & p.b2=0 & p.b3=0 & p.b4=0))
+);
+
+#size Calling;
+
+
+
+ bool Exit( Module cm, PrCount cp )
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|((cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+);
+
+#size Exit;
+
+
+
+bool SetReturnUS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local uL,
+ Local sL,
+ Global uG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < uL,
+ uL ~+ sL,
+ uL < uG,
+ uG ~+ sG
+((false
+|(
+ (um.a1=0 & um.a2=1 & um.a3=0)& (up.b1=0 & up.b2=0 & up.b3=0 & up.b4=0)
+ & (false
+ |((tm.a1=0 & tm.a2=0 & tm.a3=0)& (tp.b1=0 & tp.b2=0 & tp.b3=0 & tp.b4=0)
+ )
+ )
+)
+));
+
+
+
+#size SetReturnUS;
+
+
+
+bool SetReturnTS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local tL,
+ Local sL,
+ Global tG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < tL,
+ tL ~+ sL,
+ tL < tG,
+ tG ~+ sG
+(false
+| (true
+));
+
+#size SetReturnTS;
+
+
+
+bool enforce(
+ Module m,
+ Local L,
+ Global G
+)
+ m < L,
+ L < G
+(false
+ | ( (m.a1=0 & m.a2=0 & m.a3=0) & ( true ) )
+ | ( (m.a1=0 & m.a2=1 & m.a3=0) & ( true ) )
+
+);
+
+
+#size enforce;
+
+
+
+bool SkipCall(
+ Module cm,
+ PrCount cp,
+ PrCount dp
+)
+cm < cp,
+dp ~+ dp
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)&(dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0))
+
+);
+
+
+#size SkipCall;
+
+
+
+bool target(Module cm, PrCount cp) ( (cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0));mu bool Reachable(
+ Module s_mod,
+ PrCount s_pc,
+ Local s_CL,
+ Global s_CG,
+ Local s_ENTRY_CL,
+ Global s_ENTRY_CG
+)
+s_mod < s_pc,
+s_pc < s_CL,
+s_CL ~+ s_ENTRY_CL,
+s_CL < s_CG,
+s_CG ~+ s_ENTRY_CG
+(
+ false
+
+ // early termination
+
+ | ( exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( target(t_mod,t_pc) &
+ Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG)
+ )
+ )
+
+|(enforce(s_mod, s_CL, s_CG) &
+
+ (
+ // initial conf
+ ( initMOD(s_mod) & initPC(s_pc) )
+
+
+ // forward propagation on call transitions
+ | ( initPC(s_pc) & CopyLocals(s_mod,s_ENTRY_CL,s_CL)
+ & (exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( (Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG) & CopyGlobals(s_mod,t_CG,s_CG) )
+ & CopyGlobals(s_mod, t_CG, s_ENTRY_CG)
+ & programCall(t_mod,s_mod,t_pc,t_CL,s_CL,t_CG)
+ ) ) )
+
+
+ // forward propagation on internal transitions on current set (not just the frontier from prev round)
+ | (exists PrCount t_pc, Local t_CL, Global t_CG.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ &(
+ ( programInt1(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ & CopyVariables_ProgramInt(s_mod,t_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ | programInt3(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ )
+ )
+
+ | (exists PrCount t_pc.
+ ( (Reachable(s_mod,t_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ & programInt2(s_mod,t_pc,s_pc,s_CL,s_CG)
+ )
+ )
+
+
+
+
+
+ // forward propagation on SkipCall (jump from exit to return)
+ | (exists PrCount t_pc, Global t_CG, Module u_mod, PrCount u_pc, Local u_ENTRY_CL.
+ ( exists Local t_CL.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) // t is reachable
+ & SkipCall(s_mod,t_pc,s_pc))
+ & programCall(s_mod,u_mod,t_pc,t_CL,u_ENTRY_CL,t_CG)
+ & SetReturnTS(s_mod,u_mod,t_pc,u_pc,t_CL,s_CL,t_CG,s_CG)
+ ))
+ &
+ ( exists Local u_CL, Global u_CG.
+ (
+ (Reachable(u_mod,u_pc,u_CL,u_CG,u_ENTRY_CL,t_CG) // u is reachable
+ & Exit(u_mod,u_pc)) // u is an exit
+ & SetReturnUS(s_mod,u_mod,t_pc,u_pc,u_CL,s_CL,u_CG,s_CG)
+ )
+ )
+ )
+
+
+ ))
+);
+
+/*****************************************************************************/
+// Reachableability formula
+/****************************************************************************/
+
+( exists Module s_mod, PrCount s_pc, Local s_CL, Global s_CG, Local s_ENTRY_CL, Global s_ENTRY_CG.
+ ( target(s_mod,s_pc) &
+ Reachable(s_mod,s_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG)
+ )
+);
+" in
+ test_mu_file p_ntest61_mu "true";
+ );
]
+let bigtests = "BoolFunctionBig" >::: [
+ "mu file: param1" >::
+ (fun () ->
+ let p_param1_mu ="
+class Module {
+bool a1;
+bool a2;
+bool a3;
+};
+
+class PrCount {
+bool b1;
+bool b2;
+bool b3;
+bool b4;
+};
+
+class Global { bool fake; };
+
+class Local { bool fake; };
+
+bool CopyLocals(
+Module m,
+Local c,
+Local d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+ |((m.a1=1 & m.a2=1 & m.a3=0))
+);
+#size CopyLocals;
+
+
+
+bool CopyGlobals(
+Module m,
+Global c,
+Global d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=0 & m.a2=0 & m.a3=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0))
+ |((m.a1=1 & m.a2=1 & m.a3=0))
+);
+
+#size CopyGlobals;
+
+
+
+bool initPC( PrCount pc)(
+true
+& !pc.b1
+& !pc.b2
+& !pc.b3
+& !pc.b4
+);
+
+bool initMOD( Module mod)(
+true
+& !mod.a1
+& !mod.a2
+& !mod.a3
+);
+
+bool programInt1(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt1;
+
+
+bool programInt2(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Global G
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L < G
+(false
+| ((cm.a1=0 & cm.a2=1 & cm.a3=0)&
+((false
+|( /* IF */
+ (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0) & ((dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0)|(dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0))
+)|(
+ /* SKIP */
+ (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+&(dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0)))))
+);
+
+#size programInt2;
+
+
+bool programInt3(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt3;
+
+
+bool CopyVariables_ProgramInt(
+ Module m,
+ PrCount p,
+ Local cL,
+ Local dL,
+ Global cG,
+ Global dG
+)
+ m < p,
+ p < cL,
+ cL ~+ dL,
+ cL < cG,
+ cG ~+ dG
+(false
+| (true
+));
+
+#size CopyVariables_ProgramInt;
+
+
+bool programCall(
+ Module cm,
+ Module dm,
+ PrCount cp,
+ Local cL,
+ Local dL,
+ Global cG
+)
+ cm ~+ dm,
+ cm < cp,
+ cp < cL,
+ cL ~+ dL,
+ cL < cG
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)&(dm.a1=1 & dm.a2=1 & dm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)|((cm.a1=0 & cm.a2=0 & cm.a3=0)&(dm.a1=0 & dm.a2=1 & dm.a3=0)& (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)
+);
+
+#size programCall;
+
+
+
+bool Calling(Module m, PrCount p)
+(false
+| ((m.a1=0 & m.a2=0 & m.a3=0) & (p.b1=0 & p.b2=0 & p.b3=0 & p.b4=0))
+| ((m.a1=0 & m.a2=0 & m.a3=0) & (p.b1=1 & p.b2=0 & p.b3=0 & p.b4=0))
+);
+
+#size Calling;
+
+
+
+ bool Exit( Module cm, PrCount cp )
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=0 & cm.a3=0) & (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|((cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|((cm.a1=1 & cm.a2=1 & cm.a3=0) & (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=1 & cm.a2=1 & cm.a3=0) & (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+);
+
+#size Exit;
+
+
+
+bool SetReturnUS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local uL,
+ Local sL,
+ Global uG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < uL,
+ uL ~+ sL,
+ uL < uG,
+ uG ~+ sG
+((false
+|(
+ (um.a1=0 & um.a2=1 & um.a3=0)& (up.b1=0 & up.b2=1 & up.b3=0 & up.b4=0)
+ & (false
+ |((tm.a1=0 & tm.a2=0 & tm.a3=0)& (tp.b1=1 & tp.b2=0 & tp.b3=0 & tp.b4=0)
+ )
+ )
+)
+|(
+ (um.a1=1 & um.a2=1 & um.a3=0)& (up.b1=0 & up.b2=0 & up.b3=0 & up.b4=0)
+ & (false
+ |((tm.a1=0 & tm.a2=0 & tm.a3=0)& (tp.b1=0 & tp.b2=0 & tp.b3=0 & tp.b4=0)
+ )
+ )
+)
+));
+
+
+
+#size SetReturnUS;
+
+
+
+bool SetReturnTS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local tL,
+ Local sL,
+ Global tG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < tL,
+ tL ~+ sL,
+ tL < tG,
+ tG ~+ sG
+(false
+| (true
+));
+
+#size SetReturnTS;
+
+
+
+bool enforce(
+ Module m,
+ Local L,
+ Global G
+)
+ m < L,
+ L < G
+(false
+ | ( (m.a1=0 & m.a2=0 & m.a3=0) & ( true ) )
+ | ( (m.a1=0 & m.a2=1 & m.a3=0) & ( true ) )
+ | ( (m.a1=1 & m.a2=1 & m.a3=0) & ( true ) )
+
+);
+
+
+#size enforce;
+
+
+
+bool SkipCall(
+ Module cm,
+ PrCount cp,
+ PrCount dp
+)
+cm < cp,
+dp ~+ dp
+(false
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)&(dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0))
+|((cm.a1=0 & cm.a2=0 & cm.a3=0)& (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0)&(dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0))
+
+);
+
+
+#size SkipCall;
+
+
+
+bool target(Module cm, PrCount cp) ( (cm.a1=0 & cm.a2=1 & cm.a3=0) & (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0));mu bool Reachable(
+ Module s_mod,
+ PrCount s_pc,
+ Local s_CL,
+ Global s_CG,
+ Local s_ENTRY_CL,
+ Global s_ENTRY_CG
+)
+s_mod < s_pc,
+s_pc < s_CL,
+s_CL ~+ s_ENTRY_CL,
+s_CL < s_CG,
+s_CG ~+ s_ENTRY_CG
+(
+ false
+
+ // early termination
+
+ | ( exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( target(t_mod,t_pc) &
+ Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG)
+ )
+ )
+
+|(enforce(s_mod, s_CL, s_CG) &
+
+ (
+ // initial conf
+ ( initMOD(s_mod) & initPC(s_pc) )
+
+
+ // forward propagation on call transitions
+ | ( initPC(s_pc) & CopyLocals(s_mod,s_ENTRY_CL,s_CL)
+ & (exists Module t_mod, PrCount t_pc, Local t_CL, Global t_CG, Local t_ENTRY_CL, Global t_ENTRY_CG.
+ ( (Reachable(t_mod,t_pc,t_CL,t_CG,t_ENTRY_CL,t_ENTRY_CG) & CopyGlobals(s_mod,t_CG,s_CG) )
+ & CopyGlobals(s_mod, t_CG, s_ENTRY_CG)
+ & programCall(t_mod,s_mod,t_pc,t_CL,s_CL,t_CG)
+ ) ) )
+
+
+ // forward propagation on internal transitions on current set (not just the frontier from prev round)
+ | (exists PrCount t_pc, Local t_CL, Global t_CG.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ &(
+ ( programInt1(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ & CopyVariables_ProgramInt(s_mod,t_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ | programInt3(s_mod,t_pc,s_pc,t_CL,s_CL,t_CG,s_CG)
+ )
+ )
+ )
+
+ | (exists PrCount t_pc.
+ ( (Reachable(s_mod,t_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG) & !Calling(s_mod,t_pc))
+ & programInt2(s_mod,t_pc,s_pc,s_CL,s_CG)
+ )
+ )
+
+
+
+
+
+ // forward propagation on SkipCall (jump from exit to return)
+ | (exists PrCount t_pc, Global t_CG, Module u_mod, PrCount u_pc, Local u_ENTRY_CL.
+ ( exists Local t_CL.
+ ( (Reachable(s_mod,t_pc,t_CL,t_CG,s_ENTRY_CL,s_ENTRY_CG) // t is reachable
+ & SkipCall(s_mod,t_pc,s_pc))
+ & programCall(s_mod,u_mod,t_pc,t_CL,u_ENTRY_CL,t_CG)
+ & SetReturnTS(s_mod,u_mod,t_pc,u_pc,t_CL,s_CL,t_CG,s_CG)
+ ))
+ &
+ ( exists Local u_CL, Global u_CG.
+ (
+ (Reachable(u_mod,u_pc,u_CL,u_CG,u_ENTRY_CL,t_CG) // u is reachable
+ & Exit(u_mod,u_pc)) // u is an exit
+ & SetReturnUS(s_mod,u_mod,t_pc,u_pc,u_CL,s_CL,u_CG,s_CG)
+ )
+ )
+ )
+
+
+ ))
+);
+
+/*****************************************************************************/
+// Reachableability formula
+/*****************************************************************************/
+
+( exists Module s_mod, PrCount s_pc, Local s_CL, Global s_CG, Local s_ENTRY_CL, Global s_ENTRY_CG.
+ ( target(s_mod,s_pc) &
+ Reachable(s_mod,s_pc,s_CL,s_CG,s_ENTRY_CL,s_ENTRY_CG)
+ )
+);
+" in
+ test_mu_file p_param1_mu "true";
+ );
+ "mu file: value-return" >::
+ (fun () ->
+ let p_value_return_mu = "
+class Module {
+bool a1;
+bool a2;
+bool a3;
+bool a4;
+};
+
+class PrCount {
+bool b1;
+bool b2;
+bool b3;
+bool b4;
+};
+
+class Global { bool fake; };
+
+class Local { bool fake; };
+
+bool CopyLocals(
+Module m,
+Local c,
+Local d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=1 & m.a2=0 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=0 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=0 & m.a3=1 & m.a4=0))
+ |((m.a1=1 & m.a2=0 & m.a3=1 & m.a4=0))
+);
+#size CopyLocals;
+
+
+
+bool CopyGlobals(
+Module m,
+Global c,
+Global d
+)
+m < c,
+c ~+ d
+(false
+ |((m.a1=1 & m.a2=0 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=1 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=0 & m.a3=0 & m.a4=0))
+ |((m.a1=0 & m.a2=0 & m.a3=1 & m.a4=0))
+ |((m.a1=1 & m.a2=0 & m.a3=1 & m.a4=0))
+);
+
+#size CopyGlobals;
+
+
+
+bool initPC( PrCount pc)(
+true
+& !pc.b1
+& !pc.b2
+& !pc.b3
+& !pc.b4
+);
+
+bool initMOD( Module mod)(
+true
+& !mod.a1
+& !mod.a2
+& !mod.a3
+& !mod.a4
+);
+
+bool programInt1(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt1;
+
+
+bool programInt2(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Global G
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L < G
+(false
+| ((cm.a1=1 & cm.a2=0 & cm.a3=0 & cm.a4=0)&
+((false
+|( /* IF */
+ (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0) & ((dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0)|(dp.b1=0 & dp.b2=1 & dp.b3=0 & dp.b4=0))
+))))
+| ((cm.a1=0 & cm.a2=1 & cm.a3=0 & cm.a4=0)&
+((false
+|(
+ /* SKIP */
+ (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+&(dp.b1=1 & dp.b2=0 & dp.b3=0 & dp.b4=0)))))
+| ((cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0)&
+((false
+|( /* IF */
+ (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0) & ((dp.b1=1 & dp.b2=1 & dp.b3=0 & dp.b4=0)|(dp.b1=0 & dp.b2=0 & dp.b3=1 & dp.b4=0))
+))))
+);
+
+#size programInt2;
+
+
+bool programInt3(
+ Module cm,
+ PrCount cp,
+ PrCount dp,
+ Local L,
+ Local dL,
+ Global G,
+ Global dG
+)
+ cm < cp,
+ cp ~+ dp,
+ cp < L,
+ L ~+ dL,
+ L < G,
+ G ~+ dG
+(false
+);
+
+#size programInt3;
+
+
+bool CopyVariables_ProgramInt(
+ Module m,
+ PrCount p,
+ Local cL,
+ Local dL,
+ Global cG,
+ Global dG
+)
+ m < p,
+ p < cL,
+ cL ~+ dL,
+ cL < cG,
+ cG ~+ dG
+(false
+| (true
+));
+
+#size CopyVariables_ProgramInt;
+
+
+bool programCall(
+ Module cm,
+ Module dm,
+ PrCount cp,
+ Local cL,
+ Local dL,
+ Global cG
+)
+ cm ~+ dm,
+ cm < cp,
+ cp < cL,
+ cL ~+ dL,
+ cL < cG
+(false
+|((cm.a1=1 & cm.a2=0 & cm.a3=0 & cm.a4=0)&(dm.a1=0 & dm.a2=1 & dm.a3=0 & dm.a4=0)& (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)|((cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0)&(dm.a1=1 & dm.a2=0 & dm.a3=1 & dm.a4=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)|((cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0)&(dm.a1=0 & dm.a2=0 & dm.a3=1 & dm.a4=0)& (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)|((cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0)&(dm.a1=0 & dm.a2=1 & dm.a3=0 & dm.a4=0)& (cp.b1=1 & cp.b2=1 & cp.b3=0 & cp.b4=0)
+)|((cm.a1=0 & cm.a2=0 & cm.a3=1 & cm.a4=0)&(dm.a1=1 & dm.a2=0 & dm.a3=0 & dm.a4=0)& (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0)
+)
+);
+
+#size programCall;
+
+
+
+bool Calling(Module m, PrCount p)
+(false
+| ((m.a1=1 & m.a2=0 & m.a3=0 & m.a4=0) & (p.b1=1 & p.b2=0 & p.b3=0 & p.b4=0))
+| ((m.a1=0 & m.a2=0 & m.a3=0 & m.a4=0) & (p.b1=0 & p.b2=0 & p.b3=0 & p.b4=0))
+| ((m.a1=0 & m.a2=0 & m.a3=0 & m.a4=0) & (p.b1=1 & p.b2=0 & p.b3=0 & p.b4=0))
+| ((m.a1=0 & m.a2=0 & m.a3=0 & m.a4=0) & (p.b1=1 & p.b2=1 & p.b3=0 & p.b4=0))
+| ((m.a1=0 & m.a2=0 & m.a3=1 & m.a4=0) & (p.b1=0 & p.b2=0 & p.b3=0 & p.b4=0))
+);
+
+#size Calling;
+
+
+
+ bool Exit( Module cm, PrCount cp )
+(false
+|((cm.a1=1 & cm.a2=0 & cm.a3=0 & cm.a4=0) & (cp.b1=0 & cp.b2=1 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=1 & cm.a2=0 & cm.a3=0 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|((cm.a1=0 & cm.a2=1 & cm.a3=0 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=1 & cm.a3=0 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|((cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0) & (cp.b1=0 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=0 & cm.a3=0 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|((cm.a1=0 & cm.a2=0 & cm.a3=1 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=0 & cm.a2=0 & cm.a3=1 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+|((cm.a1=1 & cm.a2=0 & cm.a3=1 & cm.a4=0) & (cp.b1=0 & cp.b2=0 & cp.b3=0 & cp.b4=0))
+|( (cm.a1=1 & cm.a2=0 & cm.a3=1 & cm.a4=0) & (cp.b1=1 & cp.b2=0 & cp.b3=1 & cp.b4=0))
+);
+
+#size Exit;
+
+
+
+bool SetReturnUS(
+ Module tm,
+ Module um,
+ PrCount tp,
+ PrCount up,
+ Local uL,
+ Local sL,
+ Global uG,
+ Global sG
+)
+ tm ~+ um,
+ tm < tp,
+ tp ~+ up,
+ tp < uL,
+ uL ~+ sL,
+ uL < uG,
+ uG ~+ sG
+((false
+|(
+ (um.a1=1 & um.a2=0 & um.a3=0 & um.a4=0)& (up.b1=0 & up.b2=1 & up.b3=0 & up.b4=0)
+ & (false
+ |((tm.a1=0 & tm.a2=0 & tm.a3=1 & tm.a4=0)& (tp.b1=0 & tp...
[truncated message content] |
