Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
195 lines (172 sloc) 5.33 KB
/* -*-promela-*-
*for emacs promela mode
* Created < 17-Feb-2007
*
* (C) David Farago <farago@kit.edu>
* documentation: http://lfm.iti.kit.edu/files/theses/diploma/daDavidFarago.pdf
*
* The middle node, nodeWithNPC, makes an artificial NPC
* if it would have made the first to jump back to progressSTART.
* Possible tuning/restriction:
* * select a different node to be nodeWithNPC in the init process,
* * make an artificial NPC not only if the random id 4 has been chosen.
*
*
* Questions:
* label scoping: same label names in different processes ok?
*/
bool someProgressHasBeenMade=false;
#define N 9 /* number of nodes $n$: 9 instead of 6 */
#define K 9 /* number of rounds: 9 instead of 6*/
#define L 9 /* size of FIFO-Buffers: 9 instead of 6*/
byte nr_leaders=0;
bool limitReached=false;
typedef Msg {byte round; byte id; byte hop; bool unique;};
chan q0 = [L] of {byte, byte, byte, bool};
chan q1 = [L] of {byte, byte, byte, bool};
chan q2 = [L] of {byte, byte, byte, bool};
chan q3 = [L] of {byte, byte, byte, bool};
chan q4 = [L] of {byte, byte, byte, bool};
chan q5 = [L] of {byte, byte, byte, bool};
chan q6 = [L] of {byte, byte, byte, bool};
chan q7 = [L] of {byte, byte, byte, bool};
chan q8 = [L] of {byte, byte, byte, bool};
#define __instances_node 8
#define __instances_nodeWithNPC 1
proctype node (chan in, out)
{
bool nodeActive = true, leader = false;
byte round, id;
Msg curMsg;
xr in;
xs out;
START: /*random ID */
if
:: id=0
:: id=1
:: id=2
:: id=3
:: id=4
:: id=5
:: id=6
:: id=7
fi;
someProgressHasBeenMade=true;
progress:
curMsg.id=id;
curMsg.round=round;
curMsg.hop=1;
curMsg.unique=true;
SEND_AND_RECEIVE:
out!curMsg.round,curMsg.id,curMsg.hop,curMsg.unique;
endRECEIVE:
in?curMsg.round,curMsg.id,curMsg.hop,curMsg.unique;
/* check message */
if
:: curMsg.hop<N ->
if
:: (curMsg.round > round) ||
(curMsg.round == round && curMsg.id > id) ->
round=curMsg.round; id=curMsg.id; nodeActive=false;
curMsg.hop++; goto SEND_AND_RECEIVE
:: curMsg.round < round ||
(curMsg.round == round && curMsg.id < id) ->
goto endRECEIVE
:: curMsg.round==round && curMsg.id==id ->
curMsg.hop++;curMsg.unique=false;
goto SEND_AND_RECEIVE
:: else ->
printf("ERROR: hop<N and message-cases not correct")
fi
:: curMsg.hop==N ->
if
:: nodeActive && !curMsg.unique && round<K ->
round++; goto START
:: nodeActive && !curMsg.unique && round==K ->
limitReached=true;printf("Round-Limit reached")
:: nodeActive && curMsg.unique ->
leader=true; nr_leaders++; assert(nr_leaders==1)
:: else -> printf("ERROR: hop=N and !nodeActive")
fi
fi
}
proctype nodeWithNPC (chan in, out)
{
bool nodeActive = true, leader = false;
byte round, id;
Msg curMsg;
xr in;
xs out;
START_NPC: /*random ID */
if
:: id=0
:: id=1
:: id=2
:: id=3
:: id=4; if
:: someProgressHasBeenMade!=true ->
/* artificial NPC */
do
:: skip -> skip
od
:: else -> skip
fi
:: id=5
:: id=6
:: id=7
fi;
someProgressHasBeenMade=true;
progress:
curMsg.id=id;
curMsg.round=round;
curMsg.hop=1;
curMsg.unique=true;
SEND_AND_RECEIVE_NPC:
out!curMsg.round,curMsg.id,curMsg.hop,curMsg.unique;
endRECEIVE_NPC:
in?curMsg.round,curMsg.id,curMsg.hop,curMsg.unique;
/* check message */
if
:: curMsg.hop<N ->
if
:: (curMsg.round > round) ||
(curMsg.round == round && curMsg.id > id) ->
round=curMsg.round; id=curMsg.id; nodeActive=false;
curMsg.hop++; goto SEND_AND_RECEIVE_NPC
:: curMsg.round < round ||
(curMsg.round == round && curMsg.id < id) ->
goto endRECEIVE_NPC
:: curMsg.round==round && curMsg.id==id ->
curMsg.hop++; curMsg.unique=false;
goto SEND_AND_RECEIVE_NPC
:: else ->
printf("ERROR: hop<N and message-cases not correct")
fi
:: curMsg.hop==N ->
if
:: nodeActive && !curMsg.unique && round<K ->
round++; goto START_NPC
:: nodeActive && !curMsg.unique && round==K ->
limitReached=true;printf("Round-Limit reached")
:: nodeActive && curMsg.unique ->
leader=true; nr_leaders++; assert(nr_leaders==1)
:: else -> printf("ERROR: hop=N and !nodeActive")
fi
fi
}
init {
atomic {
run node(q0, q1);
run node(q1, q2);
run node(q2, q3);
run node(q3, q4);
run nodeWithNPC(q4, q5);
run node(q5, q6);
run node(q6, q7);
run node(q7, q8);
run node(q8, q0);
}
// timeout -> assert(nr_leaders==1 || limitReached);
limitReached -> assert(nr_leaders<2);
printf("Asserted: when limit of rounds is reached, zero or one leader is elected\n")
}