From e7b96b394e504a6bb84c1d58fe3332f3d55c4a38 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Wed, 11 Jan 2023 09:43:24 +0100
Subject: [PATCH] new: use dune to build the algo cmxs (requires rdbg >= 1.200)
---
.gitlab-ci.yml | 10 +--
Makefile.sasa | 1 +
dune-project | 3 +-
lib/sasacore/genOracle.ml | 19 ++---
lib/sasacore/genOracle.mli | 4 +-
lib/sasacore/simuState.ml | 59 +++++++---------
salut/test/Makefile.inc | 37 ++++++----
salut/test/bfs-spanning-tree/dune-project | 1 +
salut/test/bfs-spanning-tree/dune-workspace | 0
salut/test/coloring/dune | 1 +
salut/test/coloring/dune-project | 1 +
salut/test/coloring/dune-workspace | 0
salut/test/dijkstra-ring/dune-project | 1 +
salut/test/dijkstra-ring/dune-workspace | 0
salut/test/kclustering/dune-project | 1 +
salut/test/kclustering/dune-workspace | 0
salut/test/rsp_tree/dune-project | 1 +
salut/test/rsp_tree/dune-workspace | 0
salut/test/unison/dune-project | 1 +
salut/test/unison/dune-workspace | 0
sasa.opam | 2 +-
test/Makefile | 12 ++--
test/Makefile.dot | 6 +-
test/Makefile.inc | 67 +++++++++++-------
test/alea-coloring-alt/Makefile | 12 ++--
test/alea-coloring-alt/Makefile.dot | 1 +
test/alea-coloring-alt/Makefile.inc | 1 +
test/alea-coloring-alt/dune | 1 +
test/alea-coloring-alt/dune-project | 1 +
test/alea-coloring-alt/dune-workspace | 0
test/alea-coloring-alt/my-rdbg-tuning.ml | 9 ---
test/alea-coloring-alt/p.ml | 7 +-
test/alea-coloring-unif/Makefile | 18 ++---
test/alea-coloring-unif/Makefile.dot | 1 +
test/alea-coloring-unif/Makefile.inc | 1 +
test/alea-coloring-unif/dune | 1 +
test/alea-coloring-unif/dune-project | 1 +
test/alea-coloring-unif/dune-workspace | 0
test/alea-coloring-unif/my-rdbg-tuning.ml | 4 --
test/alea-coloring/Makefile | 16 ++---
test/alea-coloring/Makefile.dot | 1 +
test/alea-coloring/Makefile.inc | 1 +
test/alea-coloring/dune | 1 +
test/alea-coloring/dune-project | 1 +
test/alea-coloring/dune-workspace | 0
test/alea-coloring/my-rdbg-tuning.ml | 4 --
test/async-unison/Makefile | 22 +++---
test/async-unison/Makefile.dot | 1 +
test/async-unison/Makefile.inc | 1 +
test/async-unison/dune | 1 +
test/async-unison/dune-project | 1 +
test/async-unison/dune-workspace | 0
test/async-unison/my-rdbg-tuning.ml | 4 --
test/async-unison/p.ml | 9 ++-
.../{ => rdbg}/async_unison_oracle.ml | 0
test/bfs-spanning-tree/Makefile | 28 ++++----
test/bfs-spanning-tree/Makefile.dot | 1 +
test/bfs-spanning-tree/Makefile.inc | 1 +
test/bfs-spanning-tree/dune | 1 +
test/bfs-spanning-tree/dune-project | 1 +
test/bfs-spanning-tree/dune-workspace | 0
test/bfs-spanning-tree/my-rdbg-tuning.ml | 2 -
test/bfs-spanning-tree/root.ml | 15 ++--
test/bfs-st-HC92/Makefile | 20 +++---
test/bfs-st-HC92/Makefile.dot | 1 +
test/bfs-st-HC92/Makefile.inc | 1 +
test/bfs-st-HC92/dune | 1 +
test/bfs-st-HC92/dune-project | 1 +
test/bfs-st-HC92/dune-workspace | 0
test/coloring/Makefile | 32 ++++-----
test/coloring/Makefile.dot | 1 +
test/coloring/Makefile.inc | 1 +
test/coloring/coloring_oracle.lus | 11 +--
test/coloring/config.ml | 2 +-
test/coloring/dune | 1 +
test/coloring/dune-project | 1 +
test/coloring/dune-workspace | 0
test/coloring/my-rdbg-tuning.ml | 12 ----
test/coloring/ring_oracle.lus | 43 ------------
test/dfs-list/Makefile | 17 +++--
test/dfs-list/Makefile.dot | 1 +
test/dfs-list/Makefile.inc | 1 +
test/dfs-list/dune | 1 +
test/dfs-list/dune-project | 1 +
test/dfs-list/dune-workspace | 0
test/dfs-list/p.ml | 35 +++++-----
test/dfs-list/root.ml | 10 +--
test/dfs/Makefile | 20 ++----
test/dfs/Makefile.dot | 1 +
test/dfs/Makefile.inc | 1 +
test/dfs/dune | 1 +
test/dfs/dune-project | 1 +
test/dfs/dune-workspace | 0
test/dfs/my-rdbg-tuning.ml | 4 --
test/dfs/p.ml | 22 +++---
test/dfs/root.ml | 11 ++-
test/dijkstra-ring/Makefile | 16 ++---
test/dijkstra-ring/Makefile.dot | 1 +
test/dijkstra-ring/Makefile.inc | 1 +
test/dijkstra-ring/dijkstra_ring_oracle.lus | 16 +++--
test/dijkstra-ring/dune | 1 +
test/dijkstra-ring/dune-project | 1 +
test/dijkstra-ring/dune-workspace | 0
test/dijkstra-ring/p.ml | 9 +--
test/dijkstra-ring/ring_oracle.lus | 43 ------------
test/dijkstra-ring/root.ml | 7 +-
test/dune2copy | 59 ++++++++++++++++
test/k-clustering/4.14.0/fig52_kcl.rif.exp | 4 +-
test/k-clustering/4.14.0/rtree10.rif.exp | 4 +-
test/k-clustering/Makefile | 25 ++++---
test/k-clustering/Makefile.dot | 1 +
test/k-clustering/Makefile.inc | 1 +
test/k-clustering/config.ml | 13 ++--
test/k-clustering/dune | 1 +
test/k-clustering/dune-project | 1 +
test/k-clustering/dune-workspace | 0
test/k-clustering/my-rdbg-tuning.ml | 4 --
test/lustre/dune-workspace | 0
test/rsp-tree/Makefile | 17 ++---
test/rsp-tree/Makefile.dot | 1 +
test/rsp-tree/Makefile.inc | 1 +
test/rsp-tree/dune | 1 +
test/rsp-tree/dune-project | 1 +
test/rsp-tree/dune-workspace | 0
test/rsp-tree/my-rdbg-tuning.ml | 5 --
test/skeleton/Makefile | 9 ++-
test/skeleton/Makefile.dot | 1 +
test/skeleton/Makefile.inc | 1 +
test/skeleton/config.ml | 5 ++
test/skeleton/dune | 1 +
test/skeleton/dune-project | 1 +
test/skeleton/dune-workspace | 0
test/skeleton/my-rdbg-tuning.ml | 4 --
test/skeleton/p.ml | 12 ++--
test/st-CYH91/Makefile | 22 +++---
test/st-CYH91/Makefile.dot | 1 +
test/st-CYH91/Makefile.inc | 1 +
test/st-CYH91/dune | 1 +
test/st-CYH91/dune-project | 1 +
test/st-CYH91/dune-workspace | 0
test/st-CYH91/my-rdbg-tuning.ml | 4 --
test/st-CYH91/root.ml | 6 +-
test/st-KK06-algo1/Makefile | 24 +++----
test/st-KK06-algo1/Makefile.dot | 1 +
test/st-KK06-algo1/Makefile.inc | 1 +
test/st-KK06-algo1/dune | 1 +
test/st-KK06-algo1/dune-project | 1 +
test/st-KK06-algo1/dune-workspace | 0
test/st-KK06-algo1/my-rdbg-tuning.ml | 5 --
test/st-KK06-algo2/Makefile | 22 +++---
test/st-KK06-algo2/Makefile.dot | 1 +
test/st-KK06-algo2/Makefile.inc | 1 +
test/st-KK06-algo2/dune | 1 +
test/st-KK06-algo2/dune-project | 1 +
test/st-KK06-algo2/dune-workspace | 0
test/st-KK06-algo2/my-rdbg-tuning.ml | 5 --
test/toy-example-a5sf/Makefile | 19 +++--
test/toy-example-a5sf/Makefile.dot | 1 +
test/toy-example-a5sf/Makefile.inc | 1 +
test/toy-example-a5sf/config.ml | 20 +++---
test/toy-example-a5sf/dune | 1 +
test/toy-example-a5sf/dune-project | 1 +
test/toy-example-a5sf/dune-workspace | 0
test/toy-example-a5sf/my-rdbg-tuning.ml | 5 --
test/toy-example-a5sf/p.ml | 11 ++-
test/toy-example-sum/dune | 1 +
test/toy-example-sum/dune-project | 1 +
test/toy-example-sum/dune-workspace | 0
test/toy-example-sum/my-rdbg-tuning.ml | 7 --
test/unison/Makefile | 21 +++---
test/unison/Makefile.dot | 1 +
test/unison/Makefile.inc | 1 +
test/unison/config.ml | 4 +-
test/unison/dune | 1 +
test/unison/dune-project | 1 +
test/unison/dune-workspace | 0
test/unison/my-rdbg-tuning.ml | 15 ----
tools/rdbg4sasa/gtkgui.ml | 70 +++++++++----------
tools/rdbg4sasa/sasa-rdbg-cmds.ml | 64 ++++++++---------
179 files changed, 610 insertions(+), 656 deletions(-)
create mode 120000 salut/test/bfs-spanning-tree/dune-project
create mode 100644 salut/test/bfs-spanning-tree/dune-workspace
create mode 120000 salut/test/coloring/dune
create mode 120000 salut/test/coloring/dune-project
create mode 100644 salut/test/coloring/dune-workspace
create mode 120000 salut/test/dijkstra-ring/dune-project
create mode 100644 salut/test/dijkstra-ring/dune-workspace
create mode 120000 salut/test/kclustering/dune-project
create mode 100644 salut/test/kclustering/dune-workspace
create mode 120000 salut/test/rsp_tree/dune-project
create mode 100644 salut/test/rsp_tree/dune-workspace
create mode 120000 salut/test/unison/dune-project
create mode 100644 salut/test/unison/dune-workspace
create mode 120000 test/alea-coloring-alt/Makefile.dot
create mode 120000 test/alea-coloring-alt/Makefile.inc
create mode 120000 test/alea-coloring-alt/dune
create mode 120000 test/alea-coloring-alt/dune-project
create mode 100644 test/alea-coloring-alt/dune-workspace
delete mode 100644 test/alea-coloring-alt/my-rdbg-tuning.ml
create mode 120000 test/alea-coloring-unif/Makefile.dot
create mode 120000 test/alea-coloring-unif/Makefile.inc
create mode 120000 test/alea-coloring-unif/dune
create mode 120000 test/alea-coloring-unif/dune-project
create mode 100644 test/alea-coloring-unif/dune-workspace
delete mode 100644 test/alea-coloring-unif/my-rdbg-tuning.ml
create mode 120000 test/alea-coloring/Makefile.dot
create mode 120000 test/alea-coloring/Makefile.inc
create mode 120000 test/alea-coloring/dune
create mode 120000 test/alea-coloring/dune-project
create mode 100644 test/alea-coloring/dune-workspace
delete mode 100644 test/alea-coloring/my-rdbg-tuning.ml
create mode 120000 test/async-unison/Makefile.dot
create mode 120000 test/async-unison/Makefile.inc
create mode 120000 test/async-unison/dune
create mode 120000 test/async-unison/dune-project
create mode 100644 test/async-unison/dune-workspace
delete mode 100644 test/async-unison/my-rdbg-tuning.ml
rename test/async-unison/{ => rdbg}/async_unison_oracle.ml (100%)
create mode 120000 test/bfs-spanning-tree/Makefile.dot
create mode 120000 test/bfs-spanning-tree/Makefile.inc
create mode 120000 test/bfs-spanning-tree/dune
create mode 120000 test/bfs-spanning-tree/dune-project
create mode 100644 test/bfs-spanning-tree/dune-workspace
delete mode 100644 test/bfs-spanning-tree/my-rdbg-tuning.ml
create mode 120000 test/bfs-st-HC92/Makefile.dot
create mode 120000 test/bfs-st-HC92/Makefile.inc
create mode 120000 test/bfs-st-HC92/dune
create mode 120000 test/bfs-st-HC92/dune-project
create mode 100644 test/bfs-st-HC92/dune-workspace
create mode 120000 test/coloring/Makefile.dot
create mode 120000 test/coloring/Makefile.inc
create mode 120000 test/coloring/dune
create mode 120000 test/coloring/dune-project
create mode 100644 test/coloring/dune-workspace
delete mode 100644 test/coloring/my-rdbg-tuning.ml
delete mode 100644 test/coloring/ring_oracle.lus
create mode 120000 test/dfs-list/Makefile.dot
create mode 120000 test/dfs-list/Makefile.inc
create mode 120000 test/dfs-list/dune
create mode 120000 test/dfs-list/dune-project
create mode 100644 test/dfs-list/dune-workspace
create mode 120000 test/dfs/Makefile.dot
create mode 120000 test/dfs/Makefile.inc
create mode 120000 test/dfs/dune
create mode 120000 test/dfs/dune-project
create mode 100644 test/dfs/dune-workspace
delete mode 100644 test/dfs/my-rdbg-tuning.ml
create mode 120000 test/dijkstra-ring/Makefile.dot
create mode 120000 test/dijkstra-ring/Makefile.inc
create mode 120000 test/dijkstra-ring/dune
create mode 120000 test/dijkstra-ring/dune-project
create mode 100644 test/dijkstra-ring/dune-workspace
delete mode 100644 test/dijkstra-ring/ring_oracle.lus
create mode 100644 test/dune2copy
create mode 120000 test/k-clustering/Makefile.dot
create mode 120000 test/k-clustering/Makefile.inc
create mode 120000 test/k-clustering/dune
create mode 120000 test/k-clustering/dune-project
create mode 100644 test/k-clustering/dune-workspace
delete mode 100644 test/k-clustering/my-rdbg-tuning.ml
create mode 100644 test/lustre/dune-workspace
create mode 120000 test/rsp-tree/Makefile.dot
create mode 120000 test/rsp-tree/Makefile.inc
create mode 120000 test/rsp-tree/dune
create mode 120000 test/rsp-tree/dune-project
create mode 100644 test/rsp-tree/dune-workspace
delete mode 100644 test/rsp-tree/my-rdbg-tuning.ml
create mode 120000 test/skeleton/Makefile.dot
create mode 120000 test/skeleton/Makefile.inc
create mode 100644 test/skeleton/config.ml
create mode 120000 test/skeleton/dune
create mode 120000 test/skeleton/dune-project
create mode 100644 test/skeleton/dune-workspace
delete mode 100644 test/skeleton/my-rdbg-tuning.ml
create mode 120000 test/st-CYH91/Makefile.dot
create mode 120000 test/st-CYH91/Makefile.inc
create mode 120000 test/st-CYH91/dune
create mode 120000 test/st-CYH91/dune-project
create mode 100644 test/st-CYH91/dune-workspace
delete mode 100644 test/st-CYH91/my-rdbg-tuning.ml
create mode 120000 test/st-KK06-algo1/Makefile.dot
create mode 120000 test/st-KK06-algo1/Makefile.inc
create mode 120000 test/st-KK06-algo1/dune
create mode 120000 test/st-KK06-algo1/dune-project
create mode 100644 test/st-KK06-algo1/dune-workspace
delete mode 100644 test/st-KK06-algo1/my-rdbg-tuning.ml
create mode 120000 test/st-KK06-algo2/Makefile.dot
create mode 120000 test/st-KK06-algo2/Makefile.inc
create mode 120000 test/st-KK06-algo2/dune
create mode 120000 test/st-KK06-algo2/dune-project
create mode 100644 test/st-KK06-algo2/dune-workspace
delete mode 100644 test/st-KK06-algo2/my-rdbg-tuning.ml
create mode 120000 test/toy-example-a5sf/Makefile.dot
create mode 120000 test/toy-example-a5sf/Makefile.inc
create mode 120000 test/toy-example-a5sf/dune
create mode 120000 test/toy-example-a5sf/dune-project
create mode 100644 test/toy-example-a5sf/dune-workspace
delete mode 100644 test/toy-example-a5sf/my-rdbg-tuning.ml
create mode 120000 test/toy-example-sum/dune
create mode 120000 test/toy-example-sum/dune-project
create mode 100644 test/toy-example-sum/dune-workspace
delete mode 100644 test/toy-example-sum/my-rdbg-tuning.ml
create mode 120000 test/unison/Makefile.dot
create mode 120000 test/unison/Makefile.inc
create mode 120000 test/unison/dune
create mode 120000 test/unison/dune-project
create mode 100644 test/unison/dune-workspace
delete mode 100644 test/unison/my-rdbg-tuning.ml
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index dbe40f16..d480077f 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,10 +1,10 @@
-image: ocaml/opam:ubuntu-18.04
+image: ocaml/opam:ubuntu-18.04-ocaml-4.14
stages:
- build
- release
- deploy
-
+
build:
stage: build
script:
@@ -33,13 +33,13 @@ simca-docker:
paths:
- tools/simca
-
+
test_opam_test:
stage: release
script:
- opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/test/opam-repository"
- eval `opam config env`
- - sudo opam depext -y sasa
+ - sudo opam depext -y sasa
- opam install -y sasa
allow_failure: true
only:
@@ -68,7 +68,7 @@ pages:
- make odoc
- mkdir public
- cd guides/users
- - make
+ - make
- cp README.html ../../public/index.html
- cp -rf _html ../../public/
- cp -rf ../styles/ ../../public/
diff --git a/Makefile.sasa b/Makefile.sasa
index 4da8bec4..58072565 100644
--- a/Makefile.sasa
+++ b/Makefile.sasa
@@ -8,6 +8,7 @@ build: lib/sasacore/sasaVersion.ml
test:
make
cd test; make test
+ cd salut/test; make test
odoc:
dune build @doc
diff --git a/dune-project b/dune-project
index e66023f9..6af6304d 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,5 @@
-(lang dune 2.0)
+(lang dune 2.4)
(authors "Erwan Jahier")
(maintainers "Erwan Jahier")
+
diff --git a/lib/sasacore/genOracle.ml b/lib/sasacore/genOracle.ml
index 46af2265..7b42c8e9 100644
--- a/lib/sasacore/genOracle.ml
+++ b/lib/sasacore/genOracle.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/06/2022 (at 23:15) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 16:14) by Erwan Jahier> *)
open Process
@@ -10,7 +10,7 @@ let (array_to_string : bool array -> string) =
"["^(String.concat "," l)^"]"
let (matrix_to_string : bool array array -> string) =
- fun m ->
+ fun m ->
let l = Array.fold_right (fun a acc -> (array_to_string a)::acc) m [] in
"[\n\t"^(String.concat ",\n\t" l)^"]"
@@ -30,7 +30,7 @@ let already_defined = function (* some attributes may already be defined *)
| _ -> false
let graph_attributes_to_string () =
-
+
let al = Register.graph_attribute_list () in
let l = List.map
(fun (n,v) -> if not (already_defined n) then
@@ -39,9 +39,9 @@ let graph_attributes_to_string () =
in
String.concat "" l
-
-let (f: Topology.t -> 'v Process.t list -> string) =
- fun g pl ->
+
+let (f: Topology.t -> string option -> 'v Process.t list -> string) =
+ fun g output_file_name pl ->
let actions_nb = List.map (fun p -> List.length p.actions) pl in
let m = List.fold_left max (List.hd actions_nb) (List.tl actions_nb) in
let n = List.length pl in
@@ -100,7 +100,10 @@ let (f: Topology.t -> 'v Process.t list -> string) =
else
Printf.sprintf "\tConfig = [%s];\n" (String.concat "," (List.map fst vars))
in
- let algo = Filename.basename (Sys.getcwd()) in
+ let algo = match output_file_name with
+ | None -> Filename.basename (Sys.getcwd())
+ | Some str -> str
+ in
let algo = StringOf.action algo in
Printf.sprintf "%sinclude \"%s_oracle.lus\"
const an=%d; -- actions number
@@ -147,5 +150,3 @@ tel
array_def_config
algo
(if Register.get_potential () = None then "" else "potential,")
-
-
diff --git a/lib/sasacore/genOracle.mli b/lib/sasacore/genOracle.mli
index 77fc3313..5bb3b1cf 100644
--- a/lib/sasacore/genOracle.mli
+++ b/lib/sasacore/genOracle.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/07/2019 (at 16:35) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 16:14) by Erwan Jahier> *)
(** generates oracle skeletons *)
-val f: Topology.t -> 'v Process.t list -> string
+val f: Topology.t -> string option -> 'v Process.t list -> string
diff --git a/lib/sasacore/simuState.ml b/lib/sasacore/simuState.ml
index 4c984363..4f843ad7 100644
--- a/lib/sasacore/simuState.ml
+++ b/lib/sasacore/simuState.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 28/11/2022 (at 17:38) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 16:37) by Erwan Jahier> *)
open Register
open Topology
@@ -53,14 +53,14 @@ let (neigbors_of_pid : 'v t -> pid -> 's * ('s neighbor * pid) list) =
let nl =
match StringMap.find_opt pid st.neighbors with
| Some x -> x
- | None ->
+ | None ->
Printf.eprintf "no %s found in %s\n%!" pid
(String.concat "," (List.map (fun p -> p.Process.pid) st.network));
exit 2
in
Conf.get st.config pid, List.map (fun n -> n, n.Register.pid) nl
-
+
let (update_neighbor_env:
'v Conf.t -> 'v Register.neighbor list -> 'v Register.neighbor list) =
fun e nl ->
@@ -81,7 +81,7 @@ type 'v enable_processes =
let (get_enable_processes: 'v t -> 'v enable_processes) =
fun st ->
- let pl_n = List.map (fun p -> p, StringMap.find p.pid st.neighbors) st.network in
+ let pl_n = List.map (fun p -> p, StringMap.find p.pid st.neighbors) st.network in
let e = st.config in
assert (pl_n <> []);
let all = List.fold_left
@@ -115,10 +115,10 @@ let (get_enable_processes: 'v t -> 'v enable_processes) =
all, enab_ll
let (get_inputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) list) =
- fun args pl ->
+ fun args pl ->
if args.daemon <> Custom then
if args.dummy_input then ["_dummy","bool"] else []
- else
+ else
let f acc p =
List.fold_left
(fun acc a -> (p.pid ^(if a="" then "" else "_")^(StringOf.action a) ,"bool")::acc)
@@ -136,7 +136,7 @@ let (get_outputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) li
(* Adding action vars *)
let vars =
if args.daemon = Custom then vars else
- List.fold_left
+ List.fold_left
(fun acc p ->
List.fold_left
(fun acc a ->
@@ -145,11 +145,11 @@ let (get_outputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) li
(List.rev p.actions)
)
vars
- pl
+ pl
in
(* Adding enable action vars *)
- let vars =
- List.fold_left
+ let vars =
+ List.fold_left
(fun acc p ->
List.fold_left
(fun acc a ->
@@ -171,7 +171,7 @@ let (get_outputs_rif_decl: SasArg.t -> 'v Process.t list -> (string * string) li
pl
in
vars
-
+
let (env_rif_decl: SasArg.t -> 'v Process.t list -> string) =
fun args pl ->
let ssl = get_outputs_rif_decl args pl in
@@ -181,7 +181,7 @@ let (env_rif_decl: SasArg.t -> 'v Process.t list -> string) =
let (make : bool -> string array -> 'v t) =
fun dynlink argv ->
- let args =
+ let args =
try SasArg.parse argv;
with
Failure(e) ->
@@ -224,12 +224,7 @@ let (make : bool -> string array -> 'v t) =
let ml_register_file = base ^ ".ml" in
let ml_state_file = "state.ml" in
let ml_config_file = "config.ml" in
- let ml_inputs = String.concat " " algo_files in
GenRegister.f algo_files (ml_state_file, ml_config_file, ml_register_file);
- Printf.eprintf " [sasa] Hint: you may wish to generate %s out of %s with:\n"
- cmxs ml_register_file;
- Printf.eprintf " [sasa] ocamlfind ocamlopt -package algo -shared %s %s %s %s -o %s\n%!"
- ml_state_file ml_inputs ml_config_file ml_register_file cmxs;
exit 0
);
@@ -262,7 +257,7 @@ let (make : bool -> string array -> 'v t) =
else
match value_of_string_opt with
| None -> assert false (* sno *)
- | Some f -> f n.Topology.init
+ | Some f -> f n.Topology.init
)
nl
in
@@ -284,33 +279,33 @@ let (make : bool -> string array -> 'v t) =
if Sys.file_exists fn then (
Printf.eprintf " [sasa] %s already exists: rename it to proceed.\n%!" fn;
exit 1
- ) else
+ ) else
let oc = open_out fn in
- Printf.fprintf oc "%s%!" (GenLutin.f pl);
+ Printf.fprintf oc "%s%!" (GenLutin.f pl);
close_out oc;
- Printf.eprintf " [sasa] %s has been generated.\n%!" fn;
+ Printf.eprintf " [sasa] %s has been generated.\n%!" fn;
exit 0);
if args.gen_oracle then (
let fn = (Filename.remove_extension args.topo) ^ "_oracle.lus" in
if Sys.file_exists fn then (
Printf.eprintf " [sasa] %s already exists: rename it to proceed.\n%!" fn; exit 1
- ) else
+ ) else
let oc = open_out fn in
- Printf.fprintf oc "%s%!" (GenOracle.f g pl);
+ Printf.fprintf oc "%s%!" (GenOracle.f g args.output_file_name pl);
close_out oc;
- Printf.eprintf " [sasa] %s has been generated.\n%!" fn;
+ Printf.eprintf " [sasa] %s has been generated.\n%!" fn;
exit 0);
if args.no_data_file || args.quiet then () else (
let oc = if args.rif then stderr else stdout in
if !Register.verbose_level > 0 then Printf.eprintf "==> open rif file...\n%!";
- if not args.rif then
+ if not args.rif then
Printf.fprintf oc "%s" (Mypervasives.entete "#" SasaVersion.str SasaVersion.sha);
Printf.fprintf oc "#seed %i\n" seed;
- let inputs_decl = get_inputs_rif_decl args pl in
+ let inputs_decl = get_inputs_rif_decl args pl in
Printf.printf "#inputs ";
if !Register.verbose_level > 0 then
Printf.eprintf "==> get input var names...\n%!";
- List.iter (fun (vn,vt) -> Printf.printf "\"%s\":%s " vn vt) inputs_decl;
+ List.iter (fun (vn,vt) -> Printf.printf "\"%s\":%s " vn vt) inputs_decl;
Printf.printf "\n%!";
let pot = match Register.get_potential () with
| None -> ""
@@ -350,16 +345,16 @@ let (make : bool -> string array -> 'v t) =
exit 2
-
+
let (to_dot : 'v t -> string) =
- fun ss ->
+ fun ss ->
let dot_file = ss.sasarg.topo in
let g = Topology.read dot_file in
let nodes_decl =
String.concat "\n"
(List.map
(fun node ->
- Printf.sprintf " %s [algo=\"%s\" init=\"%s\"]" node.id node.file
+ Printf.sprintf " %s [algo=\"%s\" init=\"%s\"]" node.id node.file
(Register.to_string (Conf.get ss.config node.id))
)
g.nodes)
@@ -394,7 +389,7 @@ let (to_dot : 'v t -> string) =
let trans = List.sort_uniq compare trans in
let trans_str = String.concat "\n" trans in
let attributes = String.concat " " (List.map (fun (n,v) -> n^"="^v) g.attributes) in
- Printf.sprintf
+ Printf.sprintf
"%sgraph %s {\n graph %s\n\n%s\n\n%s\n}\n"
(if g.directed then "di" else "") "g"
(if attributes="" then "" else "["^attributes^"]") nodes_decl trans_str
@@ -408,7 +403,7 @@ let (compute_potentiel: 'v t -> float) =
let p = user_pf pidl (neigbors_of_pid st) in
p
-let (legitimate: 'v t -> bool) = fun st ->
+let (legitimate: 'v t -> bool) = fun st ->
match Register.get_legitimate () with
| None -> false
| Some ulf ->
diff --git a/salut/test/Makefile.inc b/salut/test/Makefile.inc
index 1b944033..e65fb7f1 100644
--- a/salut/test/Makefile.inc
+++ b/salut/test/Makefile.inc
@@ -4,7 +4,7 @@
# DECO_PATTERN # specift how to decorate (gg generated) .dot files gg-deco
# and optionnaly
# DOT2LUSFLAGS # flags for the dot to lustre translater
-# SASAFLAGS # flags for sasa
+# SASAFLAGS # flags for sasa
# TOPOLOGY # the topology used by defaukt
#
@@ -20,11 +20,12 @@ verif: $(TOPOLOGY).lus $(TOPOLOGY).cmxs $(TOPOLOGY)_verify.lv4
genclean:
rm -f *.cmxs *.cmx *.cmi *.o
- rm -f $(TOPOLOGY).ml
- rm -f *.rif *.seed *.cov rdbg-cmds.ml read_dot.ml
+ rm -f $(TOPOLOGY).ml
+ rm -f *.rif *.seed *.cov .rdbg-cmds.ml
rm -f $(TOPOLOGY).lus
rm -f *_verify.lv4 sasa-*.dot *.gp
- rm -f *.c *.h *_const.lus *.cmt *.exec *.sh rdbg-session* *.log *.pdf
+ rm -rf *.c *.h *_const.lus *.cmt *.exec *.sh luretteSession* .rdbg-session* *.log *.pdf
+ dune clean
# generating lv6 files of out dot files
%_const.lus: %.dot
@@ -44,7 +45,7 @@ RUN_KIND2=$(ROOTDIR)/salut/test/run-kind2.sh
%.simu:
make $*.dot $*_const.lus
- luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec
+ luciole-rif lv6 $(LIB_LUS) $*.lus $*_const.lus -n $* -exec
%.rdbg:
make $*.dot $*_const.lus
@@ -52,7 +53,7 @@ RUN_KIND2=$(ROOTDIR)/salut/test/run-kind2.sh
##########################################################################################"
# Use lurette to compare the lustre and the ocaml version of the algorithm
-# nb : <dirname>/<dirname>_oracle.lus should be written
+# nb : the <dirname>/<dirname>_oracle.lus should exist and contain a valid oracle
%.lurette:
make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
@@ -62,14 +63,22 @@ RUN_KIND2=$(ROOTDIR)/salut/test/run-kind2.sh
make $*.dot $*_const.lus $*.cmxs $*_oracle.lus
lurette -sut "sasa $*.dot $(SASAFLAGS)" -oracle "lv6 $(LIB_LUS) $*.lus $*_oracle.lus -n oracle -2c-exec"
-%.cmxs: %.ml
- $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
+### now built by dune
+#%.cmxs: %.ml
+# $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
+
+%.cmxs: %.dot
+ topology=$* dune build
+%.cma: %.dot
+ topology=$* dune build
+
%_oracle.lus: %.cmxs
sasa -glos $*.dot || echo ""
-%.ml: %.dot
- sasa -reg $<
+### now built by dune
+# %.ml: %.dot
+# sasa -reg $<
##########################################################################################"
@@ -101,7 +110,7 @@ endif
%.kind2:
make $*.dot
make $*_const.lus
- make $*.verify.int8.lv4
+ make $*.verify.int8.lv4
$(TIME) kind2 --color $(color) $(kind2_opt) $*.verify.int8.lv4
%.kind2-test:
@@ -119,7 +128,7 @@ endif
sed -r "s/:int/:int8/g" \
> $@
-# Do not expand nodes
+# Do not expand nodes
%_verify.noexpand.lv4: verify.lus
make $*_const.lus
lv6 -eei $(LIB_LUS) $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
@@ -144,10 +153,10 @@ endif
%.lesar:%_verify.ec
- $(TIME)lesar $< $(prop) -forward -states 10000000
+ $(TIME)lesar $< $(prop) -forward -states 10000000
##########################################################################################"
# Compare sasa and salut simulation perf
-# cf salut-vs-sasa.sh and gen-salut-batch.sh
+# cf salut-vs-sasa.sh and gen-salut-batch.sh
-include Makefile.local
diff --git a/salut/test/bfs-spanning-tree/dune-project b/salut/test/bfs-spanning-tree/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/bfs-spanning-tree/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/bfs-spanning-tree/dune-workspace b/salut/test/bfs-spanning-tree/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/coloring/dune b/salut/test/coloring/dune
new file mode 120000
index 00000000..a1ef974a
--- /dev/null
+++ b/salut/test/coloring/dune
@@ -0,0 +1 @@
+../../../test/dune2copy
\ No newline at end of file
diff --git a/salut/test/coloring/dune-project b/salut/test/coloring/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/coloring/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/coloring/dune-workspace b/salut/test/coloring/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/dijkstra-ring/dune-project b/salut/test/dijkstra-ring/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/dijkstra-ring/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/dijkstra-ring/dune-workspace b/salut/test/dijkstra-ring/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/kclustering/dune-project b/salut/test/kclustering/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/kclustering/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/kclustering/dune-workspace b/salut/test/kclustering/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/rsp_tree/dune-project b/salut/test/rsp_tree/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/rsp_tree/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/rsp_tree/dune-workspace b/salut/test/rsp_tree/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/unison/dune-project b/salut/test/unison/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/unison/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/unison/dune-workspace b/salut/test/unison/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/sasa.opam b/sasa.opam
index 0af98f78..6f74f287 100644
--- a/sasa.opam
+++ b/sasa.opam
@@ -25,7 +25,7 @@ depends: [
"psq"
"functory"
"ledit"
- "rdbg" { >= "1.194" }
+ "rdbg" { >= "1.200" }
"lustre-v6"
"lutin"
]
diff --git a/test/Makefile b/test/Makefile
index 5001d8bf..55d5a915 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -12,9 +12,9 @@ test:
cd dfs/ && make test
cd dfs-list/ && make test
cd st-CYH91/ && make test
- cd st-KK06-algo1/ && make test
- cd st-KK06-algo2/ && make test
- cd bfs-st-HC92/ && make test
+ cd st-KK06-algo1/ && make test
+ cd st-KK06-algo2/ && make test
+ cd bfs-st-HC92/ && make test
cd rsp-tree/ && make test
cd toy-example-a5sf/ && make test
cd k-clustering/ && make test
@@ -54,9 +54,9 @@ utest:
cd dfs/ && make utest
cd dfs-list/ && make utest
cd st-CYH91/ && make utest
- cd st-KK06-algo1/ && make utest
- cd st-KK06-algo2/ && make utest
- cd bfs-st-HC92/ && make utest
+ cd st-KK06-algo1/ && make utest
+ cd st-KK06-algo2/ && make utest
+ cd bfs-st-HC92/ && make utest
cd rsp-tree/ && make utest
cd toy-example-a5sf/ && make utest
cd k-clustering/ && make utest
diff --git a/test/Makefile.dot b/test/Makefile.dot
index ca52b491..18f2db37 100644
--- a/test/Makefile.dot
+++ b/test/Makefile.dot
@@ -1,8 +1,10 @@
-# Time-stamp: <modified the 26/05/2022 (at 10:28) by Erwan Jahier>
+# Time-stamp: <modified the 16/01/2023 (at 15:45) by Erwan Jahier>
# Rules to generate various dot files.
# The DECO_PATTERN variable should be defined
+.PRECIOUS: %.dot
+
grid%.dot:
gg grid -w $* -he $* -o $@ $(SEED)
gg-deco $(DECO_PATTERN) $@ -o $@
@@ -58,4 +60,4 @@ inouttree%.dot:
cleandot:
- rm -f ring5* ring30* er30* er100* grid* ba100* udg* qudg*
+ rm -f ring5* ring30* er30* er100* grid* ba100* udg* qudg*
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 3c3c06a2..19a775c4 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 22/06/2022 (at 21:33) by Erwan Jahier>
+# Time-stamp: <modified the 18/01/2023 (at 11:33) by Erwan Jahier>
#
# Define some default rules that ought to work most of the time
#
@@ -6,38 +6,51 @@
sasa=sasa
LIB=-package algo
+
ifndef DAEMON
+# some rules uses this one
DAEMON=-dd
endif
-OCAMLOPT=ocamlfind ocamlopt -bin-annot
-%.ml: %.dot
- sasa -reg $<
-%.cmxs: %.ml
- $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
+# obselete: use 'dune build' instead
+#%.ml: %.dot
+# sasa -reg $<
+
+# ifndef OCAMLOPT
+# OCAMLOPT=ocamlfind ocamlopt -bin-annot
+# endif
+#%.cmxs: %.ml
+# $(OCAMLOPT) $(LIB) -shared state.ml $(shell sasa -algo $*.dot) config.ml $< -o $@
+# ifndef OCAMLC
+# OCAMLC=ocamlfind ocamlc -bin-annot
+# endif
+# %.cma: %.ml
+# $(OCAMLC) $(LIB) -a state.ml $(shell sasa -algo $*.dot) $< -o $@
+
+%.cmxs: %.dot
+ topology=$* dune build
+%.cma: %.dot
+ topology=$* dune build
+
genclean:
rm -f *.cmxs sasa *.cm* *.o *.pdf *.rif *.gp *.log *.dro *.seed *.c *.h sasa-*.dot *.cmt *.annot
- rm -f rdbg-session*.ml luretteSession* a.out *.cov read_dot.ml
- rm -f *.exec grid*.ml read_dot.ml rdbg-history rdbg-cmds.ml
+ rm -rf .rdbg-session*.ml luretteSession* a.out *.cov .read_dot.ml
+ rm -f *.exec grid*.ml rdbg-history .rdbg-cmds.ml
+ dune clean
clean: genclean
.PRECIOUS: %.ml
-
-
##################################################################################
-#
+#
-include Makefile.untracked
g:gnuplot
s:sim2chrogtk
-OCAMLC=ocamlfind ocamlc -bin-annot
-%.cma: %.ml
- $(OCAMLC) $(LIB) -a state.ml $(shell sasa -algo $*.dot) $< -o $@
%.lut: %.dot %.cmxs
sasa -gld $< || echo "==> ok, I'll use the existing $@ file"
@@ -65,27 +78,27 @@ EXPDIR=`rdbg --ocaml-version`
$(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
-%.gm_test: %.dot %.cmxs $(EXPDIR)
- sasa $< -seed 42 > $*.rif && \
+%.gm_test: %.cmxs $(EXPDIR)
+ sasa $*.dot -seed 42 > $*.rif && \
diff -I "# on" -I " version " -B -u -i -w $(EXPDIR)/$*.rif.exp $*.rif > $*.res
[ ! -s $*.res ] && echo "\n\n==> $*.gm_test went fine"
# update the reference
-%.ugm_test: %.dot %.cmxs $(EXPDIR)
- sasa $< -seed 42 > $*.rif && \
+%.ugm_test: %.cmxs $(EXPDIR)
+ sasa $*.dot -seed 42 > $*.rif && \
cp $*.rif $(EXPDIR)/$*.rif.exp
-# fix the seed (in Makefile.dot) for the non-regression tests
-SEED=--seed 42
-
+# fix the seed (used, e.g., in Makefile.dot) for the non-regression tests
+ifndef SEED
+ SEED=--seed 42
+endif
############################################################################################
-
-%.rdbg: %.dot %.ml
+%.rdbg: %.dot
ledit -h rdbg-history -x rdbg --sasa -sut "sasa $< $(DAEMON)" -l 500
-%.rdbg-test: %.dot %.ml
- rdbg --sasa -sut "sasa $< $(DAEMON)" -go --input some_session -l 500
+%.rdbg-test: %.cma
+ rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 500
-%.rdbgui: %.dot %.ml
- rdbgui4sasa -sut "sasa $< $(DAEMON)"
+%.rdbgui: %.cma
+ rdbgui4sasa -sut "sasa $*.dot $(DAEMON)"
diff --git a/test/alea-coloring-alt/Makefile b/test/alea-coloring-alt/Makefile
index 1c5ed2ea..687b288a 100644
--- a/test/alea-coloring-alt/Makefile
+++ b/test/alea-coloring-alt/Makefile
@@ -1,9 +1,9 @@
-# Time-stamp: <modified the 11/06/2022 (at 14:59) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier>
-DECO_PATTERN="0-:algo_331.ml"
+DECO_PATTERN="0-:algo_331.ml"
DAEMON=-sd
--include ../Makefile.dot
--include ../Makefile.inc
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
@@ -22,8 +22,8 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
grid44.dot:
gg grid -w 4 -he 4 -o grid44.dot
diff --git a/test/alea-coloring-alt/Makefile.dot b/test/alea-coloring-alt/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/alea-coloring-alt/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/alea-coloring-alt/Makefile.inc b/test/alea-coloring-alt/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/alea-coloring-alt/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/alea-coloring-alt/dune b/test/alea-coloring-alt/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/alea-coloring-alt/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/alea-coloring-alt/dune-project b/test/alea-coloring-alt/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/alea-coloring-alt/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/alea-coloring-alt/dune-workspace b/test/alea-coloring-alt/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/alea-coloring-alt/my-rdbg-tuning.ml b/test/alea-coloring-alt/my-rdbg-tuning.ml
deleted file mode 100644
index 0e95c817..00000000
--- a/test/alea-coloring-alt/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-
-
-
-
-
diff --git a/test/alea-coloring-alt/p.ml b/test/alea-coloring-alt/p.ml
index b64c2f1e..33e9f740 100644
--- a/test/alea-coloring-alt/p.ml
+++ b/test/alea-coloring-alt/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 22/04/2020 (at 10:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier> *)
(* A variant of test/alea-coloring:
@@ -37,7 +37,7 @@ let (free : 'v neighbor list -> 'v list) = fun nl ->
let res = aux [] n_colors 0 in
List.rev res
-let agree_i ri vl =
+let agree_i ri nl =
ri = List.hd (free nl)
let (enable_f: 'v -> 'v neighbor list -> action list) =
@@ -47,6 +47,3 @@ let (enable_f: 'v -> 'v neighbor list -> action list) =
let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
fun e nl _ ->
if (Random.bool ()) then e else (List.hd (free nl))
-
-
-
diff --git a/test/alea-coloring-unif/Makefile b/test/alea-coloring-unif/Makefile
index 05842506..2fd1e73f 100644
--- a/test/alea-coloring-unif/Makefile
+++ b/test/alea-coloring-unif/Makefile
@@ -1,14 +1,14 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:00) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier>
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
# Non-regression tests
-test: ring.cmxs
+test: ring.cmxs
sasa -l 200 ring.dot && make clean
utest: clean
clean: genclean
@@ -20,9 +20,9 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
-rdbg: ring.ml ring.lut
+rdbg: ring.ml ring.lut
rdbg -o ring.rif \
- -env "$(sasa) g.dot -cd"
+ -env "$(sasa) g.dot -cd"
diff --git a/test/alea-coloring-unif/Makefile.dot b/test/alea-coloring-unif/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/alea-coloring-unif/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/alea-coloring-unif/Makefile.inc b/test/alea-coloring-unif/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/alea-coloring-unif/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/alea-coloring-unif/dune b/test/alea-coloring-unif/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/alea-coloring-unif/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/alea-coloring-unif/dune-project b/test/alea-coloring-unif/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/alea-coloring-unif/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/alea-coloring-unif/dune-workspace b/test/alea-coloring-unif/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/alea-coloring-unif/my-rdbg-tuning.ml b/test/alea-coloring-unif/my-rdbg-tuning.ml
deleted file mode 100644
index 35c216cd..00000000
--- a/test/alea-coloring-unif/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/alea-coloring/Makefile b/test/alea-coloring/Makefile
index ec5339c8..68155fc4 100644
--- a/test/alea-coloring/Makefile
+++ b/test/alea-coloring/Makefile
@@ -1,20 +1,20 @@
-# Time-stamp: <modified the 11/06/2022 (at 14:59) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:34) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
DAEMON=-sd
--include ../Makefile.dot
--include ../Makefile.inc
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
# Non-regression tests
-test: ring.cmxs test_rdbg
+test: ring.cmxs test_rdbg
$(sasa) -l 200 ring.dot -cd && make clean
utest: clean
# Interactive session with internal deamons
-test_rdbg: ring.lut ring.ml
+test_rdbg: ring.lut ring.cma
rdbg --sasa -o ring.rif -env "$(sasa) ring.dot -dd" -go --input some_session
clean: genclean
@@ -26,8 +26,8 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
# Interactive session with lutin
rdbg: ring.lut ring.ml
@@ -36,5 +36,5 @@ rdbg: ring.lut ring.ml
-sut-nd "lutin ring.lut -n distributed"
-rdbg3: ring.ml
+rdbg3: ring.ml
rdbg --sasa -o ring.rif -sut "$(sasa) ring.dot -cd -rif"
diff --git a/test/alea-coloring/Makefile.dot b/test/alea-coloring/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/alea-coloring/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/alea-coloring/Makefile.inc b/test/alea-coloring/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/alea-coloring/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/alea-coloring/dune b/test/alea-coloring/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/alea-coloring/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/alea-coloring/dune-project b/test/alea-coloring/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/alea-coloring/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/alea-coloring/dune-workspace b/test/alea-coloring/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/alea-coloring/my-rdbg-tuning.ml b/test/alea-coloring/my-rdbg-tuning.ml
deleted file mode 100644
index a2caa834..00000000
--- a/test/alea-coloring/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/async-unison/Makefile b/test/async-unison/Makefile
index d0338d27..ab36c51c 100644
--- a/test/async-unison/Makefile
+++ b/test/async-unison/Makefile
@@ -1,8 +1,8 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:06) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:28) by Erwan Jahier>
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
@@ -20,9 +20,9 @@ utest: ring.cmxs
lurette: ring.cmxs ring_oracle.lus
lurette -o ring.rif -l 10000 \
-sut "sasa -rif ring.dot -cd" \
- -oracle "lv6 -2c-exec ring_oracle.lus -n oracle"
+ -oracle "lv6 -2c-exec ring_oracle.lus -n oracle"
-rdbg_test: ring.ml
+rdbg_test: ring.cma
rdbg --sasa -o ring.rif -l 10000 -env "$(sasa) -vl 1 ring.dot -cd" -go --input some_session
clean: genclean
@@ -30,21 +30,21 @@ clean: genclean
##############################################################################
# Other examples of use
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
rdbg: ring.ml
- rdbg --sasa -o ring.rif -l 10000 -env "sasa -vl 1 ring.dot -cd"
+ rdbg --sasa -o ring.rif -l 10000 -env "sasa -vl 1 ring.dot -cd"
rdbgui: ring.ml
- rdbgui4sasa -o ring.rif -l 10000 -env "sasa -vl 1 ring.dot -cd"
+ rdbgui4sasa -o ring.rif -l 10000 -env "sasa -vl 1 ring.dot -cd"
rdbg4: grid4.ml
rdbg --sasa -o ring.rif -l 10000 \
- -env "sasa grid4.dot -dd"
+ -env "sasa grid4.dot -dd"
rdbgl: ring4.cmxs
rdbg -lurette --sasa -o lurette-ring.rif \
diff --git a/test/async-unison/Makefile.dot b/test/async-unison/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/async-unison/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/async-unison/Makefile.inc b/test/async-unison/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/async-unison/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/async-unison/dune b/test/async-unison/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/async-unison/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/async-unison/dune-project b/test/async-unison/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/async-unison/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/async-unison/dune-workspace b/test/async-unison/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/async-unison/my-rdbg-tuning.ml b/test/async-unison/my-rdbg-tuning.ml
deleted file mode 100644
index 35c216cd..00000000
--- a/test/async-unison/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/async-unison/p.ml b/test/async-unison/p.ml
index f84148af..4df34f8a 100644
--- a/test/async-unison/p.ml
+++ b/test/async-unison/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/04/2022 (at 17:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:26) by Erwan Jahier> *)
(* Couvreur, J., Francez, N., and Gouda, M. G. (1992) Asynchronous
unison (extended abstract). Proceedings of the 12th International
@@ -11,7 +11,7 @@ let k = n * n + 1
let (init_state: int state_init_fun) = fun _n _ -> (Random.int k)
-let modulo x n = if x < 0 then n+x mod n else x mod n
+let modulo x n = if x < 0 then n+x mod n else x mod n
let behind pc qc = (modulo (qc-pc) k) <= n
@@ -23,9 +23,8 @@ let (enable_f: int enable_fun) =
&& c <> 0 then ["R(p)"] else []
let (step_f: int step_fun) =
- fun c nl a ->
+ fun c _nl a ->
match a with
| "I(p)" -> modulo (c + 1) k
- | "R(p)" -> 0
+ | "R(p)" -> 0
| _ -> assert false
-
diff --git a/test/async-unison/async_unison_oracle.ml b/test/async-unison/rdbg/async_unison_oracle.ml
similarity index 100%
rename from test/async-unison/async_unison_oracle.ml
rename to test/async-unison/rdbg/async_unison_oracle.ml
diff --git a/test/bfs-spanning-tree/Makefile b/test/bfs-spanning-tree/Makefile
index fb84eaaf..6f338974 100644
--- a/test/bfs-spanning-tree/Makefile
+++ b/test/bfs-spanning-tree/Makefile
@@ -1,8 +1,8 @@
-# Time-stamp: <modified the 05/12/2022 (at 10:24) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 13:46) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
@@ -17,16 +17,16 @@ utest: fig51_noinit.cmxs
$(sasa) -rif -l 200 fig51_noinit.dot -sd -seed 42 > fig51_noinit.rif && \
cp fig51_noinit.rif fig51_noinit.rif.exp ; true
-test0: fig51_noinit.cmxs
-test2: fig51.cmxs
+test0: fig51_noinit.cmxs
+test2: fig51.cmxs
$(sasa) -l 200 fig51.dot -sd
-lurette0: fig51_noinit.cmxs fig51_noinit.lut fig51_noinit_oracle.lus
+lurette0: fig51_noinit.cmxs fig51_noinit.lut
lurette --sasa -o lurette.rif \
-env "sasa fig51_noinit.dot -dd -rif -seed 42" \
-oracle "lv6 fig51_noinit_oracle.lus -n oracle"
-test_rdbg: fig51_noinit.ml fig51_noinit.lut
+test_rdbg: fig51_noinit.cma fig51_noinit.lut
rdbg --sasa -sut "sasa fig51_noinit.dot " -go --input some_session
clean: genclean
@@ -42,11 +42,11 @@ lutin: fig51_noinit.cmxs
sim2chrogtk: fig51_noinit.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: fig51_noinit.rif
- gnuplot-rif $<
+gnuplot: fig51_noinit.rif
+ gnuplot-rif $<
-gnuplot2: fig52.rif
- gnuplot-rif $<
+gnuplot2: fig52.rif
+ gnuplot-rif $<
rdbg-lurette1:rdbg-lurette1.rif
rdbg-lurette1.rif: fig51.cmxs fig51.lut fig51_oracle.lus
@@ -66,7 +66,7 @@ lurette: lurette0
rdbgui: fig51_noinit.ml fig51_noinit.lut fig51_noinit_oracle.lus
rdbgui4sasa -sut "sasa -seed 42 fig51_noinit.dot -dd " \
- -oracle-nd "lv6 fig51_noinit_oracle.lus -n oracle"
+ -oracle-nd "lv6 fig51_noinit_oracle.lus -n oracle"
rdbg2: fig51.ml fig51.lut
rdbg --sasa -o lurette.rif \
@@ -78,4 +78,4 @@ manual: fig51_noinit.cmxs fig51_noinit.lut
lurette --sasa -o lurette.rif --sim2chro \
-sut "$(sasa) fig51_noinit.dot -custd -rif -ifi" \
-env "lutin fig51_noinit.lut -n manual" &&\
- gnuplot-rif lurette.rif
+ gnuplot-rif lurette.rif
diff --git a/test/bfs-spanning-tree/Makefile.dot b/test/bfs-spanning-tree/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/bfs-spanning-tree/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/Makefile.inc b/test/bfs-spanning-tree/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/bfs-spanning-tree/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/dune b/test/bfs-spanning-tree/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/bfs-spanning-tree/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/dune-project b/test/bfs-spanning-tree/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/bfs-spanning-tree/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/bfs-spanning-tree/dune-workspace b/test/bfs-spanning-tree/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/bfs-spanning-tree/my-rdbg-tuning.ml b/test/bfs-spanning-tree/my-rdbg-tuning.ml
deleted file mode 100644
index 19e0625c..00000000
--- a/test/bfs-spanning-tree/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
diff --git a/test/bfs-spanning-tree/root.ml b/test/bfs-spanning-tree/root.ml
index dc0aea30..a307f8be 100644
--- a/test/bfs-spanning-tree/root.ml
+++ b/test/bfs-spanning-tree/root.ml
@@ -1,22 +1,21 @@
-(* Time-stamp: <modified the 05/03/2020 (at 21:41) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 17:07) by Erwan Jahier> *)
(* This is algo 5.3 in the book *)
open Algo
open State
-
+
let (init_state: int -> string -> State.t) =
- fun i _ ->
+ fun _i _ ->
{
d = Random.int d;
par = -1;
- }
-
+ }
+
let (enable_f: State.t -> State.t neighbor list -> action list) =
- fun st nl ->
+ fun st _nl ->
if st.d <> 0 then ["CD"] else []
-
+
let (step_f : State.t -> State.t neighbor list -> action -> State.t) =
fun st _nl ->
function | _ -> { st with d = 0 }
-
diff --git a/test/bfs-st-HC92/Makefile b/test/bfs-st-HC92/Makefile
index cb4b5f16..b7a58b11 100644
--- a/test/bfs-st-HC92/Makefile
+++ b/test/bfs-st-HC92/Makefile
@@ -1,6 +1,6 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:03) by Erwan Jahier>
+# Time-stamp: <modified the 18/01/2023 (at 10:53) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
+DECO_PATTERN="0:root.ml 1-:p.ml"
-include ../Makefile.dot
-include ../Makefile.inc
-include Makefile.untracked
@@ -9,14 +9,14 @@ DECO_PATTERN="0:root.ml 1-:p.ml"
# Non-regression tests
test: test0 lurette rdbg_test clean
-test0: ring.cmxs
+test0: ring.cmxs
sasa -l 200 ring.dot
utest:clean
-lurette: grid4.cmxs
+lurette: grid4.cmxs
lurette --sasa -o rdbg.rif -sut "sasa -rif grid4.dot" -l 1000
-rdbg_test : grid4.ml
+rdbg_test : grid4.cma
rdbg --sasa -o rdbg.rif -sut "sasa grid4.dot" -l 1000 -go --input some_session
clean: genclean
@@ -28,19 +28,19 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
ocd: grid4.ml grid4.cma
rdbg --sasa --ocamldebug -sut "sasa grid4.dot" -l 1000
-rdbg: grid4.ml
+rdbg: grid4.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid4.dot" -l 1000
-rdbg10: grid10.ml
+rdbg10: grid10.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid10.dot" -l 1000
-rdbg-ring: ring.ml
+rdbg-ring: ring.ml
rdbg --sasa -o rdbg.rif -sut "sasa ring.dot" -l 1000
ER-1000.dot:
diff --git a/test/bfs-st-HC92/Makefile.dot b/test/bfs-st-HC92/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/bfs-st-HC92/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/bfs-st-HC92/Makefile.inc b/test/bfs-st-HC92/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/bfs-st-HC92/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/bfs-st-HC92/dune b/test/bfs-st-HC92/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/bfs-st-HC92/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/bfs-st-HC92/dune-project b/test/bfs-st-HC92/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/bfs-st-HC92/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/bfs-st-HC92/dune-workspace b/test/bfs-st-HC92/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index b0b0d7d9..e8c8b940 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,11 +1,11 @@
-# Time-stamp: <modified the 22/06/2022 (at 10:56) by Erwan Jahier>
+# Time-stamp: <modified the 16/01/2023 (at 10:43) by Erwan Jahier>
sasa=$(DIR)/bin/sasa -l 100
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
@@ -20,7 +20,7 @@ utest:
lurette: ring.cmxs ring_oracle.lus
lurette --sasa -o lurette-ring.rif \
-sut "sasa ring.dot -rif -lcd -seed 42" \
- -oracle "lv6 ring_oracle.lus -n oracle -exec"
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
clean: genclean
rm -f ring.lut ring.ml ring_oracle.ml
@@ -31,28 +31,28 @@ clean: genclean
sim2chrogtk: coloring.rif
sim2chrogtk -screenrealheight 2000 -ecran -in $< > /dev/null
-gnuplot: coloring.rif
- gnuplot-rif $<
+gnuplot: coloring.rif
+ gnuplot-rif $<
# do not work with ocaml >3.08
rdbg-lurette: ring.cmxs ring_oracle.lus
rdbg -lurette --sasa -o lurette-ring.rif \
-sut "sasa ring.dot -rif -lcd " \
- -oracle "lv6 ring_oracle.lus -n oracle -exec"
+ -oracle "lv6 ring_oracle.lus -n oracle -exec"
test100:
for i in $$(seq 100); do make lurette && make clean; done
rdbg: grid4.ml
echo "" > include.ml
- ledit rdbg --sasa -sut "sasa grid4.dot --locally-central-daemon"
+ ledit rdbg --sasa -sut "sasa grid4.dot --locally-central-daemon"
rdbgui: grid4.ml
echo "" > include.ml
- rdbgui4sasa -sut "sasa grid4.dot --locally-central-daemon"
+ rdbgui4sasa -sut "sasa grid4.dot --locally-central-daemon"
rdbgui-demo: grid10.ml
echo "" > include.ml
- rdbgui4sasa -sut "sasa grid10.dot --central-daemon"
+ rdbgui4sasa -sut "sasa grid10.dot --central-daemon"
rdbg-luciole: grid4.ml
echo "" > include.ml
@@ -60,12 +60,12 @@ rdbg-luciole: grid4.ml
rdbgui-custd: grid4.ml
echo "" > include.ml
- rdbgui4sasa -sut "sasa -rif grid4.dot --custom-daemon"
+ rdbgui4sasa -sut "sasa -rif grid4.dot --custom-daemon"
rdbg3: ring.ml
echo "" > include.ml
- ledit rdbg --sasa -sut "sasa ring.dot -wd"
+ ledit rdbg --sasa -sut "sasa ring.dot -wd"
rdbg1: ring.ml ring_oracle.lus
echo "" > include.ml
@@ -73,13 +73,11 @@ rdbg1: ring.ml ring_oracle.lus
-sut "sasa --replay ring.dot -rif -lcd " \
-oracle "lv6 ring_oracle.lus -n oracle -exec"
-rdbg2: ring.cmxs ring.lut
+rdbg2: ring.cmxs ring.lut
echo "" > include.ml
ledit rdbg --sasa -o ring.rif \
-env "$(sasa) --replay ring.dot -custd -rif" \
- -sut-nd "lutin ring.lut -n distributed"
+ -sut-nd "lutin ring.lut -n distributed"
rdbg4: ring.ml
ledit rdbg --sasa -o ring.rif -env "sasa ring.dot -custd "
-
-
diff --git a/test/coloring/Makefile.dot b/test/coloring/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/coloring/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/coloring/Makefile.inc b/test/coloring/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/coloring/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index 668b2f0d..53ef2bb6 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/test/coloring/coloring_oracle.lus
@@ -1,11 +1,12 @@
include "../lustre/oracle_utils.lus"
+type state = int;
-----------------------------------------------------------------------------
--- Lemma 3.14 The execution e terminates after at most n-1 moves
+-- Lemma 3.14 The execution e terminates after at most n-1 moves
-- (under a Locally Central demon).
node lemma_3_14<<const an:int; const pn: int>> (legitimate: bool; Enab, Acti: bool^an^pn) returns (res:bool;MoveNb:int);
---var
+--var
-- MoveNb:int;
let
MoveNb = move_count(Acti);
@@ -23,11 +24,11 @@ tel
node coloring_oracle<<const an:int; const pn:int>> (legitimate: bool; potential:real; Enab, Acti: bool^an^pn;
config:int^pn; round:bool; round_nb:int)
-returns (res:bool; move_nb:int);
-var res0:bool;
+returns (res:bool);
+var res0:bool; move_nb:int;
let
res0, move_nb = lemma_3_14<<an,pn>>(legitimate, Enab,Acti);
- res = theorem_3_17<<an,pn>>(Enab,Acti, round_nb)
+ res = theorem_3_17<<an,pn>>(Enab,Acti, round_nb)
and res0
;
tel
diff --git a/test/coloring/config.ml b/test/coloring/config.ml
index 11a5d814..2a6fba53 100644
--- a/test/coloring/config.ml
+++ b/test/coloring/config.ml
@@ -17,7 +17,7 @@ let fault = None
let md = max_degree ()
let s2n s = [I (0, s, md)]
-let n2s nl s =
+let n2s nl _s =
match nl with
| [I(_, i, _)] -> i
| _ -> assert false
diff --git a/test/coloring/dune b/test/coloring/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/coloring/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/coloring/dune-project b/test/coloring/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/coloring/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/coloring/dune-workspace b/test/coloring/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/coloring/my-rdbg-tuning.ml b/test/coloring/my-rdbg-tuning.ml
deleted file mode 100644
index b7eaf703..00000000
--- a/test/coloring/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,12 +0,0 @@
-(* *)
-
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-#use "include.ml";;
-
-let _ =
- del_hook "print_event";
- add_hook "print_event" (print_event)
-
-let pp () = List.assoc "potential" !e.data;;
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
deleted file mode 100644
index 7a256c5d..00000000
--- a/test/coloring/ring_oracle.lus
+++ /dev/null
@@ -1,43 +0,0 @@
--- Automatically generated by /home/jahier/.opam/4.13.1/bin/sasa version "v4.6.0" ("169b4f7")
--- on crevetete the 22/6/2022 at 10:52:23
---sasa -glos ring.dot
-
-include "coloring_oracle.lus"
-const an=1; -- actions number
-const pn=7; -- processes number
-const max_degree=2;
-const min_degree=2;
-const mean_degree=2.000000;
-const diameter=3;
-const card=7;
-const links_number=7;
-const is_cyclic=true;
-const is_connected=true;
-const is_a_tree=false;
-const f=false;
-const t=true;
-const adjacency=[
- [f,t,f,f,f,f,t],
- [t,f,t,f,f,f,f],
- [f,t,f,t,f,f,f],
- [f,f,t,f,t,f,f],
- [f,f,f,t,f,t,f],
- [f,f,f,f,t,f,t],
- [t,f,f,f,f,t,f]];
-
-node oracle(legitimate:bool;potential:real;
- p1_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;
- Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict:bool;
- p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict:bool;round:bool; round_nb:int)
-returns (ok:bool; move_nb:int);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- Config:p1_c^7;
-let
- Acti = [[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict]];
- Enab = [[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict]];
- Config = [p1_c,p2_c,p3_c,p4_c,p5_c,p6_c,p7_c];
-
- ok,move_nb = coloring_oracle(legitimate,potential, Enab, Acti, Config, round, round_nb);
-tel
diff --git a/test/dfs-list/Makefile b/test/dfs-list/Makefile
index aca52433..38ec0262 100644
--- a/test/dfs-list/Makefile
+++ b/test/dfs-list/Makefile
@@ -1,9 +1,9 @@
-# Time-stamp: <modified the 30/05/2022 (at 14:39) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:44) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
-include Makefile.untracked
--include ../Makefile.inc
+-include ./Makefile.inc
##############################################################################
# Non-regression tests
@@ -26,13 +26,13 @@ lurette: lurette0
sim2chrogtk: g.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: g.rif
- gnuplot-rif $<
+gnuplot: g.rif
+ gnuplot-rif $<
rdbg: g.ml
- rdbg --sasa -o lurette.rif -env "sasa g.dot -rif"
+ rdbg --sasa -o lurette.rif -env "sasa g.dot -rif"
rdbgui: g.ml
- rdbgui4sasa -o lurette.rif -env "sasa g.dot -rif"
+ rdbgui4sasa -o lurette.rif -env "sasa g.dot -rif"
rdbg2: g.ml g.lut
rdbg --sasa -o lurette.rif \
@@ -42,4 +42,3 @@ rdbg2: g.ml g.lut
clean: genclean
rm -f g.ml
-
diff --git a/test/dfs-list/Makefile.dot b/test/dfs-list/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/dfs-list/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/dfs-list/Makefile.inc b/test/dfs-list/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/dfs-list/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/dfs-list/dune b/test/dfs-list/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/dfs-list/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/dfs-list/dune-project b/test/dfs-list/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/dfs-list/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/dfs-list/dune-workspace b/test/dfs-list/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/dfs-list/p.ml b/test/dfs-list/p.ml
index e7c178f4..bb02de81 100644
--- a/test/dfs-list/p.ml
+++ b/test/dfs-list/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/03/2020 (at 21:27) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:44) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
@@ -19,15 +19,15 @@ let min_path al =
let (get_paths: 'v neighbor list -> int list list) =
fun nl ->
- List.map (fun n -> (state n).path) nl
-
+ List.map (fun n -> (state n).path) nl
+
(* concat or truncate *)
let (concat_path : int list -> int -> int list) =
fun l alpha ->
let l = if List.length l = delta then (List.tl l) else l
in
- l@[alpha]
-
+ l@[alpha]
+
let is_sub_list l1 l2 = (List.rev (List.tl (List.rev l2))) = l1
let (compute_parent : State.t neighbor list -> int list -> int) =
@@ -36,10 +36,10 @@ let (compute_parent : State.t neighbor list -> int list -> int) =
subpath of p *)
let paths = List.mapi (fun i n -> (state n).path, i) nl in
let _,parent =
- match
+ match
List.find_opt
(fun (npath, _) ->
- is_sub_list npath p
+ is_sub_list npath p
)
paths
with
@@ -48,22 +48,22 @@ let (compute_parent : State.t neighbor list -> int list -> int) =
in
parent
-let compute_path nl e =
+let compute_path nl _e =
let paths = get_paths nl in
let paths = List.map2 (fun p n -> concat_path p (reply n)) paths nl in
let path = min_path paths in
path
-
+
let (enable_f: 'v -> 'v neighbor list -> action list) =
fun v nl ->
(*
- Printf.eprintf " compute_path %d \n" (List.length nl) ; flush stderr;
- let p_str = array_to_string v.path in
+ Printf.eprintf " compute_path %d \n" (List.length nl) ; flush stderr;
+ let p_str = array_to_string v.path in
Printf.eprintf " p=[%s] parent=%d \n" p_str v.par ;
- List.iter (fun n ->
- let n_str = array_to_string (state n).path in
- Printf.eprintf " n=[%s] parent=%d\n" n_str (state n).par
- ) nl ; flush stderr;
+ List.iter (fun n ->
+ let n_str = array_to_string (state n).path in
+ Printf.eprintf " n=[%s] parent=%d\n" n_str (state n).par
+ ) nl ; flush stderr;
*)
let path = compute_path nl v in
if path <> v.path then ["update_path"] else
@@ -71,7 +71,7 @@ let (enable_f: 'v -> 'v neighbor list -> action list) =
else []
let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
- fun v nl ->
+ fun v nl ->
function
| "update_path" ->
let path = compute_path nl v in
@@ -79,6 +79,3 @@ let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
| "compute_parent" ->
{ v with par = compute_parent nl v.path }
| _ -> assert false
-
-
-
diff --git a/test/dfs-list/root.ml b/test/dfs-list/root.ml
index 4cd61965..49b5876c 100644
--- a/test/dfs-list/root.ml
+++ b/test/dfs-list/root.ml
@@ -1,12 +1,12 @@
-(* Time-stamp: <modified the 05/03/2020 (at 21:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:43) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
open State
-
+
let (init_state: int -> string -> 'v) =
- fun i _ ->
+ fun _i _ ->
{
path = [-1];
par = -10
@@ -16,9 +16,9 @@ let (enable_f: 'v -> 'v neighbor list -> action list) =
fun v _nl ->
if v.path = [-1] then [] else ["update_path"]
-
+
let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
- fun v nl ->
+ fun v _nl ->
function
| "update_path" -> { v with path = [-1] }
| _ -> assert false
diff --git a/test/dfs/Makefile b/test/dfs/Makefile
index a0c02306..3f7a8e41 100644
--- a/test/dfs/Makefile
+++ b/test/dfs/Makefile
@@ -1,10 +1,10 @@
-# Time-stamp: <modified the 30/05/2022 (at 14:39) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
-include Makefile.untracked
--include ../Makefile.inc
+-include ./Makefile.inc
##############################################################################
# Non-regression tests
@@ -16,7 +16,7 @@ utest:
make g.ugm_test || echo "g ok"
make ER.ugm_test || echo "ER ok"
-lurette0.rif: g.cmxs g.lut
+lurette0.rif: g.cmxs g.lut
lurette --sasa -o $@ \
-env "sasa -seed 42 g.dot -custd -rif" \
-sut "lutin -seed 42 g.lut -n distributed"
@@ -30,8 +30,8 @@ clean: genclean
sim2chrogtk: g.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: g.rif
- gnuplot-rif $<
+gnuplot: g.rif
+ gnuplot-rif $<
lurette: lurette0.rif
sim2chrogtk -ecran -in lurette0.rif > /dev/null
@@ -48,9 +48,3 @@ rdbg2: g.lut g.ml
rdbg --sasa -o lurette.rif \
-env "$(sasa) g.dot -rif" \
-sut-nd "lutin g.lut -n dummy"
-
-
-
-
-
-
diff --git a/test/dfs/Makefile.dot b/test/dfs/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/dfs/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/dfs/Makefile.inc b/test/dfs/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/dfs/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/dfs/dune b/test/dfs/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/dfs/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/dfs/dune-project b/test/dfs/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/dfs/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/dfs/dune-workspace b/test/dfs/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/dfs/my-rdbg-tuning.ml b/test/dfs/my-rdbg-tuning.ml
deleted file mode 100644
index 35c216cd..00000000
--- a/test/dfs/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/dfs/p.ml b/test/dfs/p.ml
index 483d5c8a..fa3d17db 100644
--- a/test/dfs/p.ml
+++ b/test/dfs/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/03/2020 (at 21:43) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:41) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
@@ -23,7 +23,7 @@ let min_path al =
let (get_paths: 'v neighbor list -> int array list) =
fun nl ->
- List.mapi (fun alpha_i n -> (state n).path) nl
+ List.mapi (fun _alpha_i n -> (state n).path) nl
(* The index of the first negative elt in [a] starting from 1. Returns
the size of the [a] if none is found *)
@@ -31,7 +31,7 @@ let end_of_a a =
let s = Array.length a in
let rec aux a i =
if i=s then s else
- if a.(i) < 0 then i else aux a (i+1)
+ if a.(i) < 0 then i else aux a (i+1)
in
let res = aux a 1 in
res
@@ -41,8 +41,8 @@ let _ = (
)
(* concat or truncate:
- concat [i;j;k;-1;...] l = [i;j;k;l;-1;...]
- concat [i;j;k;] l = [j;k;l]
+ concat [i;j;k;-1;...] l = [i;j;k;l;-1;...]
+ concat [i;j;k;] l = [j;k;l]
*)
let (concat_path : int array -> int -> int array) =
fun a alpha ->
@@ -84,10 +84,10 @@ let (compute_parent : t neighbor list -> int array -> int) =
let last_p = end_of_a p in
let paths = List.mapi (fun i n -> (state n).path, i) nl in
let _,parent =
- match
+ match
List.find_opt
(fun (npath, _) ->
- let last_n = end_of_a npath in
+ let last_n = end_of_a npath in
last_n = last_p-1 && equals_up_to npath p (last_n-1)
)
paths
@@ -97,12 +97,12 @@ let (compute_parent : t neighbor list -> int array -> int) =
in
parent
-let compute_path nl e =
+let compute_path nl _e =
let paths = get_paths nl in
let paths = List.map2 (fun p n -> concat_path p (reply n)) paths nl in
let path = min_path paths in
path
-
+
let (enable_f: t -> t neighbor list -> action list) =
fun v nl ->
let path = compute_path nl v in
@@ -111,7 +111,7 @@ let (enable_f: t -> t neighbor list -> action list) =
else []
let (step_f : t -> t neighbor list -> action -> t) =
- fun v nl ->
+ fun v nl ->
function
| "update_path" ->
let path = compute_path nl v in
@@ -120,5 +120,3 @@ let (step_f : t -> t neighbor list -> action -> t) =
let path = compute_path nl v in
{ v with par = compute_parent nl path }
| _ -> assert false
-
-
diff --git a/test/dfs/root.ml b/test/dfs/root.ml
index 8f398c3e..84c0f666 100644
--- a/test/dfs/root.ml
+++ b/test/dfs/root.ml
@@ -1,12 +1,12 @@
-(* Time-stamp: <modified the 05/03/2020 (at 21:43) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:42) by Erwan Jahier> *)
(* cf Collin-Dolex-94 *)
open Algo
open State
-
+
let (init_state: int -> string -> State.t) =
- fun i _ ->
+ fun _i _ ->
{
path = Array.make delta (-1);
par = -10
@@ -16,10 +16,9 @@ let (enable_f: t -> t neighbor list -> action list) =
fun v _nl ->
if v.path = (Array.make delta (-1)) then [] else ["update_path"]
-
+
let (step_f : t -> t neighbor list -> action -> t) =
- fun v nl ->
+ fun v _nl ->
function
| "update_path" -> { v with path = Array.make delta (-1) }
| _ -> assert false
-
diff --git a/test/dijkstra-ring/Makefile b/test/dijkstra-ring/Makefile
index 940e5384..90ec0642 100644
--- a/test/dijkstra-ring/Makefile
+++ b/test/dijkstra-ring/Makefile
@@ -1,9 +1,9 @@
-# Time-stamp: <modified the 11/06/2022 (at 14:56) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:11) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
@@ -19,8 +19,8 @@ utest: ring.cmxs
$(sasa) ring.dot -seed 42 > ring.rif && \
cp ring.rif ring.rif.exp ; true
-rdbg_test: ring.ml
- printf "\nnr\nsd\nq\n" | rdbg --sasa -o ring.rif -l 10000 -sut "$(sasa) -vl 1 ring.dot -dd"
+rdbg_test: ring.cma
+ printf "\nnr\nsd\nq\n" | rdbg --sasa -o ring.rif -l 10000 -sut "$(sasa) -vl 1 ring.dot -dd"
lurette1: ring.lut ring_oracle.lus
lurette --sasa \
@@ -36,8 +36,8 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
rdbg: ring.ml ring.lut
diff --git a/test/dijkstra-ring/Makefile.dot b/test/dijkstra-ring/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/dijkstra-ring/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/dijkstra-ring/Makefile.inc b/test/dijkstra-ring/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/dijkstra-ring/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/dijkstra-ring/dijkstra_ring_oracle.lus b/test/dijkstra-ring/dijkstra_ring_oracle.lus
index 4b570f77..f9e05c9a 100644
--- a/test/dijkstra-ring/dijkstra_ring_oracle.lus
+++ b/test/dijkstra-ring/dijkstra_ring_oracle.lus
@@ -2,10 +2,13 @@ include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
+type state = int;
+const k = card;
+
node theorem_6_29<<const m : int; const n: int>> (legitimate:bool; Acti: bool^m^n)
returns (res:bool);
var
- MoveNb:int ;
+ MoveNb:int;
let
MoveNb = move_count(Acti);
res = (k>=n)=>(( (3*n*(n-1))/2 < MoveNb) => legitimate) ; -- Theorem 6.29
@@ -19,13 +22,14 @@ var
MoveNb:int;
let
Xn = 0 -> if(Acti[0][0]) then pre(Xn) + 1 else pre(Xn) ;
- MoveNb = move_count(Acti);
+ MoveNb = move_count(Acti);
res = (((n*(n-1)/2) + Xn*n)<MoveNb) => legitimate ; -- Lemma 6.28
tel
-----------------------------------------------------------------------------
node dijkstra_ring_oracle<<const an:int; const pn:int>>
-(legitimate:bool; Enab, Acti: bool^an^pn) returns (ok:bool);
+(legitimate:bool; potential: real; Enab, Acti: bool^an^pn; Config:state^card ; round:bool; round_nb:int)
+returns (ok:bool);
let
ok = lemma_6_28 <<an,pn>> (legitimate, Acti) and
theorem_6_29<<an,pn>> (legitimate, Acti);
@@ -33,7 +37,7 @@ tel
node dijkstra_ring_oracle_cov<<const an:int; const pn:int>>
-(legitimate:bool; Enab, Acti: bool^an^pn;round:bool; round_nb:int)
+(legitimate:bool; Enab, Acti: bool^an^pn; Config:state^card ; round:bool; round_nb:int)
returns (ok:bool; WortCaseReached : bool);
var
WortCase : int;
@@ -42,6 +46,6 @@ let
MoveNb = move_count(Acti);
WortCase=(3*pn*(pn-1))/2;
WortCaseReached = (WortCase = MoveNb);
-
- ok = dijkstra_ring_oracle <<an,pn>> (legitimate, Enab, Acti);
+
+ ok = dijkstra_ring_oracle <<an,pn>> (legitimate, Enab, Acti, Config, round, round_nb);
tel
diff --git a/test/dijkstra-ring/dune b/test/dijkstra-ring/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/dijkstra-ring/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/dijkstra-ring/dune-project b/test/dijkstra-ring/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/dijkstra-ring/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/dijkstra-ring/dune-workspace b/test/dijkstra-ring/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/dijkstra-ring/p.ml b/test/dijkstra-ring/p.ml
index 64102a24..13fdff31 100644
--- a/test/dijkstra-ring/p.ml
+++ b/test/dijkstra-ring/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 09/05/2022 (at 09:46) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 22:13) by Erwan Jahier> *)
open Algo
@@ -22,12 +22,9 @@ let (enable_f: 's -> 's neighbor list -> action list) =
failwith "Error: the topology should be a directed ring!\n%!"
in
if e.v <> (state pred).v then ["T"] else []
-
+
let (step_f : 's -> 's neighbor list -> action -> 's) =
fun e nl a ->
let pred = match nl with [n] -> n | _ -> assert false in
- match a with
+ match a with
| _ -> { e with v = (state pred).v }
-
-
-
diff --git a/test/dijkstra-ring/ring_oracle.lus b/test/dijkstra-ring/ring_oracle.lus
deleted file mode 100644
index e5876c4b..00000000
--- a/test/dijkstra-ring/ring_oracle.lus
+++ /dev/null
@@ -1,43 +0,0 @@
--- Automatically generated by /home/jahier/.opam/4.12.0/bin/sasa version "v4.5.2" ("6122a58")
--- on crevetete the 28/7/2021 at 11:23:11
---sasa -glos ring.dot
-
-include "dijkstra_ring_oracle.lus"
-const an=1; -- actions number
-const pn=8; -- processes number
-const degree=2;
-const min_degree=2;
-const mean_degree=2.000000;
-const diameter=7;
-const card=8;
-const links_number=8;
-const is_cyclic=true;
-const is_connected=true;
-const is_a_tree=false;
-const f=false;
-const t=true;
-const adjacency=[
- [f,t,f,f,f,f,f,f],
- [f,f,t,f,f,f,f,f],
- [f,f,f,t,f,f,f,f],
- [f,f,f,f,t,f,f,f],
- [f,f,f,f,f,t,f,f],
- [f,f,f,f,f,f,t,f],
- [f,f,f,f,f,f,f,t],
- [t,f,f,f,f,f,f,f]];
-const k=3;
-
-node oracle(legitimate:bool;
- root_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;p8_c:int;
- Enab_root_T,Enab_p2_T,Enab_p3_T,Enab_p4_T,Enab_p5_T,Enab_p6_T,Enab_p7_T,Enab_p8_T:bool;
- root_T,p2_T,p3_T,p4_T,p5_T,p6_T,p7_T,p8_T:bool;round:bool; round_nb:int)
-returns (ok, WCReached:bool);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
-let
- Acti = [[root_T],[p2_T],[p3_T],[p4_T],[p5_T],[p6_T],[p7_T],[p8_T]];
- Enab = [[Enab_root_T],[Enab_p2_T],[Enab_p3_T],[Enab_p4_T],[Enab_p5_T],[Enab_p6_T],[Enab_p7_T],[Enab_p8_T]];
-
- ok, WCReached = dijkstra_ring_oracle_cov(legitimate, Enab, Acti, round, round_nb);
-tel
diff --git a/test/dijkstra-ring/root.ml b/test/dijkstra-ring/root.ml
index 6d0b93ba..a3f29489 100644
--- a/test/dijkstra-ring/root.ml
+++ b/test/dijkstra-ring/root.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/09/2020 (at 17:18) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 22:23) by Erwan Jahier> *)
open Algo
@@ -17,10 +17,7 @@ let (enable_f: 's -> 's neighbor list -> action list) =
if e.v = (state pred).v then ["T"] else []
let (step_f : 's -> 's neighbor list -> action -> 's) =
- fun e nl a ->
+ fun e _nl a ->
(* let k = (card() - 1) in *)
match a with
| _ -> { e with v = (e.v + 1) mod k }
-
-
-
diff --git a/test/dune2copy b/test/dune2copy
new file mode 100644
index 00000000..62240466
--- /dev/null
+++ b/test/dune2copy
@@ -0,0 +1,59 @@
+;; dune file to build the cmxs (resp the cma) needed by sasa (resp rdbgui4sasa)
+
+(library
+ (name user_algo_files) ;; a fake name because "%{env:topology=ring4}" is rejected
+ (libraries algo)
+ (wrapped false) ; so that user_algo_files is not used in the .cm*
+ (library_flags -linkall)
+)
+
+;; copy the <topology>.dot to the build dir if it already exists
+;; or create it via make otherwise
+(rule
+ (mode (promote (until-clean)))
+ (target %{env:topology=ring4}.dot)
+ (deps
+ (:makefile Makefile)
+ (:makefiledot Makefile.dot)
+ )
+ (action
+ (bash "[ -f ../../%{env:topology=ring4}.dot ] && cp ../../%{env:topology=ring4}.dot . || \
+ make %{env:topology=ring4}.dot")
+ )
+)
+
+;; generate the registration file (out of the dot file)
+(rule
+ (target %{env:topology=ring4}.ml)
+ (deps (:dotfile ./%{env:topology=ring4}.dot))
+ (action
+ (bash "sasa -reg %{dotfile}")
+ )
+)
+
+(rule
+ (mode (promote (until-clean)))
+ (action
+ (progn
+ ;; give them back the rigth name
+ (copy user_algo_files.cmxs %{env:topology=ring4}.cmxs)
+ (copy user_algo_files.cmxa %{env:topology=ring4}.cmxa)
+ (copy user_algo_files.cma %{env:topology=ring4}.cma)
+ (copy user_algo_files.a %{env:topology=ring4}.a)
+ ;; we can have only one registering file in the build dir
+ (bash "rm %{env:topology=ring4}.ml")
+ )
+ )
+ (deps (:src ./%{env:topology=ring4}.dot))
+)
+
+;; The glue lustre code between the oracle and the topology
+(rule
+ (target %{env:topology=ring4}_oracle.lus)
+ (mode (promote (until-clean)))
+ (deps
+ (:dotfile ./%{env:topology=ring4}.dot)
+ (:cmxs ./%{env:topology=ring4}.cmxs)
+ )
+ (action (bash "sasa -glos %{dotfile} -o $(basename $(realpath $PWD/../..))"))
+ )
diff --git a/test/k-clustering/4.14.0/fig52_kcl.rif.exp b/test/k-clustering/4.14.0/fig52_kcl.rif.exp
index 3f7fb689..7a018284 100644
--- a/test/k-clustering/4.14.0/fig52_kcl.rif.exp
+++ b/test/k-clustering/4.14.0/fig52_kcl.rif.exp
@@ -1,5 +1,5 @@
-# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.7.0" ("1f6fd7d")
-# on crevetete the 25/7/2022 at 17:12:38
+# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.8.0" ("2af1617")
+# on crevetete the 18/1/2023 at 11:49:34
#sasa fig52_kcl.dot -seed 42
#seed 42
diff --git a/test/k-clustering/4.14.0/rtree10.rif.exp b/test/k-clustering/4.14.0/rtree10.rif.exp
index 4ac022a6..d36c8b4e 100644
--- a/test/k-clustering/4.14.0/rtree10.rif.exp
+++ b/test/k-clustering/4.14.0/rtree10.rif.exp
@@ -1,5 +1,5 @@
-# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.7.0" ("1f6fd7d")
-# on crevetete the 25/7/2022 at 17:12:38
+# Automatically generated by /home/jahier/.opam/4.14.0/bin/sasa version "v4.8.0" ("2af1617")
+# on crevetete the 18/1/2023 at 11:49:35
#sasa rtree10.dot -seed 42
#seed 42
diff --git a/test/k-clustering/Makefile b/test/k-clustering/Makefile
index 70ace4c8..53467270 100644
--- a/test/k-clustering/Makefile
+++ b/test/k-clustering/Makefile
@@ -1,11 +1,12 @@
-# Time-stamp: <modified the 24/06/2022 (at 15:16) by Erwan Jahier>
+# Time-stamp: <modified the 18/01/2023 (at 11:49) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
--include ../Makefile.inc
+SEED=--seed 42
+-include ./Makefile.inc
-include Makefile.untracked
# dot files cannot be autommatically generated as the algo inputs a spanning tree
--include ../Makefile.dot
+-include ./Makefile.dot
##############################################################################
# Non-regression tests
@@ -20,25 +21,23 @@ clean: genclean
##############################################################################
# Other examples of use
-cd: fig52_kcl.cmxs
- sasa -cd fig52_kcl.dot
+cd: fig52_kcl.cmxs
+ sasa -cd fig52_kcl.dot
sim2chrogtk: fig52_kcl.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: fig52_kcl.rif
- gnuplot-rif $<
+gnuplot: fig52_kcl.rif
+ gnuplot-rif $<
-rdbg: fig52_kcl.ml
- rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -gcd"
+rdbg: fig52_kcl.ml
+ rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -gcd"
rdbg: fig52_kcl.ml
- rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -cd"
+ rdbg --sasa -o fig52_kcl.rif -env "sasa fig52_kcl.dot -cd"
rdbgui: fig52_kcl.ml
- rdbgui4sasa -o tree4.rif -env "sasa -seed 178451767 tree4.dot -dd"
+ rdbgui4sasa -o tree4.rif -env "sasa -seed 178451767 tree4.dot -dd"
rtree50: rtree50.cmxs
sasa -cd rtree50.dot
-
-
diff --git a/test/k-clustering/Makefile.dot b/test/k-clustering/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/k-clustering/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/k-clustering/Makefile.inc b/test/k-clustering/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/k-clustering/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/k-clustering/config.ml b/test/k-clustering/config.ml
index 73755430..8ee15431 100644
--- a/test/k-clustering/config.ml
+++ b/test/k-clustering/config.ml
@@ -1,7 +1,6 @@
open Algo
-open State
-open P
+open State
let debug = false
@@ -48,7 +47,7 @@ let rec (pot : pid -> (pid -> ('a * ('a neighbor*pid) list)) -> int -> int -> in
let root = ref None
let get_root pidl get =
match !root with
- | None ->
+ | None ->
( match List.filter (fun pid -> (fst (get pid)).isRoot) pidl with
[ pid ] -> root := Some pid; pid
| [] -> exit2 "at least one node should be the root"
@@ -76,8 +75,7 @@ let (pf: pid list -> (pid -> ('a * ('a neighbor * pid) list)) -> float) =
);
(* (String.concat "," (List.map (fun pid -> Printf.sprintf "%s=%b" get pid) pidl) root_pot ; *)
float_of_int root_pot
-
-let potential = None
+
let potential = Some pf
let legitimate = None (* None => only silent configuration are legitimate *)
@@ -85,12 +83,11 @@ let fault = None
open State
let maxi = 2*k+1
-
+
let s2n s = [I (0, s.alpha, maxi)]
let n2s nl s =
match nl with
| [I(_, i, _)] -> { s with alpha = i }
| _ -> assert false
-
-let init_search_utils = Some (s2n, n2s)
+let init_search_utils = Some (s2n, n2s)
diff --git a/test/k-clustering/dune b/test/k-clustering/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/k-clustering/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/k-clustering/dune-project b/test/k-clustering/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/k-clustering/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/k-clustering/dune-workspace b/test/k-clustering/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/k-clustering/my-rdbg-tuning.ml b/test/k-clustering/my-rdbg-tuning.ml
deleted file mode 100644
index 27f57cc1..00000000
--- a/test/k-clustering/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-dot_view := fd;;
diff --git a/test/lustre/dune-workspace b/test/lustre/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/rsp-tree/Makefile b/test/rsp-tree/Makefile
index 56b3cf60..bd71db15 100644
--- a/test/rsp-tree/Makefile
+++ b/test/rsp-tree/Makefile
@@ -1,8 +1,9 @@
-# Time-stamp: <modified the 30/05/2022 (at 14:38) by Erwan Jahier>
+# Time-stamp: <modified the 18/01/2023 (at 11:33) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+SEED=--seed 42
+-include ./Makefile.inc
+-include ./Makefile.dot
##############################################################################
# Non-regression tests
@@ -16,11 +17,11 @@ utest:
make udg100.ugm_test || echo "udg100 ok"
make ba100.ugm_test || echo "ba100 ok"
-%.lurette: %.dot %.cmxs %_oracle.lus rsp_tree_oracle.lus
- lurette -sut "sasa $< -dd" -oracle "lv6 -2c-exec $*_oracle.lus -n oracle"
+%.lurette: %.cmxs
+ lurette -sut "sasa $*.dot -dd" -oracle "lv6 -2c-exec $*_oracle.lus -n oracle"
-%.lurette2: %.dot %.cmxs %_oracle.lus rsp_tree_oracle.lus
- lurette -sut "sasa $< -dd" -oracle "lv6 $*_oracle.lus -n oracle"
+%.lurette2: %.cmxs
+ lurette -sut "sasa $*.dot -dd" -oracle "lv6 $*_oracle.lus -n oracle"
clean: genclean cleandot
diff --git a/test/rsp-tree/Makefile.dot b/test/rsp-tree/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/rsp-tree/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/rsp-tree/Makefile.inc b/test/rsp-tree/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/rsp-tree/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/rsp-tree/dune b/test/rsp-tree/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/rsp-tree/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/rsp-tree/dune-project b/test/rsp-tree/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/rsp-tree/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/rsp-tree/dune-workspace b/test/rsp-tree/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/rsp-tree/my-rdbg-tuning.ml b/test/rsp-tree/my-rdbg-tuning.ml
deleted file mode 100644
index 15658a77..00000000
--- a/test/rsp-tree/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,5 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-dot_view := d_par;;
diff --git a/test/skeleton/Makefile b/test/skeleton/Makefile
index 5855893e..5ec1c243 100644
--- a/test/skeleton/Makefile
+++ b/test/skeleton/Makefile
@@ -1,8 +1,8 @@
-# Time-stamp: <modified the 01/07/2022 (at 14:40) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 13:28) by Erwan Jahier>
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
##############################################################################
# Non-regression tests
@@ -21,4 +21,3 @@ rdbg: grid4.dot grid4.ml
clean: genclean
rm -f grid*.* diring*.* clique*.* er*.*
-
diff --git a/test/skeleton/Makefile.dot b/test/skeleton/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/skeleton/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/skeleton/Makefile.inc b/test/skeleton/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/skeleton/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/skeleton/config.ml b/test/skeleton/config.ml
new file mode 100644
index 00000000..1e0e05f1
--- /dev/null
+++ b/test/skeleton/config.ml
@@ -0,0 +1,5 @@
+
+let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
+let legitimate = None (* None => only silent configuration are legitimate *)
+let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
+let init_search_utils = None (* To provide to use --init-search *)
diff --git a/test/skeleton/dune b/test/skeleton/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/skeleton/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/skeleton/dune-project b/test/skeleton/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/skeleton/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/skeleton/dune-workspace b/test/skeleton/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/skeleton/my-rdbg-tuning.ml b/test/skeleton/my-rdbg-tuning.ml
deleted file mode 100644
index 35c216cd..00000000
--- a/test/skeleton/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/skeleton/p.ml b/test/skeleton/p.ml
index 89840550..411c24f2 100644
--- a/test/skeleton/p.ml
+++ b/test/skeleton/p.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 10/11/2020 (at 12:03) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 21:58) by Erwan Jahier> *)
(* a dumb algo that compiles *)
@@ -9,18 +9,16 @@ let (init_state: int -> string -> 'st) =
let (enable_f: 'st -> 'st neighbor list -> action list) =
- fun e nl ->
+ fun _ nl ->
match state (List.hd nl) with
| 0 -> ["action2"]
| 1 -> []
| _ -> ["action1"]
-
-
+
+
let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
- fun e nl ->
+ fun e _ ->
function
| "action1" -> 0
| "action2" -> 1
| _ -> e
-
-
diff --git a/test/st-CYH91/Makefile b/test/st-CYH91/Makefile
index 3fcf0cef..166e8310 100644
--- a/test/st-CYH91/Makefile
+++ b/test/st-CYH91/Makefile
@@ -1,18 +1,18 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:01) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:44) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
# Non-regression tests
test: test0 lurette ring.rdbg-test clean
-test0: ring.cmxs
+test0: ring.cmxs
sasa -l 200 ring.dot -cd
utest: clean
-lurette: grid4.cmxs
+lurette: grid4.cmxs
lurette --sasa -o rdbg.rif -sut "sasa grid4.dot -cd" -l 1000
clean: genclean
@@ -23,18 +23,18 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
ocd: grid4.ml grid4.cma
rdbg --sasa --ocamldebug -sut "sasa grid4.dot -cd -seed 42" -l 1000
-rdbg: grid4.ml
+rdbg: grid4.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid4.dot -cd" -l 1000
-rdbg-ring: ring.ml
+rdbg-ring: ring.ml
rdbg --sasa -o rdbg.rif -sut "sasa ring.dot -cd" -l 1000
-test10: grid10.cmxs
+test10: grid10.cmxs
sasa -l 20000 grid10.dot -cd > test10.rif
diff --git a/test/st-CYH91/Makefile.dot b/test/st-CYH91/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/st-CYH91/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/st-CYH91/Makefile.inc b/test/st-CYH91/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/st-CYH91/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/st-CYH91/dune b/test/st-CYH91/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/st-CYH91/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/st-CYH91/dune-project b/test/st-CYH91/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/st-CYH91/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/st-CYH91/dune-workspace b/test/st-CYH91/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/st-CYH91/my-rdbg-tuning.ml b/test/st-CYH91/my-rdbg-tuning.ml
deleted file mode 100644
index 35c216cd..00000000
--- a/test/st-CYH91/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,4 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
diff --git a/test/st-CYH91/root.ml b/test/st-CYH91/root.ml
index 3d3bb454..ea43d8a7 100644
--- a/test/st-CYH91/root.ml
+++ b/test/st-CYH91/root.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/03/2020 (at 09:43) by Erwan Jahier> *)
+(* Time-stamp: <modified the 17/01/2023 (at 14:58) by Erwan Jahier> *)
(* "A self-stabilizing algoritm for constructing spanning trees"
Nian-Shing Chen, Wey-Pyng Yu and Shing-Tsaan Huang
@@ -11,7 +11,7 @@ Hyp:
*)
let (init_state: int -> string -> 'st) =
- fun i _ ->
+ fun _i _ ->
{
State.level = 0;
State.par = -1
@@ -22,5 +22,3 @@ let enable_f = fun _ _ -> []
(* ... nor activated! *)
let step_f = fun e _nl _a -> e
-
-
diff --git a/test/st-KK06-algo1/Makefile b/test/st-KK06-algo1/Makefile
index 5cc71a7d..4494083d 100644
--- a/test/st-KK06-algo1/Makefile
+++ b/test/st-KK06-algo1/Makefile
@@ -1,27 +1,27 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:01) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:51) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
# Non-regression tests
test: test0 lurette lurette-alt rdbg-test clean
-test0: ring.cmxs
- sasa -l 200 ring.dot
+test0: ring.cmxs
+ sasa -l 200 ring.dot
utest: clean
lurette: grid4.cmxs grid4_oracle.lus
lurette --sasa -o rdbg.rif -sut "sasa grid4.dot -rif" \
-oracle "lv6 grid4_oracle.lus -n oracle -exec" -l 1000
-lurette-alt: grid4.cmxs grid4_oracle.lus
+lurette-alt: grid4.cma grid4_oracle.lus
rdbg -lurette --sasa -o rdbg.rif -sut "sasa grid4.dot -rif" \
-oracle "lv6 grid4_oracle.lus -n oracle -exec" -l 1000
-rdbg-test: ring.ml
+rdbg-test: ring.cma
rdbg --sasa -o rdbg.rif -sut "sasa ring.dot" -l 1000 -go --input some_session
clean: genclean
@@ -33,14 +33,14 @@ clean: genclean
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
ocd: grid4.ml grid4.cma
rdbg --sasa --ocamldebug -sut "sasa grid4.dot" -l 1000
-rdbg: grid4.ml
+rdbg: grid4.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid4.dot" -l 1000
-rdbg-ring: ring.ml
+rdbg-ring: ring.ml
rdbg --sasa -o rdbg.rif -sut "sasa ring.dot" -l 1000
diff --git a/test/st-KK06-algo1/Makefile.dot b/test/st-KK06-algo1/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/st-KK06-algo1/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/st-KK06-algo1/Makefile.inc b/test/st-KK06-algo1/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/st-KK06-algo1/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/st-KK06-algo1/dune b/test/st-KK06-algo1/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/st-KK06-algo1/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/st-KK06-algo1/dune-project b/test/st-KK06-algo1/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/st-KK06-algo1/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/st-KK06-algo1/dune-workspace b/test/st-KK06-algo1/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/st-KK06-algo1/my-rdbg-tuning.ml b/test/st-KK06-algo1/my-rdbg-tuning.ml
deleted file mode 100644
index 2839202f..00000000
--- a/test/st-KK06-algo1/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,5 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-
diff --git a/test/st-KK06-algo2/Makefile b/test/st-KK06-algo2/Makefile
index 5c7c1559..98f89822 100644
--- a/test/st-KK06-algo2/Makefile
+++ b/test/st-KK06-algo2/Makefile
@@ -1,16 +1,16 @@
-# Time-stamp: <modified the 11/06/2022 (at 15:02) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:58) by Erwan Jahier>
-DECO_PATTERN="0:root.ml 1-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0:root.ml 1-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
# Non-regression tests
test: test0 lurette lurette-alt grid4.rdbg-test clean
-test0: ring.cmxs
- sasa -l 200 ring.dot
+test0: ring.cmxs
+ sasa -l 200 ring.dot
utest: clean
lurette: grid4.cmxs grid4_oracle.lus
@@ -27,20 +27,20 @@ clean: genclean
##############################################################################
# Other examples of use
-rdbg-ring: ring.ml
+rdbg-ring: ring.ml
rdbg --sasa -o rdbg.rif -sut "sasa ring.dot" -l 1000
sim2chrogtk: ring.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: ring.rif
- gnuplot-rif $<
+gnuplot: ring.rif
+ gnuplot-rif $<
ocd: grid4.ml grid4.cma
rdbg --sasa --ocamldebug -sut "sasa grid4.dot" -l 1000
-rdbg: grid4.ml
+rdbg: grid4.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid4.dot" -l 100
-rdbg10: grid10.ml
+rdbg10: grid10.ml
rdbg --sasa -o rdbg.rif -sut "sasa grid10.dot" -l 1000
diff --git a/test/st-KK06-algo2/Makefile.dot b/test/st-KK06-algo2/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/st-KK06-algo2/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/st-KK06-algo2/Makefile.inc b/test/st-KK06-algo2/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/st-KK06-algo2/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/st-KK06-algo2/dune b/test/st-KK06-algo2/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/st-KK06-algo2/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/st-KK06-algo2/dune-project b/test/st-KK06-algo2/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/st-KK06-algo2/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/st-KK06-algo2/dune-workspace b/test/st-KK06-algo2/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/st-KK06-algo2/my-rdbg-tuning.ml b/test/st-KK06-algo2/my-rdbg-tuning.ml
deleted file mode 100644
index 2839202f..00000000
--- a/test/st-KK06-algo2/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,5 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-
diff --git a/test/toy-example-a5sf/Makefile b/test/toy-example-a5sf/Makefile
index 88c60374..8a2b9e88 100644
--- a/test/toy-example-a5sf/Makefile
+++ b/test/toy-example-a5sf/Makefile
@@ -1,9 +1,9 @@
-# Time-stamp: <modified the 30/05/2022 (at 11:02) by Erwan Jahier>
+# Time-stamp: <modified the 18/01/2023 (at 11:38) by Erwan Jahier>
-DECO_PATTERN="0-:p.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
##############################################################################
@@ -14,7 +14,7 @@ test: test1 test2 test_rdbg
diff -I "# on" -I " version " -B -u -i -w te.rif.exp te.rif > test.res
[ ! -s test.res ] && make clean
-test1: te.cmxs
+test1: te.cmxs
utest: te.rif
cp te.rif te.rif.exp ; true
@@ -22,7 +22,7 @@ utest: te.rif
test2:te.cmxs
sasa -gcd te.dot
-test_rdbg: te.ml
+test_rdbg: te.cma
rdbg --sasa -o te.rif -env "sasa te.dot -gcd" -go --input some_session
clean: genclean
@@ -34,9 +34,8 @@ clean: genclean
sim2chrogtk: te.rif
sim2chrogtk -ecran -in $< > /dev/null
-gnuplot: te.rif
- gnuplot-rif $<
+gnuplot: te.rif
+ gnuplot-rif $<
-rdbg: te.ml
+rdbg: te.ml
rdbg --sasa -o te.rif -env "sasa te.dot -gcd"
-
diff --git a/test/toy-example-a5sf/Makefile.dot b/test/toy-example-a5sf/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/toy-example-a5sf/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/toy-example-a5sf/Makefile.inc b/test/toy-example-a5sf/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/toy-example-a5sf/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/toy-example-a5sf/config.ml b/test/toy-example-a5sf/config.ml
index 063b713a..aafb446d 100644
--- a/test/toy-example-a5sf/config.ml
+++ b/test/toy-example-a5sf/config.ml
@@ -1,10 +1,10 @@
open Algo
open P
open State
-
+
let (isEnabledS: pid -> (pid -> ('a * 'a neighbor list)) -> bool) =
fun id get -> ((fst (get id))).sub <> (((fst (get id))).input + (sum_sub (snd (get id))))
-
+
let (isEnabledR: pid -> (pid -> ('a * 'a neighbor list)) -> bool) =
fun id get ->
let id_v, id_nl = get id in
@@ -14,13 +14,13 @@ let (isEnabledR: pid -> (pid -> ('a * 'a neighbor list)) -> bool) =
(id_v.res <> max [p_par_res; id_v.sub] 0)
let (loc_pot: pid -> pid list -> (pid -> ('a * 'a neighbor list)) -> int) =
- fun p pidl get ->
+ fun p _pidl get ->
if isEnabledS p get then
1 + vn*(vn-1) + int_of_string (String.sub p 1 ((String.length p) - 1))
else if isEnabledR p get then
1 + (vn - (int_of_string (String.sub p 1 ((String.length p) - 1))))
else 0
-
+
let rec (sum_loc_pots: pid list -> pid list -> (pid -> ('a * 'a neighbor list)) -> int) =
fun pidl pidl_mem get ->
match pidl with
@@ -31,26 +31,26 @@ let (pf: pid list -> (pid -> ('a * ('a neighbor * pid) list)) -> float) =
fun pidl get ->
let get pid =
let v, l = get pid in
- v, fst (List.split l)
+ v, fst (List.split l)
in
float_of_int (sum_loc_pots pidl pidl get)
-
+
let potential = Some pf
let legitimate = None (* None => only silent configuration are legitimate *)
-let fault = None
+let fault = None
let mini= 0
let maxi = max_degree ()
-
+
let s2n s = [I(mini, s.input, 100); I(mini, s.par, maxi);
I(mini, s.sub, 100); I(mini, s.res, 100)]
let n2s nl s =
match nl with
| [I(_, input, _); I(_, par, _); I(_, sub, _); I(_, res, _)] ->
- { s with input; par; sub; res }
+ { s with input; par; sub; res }
| _ -> assert false
-
+
let init_search_utils = Some (s2n, n2s)
diff --git a/test/toy-example-a5sf/dune b/test/toy-example-a5sf/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/toy-example-a5sf/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/toy-example-a5sf/dune-project b/test/toy-example-a5sf/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/toy-example-a5sf/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/toy-example-a5sf/dune-workspace b/test/toy-example-a5sf/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/toy-example-a5sf/my-rdbg-tuning.ml b/test/toy-example-a5sf/my-rdbg-tuning.ml
deleted file mode 100644
index 6ed041d9..00000000
--- a/test/toy-example-a5sf/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,5 +0,0 @@
- (* *)
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-dot_view := fd;;
diff --git a/test/toy-example-a5sf/p.ml b/test/toy-example-a5sf/p.ml
index d15f18fd..974bb160 100644
--- a/test/toy-example-a5sf/p.ml
+++ b/test/toy-example-a5sf/p.ml
@@ -11,7 +11,7 @@ let (init_state: int -> string -> 'st) =
par = Random.int (max_degree ());
sub = Random.int 100;
res = Random.int 100
- }
+ }
let rec (children: 'st neighbor list -> 'st list) =
fun nl ->
@@ -25,13 +25,13 @@ let rec (max: int list -> int -> int) =
[] -> mem
| i::listi -> if (i>mem) then (max listi i) else (max listi mem)
-let rec (sum: int list -> int) = fun l -> List.fold_left (+) 0 l
-
+let (sum: int list -> int) = fun l -> List.fold_left (+) 0 l
+
let (sum_sub: 'st neighbor list -> int) =
fun nl ->
sum (List.map (fun st -> st.sub) (children nl))
-
-
+
+
let (enable_f: 'st -> 'st neighbor list -> action list) =
fun p nl ->
if p.sub <> (p.input + (sum_sub nl)) then ["S"]
@@ -47,4 +47,3 @@ let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
| "RR" -> {p with res = p.sub}
| "RP" -> {p with res = max [(state (List.nth nl p.par)).res; p.sub] 0}
| _ -> assert false
-
diff --git a/test/toy-example-sum/dune b/test/toy-example-sum/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/toy-example-sum/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/toy-example-sum/dune-project b/test/toy-example-sum/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/toy-example-sum/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/toy-example-sum/dune-workspace b/test/toy-example-sum/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/toy-example-sum/my-rdbg-tuning.ml b/test/toy-example-sum/my-rdbg-tuning.ml
deleted file mode 100644
index 3214875d..00000000
--- a/test/toy-example-sum/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,7 +0,0 @@
-
- (* Generated by rdbg because not existing *)
-#use "rdbg-cmds.ml";;
-
-#use "sasa-rdbg-cmds.ml";;
-
-#use "include.ml";;
diff --git a/test/unison/Makefile b/test/unison/Makefile
index 11fc522c..bb681c3f 100644
--- a/test/unison/Makefile
+++ b/test/unison/Makefile
@@ -1,8 +1,8 @@
-# Time-stamp: <modified the 11/06/2022 (at 14:58) by Erwan Jahier>
+# Time-stamp: <modified the 17/01/2023 (at 14:22) by Erwan Jahier>
-DECO_PATTERN="0-:unison.ml"
--include ../Makefile.dot
--include ../Makefile.inc
+DECO_PATTERN="0-:unison.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
-include Makefile.untracked
DAEMON=-sd
@@ -64,11 +64,10 @@ rdbg_daemon: ring.cmxs
lurette: lurette0 s g
-rdbg: ring.ml
- rdbg --sasa -o unison.rif -sut "$(sasa) ring.dot -sd -rif"
-rdbgui: ring.ml
- rdbgui4sasa -o unison.rif -sut "$(sasa) ring.dot -sd -rif"
-
-rdbg2: ring.ml
- rdbg --sasa -o unison.rif -sut "sasa ring.dot -custd -rif"
+rdbg: ring.ml
+ rdbg --sasa -o unison.rif -sut "$(sasa) ring.dot -sd -rif"
+rdbgui: ring.ml
+ rdbgui4sasa -o unison.rif -sut "$(sasa) ring.dot -sd -rif"
+rdbg2: ring.ml
+ rdbg --sasa -o unison.rif -sut "sasa ring.dot -custd -rif"
diff --git a/test/unison/Makefile.dot b/test/unison/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/unison/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/unison/Makefile.inc b/test/unison/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/unison/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/unison/config.ml b/test/unison/config.ml
index 7dc3ade9..92348ed0 100644
--- a/test/unison/config.ml
+++ b/test/unison/config.ml
@@ -2,7 +2,6 @@
let potential = None (* None => only -sd, -cd, -lcd, -dd, or -custd are possible *)
let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
-let fault = None
let legitimate pidl from_pid =
(* a legitimate configuration is reached when all states have the same values *)
@@ -11,7 +10,6 @@ let legitimate pidl from_pid =
(fun acc pid -> acc && fst(from_pid pid) = v)
true
(List.tl pidl)
-
+
let legitimate = Some legitimate
let init_search_utils = None
-
diff --git a/test/unison/dune b/test/unison/dune
new file mode 120000
index 00000000..5cb715b8
--- /dev/null
+++ b/test/unison/dune
@@ -0,0 +1 @@
+../dune2copy
\ No newline at end of file
diff --git a/test/unison/dune-project b/test/unison/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/unison/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/unison/dune-workspace b/test/unison/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/unison/my-rdbg-tuning.ml b/test/unison/my-rdbg-tuning.ml
deleted file mode 100644
index cff928a7..00000000
--- a/test/unison/my-rdbg-tuning.ml
+++ /dev/null
@@ -1,15 +0,0 @@
- (* *)
-
-#use "rdbg-cmds.ml";;
-#use "sasa-rdbg-cmds.ml";;
-
-(*
-let sync sl =
- let sl = List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = "Enab_") sl in
- Some (List.map (fun (n,v) -> String.sub n 5 ((String.length n)-5),v) sl)
-let _ =
- rdbg_mv_hook := Some sync;
- rdbg_mv_hook := None;
- ()
-;;
-*)
diff --git a/tools/rdbg4sasa/gtkgui.ml b/tools/rdbg4sasa/gtkgui.ml
index d5079d04..12acb22e 100644
--- a/tools/rdbg4sasa/gtkgui.ml
+++ b/tools/rdbg4sasa/gtkgui.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/01/2023 (at 16:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 16/01/2023 (at 21:36) by Erwan Jahier> *)
#thread
#require "lablgtk3"
@@ -15,7 +15,7 @@ open Data
let rdbg_nodes_info e: (string * string * bool) list =
let enabled =
List.filter (fun (n,v) -> String.length n > 5 && String.sub n 0 5 = "Enab_") e.data
- in
+ in
let split_var (str, value) =
let v = match value with B v -> v | _ -> assert false in
let p, label =
@@ -25,7 +25,7 @@ let rdbg_nodes_info e: (string * string * bool) list =
| true, _::x::y::z -> x^y, String.concat "_" z
in
p, label,v
- in
+ in
List.map split_var enabled
(** Liste qui dit pour chaque noeud s'il est activable. On suppose
@@ -54,7 +54,7 @@ let rdbg_nodes_enabled e =
(**********************************************************************************)
type daemon_kind =
- Distributed | Synchronous | Central | LocCentral | ManualCentral | Manual
+ Distributed | Synchronous | Central | LocCentral | ManualCentral | Manual
let daemon_kind = ref ManualCentral
type daemon_mode = Internal (* sasa with internal daemon *) | GuiAuto | GuiManual
@@ -77,28 +77,28 @@ let gui_mode = custom_mode (* a better name? *)
let check_point_event e =
(* Depending on the way rdbgui4sasa is used, some kinds of events
- make more sense as checkpoint candidate. Moreover, it is better to have only
+ make more sense as checkpoint candidate. Moreover, it is better to have only
one checkpoint per step.
*)
match daemon_mode () with
- | Internal -> e.kind = Ltop
+ | Internal -> e.kind = Ltop
(* | GuiAuto -> e.kind = Ltop *)
| GuiAuto -> e.kind = Call && e.name = "mv_hook"
| GuiManual -> e.kind = Call && e.name = "mv_hook"
let _ = check_ref := fun e -> e.nb = 1 || (check_point_event e) && round e;;
-(* modify the one in rdbg-cmd.ml to inhibit it when the undo is
+(* modify the one in .rdbg-cmd.ml to inhibit it when the undo is
impossible: in manual modes, it would require to store all the
user manual inputs to replay the simulation from the last
checkpoint (because of the PRGs) *)
let store i = if daemon_mode() = GuiManual then () else store i
-
+
let refresh_fun_tbl = Hashtbl.create 1
let _ = Hashtbl.add refresh_fun_tbl "update dot" d
let refresh () =
Hashtbl.iter (fun str f -> f()) refresh_fun_tbl
-
+
(** Met en place le hook *)
let daemongui_activate : (string, bool) Hashtbl.t = Hashtbl.create 1
(* states whether a node should be activated *)
@@ -156,7 +156,7 @@ let display_event b =
blue_add b#buffer "----------------------------------------\n";
blue_add b#buffer (str_of_sasa_event false !e)
-
+
(* *)
@@ -173,7 +173,7 @@ let goto_hook_exit e =
e
let goto_top e = next_cond e (fun e -> e.kind = Ltop)
-
+
let init_rdbg_hook () =
let guidaemon sl =
if sl = [] then
@@ -187,7 +187,7 @@ let init_rdbg_hook () =
n, v) (snd !rdbg_mv)
in
Some res
- else
+ else
let sl = List.filter
(fun (n,v) -> String.length n>5 && String.sub n 0 5 = "Enab_") sl
in
@@ -224,8 +224,8 @@ let init_rdbg_hook () =
match !rdbg_mv_hook with
| None -> rdbg_mv_hook := Some guidaemon
| _ -> ()
-
-let set_tooltip b = b#misc#set_tooltip_text
+
+let set_tooltip b = b#misc#set_tooltip_text
let start () =
if gui_mode then init_rdbg_hook ();
@@ -324,7 +324,7 @@ let update_daemongui_tbl e =
| ManualCentral -> () (* SNO; the step is done in pushbox callbacks *)
| Manual -> ()
)
-
+
(* redraws the gui buttons a each move, to show only buttons related to enabled nodes *)
let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_button
legitimate_button undo_button =
@@ -378,7 +378,7 @@ let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_
(* build manually a m x m grid *)
let i = ref 0 in
let checkbox_grid = GPack.vbox ~packing:vbox#add () in
- let checkbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
+ let checkbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
~vpolicy:`AUTOMATIC
~height:300
~shadow_type:`OUT ~packing:checkbox_grid#add ()
@@ -408,8 +408,8 @@ let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_
(* Des boutons pour le mode Manuel Central *)
let pushbox_grid = GPack.vbox ~packing:vbox#add () ~homogeneous:true in
- let pushbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
- ~vpolicy:`AUTOMATIC
+ let pushbox_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
+ ~vpolicy:`AUTOMATIC
~height:300
~shadow_type:`OUT ~packing:pushbox_grid#add ()
in
@@ -446,7 +446,7 @@ let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_
(* Des compteurs pour les modes automatiques *)
let counter_grid = GPack.vbox ~packing:vbox#add () in
- let counter_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
+ let counter_scrolled_grid = GBin.scrolled_window ~border_width:10 ~hpolicy:`AUTOMATIC
~vpolicy:`AUTOMATIC ~height:400
~shadow_type:`OUT ~packing:counter_grid#add ()
in
@@ -465,7 +465,7 @@ let draw_manual_daemons_buttons p gtext vbox step_button back_step_button round_
let counter_container_frame = GBin.frame ~label:name ~packing:!counter_line_ref#add () in
let counter_container =
GPack.hbox ~homogeneous:true ~border_width: 2 ~spacing:0
- ~packing:counter_container_frame#add ()
+ ~packing:counter_container_frame#add ()
in
let incr_container = GPack.vbox ~packing:counter_container#add () in
@@ -575,9 +575,9 @@ let ic_stdout = stdin
open GButton
- (* GTK3 *)
+ (* GTK3 *)
let main () =
- let _locale = GtkMain.Main.init () in
+ let _locale = GtkMain.Main.init () in
let _thread = GtkThread.start () in
let window = GWindow.window
(* ~width:320 ~height:240 *)
@@ -593,8 +593,8 @@ let main () =
~packing:box#add ()
in
set_tooltip sw2 "This window displays commands outputs";
- let text_out = GText.view ~wrap_mode:`CHAR ~height:250 ~editable:false
- ~packing: sw2#add () ~cursor_visible:true
+ let text_out = GText.view ~wrap_mode:`CHAR ~height:250 ~editable:false
+ ~packing: sw2#add () ~cursor_visible:true
in
let p str = black text_out#buffer str in
(* It should be better to rely on the gtk event handler *)
@@ -648,7 +648,7 @@ let main () =
back_round, and undo. *)
let goto_gui i =
if not gui_mode then ( u(); d() )
- else
+ else
let lnext e =
if args.salut_mode then (
update_daemongui_tbl e;
@@ -667,7 +667,7 @@ let main () =
rev_cond_gen !e (fun ne -> ne.nb = i) lnext (fun _ -> ())
else if i > !e.nb then
next_cond_gen !e (fun ne -> ne.nb = i) lnext
- else
+ else
!e
in
e:=ne;
@@ -675,8 +675,8 @@ let main () =
d()
in
let undo_gui () =
- let i =
- match !redos with
+ let i =
+ match !redos with
| _::i::t -> redos := i::t; i
| i::[] -> i
| [] -> 1
@@ -767,7 +767,7 @@ let main () =
e := back_step !e;
pe()
)
- else (
+ else (
if args.salut_mode then
let lnext e =
update_daemongui_tbl e; (* necessary to get the PRGs rigth during backward moves *)
@@ -895,11 +895,11 @@ let main () =
e:=goto_hook_call !e;
d()))
in
- let graph () =
+ let graph () =
let graph_button = button ~use_mnemonic:true ~packing:bbox#add () in
set_tooltip graph_button "Visualize the Topology states: Green=Enabled ; Gold=Active";
let image = GMisc.image ~file:(libui_prefix^"/graph_small.png") () in
- graph_button#set_image image#coerce;
+ graph_button#set_image image#coerce;
ignore (graph_button#connect#clicked ~callback:(button_cb false false graph_view));
in
@@ -957,10 +957,10 @@ let main () =
dot_view := cmd; !dot_view()))
in
let have_parent () = (* is there a parent field in the state ? *)
- List.exists (fun (v,_) -> Str.string_match (Str.regexp ".*_par.*") v 0) !e.data
+ List.exists (fun (v,_) -> Str.string_match (Str.regexp ".*_par.*") v 0) !e.data
in
if have_parent () then (
- let make_but lbl = GButton.radio_button ~packing:gbox2#add
+ let make_but lbl = GButton.radio_button ~packing:gbox2#add
~group:dot_button#group ~label:lbl ()
in
let par_dot_button = make_but "dot*" in
@@ -1015,13 +1015,13 @@ let main () =
ignore(Seed.get dotfile);
refresh ()
-let gui = main
+let gui = main
(* todo
- les oracles sont violés en silence (lancer un pop-up ?)
- couper les grosses fonctions en morceaux
- cacher les messages issus du #use
- lire les commandes dans text_in (comment ? c'est rdbgtop qui lance gtk maintenant...)
-- reglage de la taille des boites
+- reglage de la taille des boites
- utiliser les GEdit.spin_button ?
cf lablgtk/examples/spin.ml
https://lazka.github.io/pgi-docs/Gtk-3.0/classes/SpinButton.html#Gtk.SpinButton
diff --git a/tools/rdbg4sasa/sasa-rdbg-cmds.ml b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
index 334523af..a69192e2 100644
--- a/tools/rdbg4sasa/sasa-rdbg-cmds.ml
+++ b/tools/rdbg4sasa/sasa-rdbg-cmds.ml
@@ -1,6 +1,6 @@
-(* This file defines sasa specific commands.
+(* This file defines sasa specific commands.
-It is meant to be loaded after the (rdbg-generated) "rdbg-cmds.ml" file.
+It is meant to be loaded after the (rdbg-generated) ".rdbg-cmds.ml" file.
*)
open RdbgMain
#require "sasacore";;
@@ -79,14 +79,14 @@ let sf () = sfdp false (get_round_nb !e) p dotfile !e;;
let pa () = patchwork false (get_round_nb !e) p dotfile !e;;
let os () = osage false (get_round_nb !e) p dotfile !e;;
-(* To change the default dot/graph viewer:
+(* To change the default dot/graph viewer:
dot_view := ci;;
*)
let dot_view : (unit -> unit) ref =
ref ( (* Make our best to chose the most sensible default viewer *)
if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else
if Algo.is_directed () then dot else ne)
-
+
let d () = !dot_view ()
(**********************************************************************)
@@ -95,7 +95,7 @@ let sasa_next e =
let ne = e.next () in
List.iter
(fun str -> if str<>"print_event" then (RdbgStdLib.get_hook str) ne)
- (RdbgStdLib.list_hooks ());
+ (RdbgStdLib.list_hooks ());
ne
let next_cond e =
@@ -104,7 +104,7 @@ let next_cond e =
let next_cond_gen e p n =
if e.step = args.step_nb then d ();
- next_cond_gen e p n
+ next_cond_gen e p n
let next_round e =
next_cond_gen e (fun e -> round e || is_legitimate e) sasa_next
@@ -116,7 +116,7 @@ let back_step e =
in
store e.nb;
e
-
+
(**********************************************************************)
(* redefine (more meaningful) step and back-step for sasa *)
let sasa_step e = next_cond e (fun ne -> ne.kind = e.kind && ne.name = e.name)
@@ -139,7 +139,7 @@ let pr () =
e:=goto_last_ckpt !e.nb;
!dot_view ();
store !e.nb
-
+
(* I need to overrides those *)
@@ -160,7 +160,7 @@ let (change_ocaml_plugin_seed: int -> RdbgPlugin.t -> RdbgPlugin.t) =
let new_sasa_call = Printf.sprintf "%s --seed %d" rdbgplugin.id seed in
Printf.printf "%s\n%!" new_sasa_call;
Sasa.SasaRun.make (Array.of_list (string_to_string_list new_sasa_call))
-
+
let (change_plugin_seed : int -> RdbgArg.reactive_program -> RdbgArg.reactive_program) =
fun seed plugin ->
@@ -171,11 +171,11 @@ let (change_plugin_seed : int -> RdbgArg.reactive_program -> RdbgArg.reactive_pr
let change_sasa_seed seed =
args.suts <- List.map (change_plugin_seed seed) args.suts;
args.envs <- List.map (change_plugin_seed seed) args.envs
-
+
(**********************************************************************)
(* won't work in semi-auto modes, but the buttons are hided *)
-let u () = undo (); ignore (round !e);;
+let u () = undo (); ignore (round !e);;
let r () =
let seed = Seed.get dotfile in
Seed.set seed;
@@ -224,23 +224,23 @@ let _ =
(* split the vars into returns (the enab vars, the activated vars,
the other vars) nb: in the "Enab" prefix is removed from enab vars
names; ie we leave only the pid and the action name *)
-type s = (string * string * Data.v)
-let split_data (l:Data.subst list) : s list * s list * s list =
+type s = (string * string * Data.v)
+let split_data (l:Data.subst list) : s list * s list * s list =
let l = List.map (fun (x,v) -> Str.split (Str.regexp "_") x, v) l in
let rec sortv (enab, other) (x,v) =
- match x with
+ match x with
| "Enab"::pid::tail -> (pid, String.concat "_" tail,v)::enab, other
| pid::tail -> enab, (pid,(String.concat "_" tail),v)::other
| [] -> assert false
in
let enab, other = List.fold_left sortv ([],[]) l in
- let acti_names = List.map (fun (pid, n, v) -> pid, n) enab in
+ let acti_names = List.map (fun (pid, n, v) -> pid, n) enab in
let act, vars =
List.partition (fun (pid,n, _) -> List.mem (pid,n) acti_names) other
in
enab, act, vars
-
-
+
+
let only_true l = List.filter (fun (_,_, v) -> v = B true) l
(* Only print the active process values *)
let str_of_sasa_event short e =
@@ -249,7 +249,7 @@ let str_of_sasa_event short e =
let act = only_true act in
let act_pid = List.map (fun (pid,_,_) -> pid) act in
let vars = List.filter (fun (pid, _,_) -> List.mem pid act_pid) vars in
- let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in
+ let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in
let to_string_var (pid, n, v) =
Printf.sprintf "%s_%s=%s" pid n (Data.val_to_string string_of_float v)
in
@@ -258,7 +258,7 @@ let str_of_sasa_event short e =
| _ -> ""
in
let leg = match List.assoc_opt "legitimate" e.data with
- | Some B true -> Printf.sprintf "The current configuration is legitimate\n"
+ | Some B true -> Printf.sprintf "The current configuration is legitimate\n"
| Some B false -> ""
| _ -> ""
in
@@ -272,12 +272,12 @@ let str_of_sasa_event short e =
else
Printf.sprintf "Round %i - Step %i%s%s\n%s%s\n%s%s" (get_round_nb e) e.step
(if e.step <> e.nb then (" - Event " ^ (string_of_int e.nb)) else "") pot
- (RdbgStdLib.string_of_event e)
+ (RdbgStdLib.string_of_event e)
(if vars = [] then "" else
("Active node states: "^(String.concat " " (List.map to_string_var vars))))
leg silent
- )
-
+ )
+
let print_sasa_event short e =
if e.kind <> Ltop then print_event e else
(
@@ -300,7 +300,7 @@ let goto_next_false_oracle e =
next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" &&
List.mem ("ok", Bool) e.outputs &&
not (vb "ok" e))
-
+
let viol_string () =
if args.oracles <> [] then (
e:=goto_next_false_oracle !e; !dot_view (); "An oracle has been violated. Cf the .rif file"
@@ -331,12 +331,12 @@ let _ = add_doc_entry
(**********************************************************************)
(* overide the default checkpointing at rounds
-nb : this is overridden in gtkgui.ml
+nb : this is overridden in gtkgui.ml
*)
let _ = check_ref := fun e -> e.nb = 1 || (e.kind=Exit && e.name="sasa" && round e);;
(**********************************************************************)
-let _ =
+let _ =
add_doc_entry "d"
"unit -> unit" "update the current network with dot" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "ne"
@@ -353,7 +353,7 @@ let _ =
"unit -> unit" "update the current network with patchwork" "sasa" "sasa-rdbg-cmds.ml";
add_doc_entry "os"
"unit -> unit" "update the current network with osage" "sasa" "sasa-rdbg-cmds.ml";
-
+
add_doc_entry "sd" "unit -> unit"
"go to the next step and update the network with one of the GraphViz tools" "sasa"
"sasa-rdbg-cmds.ml";
@@ -395,8 +395,8 @@ let l () =
sf: "^(RdbgMain.doc_msg "sf")^"
pa: "^(RdbgMain.doc_msg "pa")^"
os: "^(RdbgMain.doc_msg "os")^"
-
- nb: for algorithms that have a field named 'par', you can try
+
+ nb: for algorithms that have a field named 'par', you can try
one of the following (which only draw the parent arcs)
d_par: "^(RdbgMain.doc_msg "d")^" (parent arcs only)
ne_par: "^(RdbgMain.doc_msg "ne")^" (parent arcs only)
@@ -406,7 +406,7 @@ let l () =
sf_par: "^(RdbgMain.doc_msg "sf")^" (parent arcs only)
pa_par: "^(RdbgMain.doc_msg "pa")^" (parent arcs only)
os_par: "^(RdbgMain.doc_msg "os")^" (parent arcs only)
-
+
+ Moving commands [*]
sd: "^(RdbgMain.doc_msg "sd")^"
nd: "^(RdbgMain.doc_msg "nd")^"
@@ -430,8 +430,8 @@ let pdf_viewer =
Printf.printf "Warning: no pdf viewer is found to visualize %s\n%!" dotfile;
"ls"
)
-
-let graph_view () =
+
+let graph_view () =
!dot_view ();
let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in
Printf.printf "%s\n!" cmd;
@@ -441,7 +441,7 @@ let graph_view () =
(* let _ = graph_view () *)
let gv = graph_view
-let _ =
+let _ =
add_doc_entry "gv" "unit -> unit"
"launch a pdf viewer of the current network
--
GitLab