-
Déclaration de variables :
- On indique le type (un des bit, byte, short, or int), le nom de la variable et optionnellement sa valeur initiale.
bool b1 = false, b2 = false;
bit k = 0;
Les variables de type tableau sont déclarées comme en C, par exemple :
bit porteouverte[3];
- Déclaration de canaux :
- On l'introduit par le mot clé chan, suivi du nom du canal et optionnellement de la longueur du fifo et du type des messages qui circulent. Par exemple :
chan Ouvreporte=[0] of {byte, bit},
Transfert=[2] of {bit, short, chan};
ouvreporte est un canal synchrone, car sa longueur est 0, ce qui correspond à un rendez-vous ; sur ce canal circulent des messages ayant une partie byte et une partie bit.
Transfert est un canal asynchrone, car il peut stocker (au plus) deux messages.
- Déclaration de processus :
- La forme la plus simple de déclaration de processus est :
proctype nom ( paramètres_formels )
{ instructions }
Un processus est instancié en utilisant l'instruction run :
run nom ( paramètres_actuels )
Par exemple :
proctype P (bit i) {
...
}
proctype porte (byte i) {
...
}
proctype ascenseur () {
...
}
- Opérations sur les canaux :
- Sur un canal on peut envoyer (opération ``!'') ou recevoir (opération ``?'') des messages. Par exemple :
ouvreporte!i,0;
ouvreporte?i,1;
ouvreporte?eval(etage),1
La fonction ``eval'' force l'égalité des valeurs reçues avec etage, la variable etage n'est pas changée.
- Expressions :
- Un expression peut être utilisée comme une instruction si elle ne fait pas des effet de bord (opérations ``--'' et ``++'' de C). Dans ce cas, elle est exécutable quand sa valeur devient vraie (par le changement des valeurs des variables partagées). Par exemple :
(a == b);
est équivalent à :
while (a != b) skip;
- Instruction ``init'' :
- L'exécution du système commence par le processus init (c'est le main de Promela). Par exemple :
init {
run porte(1); run porte(2); run porte(3);
run ascenseur()
}
- Instruction ``atomic'' :
- L'exécution d'une séquence d'instructions préfixée par ``atomic'' peut être rendue indivisible, c'est-à-dire sans l'entrelacement des actions des autres processus. Par exemple :
atomic {
run porte(1); run porte(2); run porte(3);
run ascenseur()
}
- Instruction ``if'' :
- Un branche de l'instruction ``if'' est exécutable si la première instruction de la branche, appelée aussi sa garde, est vraie. L'instruction ``if'' bloque jusque à ce qu'une branche devient exécutable, dans quel cas la branche est exécutée.
Si plusieurs branches sont exécutables, l'une est choisie aléatoirement (non-déterminisme).
L'exemple suivant incrémente ou décrémente la valeur de count une fois.
if
:: count = count + 1
:: count = count - 1
fi
- Instruction ``do'' :
- Similaire à l'instruction ``if'', sauf que l'instruction est exécutée et puis la sélection est répétée jusque à l'exécution d'une instruction ``break''.
proctype ascenseur () {
show byte etage = 1;
do
:: (etage != 3) -> etage++
:: (etage != 1) -> etage--
:: ouvreporte!etage,1; ouvreporte?eval(etage),0
od
}