Add --eval and --include args to evaluate environments.

examples/environment/env1.json

@@ -1,56 +1,57 @@
 {
+	"t": 0.0,
 	"trc": [
 		[
 			"a",
-			0
+			0.0
 		],
 		[
 			"b",
-			1
+			1.0
 		],
 		[
 			"idle",
-			2
+			2.0
 		],
 		[
 			"c",
-			3
+			3.0
 		],
 		[
 			"b",
-			4
+			4.0
 		],
 		[
 			"c",
-			5
+			5.0
 		],
 		[
 			"b",
-			6
+			6.0
 		],
 		[
 			"c",
-			7
+			7.0
 		],
 		[
 			"idle",
-			8
+			8.0
 		],
 		[
 			"c",
-			9
+			9.0
 		],
 		[
 			"a",
-			10
+			10.0
 		],
 		[
 			"idle",
-			11
+			11.0
 		],
 		[
 			"idle",
-			12
+			12.0
 		]
 	]
 }

src/helper.ml

@@ -47,6 +47,13 @@ let set_setting name v tbl = Hashtbl.add tbl name v
 
 let set_setting_replace name v tbl = Hashtbl.replace tbl name v
 
+let get_setting_bool name tbl =
+  try
+  match Hashtbl.find tbl name with
+  | Sel a -> a
+  | _ -> false
+  with _ -> false
+
 let get_setting_int name tbl =
   match Hashtbl.find tbl name with
   | Num a -> a

src/rmtld3.ml

@@ -611,6 +611,16 @@ let of_rmtld3_eval_env ({trc= i; evaluate= operator} : Rmtld3_eval.env) : env
 let of_env ({trc= i; evaluate= operator} : env) : Rmtld3_eval.env =
   {trc= i; evaluate= of_trace operator}
 
+let of_rmtld3_eval_duration (a : Rmtld3_eval.duration) : duration =
+  match a with 
+  | Rmtld3_eval.Dnone ->  Dnone
+  | Rmtld3_eval.Dsome n -> Dsome n
+
+let of_duration (a: duration) : Rmtld3_eval.duration =
+  match a with 
+  | Dnone ->  Rmtld3_eval.Dnone
+  | Dsome n -> Rmtld3_eval.Dsome n
+
 (* 
  * Interpretation of RMTLD3 terms and formulas
  * 
@@ -627,7 +637,7 @@ let of_env ({trc= i; evaluate= operator} : env) : Rmtld3_eval.env =
 let rec eval_term m t term =
   match term with
   | Constant value -> Dsome value
-  | Duration (di, phi) -> eval_term_duration m (t, eval_term m t di) phi
+  | Duration (di, phi) -> eval_term_duration m t di phi
   | FPlus (tr1, tr2) -> (
     match (eval_term m t tr1, eval_term m t tr2) with
     | Dsome v1, Dsome v2 -> Dsome (v1 +. v2)
@@ -638,41 +648,12 @@ let rec eval_term m t term =
     | _ -> Dnone )
   | _ -> raise (Failure "eval_term: the term definition is missing")
 
-and eval_term_duration (k, u) dt formula =
-  let indicator_function (k, u) t phi =
-    if eval (k, u, t) phi = True then 1. else 0.
-  in
-  let riemann_sum m dt (i, i') phi =
-    (* dt=(t,t') and t in ]i,i'] or t' in ]i,i'] *)
-    count_duration := !count_duration + 1 ;
-    let t, t' = dt in
-    if i <= t && t < i' then
-      (* lower bound *)
-      (i' -. t) *. indicator_function m t phi
-    else if i <= t' && t' < i' then
-      (* upper bound *)
-      (t' -. i) *. indicator_function m t' phi
-    else (i' -. i) *. indicator_function m i phi
-  in
-  let eval_eta m dt phi x =
-    (* fold_left (fun s (_, (i, t')) -> riemann_sum m dt (i, t') phi +. s) 0.
-       x *)
-    let rec f lst acc =
-      if length lst <= 1 then acc
-      else
-        let _, i = hd lst in
-        if tl lst = [] then acc
-        else f (tl lst) (riemann_sum m dt (i, snd (hd (tl lst))) phi +. acc)
-    in
-    f x 0.
-  in
-  match dt with
-  | t, Dsome t'
-    when List.exists
-           (fun (_, a) -> a >= t +. t')
-           k.trc (*when k.duration_of_trace >= t +. t'*) ->
-      Dsome (eval_eta (k, u) (t, t') formula (sub_k (k, u, t) t'))
-  | _ -> Dnone
+and eval_term_duration (k, u) t tm fm =
+  of_rmtld3_eval_duration
+    (Rmtld3_eval.eval_tm_duration
+       (fun k u t -> of_duration (eval_term (of_rmtld3_eval_env k, u) t tm))
+       (fun k u t -> of_tree_valued (eval (of_rmtld3_eval_env k, u, t) fm))
+       (of_env k) u t )
 
 and eval (env, lg_env, t) formula =
   match formula with

src/rmtld3synth.ml

@@ -56,14 +56,19 @@ let set_trace_style f = trace_style := f
 
 let set_gen_rmtld_formula f = gen_rmtld_formula := true
 
-let set_eval f = failwith "!"
+let set_eval _ = set_setting "evaluate" (Sel true) helper
 
 let set_env v =
   let json =
     (* check whether this is a filename or a json string *)
-    Yojson.Safe.from_string v
+    let re = Str.regexp "^\\([.]?/[^/ ]*\\)+/?$" in
+    if Str.string_match re v 0 then
+      Yojson.Safe.from_file v
+    else
+      Yojson.Safe.from_string v
   in
-  failwith "!"
+  let x = (json |> Yojson.Safe.to_string) in
+  set_setting "environment" (Txt x) helper
 
 (* output settings *)
 let set_out_file v =
@@ -495,4 +500,15 @@ let _ =
   else if !gen_rmtld_formula then
     let fm = gen_formula_default () in
     slatex_of_rmtld_fm fm |> print_endline
+  else if get_setting_bool "evaluate" helper then
+    (* get trc *)
+    let json = get_setting_string "environment" helper |> Yojson.Safe.from_string in
+    let json_trc = json |> Yojson.Safe.Util.member "trc" in
+    let json_t = json |> Yojson.Safe.Util.member "t" in
+    let trc = if json_trc <> `Null then trace_of_yojson json_trc else failwith "No 'trc' available!" in
+    let env = Rmtld3.environment trc in
+    let lg_env = Rmtld3.lenv in
+    let t = if json_t <> `Null then Rmtld3.time_of_yojson json_t else 0. in
+    let res = Rmtld3.eval (env, lg_env, t) input_fm in
+    res |> b3_to_string |> print_endline
   else print_endline "Nothing to do. Type --help"

unittests/test.sh

@@ -52,18 +52,17 @@ CMDSAT="$CMDSAT_NO_TRACE --get-trace"
 # dsl expressions
 declare -a dsl_expressions=(
   "a"
-  "a or b"
-  "not a"
+  "a || b"
+  "~ a"
   "a until b within 10s"
   "a on 10s"
 
   # got from documentation
   "always (a until b within 3s) within 10s"
-  "always ((rise a) -> (eventually b within 3s)) within 10s"
-  "always ((rise a) -> (b on 3s)) within 10s"
-  "always ((rise a) -> (eventually b within =3s)) within 10s"
-  "duration of a in 0 .. 2"
-  "duration of a in [0, 2]"
+  #"always ((rise a) -> (eventually b within 3s)) within 10s"
+  #"always ((rise a) -> (b on 3s)) within 10s"
+  #"always ((rise a) -> (eventually b within =3s)) within 10s"
+  "duration of a in 0 .. 2 < 10"
   "duration of a in [0, 2] < 10"
   "a until b within range 10ns .. 1s"
   "a until b within range [10ns, 1s]"
@@ -189,11 +188,13 @@ declare -a arrayrmtld_sat_expected_result=(
   echo "Executing eval tests..."
 
   # get test.sh directory
-  DIR="$(dirname -- "${BASH_SOURCE[0]}")"
+  DIR_PATH="$(dirname -- "${BASH_SOURCE[0]}")"
+  DIR_PATH="$(realpath -e -- "$DIR_PATH")"
+  echo $DIR_PATH
 
   for ((i = 1; i < ${dsl_expressions_length} + 1; i++)); do
     echo "expression: '${dsl_expressions[$i - 1]}'"
-    #rmtld3synth --eval --include "$DIR/../examples/environment/env1.json" --input-dsl ${dsl_expressions[$i - 1]}
+    rmtld3synth --eval --include "$(path "$DIR_PATH/../examples/environment/env1.json")" --input-dsl "${dsl_expressions[$i - 1]}"
   done
 
   sleep 10