diff --git a/lib/sas.lus b/lib/sas.lus
index f2b6616402edfe4ac7cb6aeac3f63d6f40ab5f6c..847108d51a75382de775ec05e2c3412ede0af7fc 100644
--- a/lib/sas.lus
+++ b/lib/sas.lus
@@ -65,5 +65,5 @@ tel;
node move_count<<const an:int; const pn:int>>(acti : bool^an^pn)
returns (count:int);
let
- count = (-1 -> pre(count)) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti));
+ count = 0 -> (pre(count) + pop_count<<pn>>(map<<boolany<<an>>, pn>>(acti)));
tel;
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 99a6691a08c7916afb8e8e79d3839154a024e02d..ce2e784ca7fddfcd6614b851c8d455453e21aabe 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -27,7 +27,7 @@ test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus
lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle"
verify: $(TOPOLOGY)_verify.lv4
- kind2 -v $<
+ kind2 $<
%.verify: %_verify.lv4
kind2 $<
diff --git a/test/coloring/er.dot b/test/coloring/ER.dot
similarity index 100%
rename from test/coloring/er.dot
rename to test/coloring/ER.dot
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index de7c523940e18e7f84424f3b76295a272f4ff297..e5ff2de8a14934839d66eb0bc0fdf6afd77fd0b8 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,4 +1,4 @@
-TOPOLOGY ?= clique4
+TOPOLOGY ?= clique3
DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml
SASAFLAGS += --locally-central-daemon
diff --git a/test/coloring/clique3.dot b/test/coloring/clique3.dot
new file mode 100644
index 0000000000000000000000000000000000000000..1672a3b5fc62988ec103c8229c36296c538160eb
--- /dev/null
+++ b/test/coloring/clique3.dot
@@ -0,0 +1,12 @@
+graph graph0 {
+graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=3]
+ p0 [algo="p.ml"]
+ p1 [algo="p.ml"]
+ p2 [algo="p.ml"]
+
+
+ p0 -- p1
+ p0 -- p2
+ p1 -- p2
+}
+
diff --git a/test/coloring/clique3_oracle.lus b/test/coloring/clique3_oracle.lus
new file mode 100644
index 0000000000000000000000000000000000000000..42222151ac27b36aa6585a2c26ba1db5b7072bc5
--- /dev/null
+++ b/test/coloring/clique3_oracle.lus
@@ -0,0 +1,26 @@
+include "clique3.lus"
+include "verify.lus"
+
+node topology = clique3;
+const an = actions_number;
+const pn = card;
+
+node oracle(
+ p0_color:int;p1_color:int;p2_color:int;
+ Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor:bool;
+ p0_recolor,p1_recolor,p2_recolor:bool)
+returns (ok:bool);
+var
+ Acti:bool^an^pn;
+ Enab:bool^an^pn;
+ Stat : state^pn;
+ nodes : state^pn;
+ enables : bool^an^pn;
+let
+ Acti = [[p0_recolor],[p1_recolor],[p2_recolor]];
+ Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor]];
+ Stat = [ p0_color, p1_color, p2_color ];
+
+ nodes, enables = topology(pre(Acti), Stat);
+ ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
+tel
diff --git a/test/coloring/clique4.dot b/test/coloring/clique4.dot
deleted file mode 100644
index 9509c80474fab2fdea2f2237f6992631cb387414..0000000000000000000000000000000000000000
--- a/test/coloring/clique4.dot
+++ /dev/null
@@ -1,15 +0,0 @@
-graph graph0 {
-graph [min_deg=3 mean_deg=3. max_deg=3 is_connected=true is_cyclic=true is_tree=false links_number=6]
- p0 [algo="p.ml"]
- p1 [algo="p.ml"]
- p2 [algo="p.ml"]
- p3 [algo="p.ml"]
-
- p0 -- p1
- p0 -- p2
- p0 -- p3
- p1 -- p2
- p1 -- p3
- p2 -- p3
-}
-
diff --git a/test/coloring/clique4_oracle.lus b/test/coloring/clique4_oracle.lus
deleted file mode 100644
index 1cd6e7bfc724e20efc5604275985b90666fee4d7..0000000000000000000000000000000000000000
--- a/test/coloring/clique4_oracle.lus
+++ /dev/null
@@ -1,26 +0,0 @@
-include "clique4.lus"
-include "verify.lus"
-
-node topology = clique4;
-const an = actions_number;
-const pn = card;
-
-node oracle(
- p0_color:int;p1_color:int;p2_color:int;p3_color:int;
- Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor:bool;
- p0_recolor,p1_recolor,p2_recolor,p3_recolor:bool)
-returns (ok:bool);
-var
- Acti:bool^an^pn;
- Enab:bool^an^pn;
- Stat : state^pn;
- nodes : state^pn;
- enables : bool^an^pn;
-let
- Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor]];
- Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor]];
- Stat = [ p0_color, p1_color, p2_color, p3_color ];
-
- nodes, enables = topology(pre(Acti), Stat);
- ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
-tel
diff --git a/test/coloring/grid.dot b/test/coloring/grid.dot
new file mode 100644
index 0000000000000000000000000000000000000000..13bcbade2c335189825658ab08805bdcbf55b524
--- /dev/null
+++ b/test/coloring/grid.dot
@@ -0,0 +1,286 @@
+graph graph0 {
+graph [min_deg=2 mean_deg=3.6 max_deg=4 is_connected=true is_cyclic=true is_tree=false links_number=180]
+ p0 [algo="p.ml"]
+ p1 [algo="p.ml"]
+ p2 [algo="p.ml"]
+ p3 [algo="p.ml"]
+ p4 [algo="p.ml"]
+ p5 [algo="p.ml"]
+ p6 [algo="p.ml"]
+ p7 [algo="p.ml"]
+ p8 [algo="p.ml"]
+ p9 [algo="p.ml"]
+ p10 [algo="p.ml"]
+ p11 [algo="p.ml"]
+ p12 [algo="p.ml"]
+ p13 [algo="p.ml"]
+ p14 [algo="p.ml"]
+ p15 [algo="p.ml"]
+ p16 [algo="p.ml"]
+ p17 [algo="p.ml"]
+ p18 [algo="p.ml"]
+ p19 [algo="p.ml"]
+ p20 [algo="p.ml"]
+ p21 [algo="p.ml"]
+ p22 [algo="p.ml"]
+ p23 [algo="p.ml"]
+ p24 [algo="p.ml"]
+ p25 [algo="p.ml"]
+ p26 [algo="p.ml"]
+ p27 [algo="p.ml"]
+ p28 [algo="p.ml"]
+ p29 [algo="p.ml"]
+ p30 [algo="p.ml"]
+ p31 [algo="p.ml"]
+ p32 [algo="p.ml"]
+ p33 [algo="p.ml"]
+ p34 [algo="p.ml"]
+ p35 [algo="p.ml"]
+ p36 [algo="p.ml"]
+ p37 [algo="p.ml"]
+ p38 [algo="p.ml"]
+ p39 [algo="p.ml"]
+ p40 [algo="p.ml"]
+ p41 [algo="p.ml"]
+ p42 [algo="p.ml"]
+ p43 [algo="p.ml"]
+ p44 [algo="p.ml"]
+ p45 [algo="p.ml"]
+ p46 [algo="p.ml"]
+ p47 [algo="p.ml"]
+ p48 [algo="p.ml"]
+ p49 [algo="p.ml"]
+ p50 [algo="p.ml"]
+ p51 [algo="p.ml"]
+ p52 [algo="p.ml"]
+ p53 [algo="p.ml"]
+ p54 [algo="p.ml"]
+ p55 [algo="p.ml"]
+ p56 [algo="p.ml"]
+ p57 [algo="p.ml"]
+ p58 [algo="p.ml"]
+ p59 [algo="p.ml"]
+ p60 [algo="p.ml"]
+ p61 [algo="p.ml"]
+ p62 [algo="p.ml"]
+ p63 [algo="p.ml"]
+ p64 [algo="p.ml"]
+ p65 [algo="p.ml"]
+ p66 [algo="p.ml"]
+ p67 [algo="p.ml"]
+ p68 [algo="p.ml"]
+ p69 [algo="p.ml"]
+ p70 [algo="p.ml"]
+ p71 [algo="p.ml"]
+ p72 [algo="p.ml"]
+ p73 [algo="p.ml"]
+ p74 [algo="p.ml"]
+ p75 [algo="p.ml"]
+ p76 [algo="p.ml"]
+ p77 [algo="p.ml"]
+ p78 [algo="p.ml"]
+ p79 [algo="p.ml"]
+ p80 [algo="p.ml"]
+ p81 [algo="p.ml"]
+ p82 [algo="p.ml"]
+ p83 [algo="p.ml"]
+ p84 [algo="p.ml"]
+ p85 [algo="p.ml"]
+ p86 [algo="p.ml"]
+ p87 [algo="p.ml"]
+ p88 [algo="p.ml"]
+ p89 [algo="p.ml"]
+ p90 [algo="p.ml"]
+ p91 [algo="p.ml"]
+ p92 [algo="p.ml"]
+ p93 [algo="p.ml"]
+ p94 [algo="p.ml"]
+ p95 [algo="p.ml"]
+ p96 [algo="p.ml"]
+ p97 [algo="p.ml"]
+ p98 [algo="p.ml"]
+ p99 [algo="p.ml"]
+
+
+ p0 -- p1
+ p0 -- p10
+ p1 -- p11
+ p1 -- p2
+ p10 -- p11
+ p10 -- p20
+ p11 -- p12
+ p11 -- p21
+ p12 -- p13
+ p12 -- p2
+ p12 -- p22
+ p13 -- p14
+ p13 -- p23
+ p13 -- p3
+ p14 -- p15
+ p14 -- p24
+ p14 -- p4
+ p15 -- p16
+ p15 -- p25
+ p15 -- p5
+ p16 -- p17
+ p16 -- p26
+ p16 -- p6
+ p17 -- p18
+ p17 -- p27
+ p17 -- p7
+ p18 -- p19
+ p18 -- p28
+ p18 -- p8
+ p19 -- p29
+ p19 -- p9
+ p2 -- p3
+ p20 -- p21
+ p20 -- p30
+ p21 -- p22
+ p21 -- p31
+ p22 -- p23
+ p22 -- p32
+ p23 -- p24
+ p23 -- p33
+ p24 -- p25
+ p24 -- p34
+ p25 -- p26
+ p25 -- p35
+ p26 -- p27
+ p26 -- p36
+ p27 -- p28
+ p27 -- p37
+ p28 -- p29
+ p28 -- p38
+ p29 -- p39
+ p3 -- p4
+ p30 -- p31
+ p30 -- p40
+ p31 -- p32
+ p31 -- p41
+ p32 -- p33
+ p32 -- p42
+ p33 -- p34
+ p33 -- p43
+ p34 -- p35
+ p34 -- p44
+ p35 -- p36
+ p35 -- p45
+ p36 -- p37
+ p36 -- p46
+ p37 -- p38
+ p37 -- p47
+ p38 -- p39
+ p38 -- p48
+ p39 -- p49
+ p4 -- p5
+ p40 -- p41
+ p40 -- p50
+ p41 -- p42
+ p41 -- p51
+ p42 -- p43
+ p42 -- p52
+ p43 -- p44
+ p43 -- p53
+ p44 -- p45
+ p44 -- p54
+ p45 -- p46
+ p45 -- p55
+ p46 -- p47
+ p46 -- p56
+ p47 -- p48
+ p47 -- p57
+ p48 -- p49
+ p48 -- p58
+ p49 -- p59
+ p5 -- p6
+ p50 -- p51
+ p50 -- p60
+ p51 -- p52
+ p51 -- p61
+ p52 -- p53
+ p52 -- p62
+ p53 -- p54
+ p53 -- p63
+ p54 -- p55
+ p54 -- p64
+ p55 -- p56
+ p55 -- p65
+ p56 -- p57
+ p56 -- p66
+ p57 -- p58
+ p57 -- p67
+ p58 -- p59
+ p58 -- p68
+ p59 -- p69
+ p6 -- p7
+ p60 -- p61
+ p60 -- p70
+ p61 -- p62
+ p61 -- p71
+ p62 -- p63
+ p62 -- p72
+ p63 -- p64
+ p63 -- p73
+ p64 -- p65
+ p64 -- p74
+ p65 -- p66
+ p65 -- p75
+ p66 -- p67
+ p66 -- p76
+ p67 -- p68
+ p67 -- p77
+ p68 -- p69
+ p68 -- p78
+ p69 -- p79
+ p7 -- p8
+ p70 -- p71
+ p70 -- p80
+ p71 -- p72
+ p71 -- p81
+ p72 -- p73
+ p72 -- p82
+ p73 -- p74
+ p73 -- p83
+ p74 -- p75
+ p74 -- p84
+ p75 -- p76
+ p75 -- p85
+ p76 -- p77
+ p76 -- p86
+ p77 -- p78
+ p77 -- p87
+ p78 -- p79
+ p78 -- p88
+ p79 -- p89
+ p8 -- p9
+ p80 -- p81
+ p80 -- p90
+ p81 -- p82
+ p81 -- p91
+ p82 -- p83
+ p82 -- p92
+ p83 -- p84
+ p83 -- p93
+ p84 -- p85
+ p84 -- p94
+ p85 -- p86
+ p85 -- p95
+ p86 -- p87
+ p86 -- p96
+ p87 -- p88
+ p87 -- p97
+ p88 -- p89
+ p88 -- p98
+ p89 -- p99
+ p90 -- p91
+ p91 -- p92
+ p92 -- p93
+ p93 -- p94
+ p94 -- p95
+ p95 -- p96
+ p96 -- p97
+ p97 -- p98
+ p98 -- p99
+}
+
diff --git a/test/coloring/simu.lus b/test/coloring/simu.lus
index 133a3f3b0f33521379c9eb4746e6b5d053788bf2..a0fa0f42de8dd155261b3d302dda6dce2d000a3f 100644
--- a/test/coloring/simu.lus
+++ b/test/coloring/simu.lus
@@ -1,34 +1,25 @@
include "../../lib/sas.lus"
-
-node sync(p_c : state^card; Enab_p : bool^actions_number^card)
-returns (p : bool^actions_number^card; initials : state^card);
-var
- _d:int;
-let
- p=Enab_p;
- _d, initials= fill<<incr; card>>(0);
-tel;
+include "ER.lus"
node incr(ain : int) returns (aout, z : int);
let
z = ain; aout = ain + 1;
tel;
-node simu(x:bool) returns (cpt:int);
+node simu(x:bool) returns (s : bool);
var
initials : state^card;
Enab_p : bool^actions_number^card;
- p : bool^actions_number^card;
+ p : bool^actions_number^card;
_d:int;
-
+
p_c : state^card;
-let
- cpt = 0 -> pre cpt +1;
- assert (cpt < 10);
+let
_d, initials= fill<<incr; card>>(0);
p = false^actions_number^card -> pre Enab_p;
- p_c, Enab_p = er(p, initials -> 0^card);
+ p_c, Enab_p = ER(p, initials -> 0^card);
+ s = silent<<actions_number,card>>(Enab_p);
tel
diff --git a/test/token/verify.lus b/test/token/verify.lus
index 9a9ab63dadbb7a2d512312fd0d679bfc66c17ce9..574112307af08a9f29e5f82ca71df7629c6b3fbd 100644
--- a/test/token/verify.lus
+++ b/test/token/verify.lus
@@ -21,6 +21,7 @@ let
closure = true -> (pre(legitimate) => legitimate);
steps = 0 -> pre(steps) ;
+ steps = 0 -> (pre(steps) + 1);
ok = tokens >= 1 -- there should always be at least one token holder
and closure
and (steps >= 3*card*(card-1)/2 - card - 1 => legitimate); -- worst-case stabilization