-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version include "../../lib/utils.lus" -- include "cost.lus" node ghosh_oracle<<const actions_number:int; const card:int>>( legitimate : bool; -- ocaml_cost : real; ocaml_enabled : bool^actions_number^card; active : bool^actions_number^card; ocaml_config : state^card; round:bool; round_nb:int; ) returns (ok : bool); var lustre_config : state^card; lustre_enabled : bool^actions_number^card; -- lustre_cost:int; lustre_round:bool; lustre_round_nb:int; let lustre_config, lustre_enabled, lustre_round, lustre_round_nb = topology(active -> pre active, -- ignored at the first step ocaml_config -- used at the first step only ); ok = lustre_enabled = ocaml_enabled -- compare the sasa dot interpretation and the salut dot to lustre compilation and lustre_config = ocaml_config -- and round = lustre_round and round_nb = lustre_round_nb ; tel