Skip to content
Snippets Groups Projects
Commit d54ddc90 authored by erwan's avatar erwan
Browse files

fix: lv6 now checks if static args are present (even if unused)

parent 0973b02b
No related branches found
No related tags found
No related merge requests found
(* Time-stamp: <modified the 09/02/2024 (at 10:07) by Erwan Jahier> *)
(* Time-stamp: <modified the 09/02/2024 (at 13:55) by Erwan Jahier> *)
open Process
......@@ -132,7 +132,7 @@ node oracle_debug(legitimate:bool;%s%s) \nreturns (ok:bool;
);
let
%s %s %s
ok, lustre_config, lustre_enabled,lustre_round,lustre_round_nb = %s_oracle_debug(legitimate,%s Enab, Acti, Config, round, round_nb);
ok, lustre_config, lustre_enabled,lustre_round,lustre_round_nb = %s_oracle_debug<<an,pn>>(legitimate,%s Enab, Acti, Config, round, round_nb);
tel
"
(Mypervasives.entete "--" SasaVersion.str SasaVersion.sha)
......
......@@ -9,7 +9,7 @@ let
res = state { d=d ; par=par };
tel;
node bfs_spanning_tree_oracle(
node bfs_spanning_tree_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
ocaml_enabled : bool^actions_number^card;
active : bool^actions_number^card;
......@@ -34,7 +34,7 @@ let
nd=d -> pre nd;
tel;
node bfs_spanning_tree_oracle_debug(
node bfs_spanning_tree_oracle_debug<<an,pn>>(
legitimate : bool;
ocaml_enabled : bool^actions_number^card;
active : bool^actions_number^card;
......
......@@ -3,7 +3,7 @@
include "../../lib/utils.lus"
node coloring_oracle(
node coloring_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......
-- Here, we use the Lustre version of the algorithm as an oracle for the ocaml version
include "../../lib/utils.lus"
include "cost.lus"
node dijkstra_ring_oracle(
node dijkstra_ring_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
active : bool^actions_number^card;
active : bool^actions_number^card;
ocaml_config : state^card;
round:bool;
round_nb:int;
)
)
returns (ok : bool;
);
var
......@@ -27,7 +27,7 @@ let
ocaml_config -- used at the first step only
);
lustre_cost = cost(lustre_enabled, lustre_config);
ok = lustre_enabled = ocaml_enabled
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
......@@ -35,26 +35,26 @@ let
and round = lustre_round
and round_nb = lustre_round_nb
;
-- compare the cost functions
-- compare the cost functions
tel
node _dijkstra_ring_oracle(
node _dijkstra_ring_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;
)
active : bool^actions_number^card;
ocaml_config : state^card;
)
returns (ok : bool);
var
lustre_config : state^card;
lustre_enabled : bool^actions_number^card;
lustre_round:bool;
lustre_round:bool;
lustre_round_nb:int;
let
ok= lustre_enabled[0][0] or true;
lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
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
);
tel
\ No newline at end of file
tel
......@@ -4,7 +4,7 @@
include "../../lib/utils.lus"
-- include "cost.lus"
node ghosh_oracle(
node ghosh_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
-- ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......
......@@ -9,7 +9,7 @@ let
res = state { isRoot=isRoot; par=par; alpha=alpha };
tel;
node kclustering_oracle(
node kclustering_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......
......@@ -2,8 +2,9 @@
include "../../lib/utils.lus"
-- This oracle checks that the ocaml and the lustre version agrees
node ring_orientation_oracle(
node ring_orientation_oracle<<const actions_number:int; const card:int>>(
legitimate : bool;
-- ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......@@ -25,7 +26,7 @@ let
tel;
node ring_orientation_oracle_debug(
node ring_orientation_oracle_debug<<const actions_number:int; const card:int>>(
legitimate : bool;
-- ocaml_cost : real;
ocaml_enabled : bool^actions_number^card;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment