diff --git a/test/token/Makefile b/test/token/Makefile index ee04475bd0d92c08787dcfba933bb7f84bdbfd32..cd08a78be34ca240d8e870dd6ec4d76ae820f973 100644 --- a/test/token/Makefile +++ b/test/token/Makefile @@ -1,4 +1,4 @@ -TOPOLOGY ?= ring8 +TOPOLOGY ?= ring4 DOT2LUSFLAGS ?= SASA_ALGOS := p.ml root.ml diff --git a/test/token/ring4.dot b/test/token/ring4.dot new file mode 100644 index 0000000000000000000000000000000000000000..3b05c11306fc9b3129609f600aff38d976d69ded --- /dev/null +++ b/test/token/ring4.dot @@ -0,0 +1,14 @@ +digraph graph0 { +graph [min_deg=2 mean_deg=2. max_deg=2 is_connected=true is_cyclic=true is_tree=false links_number=4] + p0 [algo="root.ml"] + p1 [algo="p.ml"] + p2 [algo="p.ml"] + p3 [algo="p.ml"] + + + p0 -> p1 + p1 -> p2 + p2 -> p3 + p3 -> p0 +} + diff --git a/test/token/ring4_oracle.lus b/test/token/ring4_oracle.lus new file mode 100644 index 0000000000000000000000000000000000000000..794c50d6d31d0c8023faba7e79f66ba60bf34b09 --- /dev/null +++ b/test/token/ring4_oracle.lus @@ -0,0 +1,26 @@ +include "ring4.lus" +include "verify.lus" + +node topology = ring4; +const an = actions_number; +const pn = card; + +node oracle( + p0_c:int;p1_c:int;p2_c:int;p3_c:int; + Enab_p0_T,Enab_p1_T,Enab_p2_T,Enab_p3_T:bool; + p0_T,p1_T,p2_T,p3_T: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_T],[p1_T],[p2_T],[p3_T]]; + Enab = [[Enab_p0_T],[Enab_p1_T],[Enab_p2_T],[Enab_p3_T]]; + Stat = [ p0_c, p1_c, p2_c, p3_c ]; + + nodes, enables = topology(pre(Acti), Stat); + ok = enables = Enab and boolred<<pn,pn,pn>>(map<<=,pn>>(nodes, Stat)); +tel; diff --git a/test/token/verify.lus b/test/token/verify.lus index 53d11a6884141c99b917ce77afd4a64b0d6291f2..27898491d4004096df77e37f742f9c18449a891e 100644 --- a/test/token/verify.lus +++ b/test/token/verify.lus @@ -24,5 +24,5 @@ let steps = (-1 -> pre(steps)) + 1; ok = closure and tokens >= 1 and -- there always exists at least one token holder - ((steps >= card*(card-1) + ((card-4)*(card+1)/2) + 1) => legitimate); -- worst-case stabilization + ((steps >= 4) => legitimate); -- worst-case stabilization tel;