From cfd4214086d209006ab70a6bb28f9567b3798f68 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr> Date: Mon, 8 Apr 2024 17:36:23 +0200 Subject: [PATCH] test: add a debug version of the oracle --- .../dijkstra-ring/dijkstra_ring_oracle.lus | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus b/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus index 7a56ea42..504d8601 100644 --- a/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus +++ b/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus @@ -37,6 +37,38 @@ let ; -- compare the cost functions tel +node dijkstra_ring_oracle_debug<<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; + lustre_config : state^card; + lustre_enabled : bool^actions_number^card; + lustre_round:bool; + lustre_round_nb:int); +var + 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 round = lustre_round + and round_nb = lustre_round_nb +; + -- compare the cost functions +tel node _dijkstra_ring_oracle<<const actions_number:int; const card:int>>( legitimate : bool; -- GitLab