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

Merge branch 'master' of gricad-gitlab.univ-grenoble-alpes.fr:baiocchg/salut

parents b933255e 3962f096
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
lib/sas.lus
+ 1
− 1
View file @ 22658c12
...@@ -65,5 +65,5 @@ tel; ...@@ -65,5 +65,5 @@ tel;
node move_count<<const an:int; const pn:int>>(acti : bool^an^pn) node move_count<<const an:int; const pn:int>>(acti : bool^an^pn)
returns (count:int); returns (count:int);
let 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; tel;
test/Makefile.inc
+ 1
− 1
View file @ 22658c12
...@@ -27,7 +27,7 @@ test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus ...@@ -27,7 +27,7 @@ test: $(TOPOLOGY).cmxs $(TOPOLOGY).lus
lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle" lurette -sut "sasa $(TOPOLOGY).dot $(SASAFLAGS)" -oracle "lv6 $(TOPOLOGY)_oracle.lus -n oracle"
verify: $(TOPOLOGY)_verify.lv4 verify: $(TOPOLOGY)_verify.lv4
kind2 -v $< kind2 $<
%.verify: %_verify.lv4 %.verify: %_verify.lv4
kind2 $< kind2 $<
......
test/coloring/er.dot → test/coloring/ER.dot
+ 0
− 0
View file @ 22658c12
File moved
test/coloring/Makefile
+ 1
− 1
View file @ 22658c12
TOPOLOGY ?= clique4 TOPOLOGY ?= clique3
DOT2LUSFLAGS ?= DOT2LUSFLAGS ?=
SASA_ALGOS := p.ml SASA_ALGOS := p.ml
SASAFLAGS += --locally-central-daemon SASAFLAGS += --locally-central-daemon
......
test/coloring/clique4.dot → test/coloring/clique3.dot
+ 12
− 0
View file @ 22658c12
graph graph0 { graph graph0 {
graph [min_deg=3 mean_deg=3. max_deg=3 is_connected=true is_cyclic=true is_tree=false links_number=6] 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"] p0 [algo="p.ml"]
p1 [algo="p.ml"] p1 [algo="p.ml"]
p2 [algo="p.ml"] p2 [algo="p.ml"]
p3 [algo="p.ml"]
p0 -- p1 p0 -- p1
p0 -- p2 p0 -- p2
p0 -- p3
p1 -- p2 p1 -- p2
p1 -- p3
p2 -- p3
} }
test/coloring/clique4_oracle.lus → test/coloring/clique3_oracle.lus
+ 26
− 0
View file @ 22658c12
include "clique4.lus" include "clique3.lus"
include "verify.lus" include "verify.lus"
node topology = clique4; node topology = clique3;
const an = actions_number; const an = actions_number;
const pn = card; const pn = card;
node oracle( node oracle(
p0_color:int;p1_color:int;p2_color:int;p3_color:int; p0_color:int;p1_color:int;p2_color:int;
Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor,Enab_p3_recolor:bool; Enab_p0_recolor,Enab_p1_recolor,Enab_p2_recolor:bool;
p0_recolor,p1_recolor,p2_recolor,p3_recolor:bool) p0_recolor,p1_recolor,p2_recolor:bool)
returns (ok:bool); returns (ok:bool);
var var
Acti:bool^an^pn; Acti:bool^an^pn;
...@@ -17,9 +17,9 @@ var ...@@ -17,9 +17,9 @@ var
nodes : state^pn; nodes : state^pn;
enables : bool^an^pn; enables : bool^an^pn;
let let
Acti = [[p0_recolor],[p1_recolor],[p2_recolor],[p3_recolor]]; Acti = [[p0_recolor],[p1_recolor],[p2_recolor]];
Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor],[Enab_p3_recolor]]; Enab = [[Enab_p0_recolor],[Enab_p1_recolor],[Enab_p2_recolor]];
Stat = [ p0_color, p1_color, p2_color, p3_color ]; Stat = [ p0_color, p1_color, p2_color ];
nodes, enables = topology(pre(Acti), Stat); nodes, enables = topology(pre(Acti), Stat);
ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat));
......
test/coloring/grid.dot 0 → 100644
+ 286
− 0
View file @ 22658c12
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
}
test/coloring/simu.lus
+ 7
− 16
View file @ 22658c12
include "../../lib/sas.lus" include "../../lib/sas.lus"
include "ER.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;
node incr(ain : int) returns (aout, z : int); node incr(ain : int) returns (aout, z : int);
let let
z = ain; aout = ain + 1; z = ain; aout = ain + 1;
tel; tel;
node simu(x:bool) returns (cpt:int); node simu(x:bool) returns (s : bool);
var var
initials : state^card; initials : state^card;
Enab_p : bool^actions_number^card; Enab_p : bool^actions_number^card;
p : bool^actions_number^card; p : bool^actions_number^card;
_d:int; _d:int;
p_c : state^card; p_c : state^card;
let let
cpt = 0 -> pre cpt +1;
assert (cpt < 10);
_d, initials= fill<<incr; card>>(0); _d, initials= fill<<incr; card>>(0);
p = false^actions_number^card -> pre Enab_p; 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 tel
test/token/verify.lus
+ 1
− 0
View file @ 22658c12
...@@ -21,6 +21,7 @@ let ...@@ -21,6 +21,7 @@ let
closure = true -> (pre(legitimate) => legitimate); closure = true -> (pre(legitimate) => legitimate);
steps = 0 -> pre(steps) ; steps = 0 -> pre(steps) ;
steps = 0 -> (pre(steps) + 1);
ok = tokens >= 1 -- there should always be at least one token holder ok = tokens >= 1 -- there should always be at least one token holder
and closure and closure
and (steps >= 3*card*(card-1)/2 - card - 1 => legitimate); -- worst-case stabilization and (steps >= 3*card*(card-1)/2 - card - 1 => legitimate); -- worst-case stabilization
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment