High and Low Level Syntax for Global/Local Machines

Global/Local machines

Global Declarations

The global declarations consist of Boolean variables, set of local machines, and initial global states.
Every local machine may have either K (integer) copies or any (i.e. K >=1) in the initial global state.

Syntax:

Global Machine <Name>:
begin
Bool B₁,....,B_k
Actions L₁,...,L_q; %labels

Local Machine M₁
<Dec>
...
Local Machine M_n;
<Dec>

Initial Global State
    B₁=true/false;... B_k=true/false;
    #M₁=any/K₁;            %#=no. copies of machine M₁
    ....
    #M_n=any/K_n;
Unsafe States   (modificato il 7.1.02)
    <Prop>          %explained later
end.

Definizioni locali

Local Machine M:
begin
    States S₁,....,S_p
    Transitions list-of-rules;
    Initial state S;
end;

Rule:

S - Alpha ->S' : Guard, Action

where:
    -Guardia: conjunction of literals L₁,...,L_k(i.e. either B or not(B), B =Boolean var)
   - Action: conjuncrtion of assignments    B:=Val (Val either B, true, or false) for all declared Boolean variable B
        (by default B:=B ).
- S, S' local states
-Alpha:
        L (internal action)
        L!    (send rendez-vous)
        L!! (send broadcast)
         L? (receive rendez-vous)
        L?? (receive broadcast)
        L^ (send asyc. rendez-vous)
        L^^ (receive async. rendez-vous)

Initial States

Given the Booleran variables B1,...,Bn and the locval machines M1,...,Mn, the declaration of the initial
state is as follows:

    B1=true/false;
     ....
    Bk=true/false;
    #M1=any/K1;            %#=no. copies of machine M1
    ....
    #Mn=any/Kn;

Unsafe States (modificato il 7.01.02)

The negation of this safety property is supposed to hold in every global state reachable from the initial one

Unsafe States are a list of Propositions

Prop1
...
Propm

where

Prop is a conjunction A1,..., An of atoms
Ai is either #S >= K or a literal L
where
- S is a local states (#S = no. processes with local state =S)
- L = literal (B, not(B) dove B=Boolean variable)

Example

Global Machine Client-Server Protocol:
begin
Bool served;

Local Machine Server:
begin
    States
        Idle,Serve,Busy;
    Transitions
           Idle -req? -> Serve;
          Serve -inv!! -> Inv : served:=true;
          Inv -> ack! -> Busy;
           Busy -> rel? -> Idle;
    Initial state
            Idle;
end.

Local Machine Client:
begin
    States
        Null,Wait,Use
    Transitions
         Null - req! -> Wait;
        Wait - ack? -> Use;
        Use -> rel!   -> Null;
        Use -> inv?? -> Null;
    Initial state
        Null;
end;

Initial Global State
        served=false;
        #Server=1;
        #Client=any;

Unsafe States
#Use >=2
end.

Low Level Language: Counter Machines

We associate counters X1....Xz to each local state numbered M₁ ... M_z.
(Actually we should also keep the correspondence counter machine state (Xi --> LM.Sj ecc).

The grammar of the low level syntax is given here.

Informally, a spec in this language is as follows:

Vars
Number of Counters (Integer)
Rules
List of Transitions
Initial state
List of Guards
Target state
List of Guards
Invariant
List of Guards

Nota (7.1.02): le invarianti (invariants) sono generate separatamente attraverso altri tool e non derivano (per ora) dalla fase di compilazione

where

-List of Transitions
(separated by a blank line)

Transition₁

Transition₂

...

Transition_n

- A Transition is defined as follows

Conjunction of Guards ->
    Assignment₁
    ...
    Assignment_n

where

- Assignment

Xi=Exp where Exp::= Xj+Exp | Xj | C and Xi,Xj are counter names and C is a constant.

-Conjunction of Guards

Guard_1, ... , Guard_n (comma (virgola) as separator)

-Guard is defined either as Xi >= C or Xi = C or Xi in [C,D] where C and D are integers.
If there are no guards we assume that Xi >=0.

List of Guards

Guard₁
Guard₂
...
Guard_n

Example

Vars
3

Rules
X1>=1 ->
X1=0
X2=X1+X2+1

X1=0, X2>=1 ->
X1=X1+1
X2=X2-1

X3>=1 ->
X3=X3-1
X1=X1+1

Initial state
X1>=1,X2=0

Target state
X1>=2
X1>=1,X2>=1

Invariants
X1 in [1,5]