Как отправить REQ и распространить его с помощью Promela? - PullRequest
Новая
       18

Как отправить REQ и распространить его с помощью Promela?

0 голосов
/ 03 января 2019

Я хочу сделать в Promela протокол, который применяет следующее:

Пользователь A отправляет запрос REQ в сетевой протокол N1.N1 распространяет запрос через req в сетевой процесс N2.Затем он отправляет указание IND пользовательскому процессу B и получает ответное сообщение RSP.Этот ответ распространяется от A до N1 с использованием сообщений rsp и CNF.

Чтобы сделать это, я попытался с этим кодом: 

mtype = {m}
chan REQ = [5] of {mtype,bit}
chan req = [5] of {mtype,bit}
chan IND = [5]  of {mtype,bit}
chan RSP = [5] of {mtype,bit}
chan rsp = [5] of {mtype,bit}
chan CNF = [5] of {mtype,bit}


active proctype A(){
bit b =0;
bit v=0;
   bit x;
do
  :: true;
env:        if
    :: REQ!m,b;
    :: skip;
    fi;
espera:     if
    :: CNF?x
    if
    ::x==b->b=!b; goto env;
    fi;

    fi;
    od;
}

active proctype N1(){
   bit b =0;
   bit x;
   bit y=0;
do
::true;
recibomensaje:
  :: REQ?m,b;
espera_confirmacion:
            if
    ::x==b->req!b;b!=b;goto espera2;
    fi;
espera2:
        ::rsp?x
    if
       ::x == y->RSP?y;y!=y;goto recibomensaje;
    fi;

od;
}
active proctype N2(){
   bit b =0;
   bit x;
   bit y=1;
do
::true;
recibomensaje:
  :: req?m,b;
espera_confirmacion:
                if
    ::x==b->IND!b;b!=b;goto espera2;
    fi;
espera2:
        ::RSP?x
    if
       ::x == y->rsp?y;y!=y;goto recibomensaje;
    fi;

od;
}

Ошибка, которая дает мне: 

 proc  0 (A:1) Ejercicio2.1:15 (state 1)    [(1)]
    proc  2 (N2:1) Ejercicio2.1:55 (state 1)    [(1)]
proc  1 (N1:1) Ejercicio2.1:35 (state 1)    [(1)]
proc  2 (N2:1) Ejercicio2.1:57 (state 2)    [(1)]
proc  0 (A:1) Ejercicio2.1:17 (state 2) [REQ!m,b]
proc  1 (N1:1) Ejercicio2.1:37 (state 2)    [(1)]
proc  2 (N2:1) Ejercicio2.1:55 (state 1)    [(1)]
proc  1 (N1:1) Ejercicio2.1:37 (state 3)    [REQ?m,b]
proc  2 (N2:1) Ejercicio2.1:57 (state 2)    [(1)]
proc  1 (N1:1) Ejercicio2.1:40 (state 4)    [((x==b))]
proc  2 (N2:1) Ejercicio2.1:55 (state 1)    [(1)]
    warning: missing params in send
...