Commit 2d14a6b4 authored by Kirill Smelkov's avatar Kirill Smelkov

.

parent e62f82e5
......@@ -13,10 +13,13 @@ ASSUME /\ root \in Nodes
\* Connected is true if two nodes i and j are interconnected by some path.
RECURSIVE Connected(_,_)
Connected(i,j) ==
\/ {i,j} \in Edges
\/ \E x \in Nodes : ({i,x} \in Edges) /\ Connected(x,j)
RECURSIVE _Connected(_,_,_)
_Connected(i,j,Intra) ==
CASE {i,j} \in Edges -> TRUE
[] Intra = {} -> FALSE
[] OTHER -> \E x \in Intra : ({i,x} \in Edges) /\ _Connected(x,j, Intra\{x})
Connected(i,j) == _Connected(i,j, Nodes\{i,j})
\* All nodes must be connected
ASSUME \A i,j \in Nodes : Connected(i,j)
......@@ -77,7 +80,7 @@ QueuesTo(n) == {q \in Queues : q[2] = n}
with (q \in {r \in QueuesTo(self) : msgs[r] /= << >>}) {
with (m = Head(msgs[q])) {
with (msgs_ = [msgs EXCEPT ![q] = Tail(msgs[q])]) {
if (m < depth - 1) {
if (depth = Inf \/ m < depth - 1) {
depth := m + 1;
parent := q[1];
\* send m further to all neighbours except from whom we received it
......@@ -96,7 +99,7 @@ QueuesTo(n) == {q \in Queues : q[2] = n}
}
};
********)
\* BEGIN TRANSLATION (chksum(pcal) = "a6173f58" /\ chksum(tla) = "9d62fe6c")
\* BEGIN TRANSLATION (chksum(pcal) = "b56d10df" /\ chksum(tla) = "c40e6a89")
VARIABLES msgs, depth, parent
vars == << msgs, depth, parent >>
......@@ -114,7 +117,7 @@ Init == (* Global variables *)
RT(self) == \E q \in {r \in QueuesTo(self) : msgs[r] /= << >>}:
LET m == Head(msgs[q]) IN
LET msgs_ == [msgs EXCEPT ![q] = Tail(msgs[q])] IN
IF m < depth[self] - 1
IF depth[self] = Inf \/ m < depth[self] - 1
THEN /\ depth' = [depth EXCEPT ![self] = m + 1]
/\ parent' = [parent EXCEPT ![self] = q[1]]
/\ LET msgs__ == [t \in Queues |->
......
......@@ -5,7 +5,7 @@
<stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="26"/>
<intAttribute key="fpIndex" value="93"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
......
Markdown is supported
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