Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
// Wim H. Hesselink, 3 October 2004
// Some introductory Promela scripts, see whh332
// Wim H. Hesselink, 25 September 2004
// Peterson's mutual exclusion algorithm
bit aktief[2] ; // initally (0, 0)
bit last ;
byte crit, wtime[2] ;
#define tryout 2 ; // gives assert violation, replace by 3
proctype threadMX (bit self) {
do
:: break
:: aktief[self] = 1 ;
atomic {
last = self ;
wtime[self] = 1 ;
}
(last == 1-self || ! aktief[1-self]) ; // AWAIT
atomic {
wtime[1-self] =
(wtime[1-self] > 0 -> wtime[1-self]+1 : 0) ;
assert wtime[1-self] < tryout ;
wtime[self] = 0 ; }
crit ++ ;
assert crit == 1 ; // CS
crit -- ;
aktief[self] = 0 ;
od
}
init {
atomic{ // just as an ilustration
run threadMX (0) ;
run threadMX (1) ;
}
}
// Acceptance0, Wim H. Hesselink, 25 September 2004
byte x ;
bit stop ;
active proctype stepper () {
do
:: stop ;
break ;
:: ! stop ;
accept0: x = (x < 7 -> x + 1 : 3) ;
od
}
active proctype stopper () {
x >= 3 ;
stop = 1 ;
}
// Test for absence of acceptance cycles
// Complains without weak fairness
// With weak fairness, it does not.
// Progress0, Wim H. Hesselink, 25 September 2004
// Testing for progress cycles with one process
byte x ;
active proctype stepper () {
progress0:
do
:: x = (x+2) % 5 ;
:: break
od
}
// Does not complain of terminating behaviour!
// Progress1, Wim H. Hesselink, 25 September 2004
// Testing for progress cycles with three processes
byte x, y, z ;
active proctype stepper () {
do
:: x == y ;
progress0: x = (x+2) % 5 ;
od
}
active proctype equalizer () {
do
:: y = x
od
}
active proctype dummy () {
do
:: z = 1-z
od
}
// Complains of non-progress cycle
// This changes with weak fairness
/* ChanMX, Wim H. Hesselink, 1 October 2004
* Mutual exclusion by means of a channel as a binary semaphore */
#define Nproc 5
chan sema = [1] of {bit} ; // buffered channel; contents are irrelevant
byte crit, proc ;
proctype member (byte self) {
do
:: proc -- ;
break
:: sema ? _ ;
crit ++ ;
progress: assert crit == 1 ;
crit -- ;
sema ! 0
od
}
init {
atomic {
do
:: proc < Nproc ->
run member (proc) ;
proc ++ ;
:: else -> break
od ;
}
assert proc == Nproc ; // is violated
assert crit == 0 ;
sema ! 0 ;
proc == 0 ;
sema ? 1 // gives invalid end-state
}
// No invalid end-state is found when the last statement is removed.
/* The above examples are not representative in that the processes never use
* local (i.e. private) variables. Try that also. */