From 171516875707462e62fca17ea206798beae175c8 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Mon, 10 Jul 2023 11:51:17 +0200
Subject: [PATCH] test: add the Hoepman ring orientation algo (not yet
finished: the legitimate predicate is not rigth)
---
salut/test/ring-orientation/Makefile | 34 ++++++
salut/test/ring-orientation/Makefile.dot | 1 +
salut/test/ring-orientation/Makefile.inc | 1 +
salut/test/ring-orientation/config.ml | 1 +
salut/test/ring-orientation/dune | 1 +
salut/test/ring-orientation/dune-project | 1 +
salut/test/ring-orientation/dune-workspace | 0
salut/test/ring-orientation/p.lus | 115 ++++++++++++++++++
salut/test/ring-orientation/p.ml | 1 +
.../ring_orientation_oracle.lus | 65 ++++++++++
salut/test/ring-orientation/state.lus | 74 +++++++++++
salut/test/ring-orientation/state.ml | 1 +
salut/test/ring-orientation/verify.lus | 28 +++++
test/ring-orientation/Makefile | 23 ++++
test/ring-orientation/Makefile.dot | 1 +
test/ring-orientation/Makefile.inc | 1 +
test/ring-orientation/config.ml | 6 +
test/ring-orientation/dune | 59 +++++++++
test/ring-orientation/dune-project | 1 +
test/ring-orientation/dune-workspace | 0
test/ring-orientation/p.ml | 109 +++++++++++++++++
test/ring-orientation/some_session | 7 ++
test/ring-orientation/state.ml | 15 +++
23 files changed, 545 insertions(+)
create mode 100644 salut/test/ring-orientation/Makefile
create mode 120000 salut/test/ring-orientation/Makefile.dot
create mode 120000 salut/test/ring-orientation/Makefile.inc
create mode 120000 salut/test/ring-orientation/config.ml
create mode 120000 salut/test/ring-orientation/dune
create mode 120000 salut/test/ring-orientation/dune-project
create mode 100644 salut/test/ring-orientation/dune-workspace
create mode 100644 salut/test/ring-orientation/p.lus
create mode 120000 salut/test/ring-orientation/p.ml
create mode 100644 salut/test/ring-orientation/ring_orientation_oracle.lus
create mode 100644 salut/test/ring-orientation/state.lus
create mode 120000 salut/test/ring-orientation/state.ml
create mode 100644 salut/test/ring-orientation/verify.lus
create mode 100644 test/ring-orientation/Makefile
create mode 120000 test/ring-orientation/Makefile.dot
create mode 120000 test/ring-orientation/Makefile.inc
create mode 100644 test/ring-orientation/config.ml
create mode 100644 test/ring-orientation/dune
create mode 120000 test/ring-orientation/dune-project
create mode 100644 test/ring-orientation/dune-workspace
create mode 100644 test/ring-orientation/p.ml
create mode 100644 test/ring-orientation/some_session
create mode 100644 test/ring-orientation/state.ml
diff --git a/salut/test/ring-orientation/Makefile b/salut/test/ring-orientation/Makefile
new file mode 100644
index 00000000..3949e640
--- /dev/null
+++ b/salut/test/ring-orientation/Makefile
@@ -0,0 +1,34 @@
+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
diff --git a/salut/test/ring-orientation/Makefile.dot b/salut/test/ring-orientation/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/salut/test/ring-orientation/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/salut/test/ring-orientation/Makefile.inc b/salut/test/ring-orientation/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/salut/test/ring-orientation/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/salut/test/ring-orientation/config.ml b/salut/test/ring-orientation/config.ml
new file mode 120000
index 00000000..25afd9a8
--- /dev/null
+++ b/salut/test/ring-orientation/config.ml
@@ -0,0 +1 @@
+../../../test/ring-orientation/config.ml
\ No newline at end of file
diff --git a/salut/test/ring-orientation/dune b/salut/test/ring-orientation/dune
new file mode 120000
index 00000000..a1ef974a
--- /dev/null
+++ b/salut/test/ring-orientation/dune
@@ -0,0 +1 @@
+../../../test/dune2copy
\ No newline at end of file
diff --git a/salut/test/ring-orientation/dune-project b/salut/test/ring-orientation/dune-project
new file mode 120000
index 00000000..f539fb46
--- /dev/null
+++ b/salut/test/ring-orientation/dune-project
@@ -0,0 +1 @@
+../../../test/dune-project2copy
\ No newline at end of file
diff --git a/salut/test/ring-orientation/dune-workspace b/salut/test/ring-orientation/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/salut/test/ring-orientation/p.lus b/salut/test/ring-orientation/p.lus
new file mode 100644
index 00000000..5e57a8b0
--- /dev/null
+++ b/salut/test/ring-orientation/p.lus
@@ -0,0 +1,115 @@
+-- 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
diff --git a/salut/test/ring-orientation/p.ml b/salut/test/ring-orientation/p.ml
new file mode 120000
index 00000000..c3e34af2
--- /dev/null
+++ b/salut/test/ring-orientation/p.ml
@@ -0,0 +1 @@
+../../../test/ring-orientation/p.ml
\ No newline at end of file
diff --git a/salut/test/ring-orientation/ring_orientation_oracle.lus b/salut/test/ring-orientation/ring_orientation_oracle.lus
new file mode 100644
index 00000000..374b7a3f
--- /dev/null
+++ b/salut/test/ring-orientation/ring_orientation_oracle.lus
@@ -0,0 +1,65 @@
+
+
+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;
diff --git a/salut/test/ring-orientation/state.lus b/salut/test/ring-orientation/state.lus
new file mode 100644
index 00000000..3e3aaf2c
--- /dev/null
+++ b/salut/test/ring-orientation/state.lus
@@ -0,0 +1,74 @@
+-- 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
diff --git a/salut/test/ring-orientation/state.ml b/salut/test/ring-orientation/state.ml
new file mode 120000
index 00000000..b648093a
--- /dev/null
+++ b/salut/test/ring-orientation/state.ml
@@ -0,0 +1 @@
+../../../test/ring-orientation/state.ml
\ No newline at end of file
diff --git a/salut/test/ring-orientation/verify.lus b/salut/test/ring-orientation/verify.lus
new file mode 100644
index 00000000..48685d9f
--- /dev/null
+++ b/salut/test/ring-orientation/verify.lus
@@ -0,0 +1,28 @@
+-- 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
diff --git a/test/ring-orientation/Makefile b/test/ring-orientation/Makefile
new file mode 100644
index 00000000..c6838f11
--- /dev/null
+++ b/test/ring-orientation/Makefile
@@ -0,0 +1,23 @@
+# 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*.*
diff --git a/test/ring-orientation/Makefile.dot b/test/ring-orientation/Makefile.dot
new file mode 120000
index 00000000..618c8ab0
--- /dev/null
+++ b/test/ring-orientation/Makefile.dot
@@ -0,0 +1 @@
+../Makefile.dot
\ No newline at end of file
diff --git a/test/ring-orientation/Makefile.inc b/test/ring-orientation/Makefile.inc
new file mode 120000
index 00000000..b9a83c9d
--- /dev/null
+++ b/test/ring-orientation/Makefile.inc
@@ -0,0 +1 @@
+../Makefile.inc
\ No newline at end of file
diff --git a/test/ring-orientation/config.ml b/test/ring-orientation/config.ml
new file mode 100644
index 00000000..54c8032f
--- /dev/null
+++ b/test/ring-orientation/config.ml
@@ -0,0 +1,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 init_search_utils = None (* To provide to use --init-search *)
+
+let legitimate = None (* XXX this is wrong: FIXME *)
diff --git a/test/ring-orientation/dune b/test/ring-orientation/dune
new file mode 100644
index 00000000..70215208
--- /dev/null
+++ b/test/ring-orientation/dune
@@ -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/ring-orientation/dune-project b/test/ring-orientation/dune-project
new file mode 120000
index 00000000..1c5c1f50
--- /dev/null
+++ b/test/ring-orientation/dune-project
@@ -0,0 +1 @@
+../dune-project2copy
\ No newline at end of file
diff --git a/test/ring-orientation/dune-workspace b/test/ring-orientation/dune-workspace
new file mode 100644
index 00000000..e69de29b
diff --git a/test/ring-orientation/p.ml b/test/ring-orientation/p.ml
new file mode 100644
index 00000000..fbbc86c2
--- /dev/null
+++ b/test/ring-orientation/p.ml
@@ -0,0 +1,109 @@
+(* Time-stamp: <modified the 07/07/2023 (at 15:24) by Erwan Jahier> *)
+
+(* Uniform deterministic self-stabilizing ring-orientation on odd-length rings
+ Hoepman, Jaap-Henk
+ WDAG'1994
+
+ hyp: central daemon
+ *)
+
+open Algo
+open State
+
+let (init_state: int -> string -> 'st) =
+ fun _nl _ ->
+ { color_0 = Random.bool () ; phase_pos = Random.bool () ; orient_left = Random.bool () }
+
+let (enable_f: 'st -> 'st neighbor list -> action list) =
+ fun q nl ->
+ assert (card() mod 2 = 1); (* Odd rings only *)
+ match List.map state nl with
+ | [p; r] -> (match p,q,r with
+ | { color_0 = true ; _ }, { color_0 = true ; _ }, { color_0 = true ; _ } -> ["a"]
+ | { color_0 = true ; _ }, { color_0 = false ; phase_pos = true ; _ }, { color_0 = true ; _ } -> ["b"]
+ | { color_0 = false ; _ }, { color_0 = false ; _ }, { color_0 = false ; _ } -> ["c"]
+ | { color_0 = false ; _ }, { color_0 = true ; phase_pos = true; _ }, { color_0 = false ; _ } -> ["d"]
+
+ | { color_0 = true ; phase_pos = true ; _ },
+ { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = false ; phase_pos = false ; _ } -> ["e_pr"]
+
+ | { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = true ; phase_pos = true ; _ } -> ["e_rp"]
+
+ | { color_0 = false ; phase_pos = true ; _ },
+ { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = true ; phase_pos = false ; _ } -> ["f_pr"]
+
+ | { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = false ; phase_pos = true ; _ } -> ["f_rp"]
+
+ | { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = false ; _ }
+ | { color_0 = false ; _ },
+ { color_0 = true ; phase_pos = false ; _ },
+ { color_0 = true ; phase_pos = false ; _ } -> ["g"]
+
+ | { color_0 = true ; phase_pos = true ; _ },
+ { color_0 = true ; phase_pos = true ; _ },
+ { color_0 = false ; _ }
+ | { color_0 = false ; _ },
+ { color_0 = true ; phase_pos = true ; _ },
+ { color_0 = true ; phase_pos = true ; _ } -> ["h"]
+
+ | { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = true ; _ }
+ | { color_0 = true ; _ },
+ { color_0 = false ; phase_pos = false ; _ },
+ { color_0 = false ; phase_pos = false ; _ } -> ["i"]
+
+ | { color_0 = false ; phase_pos = true ; _ },
+ { color_0 = false ; phase_pos = true ; _ },
+ { color_0 = true ; _ }
+ | { color_0 = true ; _ },
+ { color_0 = false ; phase_pos = true ; _ },
+ { color_0 = false ; phase_pos = true ; _ } -> ["j"]
+
+ | _ -> []
+ )
+ | _ -> failwith "only works on rings"
+
+(* | { color_0 = cp ; phase_pos = pp ; _ },
+ { color_0 = cq ; phase_pos = pq ; _ },
+ { color_0 = cr ; phase_pos = pr ; _ } ->
+ let c2s c = if c then "0" else "1" in
+ let p2s c = if c then "+" else "-" in
+ failwith (Printf.sprintf "Missing case: %s%s %s%s %s%s "
+ (c2s cp) (p2s pp) (c2s cq) (p2s pq) (c2s cr) (p2s pr) )
+
+ *)
+
+let orientation = function
+ | [ { phase_pos = true ; _} ; { phase_pos = false; _ } ] -> true
+ | [ { phase_pos = false ; _} ; { phase_pos = true ; _ } ] -> false
+ | [ { phase_pos = true ; _} ; { phase_pos = true; _ } ] -> assert false
+ | [ { phase_pos = false ; _} ; { phase_pos = false; _ } ] -> assert false
+ | _ -> assert false
+
+let (step_f : 'st -> 'st neighbor list -> action -> 'st ) =
+ fun e nl ->
+ function
+ | "a" -> { e with color_0 = false ; phase_pos = false }
+ | "b" -> { e with color_0 = false ; phase_pos = false }
+ | "c" -> { e with color_0 = true ; phase_pos = false }
+ | "d" -> { e with color_0 = true ; phase_pos = false }
+
+ | "e_pr" -> { color_0 = false ; phase_pos = true ; orient_left = orientation (List.map state nl) }
+ | "e_rp" -> { color_0 = false ; phase_pos = true ; orient_left = orientation (List.map state nl |> List.rev) }
+ | "f_pr" -> { color_0 = true ; phase_pos = true ; orient_left = orientation (List.map state nl) }
+ | "f_rp" -> { color_0 = true ; phase_pos = true ; orient_left = orientation (List.map state nl |> List.rev) }
+
+ | "g" -> { e with color_0 = true ; phase_pos = true }
+ | "h" -> { e with color_0 = true ; phase_pos = false }
+ | "i" -> { e with color_0 = false ; phase_pos = true }
+ | "j" -> { e with color_0 = false ; phase_pos = false }
+ | _ -> e
diff --git a/test/ring-orientation/some_session b/test/ring-orientation/some_session
new file mode 100644
index 00000000..96b69b57
--- /dev/null
+++ b/test/ring-orientation/some_session
@@ -0,0 +1,7 @@
+n
+n
+n
+n
+wait 3
+print_event !e;;
+
diff --git a/test/ring-orientation/state.ml b/test/ring-orientation/state.ml
new file mode 100644
index 00000000..2f4a722b
--- /dev/null
+++ b/test/ring-orientation/state.ml
@@ -0,0 +1,15 @@
+(* Time-stamp: <modified the 29/06/2023 (at 16:45) by Erwan Jahier> *)
+
+type t = { color_0 : bool ; phase_pos : bool ; orient_left : bool }
+
+let to_string s =
+ Printf.sprintf "color_0=%b phase_pos=%b orient_left=%b" s.color_0 s.phase_pos s.orient_left
+
+let (of_string: (string -> t) option) =
+ Some (fun s ->
+ Scanf.sscanf s "color_0=%B phase_pos=%B orient_left=%B"
+ (fun color_0 phase_pos orient_left -> { color_0 ; phase_pos ; orient_left }))
+
+let copy x = x
+
+let actions = ["a";"b";"c";"d";"e_pr";"e_rp";"f_pr";"f_rp";"g";"h";"i";"j"]
--
GitLab