diff --git a/lib/sasa/dune b/lib/sasa/dune index 529a264312f5c08101ab3e3c0e81358b7507595a..f96076b6db6ce9388aa0d0cf233f47dd7b296280 100644 --- a/lib/sasa/dune +++ b/lib/sasa/dune @@ -1,9 +1,9 @@ -;; Time-stamp: <modified the 06/09/2019 (at 10:23) by Erwan Jahier> +;; Time-stamp: <modified the 07/10/2019 (at 21:44) by Erwan Jahier> (library (name sasa) (public_name sasa) - (libraries dynlink ocamlgraph rdbg algo sasacore lutils) + (libraries ocamlgraph rdbg algo sasacore lutils) ; (wrapped false) (library_flags -linkall) (synopsis "The Sasa rdbg plugin") diff --git a/lib/sasacore/main.ml b/lib/sasacore/main.ml index e0748504dc626e7253facfe0030ef2d04eb616ae..0ff817e24ba89dc43ac350ec1187344a11a1e653 100644 --- a/lib/sasacore/main.ml +++ b/lib/sasacore/main.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 07/10/2019 (at 16:38) by Erwan Jahier> *) +(* Time-stamp: <modified the 08/10/2019 (at 10:18) by Erwan Jahier> *) open Register @@ -187,11 +187,11 @@ let (make : bool -> string array -> 'v t) = Printf.printf "Hint: you may wish to generate %s out of %s with:\n" cmxs ml_register_file; Printf.printf " ocamlfind ocamlopt -package algo -shared %s %s %s -o %s\n" - ml_state_file ml_inputs ml_register_file cmxs; + ml_state_file ml_inputs ml_register_file cmxs; flush stdout; exit 0 ); - + let nidl = List.map (fun n -> n.Topology.id) nl in let nstr = String.concat "," nidl in Register.set_card (fun () -> List.length nl); @@ -212,7 +212,7 @@ let (make : bool -> string array -> 'v t) = if !Register.verbose_level > 0 then Printf.printf "Loading %s...\n" cmxs; Dynlink.loadfile_private cmxs; ) else (); - + let initl = List.map (fun n -> let algo_id = Filename.chop_suffix n.Topology.file ".ml" in let value_of_string_opt = Register.get_value_of_string () in @@ -254,26 +254,19 @@ let (make : bool -> string array -> 'v t) = flush oc; close_out oc; exit 0); - if args.rif then ( - Printf.printf "%s" - (Mypervasives.entete "#" SasaVersion.str SasaVersion.sha); - if args.demon <> Demon.Custom then - Printf.printf "#seed %i\n" args.seed; - let inputs_decl = get_inputs_rif_decl args pl in - Printf.printf "#inputs %s\n" - (String.concat " " - (List.map - (fun (vn,vt) -> Printf.sprintf "\"%s\":%s" vn vt) inputs_decl)); - flush stdout; - Printf.printf "#outputs %s\n" (env_rif_decl args pl); - flush stdout - ) else ( - if args.demon <> Demon.Custom then ( - Printf.printf "The pseudo-random engine is used with seed %i\n" - args.seed; - flush stdout - ); - ); + let oc = if args.rif then stderr else stdout in + let seed_oc = open_out "sasa.seed" in + Printf.fprintf seed_oc "%i\n" args.seed; flush seed_oc; close_out seed_oc; + Printf.fprintf oc "%s" (Mypervasives.entete "#" SasaVersion.str SasaVersion.sha); + Printf.fprintf oc "#seed %i\n" args.seed; + let inputs_decl = get_inputs_rif_decl args pl in + Printf.printf "#inputs %s\n" + (String.concat " " + (List.map + (fun (vn,vt) -> Printf.sprintf "\"%s\":%s" vn vt) inputs_decl)); + flush stdout; + Printf.printf "#outputs %s\n" (env_rif_decl args pl); + flush stdout; if args.ifi then ( List.iter (fun p -> List.iter diff --git a/lib/sasacore/sasArg.ml b/lib/sasacore/sasArg.ml index 1cfac9f8cbf08c7940fe9a64de1faddc4253c8cc..620d1d1188b5f0430eefd86613a55001eebc1935 100644 --- a/lib/sasacore/sasArg.ml +++ b/lib/sasacore/sasArg.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 12/09/2019 (at 08:54) by Erwan Jahier> *) +(* Time-stamp: <modified the 07/10/2019 (at 23:53) by Erwan Jahier> *) type t = { @@ -115,7 +115,7 @@ let (mkoptab : string array -> t -> unit) = mkopt args ["--rif";"-rif"] (Arg.Unit(fun () -> args.rif <- true)) - ["Follows RIF conventions"]; + ["Display only outputs on stdout (i.e., behave as a rif input file)"]; mkopt args ["--seed";"-seed"] (Arg.Int(fun i -> args.seed <- i)) diff --git a/src/sasaMain.ml b/src/sasaMain.ml index 81088c7a682a643d15b73cd0a145a8559c3255d0..c42cfc7b2d30080a59a07a7da33bcc6fc0ead5f1 100644 --- a/src/sasaMain.ml +++ b/src/sasaMain.ml @@ -7,7 +7,6 @@ let (print_step : int -> int -> SasArg.t -> 'v Env.t -> 'v Process.t list -> str String.concat " " (List.map (fun b -> if b then "t" else "f") (List.flatten enab_ll)) in - if args.rif then ( if args.demon = Demon.Custom then ( (* in custom mode, to be able to talk with lurette, this should not be printed on stdout @@ -17,18 +16,15 @@ let (print_step : int -> int -> SasArg.t -> 'v Env.t -> 'v Process.t list -> str Printf.printf "%s %s\n" (StringOf.env_rif e pl) enable_val; ) else ( (* rif mode, internal demons *) - 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 + if args.rif then + 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 + ); ); flush stderr; flush stdout - ) - else ( - Printf.eprintf "step %s: %s %s\n" - (string_of_int (n-i+1)) (StringOf.env e pl) activate_val; - flush stderr - ) exception Silent of int @@ -39,8 +35,7 @@ let (simustep: int -> int -> SasArg.t -> string -> let all, enab_ll = Sasacore.Main.get_enable_processes pl_n e in let pl = fst(List.split pl_n) in if - (* not (args.rif) && *) - List.for_all (fun b -> not b) (List.flatten enab_ll) + not (args.rif) && List.for_all (fun b -> not b) (List.flatten enab_ll) then ( print_step n i args e pl activate_val enab_ll; raise (Silent (n-i+1)) @@ -72,9 +67,8 @@ let rec (simuloop: int -> int -> SasArg.t -> string -> let ne, next_activate_val = simustep n i args activate_val pl_n e in if i > 0 then simuloop n (i-1) args next_activate_val pl_n ne else ( - if args.rif then ( - print_string "#q\n"; flush stdout - )) + print_string "#q\n"; flush stdout +) let () = let args, pl_n, e = Sasacore.Main.make true Sys.argv in diff --git a/test/coloring/Makefile b/test/coloring/Makefile index 9f376e4b6bf616e238133e6d40f3a6e1fe9825e4..69c78c36dc47cac722b466eb41fe8661c6f5da9f 100644 --- a/test/coloring/Makefile +++ b/test/coloring/Makefile @@ -1,11 +1,11 @@ -# Time-stamp: <modified the 17/09/2019 (at 16:54) by Erwan Jahier> +# Time-stamp: <modified the 07/10/2019 (at 23:49) by Erwan Jahier> sasa=$(DIR)/bin/sasa -l 100 test: ring.cmxs coloring.rif lurette coloring.rif: ring.cmxs - $(sasa) -l 200 ring.dot -rif > $@ + $(sasa) -l 200 ring.dot > $@ sim2chrogtk: coloring.rif sim2chrogtk -ecran -in $< > /dev/null diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus index 31621fcf46939a6072d3a7615520ebf91ed055e2..3c5105af867cc37d25f4a7ed98debff90191a9f1 100644 --- a/test/coloring/coloring_oracle.lus +++ b/test/coloring/coloring_oracle.lus @@ -31,9 +31,10 @@ tel node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) returns (res:bool; RoundNb:int); +var res0:bool; let - res, RoundNb = -- lemma_3_14<<an,pn>>(Enab,Acti) and - theorem_3_17<<an,pn>>(Enab,Acti); + res0, RoundNb = theorem_3_17<<an,pn>>(Enab,Acti); + res = res0 and lemma_3_14<<an,pn>>(Enab,Acti); tel