test: add the Hoepman ring orientation algo

(not yet finished: the legitimate predicate is not rigth)

salut/test/ring-orientation/Makefile

+TOPOLOGY ?= ring5
+DOT2LUSFLAGS ?=
+SASA_ALGOS := p.ml
+SASAFLAGS += --central-daemon
+DECO_PATTERN="0-:p.ml"
+
+
+include ./Makefile.inc
+include ./Makefile.dot
+
+##############################################################################
+# Non-regression tests
+
+test: kind2-test ring5.lurette  ring15.lurette
+
+clean: genclean
+
+kind2-test:
+	../run-kind2.sh ring 3 ok central uint8 Bitwuzla
+
+##############################################################################
+# Other examples of use
+
+## Some examples of use of ../Makefile.inc
+
+# run a simulation with luciole
+simu: ring7.simu
+
+# make diring4.simu
+kind2: ring7.kind2
+
+##############################################################################
+
+-include ./Makefile.untrack

salut/test/ring-orientation/Makefile.dot

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

salut/test/ring-orientation/Makefile.inc

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

salut/test/ring-orientation/config.ml

+../../../test/ring-orientation/config.ml
\ No newline at end of file

salut/test/ring-orientation/dune

+../../../test/dune2copy
\ No newline at end of file

salut/test/ring-orientation/dune-project

+../../../test/dune-project2copy
\ No newline at end of file

salut/test/ring-orientation/p.lus

+-- Time-stamp: <modified the 22/06/2023 (at 16:05) by Erwan Jahier>
+
+-----------------------------------------------------------
+--Step and Enable functions:
+function p_enable<<const degree:int>>(q : state; neighbors : neigh^degree)
+returns (enabled : bool^actions_number);
+var
+  na : state^degree;
+  p, r : state;
+let
+  na = map<<state,degree>>(neighbors);
+  p = na[0];
+  r = na[1];
+
+
+  enabled = [
+  -- A (0)
+      p.color_0 and     q.color_0 and     r.color_0,
+  -- B (1)
+      p.color_0 and not q.color_0  and    r.color_0
+     and  q.phase_pos, -- not in Figure 3, but necessary to converge!
+  -- C (2)
+  not p.color_0 and not q.color_0 and not r.color_0,
+  --D (3)
+  not p.color_0 and     q.color_0 and not r.color_0
+  and q.phase_pos , -- ditto
+
+  -- Epr (4)
+   (     p.color_0 and     p.phase_pos and
+          q.color_0 and not q.phase_pos and
+      not r.color_0 and not r.phase_pos),
+
+  -- Erp (5)
+  ((not p.color_0 and not p.phase_pos and
+          q.color_0 and not q.phase_pos and
+          r.color_0 and     r.phase_pos)),
+
+  -- Fpr (6)
+   ( not p.color_0 and     p.phase_pos and
+      not q.color_0 and not q.phase_pos and
+          r.color_0 and not r.phase_pos),
+
+  -- Frp (7)
+  ((    p.color_0 and not p.phase_pos and
+      not q.color_0 and not q.phase_pos and
+      not r.color_0 and     r.phase_pos)),
+
+  -- G
+  ( (     p.color_0 and not p.phase_pos and
+          q.color_0 and not q.phase_pos and
+      not r.color_0       )
+ or ((not p.color_0 and
+          q.color_0 and not q.phase_pos and
+          r.color_0 and not r.phase_pos))),
+  -- H
+  ( (     p.color_0 and     p.phase_pos and
+          q.color_0 and     q.phase_pos and
+      not r.color_0       )
+ or ((not p.color_0 and
+          q.color_0 and     q.phase_pos and
+          r.color_0 and     r.phase_pos))),
+  -- I
+  ( ( not p.color_0 and not p.phase_pos and
+      not q.color_0 and not q.phase_pos and
+          r.color_0       )
+ or ((    p.color_0 and
+      not q.color_0 and not q.phase_pos and
+      not r.color_0 and not r.phase_pos))),
+  -- J
+  ( ( not p.color_0 and     p.phase_pos and
+      not q.color_0 and     q.phase_pos and
+          r.color_0       )
+ or ((    p.color_0 and
+      not q.color_0 and     q.phase_pos and
+      not r.color_0 and     r.phase_pos)))
+];
+tel;
+
+function p_step<<const d:int>>(
+  q : state;
+  neighbors : neigh^d;
+  a : action)
+returns (new_q : state);
+var
+  na : state^d;
+  p, r : state;
+let
+  na = map<<state,d>>(neighbors);
+  p = na[0];
+  r = na[1];
+  new_q = if a = A then state { color_0 = false ; phase_pos = false ; orient_left = q.orient_left }
+     else if a = B then state { color_0 = false ; phase_pos = false ; orient_left = q.orient_left }
+     else if a = C then state { color_0 = true  ; phase_pos = false ; orient_left = q.orient_left }
+     else if a = D then state { color_0 = true  ; phase_pos = false ; orient_left = q.orient_left }
+
+     else if a = Epr then state { color_0 = false ; phase_pos = true  ; orient_left = orient(p,r) }
+     else if a = Erp then state { color_0 = false ; phase_pos = true  ; orient_left = orient(r,p) }
+     else if a = Fpr then state { color_0 = true  ; phase_pos = true  ; orient_left = orient(p,r) }
+     else if a = Frp then state { color_0 = true  ; phase_pos = true  ; orient_left = orient(r,p) }
+
+     else if a = G then state { color_0 = true  ; phase_pos = true  ; orient_left = q.orient_left }
+     else if a = H then state { color_0 = true  ; phase_pos = false ; orient_left = q.orient_left }
+     else if a = I then state { color_0 = false ; phase_pos = true  ; orient_left = q.orient_left }
+     else (* a = J *)   state { color_0 = false ; phase_pos = false ; orient_left = q.orient_left };
+tel;
+
+function orient(p,r : state) returns (res : bool);
+let
+  res = if     p.phase_pos and not r.phase_pos then true else false;
+ --       if not p.phase_pos and     r.phase_pos then false else
+ --       if     p.phase_pos and     r.phase_pos then false else
+ --       (* not p.phase_pos and not r.phase_pos *)   false
+
+
+tel;
\ No newline at end of file

salut/test/ring-orientation/p.ml

+../../../test/ring-orientation/p.ml
\ No newline at end of file

salut/test/ring-orientation/ring_orientation_oracle.lus

+
+
+include "../../lib/utils.lus"
+
+
+node ring_orientation_oracle(
+  legitimate : bool;
+--  ocaml_cost : real;
+  ocaml_enabled : bool^actions_number^card;
+  active : bool^actions_number^card;
+  ocaml_config : state^card;
+  round:bool;
+  round_nb:int;
+)
+returns (ok : bool);
+var
+  lustre_config : state^card;
+  lustre_enabled : bool^actions_number^card;
+--  lustre_cost:int;
+  lustre_round:bool;
+  lustre_round_nb:int;
+let
+  ok, lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+     ring_orientation_oracle_debug(legitimate, ocaml_enabled,active, ocaml_config, round, round_nb);
+
+tel;
+
+node ring_orientation_oracle_debug(
+  legitimate : bool;
+--  ocaml_cost : real;
+  ocaml_enabled : bool^actions_number^card;
+  active : bool^actions_number^card;
+  ocaml_config : state^card;
+  round:bool;
+  round_nb:int;
+)
+returns (ok : bool;
+  lustre_config : state^card;
+  lustre_enabled : bool^actions_number^card;
+--  lustre_cost:int;
+  lustre_round:bool;
+  lustre_round_nb:int
+);
+
+
+let
+  lustre_config, lustre_enabled, lustre_round, lustre_round_nb =
+    topology(active -> pre active, -- ignored at the first step
+             ocaml_config -- used at the first step only
+             );
+
+  ok = lustre_enabled = ocaml_enabled
+       -- compare the sasa dot interpretation and the salut dot to lustre compilation
+       and lustre_config = ocaml_config
+
+   --    and round = lustre_round
+   --    and round_nb = lustre_round_nb
+;
+tel
+
+function to_state(color_0, phase_pos, orient_left :bool)
+returns ( res : state);
+let
+  res = state {  color_0 = color_0; phase_pos = phase_pos; orient_left = orient_left };
+tel;

salut/test/ring-orientation/state.lus

+-- Time-stamp: <modified the 03/07/2023 (at 16:46) by Erwan Jahier>
+
+type state = { color_0 : bool ; phase_pos : bool ; orient_left : bool };
+
+type action = enum { A , B , C , D , Epr , Erp , Fpr , Frp , G , H , I , J };
+const actions_number = 12;
+
+function action_of_int(i : int) returns (a : action);
+let
+  a = if i = 0 then A else
+      if i = 1 then B else
+      if i = 2 then C else
+      if i = 3 then D else
+      if i = 4 then Epr else
+      if i = 5 then Erp else
+      if i = 6 then Fpr else
+      if i = 7 then Frp else
+      if i = 8 then G else
+      if i = 9 then H else
+      if i = 10 then I else J;
+tel;
+
+-- This legitimate function is not good enough to be able to prove closure
+-- Indeed, the orientation field migth be oriented by chance, while the other
+-- fields (that are used in guards) are not in a legitimate configuration.
+-- Adding  L3 property (p16) in the definition of legitimate should be enough
+-- to fix this problem.
+function legitimate<<const actions_number:int; const card:int>>(
+         enables : bool^actions_number^card; config: state^card)
+returns (res : bool);
+var
+  orientations : bool ^ card;
+  one_token : bool;
+let
+  orientations = map<<get_orientation,card>>(config);
+  one_token = nary_xor<<card>>(map<<nary_or<<actions_number>>,card>> (enables));
+  res = one_token and all_equal <<bool,card>>(orientations);
+tel;
+function get_orientation(s:state) returns (res:bool);
+let
+  res = s.orient_left;
+tel;
+
+(* XXX finish me
+function L3 <<const an:int;const card:int;const n:int>>(config: state^card) returns (res : bool);
+let
+  res = with n = 0
+        then true
+        else L3<<an,card,n>>
+tel;
+function I3 <<const an:int;const n:int>>(config: state^card) returns (res : bool);
+let
+  res = with n =
+        then ???
+        else
+            zl(config[n])
+
+tel;
+function O3 <<const an:int;const n:int>>(config: state^card) returns (res : bool);
+let
+  res = with n = 0
+        then ???
+        else
+tel;
+
+-- zero left
+function zl(s:state)  returns (res:bool); let res = s.color_0 and s.orient_left tel;
+function zpl(s:state) returns (res:bool); let res = zl(s) and s.phase_pos tel;
+function zml(s:state) returns (res:bool); let res = zl(s) and not s.phase_pos tel;
+-- one left
+function ol(s:state)  returns (res:bool); let res = (not s.color_0) and s.orient_left tel;
+function opl(s:state) returns (res:bool); let res = ol(s) and s.phase_pos tel;
+function oml(s:state) returns (res:bool); let res = ol(s) and not s.phase_pos tel;
+*)
\ No newline at end of file

salut/test/ring-orientation/state.ml

+../../../test/ring-orientation/state.ml
\ No newline at end of file

salut/test/ring-orientation/verify.lus

+-- hint: call me with ../run-kind2.sh
+include "daemon_hyp.lus"
+
+const worst_case = card * card;
+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, converge_worst_case,worst_case_is_tigth : bool;
+  steps : int;
+  round:bool; round_nb:int;
+let
+  assert(true -> daemon<<actions_number,card>> (active, pre enabled));
+  assert(config = init_config -> true);
+  steps = 0 -> (pre(steps) + 1);
+  config, enabled, round, round_nb = topology(active, init_config);
+  -- stability = mutual exclusion: exactly 1 node is enabled at a time
+  legitimate = legitimate<<actions_number,card>>(enabled,config);
+
+  closure = steps > 1 => (pre(legitimate) => legitimate);
+
+  converge_worst_case = (round_nb >= worst_case) => legitimate;
+  worst_case_is_tigth = (round_nb >= worst_case-1) => legitimate;
+  ok =
+    -- closure is wrong because legitimate needs to be more specific (cf state.lus)
+    converge_worst_case ; -- closure and;
+tel;
\ No newline at end of file

test/ring-orientation/Makefile

+# Time-stamp: <modified the 21/06/2023 (at 12:04) by Erwan Jahier>
+
+DECO_PATTERN="0-:p.ml"
+-include ./Makefile.dot
+-include ./Makefile.inc
+
+##############################################################################
+# Non-regression tests
+
+test:  grid5.gm_test grid5.rdbg-test clean
+
+# update golden-master tests (if necessary)
+utest:
+	make grid5.ugm_test || echo "grid4 ok"
+
+##############################################################################
+# Other examples of use
+
+rdbg: grid5.dot grid5.ml
+	rdbg --sasa -sut "sasa grid5.dot"
+
+clean: genclean
+	rm -f grid*.* diring*.* clique*.* er*.*

test/ring-orientation/Makefile.dot

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

test/ring-orientation/Makefile.inc

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

test/ring-orientation/config.ml

+
+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 init_search_utils = None (* To provide to use --init-search *)
+
+let legitimate = None (* XXX this is wrong: FIXME *)

test/ring-orientation/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/ring-orientation/dune-project

+../dune-project2copy
\ No newline at end of file