diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml index 71d96186fa8d6ec51b732615f1abaed2e90cfd96..f73041349741e7345973fe5a44fedc8a14c9dc4c 100644 --- a/lib/sasacore/genOracle.ml +++ b/lib/sasacore/genOracle.ml @@ -1,4 +1,4 @@ -(* 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) diff --git a/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus b/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus index d2b58bc63b8b5ac07de32956366727b4ba983b24..98df52379bcaf5f50aa32a92e1a9852b3483581a 100644 --- a/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus +++ b/salut/test/bfs-spanning-tree/bfs_spanning_tree_oracle.lus @@ -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; diff --git a/salut/test/coloring/coloring_oracle.lus b/salut/test/coloring/coloring_oracle.lus index 8389121dcc4ea0118c9aeb6ae20b660419dc67ba..bb3afdc7ddf39c68237f2c0dea574c6289dfee72 100644 --- a/salut/test/coloring/coloring_oracle.lus +++ b/salut/test/coloring/coloring_oracle.lus @@ -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; diff --git a/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus b/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus index c870b89df7ca391f4d45c52bee952c67521ae152..7a56ea426577d6cf148e0e65a5891b029cd0bf73 100644 --- a/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus +++ b/salut/test/dijkstra-ring/dijkstra_ring_oracle.lus @@ -1,18 +1,18 @@ -- 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 diff --git a/salut/test/ghosh/ghosh_oracle.lus b/salut/test/ghosh/ghosh_oracle.lus index b57288cceacb97d37f016c0f774e1c378fc9902a..528a24f97294abd8dbf1b35f5240c096d689a1b4 100644 --- a/salut/test/ghosh/ghosh_oracle.lus +++ b/salut/test/ghosh/ghosh_oracle.lus @@ -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; diff --git a/salut/test/k-clustering/kclustering_oracle.lus b/salut/test/k-clustering/kclustering_oracle.lus index 00681387941e2419b75c3b64c94ceae101d71d29..c4461e17c5c21321646c5563bf9725ce57f13747 100644 --- a/salut/test/k-clustering/kclustering_oracle.lus +++ b/salut/test/k-clustering/kclustering_oracle.lus @@ -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; diff --git a/salut/test/ring-orientation/ring_orientation_oracle.lus b/salut/test/ring-orientation/ring_orientation_oracle.lus index 374b7a3f18627ba5194accb5518e2ebc88a62a9f..8ee2225388f1cd2fadcf1824d7c9a28065e813ae 100644 --- a/salut/test/ring-orientation/ring_orientation_oracle.lus +++ b/salut/test/ring-orientation/ring_orientation_oracle.lus @@ -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;