Fix adjust_base gamma to avoid losing precision.

src/helper.ml

@@ -53,7 +53,7 @@ let mk_helper =
   (ref "", ref "", ref 0, ([], [], []), default_counter_map, tbl)
 
 (* new settings structure setters *)
-let set_setting name v (_, _, _, _, _, tbl) = Hashtbl.add tbl name v
+let set_setting name v (_, _, _, _, _, tbl) = Hashtbl.replace tbl name v
 
 let get_setting_int name (_, _, _, _, _, tbl) =
   match Hashtbl.find tbl name with
@@ -413,3 +413,13 @@ let pow base exponent =
   aux 1 base exponent
 
 let (%) f g x = fun x -> f(g x)
+
+let adjust_base gamma helper =
+  let conv = function
+  | "s" -> 1.
+  | "ms" -> 1_000.
+  | "us" -> 1_000_000.
+  | "ns" -> 1_000_000_000.
+  | _ -> failwith "adjust_base unavailable." in
+  let rst = (get_setting_string "rtm_monitor_time_unit" helper |> conv) *. gamma in
+  if rst < 1. then failwith "adjust_base loses precision. Please consider changing the monitor time units!" else rst

src/rmtld3synth.ml

@@ -104,10 +104,9 @@ let set_rtm_monitor_name_prefix v =
   set_setting "rtm_monitor_name_prefix" (Txt v) helper
 
 let set_rtm_monitor_time_unit v =
-  (* check if ns,us,ms,s *)
   if v = "ns" || v = "us" || v = "ms" || v = "s" then
     set_setting "rtm_monitor_time_unit" (Txt v) helper
-  else failwith "check if time units are ns, us, ms, s."
+  else failwith "check if time units are 'ns', 'us', 'ms', or 's'."
 
 (* general settings *)
 let set_gen_tests v = set_setting "gen_tests" (Sel v) helper

src/synthesis/cpp11.ml

@@ -80,7 +80,7 @@ let convert_to_always_equal (sf2, b) gamma helper =
   (* get new id *)
   let id = get_until_counter helper in
   ( "always_equal<T, Eval_always_b_" ^ string_of_int id ^ "<T>, "
-    ^ string_of_int (int_of_float gamma)
+    ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
     ^ ">"
   , b ^ "\n      template <typename T> class Eval_always_b_"
     ^ string_of_int id
@@ -97,7 +97,7 @@ let convert_to_always_equal (sf2, b) gamma helper =
       \  };\n\
       \  " )
 
-let convert_to_unbounded_eventually (sf2, b) gamma helper =
+let convert_to_unbounded_eventually (sf2, b) helper =
   print_endline
     "The unbounded until operator 'true U[infty] fm' is converted to \
      'Eventually[infty] fm' since cpp11 synthesis is enabled." ;
@@ -125,12 +125,12 @@ let synth_fm_uless gamma (sf1, a) (sf2, b) helper =
   if (sf1, a) = synth_fm_not (synth_fm_true helper) helper then
     convert_to_always_equal (sf2, b) gamma helper
   else if gamma = max_float && (sf1, a) = synth_fm_true helper then
-    convert_to_unbounded_eventually (sf2, b) gamma helper
+    convert_to_unbounded_eventually (sf2, b) helper
   else
     (* get new id *)
     let id = get_until_counter helper in
     ( "until_less<T, Eval_until_less_" ^ string_of_int id ^ "<T>, "
-      ^ string_of_int (int_of_float gamma)
+      ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
       ^ ">(trace, t)"
     , a ^ b ^ "\n  template <typename T> class Eval_until_less_"
       ^ string_of_int id
@@ -155,10 +155,10 @@ let synth_fm_ueq gamma (sf1, a) (sf2, b) helper =
        Until (=): A Until (=a) B <-> Always(<a) A and Always(=a) B *)
     ( "[](T &trace, timespan &t){\n    auto x = always_less<T, Eval_always_a_"
       ^ string_of_int id ^ "<T>, "
-      ^ string_of_int (int_of_float gamma)
+      ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
       ^ ">(trace, t);\n    auto y = always_equal<T, Eval_always_b_"
       ^ string_of_int id ^ "<T>, "
-      ^ string_of_int (int_of_float gamma)
+      ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
       ^ ">(trace, t);\n    return b3_and(x,y);\n  }(trace, t)\n  "
     , a ^ b ^ "template <typename T> class Eval_always_a_" ^ string_of_int id
       ^ " {\n\
@@ -190,7 +190,7 @@ let synth_fm_sless gamma (sf1, a) (sf2, b) helper =
   (* get new id *)
   let id = get_until_counter helper in
   ( "since_less<T, Eval_since_less_" ^ string_of_int id ^ "<T>, "
-    ^ string_of_int (int_of_float gamma)
+    ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
     ^ ">(trace, t)"
   , a ^ b ^ "\n  template <typename T> class Eval_since_less_"
     ^ string_of_int id
@@ -210,10 +210,10 @@ let synth_fm_seq gamma (sf1, a) (sf2, b) helper =
   ( "[](T &trace, timespan &t){\n\
     \    auto x = historically_less<T, Eval_historically_a_"
     ^ string_of_int id ^ "<T>, "
-    ^ string_of_int (int_of_float gamma)
+    ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
     ^ ">(trace, t);\n    auto y = historically_equal<T, Eval_historically_b_"
     ^ string_of_int id ^ "<T>, "
-    ^ string_of_int (int_of_float gamma)
+    ^ ((adjust_base gamma helper) |> int_of_float |> string_of_int)
     ^ ">(trace, t);\n    return b3_and(x,y);\n  }(trace, t)\n  "
   , a ^ b ^ "template <typename T> class Eval_historically_a_"
     ^ string_of_int id