Skip to content
Snippets Groups Projects
Commit abaa00b1 authored by erwan's avatar erwan
Browse files

test: change the state scan/parse conventions so that it is compatible

with the dot output of --global-init-search
parent e5a41b8a
No related branches found
No related tags found
No related merge requests found
Pipeline #137911 failed
graph fig52 { graph fig52 {
Root [algo="p.ml" init="{is_root=1 ; alpha=0; par=-1}"]
p2 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
p3 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
p4 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
p5 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
p6 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
p7 [algo="p.ml" init="{is_root=0 ; alpha=0; par=0}"]
Root -- p2 -- p3 -- p4 -- p5 -- p6 Root [algo="p.ml" init="isRoot=true alpha=0 par=-1"]
p2 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
p3 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
p4 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
p5 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
p6 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
p7 [algo="p.ml" init="isRoot=false alpha=0 par=0"]
Root -- p2 -- p3 -- p4 -- p5 -- p6
p5 -- p7 p5 -- p7
} }
(* (*
Algorithm 1 of: Algorithm 1 of:
A Framework for Certified Self-Stabilization A Framework for Certified Self-Stabilization
Case Study: Silent Self-Stabilizing k-Dominating Set on a Tree Case Study: Silent Self-Stabilizing k-Dominating Set on a Tree
https://hal.archives-ouvertes.fr/hal-01272158/document https://hal.archives-ouvertes.fr/hal-01272158/document
...@@ -15,12 +15,12 @@ Encoded by Hugo Hannot ...@@ -15,12 +15,12 @@ Encoded by Hugo Hannot
open Algo open Algo
open State open State
type s = State.t type s = State.t
type sl = s list type sl = s list
type n = State.t neighbor type n = State.t neighbor
type nl = n list type nl = n list
let isRoot p = (state p).isRoot let isRoot p = (state p).isRoot
let (isShort: n -> bool) = let (isShort: n -> bool) =
...@@ -30,13 +30,13 @@ let (isTall: n -> bool) = ...@@ -30,13 +30,13 @@ let (isTall: n -> bool) =
fun p -> (state p).alpha >= k fun p -> (state p).alpha >= k
(* Actually unused *) (* Actually unused *)
let (_kDominator: 'v -> bool) = let (_kDominator: 'v -> bool) =
fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p)) fun p -> ((state p).alpha = k) || ((isShort p) && (isRoot p))
let (children: s -> nl -> nl) = let (children: s -> nl -> nl) =
fun _p nl -> fun _p nl ->
List.filter (fun q -> (state q).par = reply q) nl List.filter (fun q -> (state q).par = reply q) nl
let (shortChildren: s -> nl -> nl) = let (shortChildren: s -> nl -> nl) =
fun p nl -> fun p nl ->
List.filter isShort (children p nl) List.filter isShort (children p nl)
...@@ -60,7 +60,7 @@ let rec (min: nl -> int -> int) = ...@@ -60,7 +60,7 @@ let rec (min: nl -> int -> int) =
| n::tail -> | n::tail ->
let s = state n in let s = state n in
if (s.alpha) < cur then min tail (s.alpha) else min tail cur if (s.alpha) < cur then min tail (s.alpha) else min tail cur
let (maxAShort: s -> nl -> int) = let (maxAShort: s -> nl -> int) =
fun p nl -> max (shortChildren p nl) (-1) fun p nl -> max (shortChildren p nl) (-1)
...@@ -83,8 +83,8 @@ let (init_state: int -> string -> s) = ...@@ -83,8 +83,8 @@ let (init_state: int -> string -> s) =
isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *) isRoot = pid = "Root"; (* ZZZ: The root of the tree should be named "Root"! *)
alpha = Random.int (2*k+1); alpha = Random.int (2*k+1);
par = if pid="Root" then -1 else 0 (* the input tree should be sorted alphabetically (wrt a bf traversal) *) par = if pid="Root" then -1 else 0 (* the input tree should be sorted alphabetically (wrt a bf traversal) *)
} }
let (enable_f: s -> nl -> action list) = let (enable_f: s -> nl -> action list) =
fun p nl -> if (p.alpha <> (newAlpha p nl)) then ["change_alpha"] else [] fun p nl -> if (p.alpha <> (newAlpha p nl)) then ["change_alpha"] else []
......
(* Time-stamp: <2022-07-12 11:01:25 emile> *) (* Time-stamp: <modified the 12/02/2023 (at 22:18) by Erwan Jahier> *)
open Algo open Algo
let d = max_degree() let d = max_degree()
type t = { type t = {
isRoot:bool; isRoot:bool;
...@@ -10,20 +10,16 @@ type t = { ...@@ -10,20 +10,16 @@ type t = {
par:int par:int
} }
(*let boolVint (b:bool):int =
if b then 1 else 0*)
let (to_string: (t -> string)) = let (to_string: (t -> string)) =
fun s -> fun s ->
Printf.sprintf "isRoot=%b alpha=%d par=%d" s.isRoot s.alpha s.par Printf.sprintf "isRoot=%b alpha=%d par=%d" s.isRoot s.alpha s.par
let (of_string: (string -> t) option) = let (of_string: (string -> t) option) =
Some (fun s -> Some (fun s ->
Scanf.sscanf s "{is_root=%d ; alpha=%d ; par=%d}" Scanf.sscanf s "isRoot=%B alpha=%d par=%d"
(fun i alpha p -> {isRoot = (i=1) ; alpha = alpha ; par = p })) (fun b alpha p -> {isRoot = b ; alpha = alpha ; par = p }))
let (copy : ('v -> 'v)) = fun x -> x let (copy : ('v -> 'v)) = fun x -> x
let actions = ["change_alpha"] let actions = ["change_alpha"]
let k = 2 let k = 2
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment