diff --git a/src/sasaMain.ml b/src/sasaMain.ml index 149c632f7bfe4ed9ba6110cdb0f0158957bfe9de..1bf87099e5a5bfbc9d22a138ff420622c2106797 100644 --- a/src/sasaMain.ml +++ b/src/sasaMain.ml @@ -20,10 +20,10 @@ let (print_step : int -> int -> SasArg.t -> 'v Env.t -> 'v Process.t list -> str ) else ( (* rif mode, internal daemons *) if args.rif then - Printf.printf " %s %s %s\n" (StringOf.env_rif e pl) enable_val activate_val + Printf.printf " %s %s %s\n%!" (StringOf.env_rif e pl) enable_val activate_val else ( Printf.printf "\n#step %s\n" (string_of_int (n-i+1)); - Printf.printf "#outs %s %s %s\n" (StringOf.env_rif e pl) enable_val activate_val + Printf.printf "#outs %s %s %s\n%!" (StringOf.env_rif e pl) enable_val activate_val ); ); flush stderr; diff --git a/test/lustre/oracle_utils.lus b/test/lustre/oracle_utils.lus index bce7fb7ff140afc65e6e57d8a2d22918665910f2..e8ef92faa226a6f713a192bc3f290d795160e981 100644 --- a/test/lustre/oracle_utils.lus +++ b/test/lustre/oracle_utils.lus @@ -5,7 +5,7 @@ include "demon.lus" ----------------------------------------------------------------------------- -- An algo is silent when no action is enable -node silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool); +function silent<<const an: int; const pn: int>> (Enab: bool^an^pn) returns (ok:bool); let ok = all_false<<an, pn>>(Enab); tel diff --git a/test/lustre/utils.lus b/test/lustre/utils.lus index 0b51e7a079a3e9ce54c2c057360b7efd94d6e6c2..1ada4177c69a2708670604a09c0d0cf3666bd0e4 100644 --- a/test/lustre/utils.lus +++ b/test/lustre/utils.lus @@ -27,34 +27,34 @@ tel node test_count_true_acc = count_true_acc <<1>> ----------------------------------------------------------------------------- -node map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n); +function map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n); let Z = map<<and,n>>(X,Y) ; tel -node map_or<<const n:int>> (X,Y:bool^n) returns (Z:bool^n); +function map_or<<const n:int>> (X,Y:bool^n) returns (Z:bool^n); let Z = map<<or,n>>(X,Y) ; tel ----------------------------------------------------------------------------- -node implies_list(A,B:bool^m) returns (res:bool^m); +function implies_list(A,B:bool^m) returns (res:bool^m); let res = map<<=>,m>>(A,B) ; tel ----------------------------------------------------------------------------- -node one_true <<const m:int ; const n:int>> (tab:bool^m^n) returns (res:bool); +function one_true <<const m:int ; const n:int>> (tab:bool^m^n) returns (res:bool); let res = (((red<<count_true_acc<<m>>,n>>(0,tab)))=1); tel ----------------------------------------------------------------------------- -node all_true <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool); +function all_true <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool); let res = boolred<<m,m,m>>((red<<map_and<<m>>,n>>(true^m,t))) ; tel -node all_false <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool); +function all_false <<const m:int ; const n:int>>(t:bool^m^n) returns (res:bool); let res = boolred<<0,0,m>>((red<<map_or<<m>>,n>>(false^m,t))) ; tel diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml index 65501bfc54b24c618ec820ec5f4f9ba253ea77b9..9d47086b892a29704bbcafeca1c6f6d9e092db37 100644 --- a/test/my-rdbg-tuning.ml +++ b/test/my-rdbg-tuning.ml @@ -66,7 +66,7 @@ let print_sasa_event e = if e.kind <> Ltop then print_event e else let enab, act, vars = split_data e.data in (* let enab = only_true enab in *) - let act = only_true act in + let act = only_true act in let act_pid = List.map (fun (pid,_,_) -> pid) act in let vars = List.filter (fun (pid, _,_) -> List.mem pid act_pid) vars in let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in @@ -383,7 +383,17 @@ let goto_next_false_oracle e = List.mem ("ok", Bool) e.outputs && not (vb "ok" e)) -let viol () = e:=goto_next_false_oracle !e +let viol () = e:=goto_next_false_oracle !e; !dot_view ();; + +(**********************************************************************) +(* Move forward until silence *) + +let is_silent e = + let enab, _act, _vars = split_data e.data in + List.for_all (fun (_,_,v) -> v = Data.B false) enab + +let goto_silence e = next_cond e is_silent +let silence () = e:=goto_silence !e; !dot_view ();; (**********************************************************************) (* Perform the checkpointing at rounds! *)