diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..03e0929abd6cf3d0a4312bb1557b32b579b92a6d --- /dev/null +++ b/test/coloring/coloring_oracle.lus @@ -0,0 +1,37 @@ + +-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version + +include "../../lib/utils.lus" + +node coloring_oracle( + 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_round : bool; + lustre_round_nb : int; +-- lustre_cost: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 + ); +-- lustre_cost = cost(lustre_enabled, lustre_config); + ok = lustre_enabled = ocaml_enabled + -- compare the sasa dot interpretation and the salut dot to lustre compilation + and lustre_config = ocaml_config + -- compare the lustre and the ocaml version of the processes +-- and Lustre::real2int(ocaml_cost) = lustre_cost +-- and lustre_round = round +-- and lustre_round_nb = round_nb +; + -- compare the cost functions +tel diff --git a/test/coloring/config.ml b/test/coloring/config.ml new file mode 120000 index 0000000000000000000000000000000000000000..69fbde97dc330f5f466f789fb7a08a84667ed763 --- /dev/null +++ b/test/coloring/config.ml @@ -0,0 +1 @@ +../../../test/coloring/config.ml \ No newline at end of file diff --git a/test/coloring/simu.lus b/test/coloring/simu.lus deleted file mode 100644 index a0fa0f42de8dd155261b3d302dda6dce2d000a3f..0000000000000000000000000000000000000000 --- a/test/coloring/simu.lus +++ /dev/null @@ -1,25 +0,0 @@ -include "../../lib/sas.lus" -include "ER.lus" - -node incr(ain : int) returns (aout, z : int); -let - z = ain; aout = ain + 1; -tel; - -node simu(x:bool) returns (s : bool); -var - initials : state^card; - Enab_p : bool^actions_number^card; - p : bool^actions_number^card; - _d:int; - - p_c : state^card; - -let - _d, initials= fill<<incr; card>>(0); - - p = false^actions_number^card -> pre Enab_p; - p_c, Enab_p = ER(p, initials -> 0^card); - - s = silent<<actions_number,card>>(Enab_p); -tel diff --git a/test/coloring/state.lus b/test/coloring/state.lus new file mode 100644 index 0000000000000000000000000000000000000000..ac99865f08f4410b2fc23b3714986f030bc362b2 --- /dev/null +++ b/test/coloring/state.lus @@ -0,0 +1,17 @@ +-- automatically generated by salut + +type state = int; + +type action = enum { recolor }; +const actions_number = 1; + +function action_of_int(i : int) returns (a : action); +let + a = recolor; +tel; + +function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card) +returns (res : bool); +let + res=silent<<actions_number,card>>(enables); +tel; \ No newline at end of file diff --git a/test/coloring/verify.lus b/test/coloring/verify.lus index c06ff6e12e748f02e3fa8c38b7f49c122164abcc..d026150e7c5f98c53e5b1b4ae936d9835f5bfe3b 100644 --- a/test/coloring/verify.lus +++ b/test/coloring/verify.lus @@ -15,7 +15,7 @@ let config, enables,r,rn = topology(activations, inits); - legitimate = legitimate<<actions_number,card>>(enables,config);; + legitimate = legitimate<<actions_number,card>>(enables,config); closure = true -> (pre(legitimate) => legitimate); moves = move_count<<actions_number,card>>(activations);