[Toss-devel-svn] SF.net SVN: toss:[1231] trunk/Toss

[<luk...@us...>]

Revision: 1231
          http://toss.svn.sourceforge.net/toss/?rev=1231&view=rev
Author:   lukaszkaiser
Date:     2010-12-07 00:26:40 +0000 (Tue, 07 Dec 2010)

Log Message:
-----------
Correct bounce, add debugging info.

Modified Paths:
--------------
    trunk/Toss/Arena/ContinuousRule.ml
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/examples/bounce.toss

Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml	2010-12-06 22:12:51 UTC (rev 1230)
+++ trunk/Toss/Arena/ContinuousRule.ml	2010-12-07 00:26:40 UTC (rev 1231)
@@ -4,7 +4,9 @@
 let get_time_step () = !time_step
 let set_time_step x = (time_step := x)
 
+let debug_level = ref 0;
 
+
 (* ---------------- BASIC TYPE DEFINITION AND CONSTRUCTOR ------------------- *)
 
 (* Specification of a continuous rewriting rule, as in modelling document. *)
@@ -82,6 +84,7 @@
 (* For now, we rewrite only single rules. Does not check postcondition. *)
 let rewrite_single_nocheck struc cur_time m r t params =
   let time = ref cur_time in
+  if !debug_level > 1 then print_endline ("ct: " ^ (string_of_float !time));
   let left_elname le =
     Structure.elem_str r.discrete.DiscreteRule.lhs_struc le in
   let subst_params tm = 
@@ -108,6 +111,7 @@
   let cur_vals = ref init_vals in
   let all_vals = ref [] in
   let end_time = !time +. t -. (0.01 *. !time_step) in (*TODO: 1% is decimals!*)
+  if !debug_level > 1 then print_endline ("et: " ^ (string_of_float end_time));
   let is_inv s = Solver.M.check_formula s r.inv_pp in
   let lhs_to_model ((f, a), _) =
     (* dynamics refer to elements by LHS matches *)
@@ -129,8 +133,14 @@
   if (is_inv !cur_struc) then (
     all_vals := !cur_vals :: !all_vals ;
     last_struc := !cur_struc
-  ) else
-    cur_vals := List.hd !all_vals ;
+  ) else (
+    if (!debug_level > 1) then (
+      print_endline "Invariant failed.";
+      print_endline (Structure.str !cur_struc);
+      print_endline (Formula.sprint r.inv);
+    ) ;
+    cur_vals := List.hd !all_vals;
+  ) ;
   let lhs_to_model_str x =
     let (f, i) = lhs_to_model x in
     f, Structure.elem_str struc i in

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2010-12-06 22:12:51 UTC (rev 1230)
+++ trunk/Toss/Arena/DiscreteRule.ml	2010-12-07 00:26:40 UTC (rev 1231)
@@ -458,12 +458,16 @@
    check invariants nor postconditions. *)
 let rewrite_single model (matching : matching) rule_obj
     : Structure.structure =
-  let ldmap =
-    try
-      List.map (fun (l,d)->
-        SIMap.find l rule_obj.lhs_elem_inv_names, d) matching
-    with _ ->
-      failwith "rewrite_single: rule_obj inconsistent with matching" in
+  let find_fst_name simap (name, x) =
+    try (SIMap.find name simap, x) with Not_found ->
+      let mtch_str (a, b) = (string_of_int a) ^ " <- " ^ (string_of_int b) in
+      let m_s = "{ "^ String.concat ", " (List.map mtch_str matching) ^ " }" in
+      let bd_add_str a  b acc = acc ^ ", " ^ (string_of_int a) ^ ": " ^ b in
+      let map_s = SIMap.fold bd_add_str simap "" in
+      let general_s = "rewrite_single: rule_obj inconsistent with matching " in
+      let name_s = string_of_int name in
+      failwith (general_s ^ m_s ^"; missing "^ name_s ^ " in: "^ map_s ^ ".") in
+  let ldmap = List.map (find_fst_name rule_obj.lhs_elem_inv_names) matching in
   rewrite_single_aux model ldmap rule_obj
 
 

Modified: trunk/Toss/examples/bounce.toss
===================================================================
--- trunk/Toss/examples/bounce.toss	2010-12-06 22:12:51 UTC (rev 1230)
+++ trunk/Toss/examples/bounce.toss	2010-12-07 00:26:40 UTC (rev 1231)
@@ -14,7 +14,7 @@
     y(1) = y(1);
     x(1) = x(1)
   pre true
-  inv ex x ((lhs_1(x) and ((((:y(x) + (-1. * 0.)) +
+  inv ex x ((_lhs_1(x) and ((((:y(x) + (-1. * 0.)) +
                              (-1. * 0.)) + (-1. * 0.)) < 0)))
   post true
 LOC 0 {


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.