Laborator SVI-SW

L2. Limbajul PROMELA. Continuare.

Canale de mesaje. Exemplificare

Rulati in Spin codul:

#define QLEN 5
mtype = {m1, m2, m3, const}

chan q = [QLEN] of {mtype, byte, mtype}

active proctype A() priority 10{
    q!m1;
    q!m2(20, const);
    q!m3, 4, 0;
    q!m2(5);
    q!m3(4, const);
}

Afisand instructiunile executate(-p) si mesajele transmise (-s). Ce se intampla daca se transmit mesaje de dimensiune mai mica decat a canalului?

Nota: proceselor li se pot aloca si prioritati(un proces de prioritate 10 este executat de 10 ori mai des decat unul de prioritate 1).

Pentru exemplul anterior, adaugati codul:

active proctype B() priority 1{
    do
    :: q?m1
    :: q?m2,_,_
    od
}

si simulati. Ce se observa?
Este recomandata specificarea tuturor parametrilor in cazul comunicatiei pe canale, chiar si a celor neutilizati. Pentru acesti parametri, la transmisie se poate specifica valoarea 0 (nula), iar la receptie poate fi specificata indiferenta protocolului fata de valoare prin caracterul _
Completati codurile celor doua precese anterior definite pentru a fi utilizate toate campurile canalului

Q1: Fie un proces C care doreste sa citeasca mesajele de tip m3 de pe canal. Suplimentar, acestea trebuie sa aiba o anumita valoare a celui de-al doilea camp (byte - specificata printr-o variabila locala), iar al treilea camp sa fie const. Codul va fi urmatorul:

active proctype C() priority 10{
    byte var = 4;
    byte var1;
    do
    :: q ? (m3,var1, const) ->
        if
        :: (var1 == var) -> break
        :: else -> skip
        fi
    od
}

Simulati, afisand si variabilele locale (-l). Ce se intampla cu procesul C?

Q2: modificati codul procesului C, schimband ? cu ?? si rulati. Ce se observa?

Functii utile in lucrul cu canalele de date:

eval - transforma o expresie intr-o constanta
Sintaxa
len - intoarce incarcarea buffer-ului unui canal
full, nfull - verifica daca buffer-ul unui canal este sau nu plin
empty, nempty - verifica daca buffer-ul unui canal este sau nu gol

Ex1. In cadrul procesului A, schimbati linia

q!m3, 4, 0;

q!m3, 2, const;

, salvati intr-un nou fisier si simulati. Observati ca procesul C citeste ambele mesaje de tip m3 de pe canal. Acum schimbati linia

:: q ?? (m3,var1, const) ->

din cadrul procesului C cu

:: q ?? (m3,eval(var), const) ->

Ce se observa la simulare? A mai fost citit primul mesaj m3? Puteti vizualiza diferentele dintre cele doua fisiere (modele) rulate cu ajutorul comenzii

# sdiff fis1 fis2

Ex2. Rulati in mod interactiv (-i) codul:

chan q = [5] of {byte}

active proctype A(){
    do
    :: q!20
    od
}

active proctype B(){
    do
    :: q?20
    od
}

active proctype C(){
    do
    :: (len(q) == 3) ->
        skip
    :: full(q) ->
        skip
    :: nfull(q) ->
        skip
    :: empty(q) ->
        skip
    :: nempty(q) ->
        skip
    od
}

Urmariti executabilitatea instructiunilor din C pentru diferite nivele de umplere a buffer-ului canalului.

Structuri de date

Sintaxa:

typedef name { decl_lst }

decl_lst: one_decl [ ';' one_decl ] *

one_decl: [ visible ] typename  ivar [',' ivar ] *
ivar    : name [ '[' const ']' ] [ '=' any_expr | '=' ch_init ]

Structurile de date pot contine alte structuri de date si pot fi transmise pe canale de date.

Fie exemplul:

mtype = {m1, m2, m3};

typedef mesaj {
    mtype tip;
    byte c1;
    byte c2;
};

chan q = [0] of {mesaj};

active proctype A(){
    mesaj mt;
    mt.tip=m1;
    mt.c1=0;
    mt.c2=5;
    
    q!mt;
}

active proctype B(){
    mesaj mt;
    q?mt;
}

Rulati codul si comentati rezultatul.

Nota: Nu este posibila copierea directa a continutului structurilor de date, ca in cazul variabilelor clasice.

Macro definitii

In cadrul primului laborator a fost prezentata posibilitatea de declarare a unor constante prin intermediul macro-definitiilor (#define). Mai pot fi declarate si expresii conditionale :

#define alias (expr)

sau chiar secvente de cod.

#define functie(arg1 [, argi] *) instr [; instr] *

De exemplu, pentru copierea datelor intre structuri de date:

#define copy(from, to) to.tip = from.tip; to.c1 = from.c1; to.c2 = from.c2;

Integrati aceasta definitie in exemplul anterior si modificati codul procesului B pentru a copia datele receptionate intr-o alta variabila mesaj.

Aplicatie - automatul unui lift (facultativ)

Fie exemplul unui lift care face curse complete intre parter si etajul final. Usile se vor deschide automat la cele doua extreme, iar pe parcurs, doar daca liftul circula pe directia utilizatorilor. Poate fi modelat cu ajutorul automatului:

Pentru simplificarea modelului consideram cazul liftului care ajunge la un etaj anume si trebuie sa ia decizia daca este necesar sa deschida sau nu usile. Un model simplificat al liftului este:

mtype = { sus, jos }
mtype directie;

chan q = [0] of {mtype};

active proctype lift(){
    if
    :: directie = sus; goto urcare;
    :: directie = jos; goto coborare;
    fi;
    
urcare:
    // "Verifica" daca a ajuns la ultimul etaj - proces nedeterminist.
    // Q: de ce?
    if
    :: directie = jos;
        goto deschide
    :: skip
    fi;
    
    if
    :: q?sus; goto deschide
    :: q?[jos] -> skip
    fi;
    

coborare:
    if
    :: directie = sus;
        goto deschide
    :: skip
    fi;
    
    if
    :: q?jos; goto deschide
    :: q?[sus] -> skip
    fi;

deschide:
    skip;
    if
    :: (directie == sus) -> goto urcare
    :: else -> goto coborare
    fi;

end:
    skip
}

active proctype panou(){
    do
    :: q ! sus
    :: q ! jos
    od
}

Q1: Simulati interactiv modelul si verificati corectitudinea codului.
Q2: Cum poate fi modificat codul pentru a modela un panou care permite apasarea in acelasi timp a ambelor butoane? Efectuati modificarile de rigoare.
Q3: Modificati codul pentru a modela un bloc cu 5 etaje.

Exercitiu: sa se simuleze si sa se studieze exemplele cu care vine aplicatia spin (aflate in directorul de instalare, de ex. /opt/spin625/Spin/Samples).