test: add the Ghosh mutual exclusion algo in sasa/test/ and salut/sasa/test/

salut/test/ghosh/p_last.lus

+
+
+function p_last_enable<<const degree:int>>(s2 : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ state(neighbors[1]) = s2 ];
+tel;
+
+function p_last_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;

salut/test/ghosh/p_last.ml

+../../../test/ghosh/p_last.ml
\ No newline at end of file

salut/test/ghosh/p_odd.lus

+
+
+function p_odd_enable<<const degree:int>>(s2 : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+let
+  enabled = [ state(neighbors[0]) = state(neighbors[1]) and
+              state(neighbors[2]) = state(neighbors[1]) and
+              s2 = not state(neighbors[0])
+             ];
+tel;
+
+function p_odd_step<<const degree:int>>(
+  this : state;
+  neighbors : neigh^degree; action : action)
+returns (new : state);
+let
+  new = not this;
+tel;

salut/test/ghosh/p_odd.ml

+../../../test/ghosh/p_odd.ml
\ No newline at end of file

salut/test/ghosh/state.lus

+
+type state = bool;
+
+type action = enum { T };
+const actions_number = 1;
+
+function action_of_int(i : int) returns (a : action);
+let
+  a = T;
+tel;
+
+function legitimate<<const actions_number:int; const card:int>>(enables : bool^actions_number^card; config: state^card)
+returns (res : bool);
+let
+  res=n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enables));
+tel;

salut/test/ghosh/state.ml

+../../../test/ghosh/state.ml
\ No newline at end of file

salut/test/ghosh/verify.lus

+
+
+const n = card;
+
+-- Theorem XXX
+
+ const worst_case=100;
+
+node verify(
+  active : bool^actions_number^card;
+  init_config : state^card
+)
+returns (ok : bool);
+var
+  config : state^card;
+  enabled : bool^actions_number^card;
+  legitimate, closure, theorem : bool;
+  steps : int;
+  round:bool; round_nb:int;
+let
+-- the worst-case in necessarily central
+--	assert(true -> daemon_is_central<<actions_number,card>>(active, pre enabled));
+	assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
+--	assert(true -> daemon_is_synchronous<<actions_number,card>>(active, pre enabled));
+
+	config, enabled, round, round_nb = topology(active, init_config);
+        assert(config = init_config -> true);
+
+	-- stability = mutual exclusion: exactly 1 node is enabled at a time
+        legitimate = legitimate<<actions_number,card>>(enabled,config);
+
+	closure = true -> (pre(legitimate) => legitimate);
+
+	steps = 0 -> (pre(steps) + 1);
+        theorem  = (steps >= worst_case) => legitimate;
+
+
+	ok =  true
+	     and closure
+             and theorem
+;
+tel;

salut/test/run-kind2.sh

@@ -100,7 +100,7 @@ fi
 kind2_opt="--timeout 36000 -json -v "
 kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
 kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
-kind2_opt="--smt_solver $solver --enable BMC --enable IND --timeout 36000 $@"
+kind2_opt="--smt_solver $solver --enable BMC --enable IND  --timeout 36000 $@"
 
 # --qe_method {precise|impl|cooper}
 
@@ -111,11 +111,12 @@ cp Makefile ${TMP}
 cp ${GITROOT}/salut/test/Makefile.inc  ${TMP}
 cp ${GITROOT}/salut/test/Makefile.dot  ${TMP}
 cp *.lus ${TMP}
+cp $main.dot ${TMP} -f
 cp ${LIB_LUS} ${TMP}
 cd  ${TMP}
 
-make $main.dot || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
-make ${main}_const.lus
+make $main.dot || [ -f $main.dot ] || (echo "E: is Makefile.dot included from Makefile?"; exit 2)
+salut $main.dot
 
 # Get rif of the lutre v6 constructs that kind2 does not handle
 lv6 -eei ${LIB_LUS} $main.lus verify.lus ${main}_const.lus -n verify --lustre-v4 -en -knc -o $main.verify.lv4

test/Makefile

@@ -18,6 +18,7 @@ test:
 	cd rsp-tree/ && make test
 	cd toy-example-a5sf/ && make test
 	cd k-clustering/ && make test
+	cd ghosh/ && make test
 	echo "Every test went fine!"
 
 clean:
@@ -40,6 +41,7 @@ clean:
 	cd rsp-tree/ && make clean
 	cd toy-example-a5sf/ && make clean
 	cd k-clustering/ && make clean
+	cd ghosh/ && make clean
 
 utest:
 	cd skeleton/ &&	make test
@@ -60,5 +62,6 @@ utest:
 	cd rsp-tree/ && make utest
 	cd toy-example-a5sf/ && make utest
 	cd k-clustering/ && make utest
+	cd ghosh/ && make utest
 
 -include Makefile.untracked

test/dijkstra-ring/state.ml

 
-(* semi-anonymous network: each node knows if its neighbors is the root! *)
-type t = { root: bool ; v : int } 
+(* semi-anonymous network: each node knows if its neighbors is the root!
+Actually only necessary to define the legitimate predicate
+*)
+type t = { root: bool ; v : int }
 let to_string s = Printf.sprintf "c=%i" s.v
 let first = ref true
 let (of_string: (string -> t) option) =
@@ -23,8 +25,8 @@ let (of_string: (string -> t) option) =
       in
       (* Printf.printf "state.ml: { root = %b ; c = %d }\n%!" res.root res.v; *)
       res
-    
+
     )
-    
+
 let copy x = x
 let actions = ["T"]

test/ghosh/Makefile

+# Time-stamp: <modified the 30/05/2023 (at 17:13) by Erwan Jahier>
+
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
+
+##############################################################################
+# Non-regression tests
+
+test:  ghosh8.gm_test clean
+
+# update golden-master tests (if necessary)
+utest:
+	make ghosh8.ugm_test || echo "grid4 ok"
+
+##############################################################################
+# Other examples of use
+
+gui: ghosh8.rdbgui
+
+clean: genclean
+	rm -f grid*.* diring*.* clique*.* er*.*

test/ghosh/Makefile.dot

+../Makefile.dot
\ No newline at end of file

test/ghosh/Makefile.inc

+# Time-stamp: <modified the 27/02/2023 (at 16:05) by Erwan Jahier>
+#
+# Define some default rules that ought to work most of the time
+#
+
+sasa=sasa
+
+LIB=-package algo
+
+ifndef DAEMON
+# some rules uses this one
+DAEMON=
+endif
+
+
+
+# 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:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.cma:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.cmxa:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+%.a:
+	[ -f $*.ml ] && rm $*.ml || true
+	topology=$* dune build
+
+
+genclean:
+	rm -f *.cmxs sasa *.cm* *.o *.pdf *.rif *.gp *.log *.dro *.seed *.c *.h sasa-*.dot *.cmt *.annot
+	rm -rf .rdbg-session*.ml rdbg-session*.ml luretteSession* a.out *.cov .read_dot.ml
+	rm -f *.exec  grid*.ml  rdbg-history .rdbg-cmds.ml rdbg-cmds.ml my-rdbg-tuning.ml
+	dune clean
+
+clean: genclean
+.PRECIOUS: %.dot
+
+##################################################################################
+#
+-include Makefile.untracked
+
+g:gnuplot
+s:sim2chrogtk
+
+
+%.lut: %.dot %.cmxs
+	sasa -gld $< || echo "==> ok, I'll use the existing $@ file"
+
+%_oracle.lus: %.dot %.cmxs
+	sasa -glos $< || echo "==> ok, I'll use the existing $@ file"
+
+%.rif: %.cmxs %.dot
+	$(sasa) $(sasaopt) $*.dot > $*.rif
+
+%.pdf:
+	dot -Tpdf $*.dot -o $*.pdf
+	xpdf $*.pdf
+
+%.ocd: %.ml
+	rdbg -camldebug -sut "sasa $.dot" -l 1000
+
+%.test: %.dot %.cmxs
+	sasa  $<
+
+############################################################################################
+# Golden master tests
+# compare the generated rif file with a previously generated reference
+EXPDIR=`rdbg --ocaml-version`
+$(EXPDIR):
+	[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
+
+%.gm_test: %.cmxs $(EXPDIR)
+	sasa  $*.dot -seed 42 -l 1000 > $*.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: %.cmxs $(EXPDIR)
+	sasa  $*.dot -seed 42 -l 1000 > $*.rif && \
+	cp $*.rif $(EXPDIR)/$*.rif.exp
+
+# fix the seed (used, e.g., in Makefile.dot) for the non-regression tests
+ifndef SEED
+  SEED = --seed 42
+endif
+############################################################################################
+
+%.rdbg: %.cma
+	ledit -h rdbg-history -x rdbg --sasa -sut "sasa $* $(DAEMON)"  -l 10000
+
+%.rdbg-test: %.cma
+	rdbg --sasa -sut "sasa $*.dot $(DAEMON)" -go --input some_session -l 10000 \
+		| grep Error > $*.rdbg-test.log && echo "Error: 'make $@' failed" \
+		  && cat $*.rdbg-test.log && exit 2  || echo "'make $@' suceeds"
+
+%.rdbgui: %.cma
+	ledit -h rdbg-history -x rdbgui4sasa -sut "sasa $*.dot"  -l 10000

test/ghosh/config.ml

+open Algo
+open State
+
+let (legitimate: pid list -> (pid -> t * (t neighbor * pid) list) -> bool) =
+  fun  pidl get ->
+  (* increment the token number i if pid is enabled *)
+  let incr_token i pid =
+    let s, nl = get pid in
+    let nl = List.map fst  nl in
+    let have_token =
+      match s.kind with
+      | Bottom -> P0.enable_f s nl <> []
+      | Odd -> P_odd.enable_f s nl <> []
+      | Even -> P_even.enable_f s nl <> []
+      | Top -> P_last.enable_f s nl <> []
+    in
+    if have_token then i+1 else i
+  in
+  (* Now let's iterate on all the nodes starting from |tokens|=0 *)
+  let token_nb = List.fold_left incr_token 0 pidl in
+  (* if there is 1 token, returns true *)
+  token_nb = 1
+let legitimate = Some legitimate
+
+let potential = None
+let fault = None (* None => the simulation stop once a legitimate configuration is reached *)
+
+open Algo
+
+let n2s nl n =
+  match nl with
+  | [B(b)] -> { n with s = b }
+  | _ -> assert false
+
+let s2vl b = [B(b.s)]
+
+let init_search_utils = Some(s2vl, n2s)

test/ghosh/dune

+;; 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/../..))"))
+ )

test/ghosh/dune-project

+(lang dune 3.0)

test/ghosh/ghosh10.dot

+graph g8 {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+
+  p1 -- p3 -- p5 -- p7 -- p9
+  p0 -- p2 -- p4 -- p6 -- p8
+}

test/ghosh/ghosh12.dot

+graph g {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_even.ml"]
+  p10 [algo="p_odd.ml"]
+  p11 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+  p10-- p9
+  p11-- p10
+
+  p1 -- p3 -- p5 -- p7 -- p9 -- p11
+  p0 -- p2 -- p4 -- p6 -- p8 -- p10
+}

test/ghosh/ghosh14.dot

+graph g {
+
+
+  p0 [algo="p0.ml"]
+  p1 [algo="p_even.ml"]
+  p2 [algo="p_odd.ml"]
+  p3 [algo="p_even.ml"]
+  p4 [algo="p_odd.ml"]
+  p5 [algo="p_even.ml"]
+  p6 [algo="p_odd.ml"]
+  p7 [algo="p_even.ml"]
+  p8 [algo="p_odd.ml"]
+  p9 [algo="p_even.ml"]
+  p10 [algo="p_odd.ml"]
+  p11 [algo="p_even.ml"]
+  p12 [algo="p_odd.ml"]
+  p13 [algo="p_last.ml"]
+
+  p1 -- p0
+  p2 -- p1
+  p3 -- p2
+  p4 -- p3
+  p5 -- p4
+  p6 -- p5
+  p7 -- p6
+  p8 -- p7
+  p9 -- p8
+  p10-- p9
+  p11-- p10
+  p12-- p11
+  p13-- p12
+
+  p1 -- p3 -- p5 -- p7 -- p9 -- p11 -- p13
+  p0 -- p2 -- p4 -- p6 -- p8 -- p10 -- p12
+}