From d96fdd14dddff259915e5cda5de6f5776f4fe29a Mon Sep 17 00:00:00 2001
From: invite <invite@debian>
Date: Fri, 1 Jul 2022 10:35:05 +0200
Subject: [PATCH] fix links
---
test/Makefile.inc | 3 +--
test/kclustering/Makefile | 4 ++--
test/kclustering/verify.lus | 12 ++++++------
3 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 9713d0bf..a127186d 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -78,8 +78,7 @@ endif
sed -i -e "s/tel/--%MAIN ;\n--%PROPERTY ok;\ntel/" $@
# Do not expand nodes
-%_verify.noexpand.lv4: verify.lus
- make $*_const.lus
+%_verify.noexpand.lv4: verify.lus %_const.lus
lv6 $*.lus $^ $*_const.lus -n $(prop) -rnc --lustre-v4 -o $@
tac $@ | sed -z "s/tel/tel\n--%MAIN ;\n--%PROPERTY ok;/" | tac > $@.tmp
mv $@.tmp $@
diff --git a/test/kclustering/Makefile b/test/kclustering/Makefile
index 19d67dcf..4e457463 100644
--- a/test/kclustering/Makefile
+++ b/test/kclustering/Makefile
@@ -4,8 +4,8 @@ SASA_ALGOS := p.ml
DECO_PATTERN="0-:p.ml"
-include ~/sasa/salut/test/Makefile.inc
--include ~/sasa/salut/test/Makefile.dot
+include ../Makefile.inc
+-include ../Makefile.dot
clean: genclean
rm -f tree*.*
diff --git a/test/kclustering/verify.lus b/test/kclustering/verify.lus
index 9a5d06e4..702ef103 100644
--- a/test/kclustering/verify.lus
+++ b/test/kclustering/verify.lus
@@ -1,5 +1,5 @@
-include "../../sasa/salut/lib/sas.lus"
-include "../../sasa/salut/lib/utils.lus"
+include "../../lib/sas.lus"
+include "../../lib/utils.lus"
include "cost.lus"
const worst_case=3*card*(card-1)/2 - card - 1;
@@ -12,7 +12,7 @@ returns (ok : bool);
var
config : state^card;
enabled : bool^actions_number^card;
- legitimate, closure : bool;
+ legitimate, closure,converge : bool;
steps, cost : int;
let
assert(true -> daemon_is_distributed<<actions_number,card>>(active, pre enabled));
@@ -22,15 +22,15 @@ let
config, enabled = topology(active, init_config);
assert(config = init_config -> true);
- -- stability in this algo means mutual exclusion: exactly 1 node is enabled at a time
- legitimate = n_xor<<card>>(map<<n_or<<actions_number>>,card>> (enabled));
+ legitimate = silent<<actions_number,card>>(enabled);
closure = true -> (pre(legitimate) => legitimate);
cost = cost(enabled, config);
- -- converge = (true -> legitimate or pre(cost)>cost);
+ converge = (true -> legitimate or pre(cost)>cost);
steps = 0 -> (pre(steps) + 1);
ok = closure
+ and converge
-- and (steps > worst_case) => legitimate -- the worst-case stabilization
-- and (steps > worst_case - 1) => legitimate -- is tigth!
--
GitLab