protocol.pml

 

byte N = 4, max_ann = 2, Ndatas = 2, STOP[Ndatas] = 0, STOP2[Ndatas] = 0, rec[N] = 0, annotators[N] = 0, annotators2[N] = 0, tokens[N] = 0, done = 0
 
mtype:mychan0 = { data, err0 }
chan cache2ttp[Ndatas] = [1] of { mtype:mychan0 } 

mtype:mychan1 = { annotated_data, err1 }
chan ttp2cache[Ndatas] = [1] of { mtype:mychan1 } 

mtype:mychan2 = { to_annot, token, available_choice, err2 }
chan ttp2user[N] = [0] of { mtype:mychan2 } 

mtype:mychan3 = { annotated, queried, data_choice, err3 }
chan user2ttp[N] = [0] of { mtype:mychan3 } 

mtype:mychan4 = { work, err4 }
chan cent2user[N] = [1] of { mtype:mychan4 } 

// array to keep track of processes evolution in ltl 
mtype:mystates = { _loop, _end_sleep, _end_query, _replace, _annotate, _end_simp}
mtype:mystates States[12] 


bit FINISHED=1, START=0

byte assignments[N] = {1,1,0,0}
byte assignments2[N] = {1,0,1,1}   

init 
{

annotators[0] = assignments[0]
annotators2[0] = 2*assignments2[0] 
annotators[1] = assignments[1]
annotators2[2] = 2*assignments2[2]
annotators2[3] = 2*assignments2[3] 
cache2ttp[0]!data 
cache2ttp[1]!data 
Ndatas = 2 

START = 1
endi: FINISHED = 0
}

active proctype central()
{      
byte n = 0, n_max = Ndatas
loop: 
    // loop through the cache to retreive annotated data 
    FINISHED == 0  
    States[_pid] = _loop
    if
      :: done < 2 -> skip
      :: else -> goto endc
    fi
    if 
      :: n<n_max -> skip 
      :: timeout -> n=0
    fi
    if
      :: len(ttp2cache[n])>0 -> 
            ttp2cache[n]?annotated_data 
            done = done + 1 
      :: else -> skip 
    fi
    n = n+1 
    goto loop
endc:
    FINISHED = 1  
}  

active [N] proctype ttp()
{
//  
byte n = _pid - 2, n_max = N, choices = 0, pass1 = 0, pass2 = 0
mtype:mychan3 choice = 0
end_sleep: // routine when ttp is waiting for an annotator to query data / send annotated data
     // checks in the cache for unannotated data and notifies users
     // or search for data not up to date and send annotation 
     FINISHED == 0 && (annotators[n]+annotators2[n]>0) 
     States[_pid] = _end_sleep

     if
       :: user2ttp[n]?queried -> goto end_query 
       :: user2ttp[n]?annotated -> goto replace 
       :: timeout -> skip
     fi  
     goto end_sleep
end_query:
     // send data to user 
     States[_pid] = _end_query 
     if
       :: annotators[n]*len(cache2ttp[0])>0 && annotators2[n]*len(cache2ttp[1])>0 -> // authorised to access both image => must choose 1
             ttp2user[n]!available_choice
             user2ttp[n]?choice
             choice = data_choice
       :: annotators[n]*len(cache2ttp[0])>0 && annotators2[n]*len(cache2ttp[1])==0 ->  
             choice = 1
       :: annotators2[n]*len(cache2ttp[1])>0 && annotators[n]*len(cache2ttp[0])==0 ->  
             choice = 2 
       :: else -> goto end_sleep
     fi   
     if
       :: choice==1 -> 
            if 
              :: cache2ttp[0]?data        // data is removed but not annotated yet
                   -> STOP[0] = STOP[0] + 1
                      ttp2user[n]!to_annot              // data is sent to user 
                      rec[n] = rec[n] + 1 
              :: len(cache2ttp[0])==0 -> annotators[n] = 0   // access is revoked 
            fi
       :: choice==2 ->  
            if 
              :: cache2ttp[1]?data        // data is removed but not annotated yet
                   -> STOP[1] = STOP[1] + 1
                      ttp2user[n]!to_annot              // data is sent to user 
                      rec[n] = rec[n] + 1 
              :: len(cache2ttp[1])==0 -> annotators2[n] = 0   // access is revoked 
            fi
     fi
     goto end_sleep
replace:
     // send annotated data to the cache 
     States[_pid] = _replace
     tokens[n] = 1
     if 
       :: choice==1 ->  
           annotators[n] = 0   // access is revoked 
           ttp2cache[0]!annotated_data
       :: choice==2 ->  
           annotators2[n] = 0  // access is revoked 
           ttp2cache[1]!annotated_data
     fi      
     States[_pid] = _end_sleep  
     goto end_sleep
}

active [N] proctype user()
{
byte id = _pid - 6
mtype:mychan3 choice = 1 
// routine when user is waiting for the central to ask for annotation
// waits    
// cent2user[id]?work  

end_sleep: 
    FINISHED == 0 && (annotators[id]>0 || annotators2[id]>0) 
    States[_pid] = _end_sleep
    
    // demand access to one of available data   
    if
      :: user2ttp[id]!queried
      :: FINISHED == 1 -> goto end_sleep  // access denied
    fi
    States[_pid] = _end_sleep
   
end_if: 
    if
      :: ttp2user[id]?available_choice -> 
           choice = 1
           if 
             :: true -> choice = 2 
             :: skip
           fi
           user2ttp[id]!choice
           if
             :: ttp2user[id]?to_annot -> goto annotate
             :: FINISHED == 1 -> goto end_sleep  // access denied
           fi 
      :: ttp2user[id]?to_annot -> goto annotate
      // :: skip -> goto end_if         // access denied
    fi  
    goto end_if
annotate: 
     // annotates data  
     States[_pid] = _annotate  
     user2ttp[id]!annotated  
     States[_pid] = _end_sleep
     goto end_sleep
} 

#define start (FINISHED == 0)  // simulation has started

////////////////////////////////
// Property 1: each data can be accessed by only one authorised annotator 
// -> if simulation completes, only 4 terminal states are valid 

#define terminal0 ( rec[0]==0 && rec[1]==1 && rec[2]+rec[3]==1 )     // 0 reveived nothing
#define terminal1 ( rec[0]==2 && rec[1]+rec[2]+rec[3]==0 )           // 0 received both images 0 and 1
#define terminal2 ( rec[0]==1 && rec[1]==1 && rec[2]+rec[3]==0 )     // 0 received 1
#define terminal3 ( rec[0]==1 && rec[1]==0 && rec[2]+rec[3]==1 )     // 0 received 0
#define terminal ( ((len(cache2ttp[0])+len(cache2ttp[1]))==0) implies (eventually (terminal0 || terminal1 || terminal2 || terminal3)) )

// but intermediates states must be checked to avoid wrong accesses 
#define itermediate_rec0 ( ((len(cache2ttp[0])+len(cache2ttp[1]))==1) implies eventually (rec[0]==1) )       // 0 reveived something
#define itermediate_rec1 ( (len(cache2ttp[0])==0 && len(cache2ttp[1])==1) implies eventually (rec[1]==1) )   // 1 reveived 1 (and never receive 2)
#define itermediate_rec2 ( (len(cache2ttp[0])==1 && len(cache2ttp[1])==0) implies eventually (rec[2]==1) )   // 2 reveived 2
#define itermediate_rec3 ( (len(cache2ttp[0])==1 && len(cache2ttp[1])==0) implies eventually (rec[3]==1) )   // 3 reveived 2
#define intermediate ( itermediate_rec0 || itermediate_rec1 || itermediate_rec2 || itermediate_rec3 )

ltl p1 { always (start implies ( terminal && intermediate )  )  }


///////////////////////////////////////////////
// Property 2: 
// -> if an image is not in the cache, it is because it has been or is beeing annotated   
#define img1 ( (start && len(cache2ttp[0])==0) -> eventually (States[6]==_annotate || States[7]==_annotate) )   
#define img2 ( (start && len(cache2ttp[1])==0) -> eventually (States[6]==_annotate || States[8]==_annotate || States[9]==_annotate) ) 

ltl p2 { always (img1 && img2) } 

//////////////////
// Property 3: if an image has been annotated, it sent back to the cache

#define annotated0 (user2ttp[0]==annotated)    // annotator 0 sent an annotation
#define annotated1 (user2ttp[1]==annotated)    // annotator 1 sent an annotation
#define annotated2 (user2ttp[2]==annotated)    // annotator 2 sent an annotation
#define annotated3 (user2ttp[3]==annotated)    // annotator 3 sent an annotation
// #define annotated4 (user2ttp[4]==annotated)

ltl p3 { always ( start implies ( (annotated1 implies (eventually len(ttp2cache[0])==1))          // annotator 1 sent its annotation so it should be sent to the cache
                               && ( (annotated2 || annotated3) implies (eventually len(ttp2cache[1])==1)) 
                               && ( annotated0 implies (eventually (len(ttp2cache[0])==1 || len(ttp2cache[1])==1)) ) )) } 

////////////////////// 
// Property 4: once an annotator sent an annotation, its access to the corresponding image is revoked 

#define rev0a (annotators[0]==0 && len(cache2ttp[0])==0 && len(cache2ttp[1])==1)
#define rev0b (annotators2[0]==0 && len(cache2ttp[1])==0 && len(cache2ttp[0])==1)
#define rev0ab (annotators2[0]+annotators[0]==0 && len(cache2ttp[0])+len(cache2ttp[1])==0)
#define rev0 ( (annotated0 implies (eventually ( rev0a || rev0b || rev0ab )))  || !annotated0 )
#define rev1 ( (annotated1 implies (eventually annotators[1]==0)) || !annotated1 )
#define rev2 ( (annotated2 implies (eventually annotators2[2]==0)) || !annotated2 )
#define rev3 ( (annotated3 implies (eventually annotators2[3]==0)) || !annotated3 )

ltl p4 {always (start implies (rev0 && rev1 && rev2 && rev3) )}

////////////////////// 
// Property 5: iff an annotator performs an annotation, it receives a token  // && u4

#define u0 ( ((annotated0 implies (eventually tokens[0]>0)) && (tokens[0]>0 implies annotated0) ) || !annotated0 )
#define u1 ( ((annotated1 implies (eventually tokens[1]>0)) && (tokens[1]>0 implies annotated1) ) || !annotated1 )
#define u2 ( ((annotated2 implies (eventually tokens[2]>0)) && (tokens[2]>0 implies annotated2) ) || !annotated2 )
#define u3 ( ((annotated3 implies (eventually tokens[3]>0)) && (tokens[3]>0 implies annotated3) ) || !annotated3 )
// #define u4 ( ((annotated4 implies (eventually tokens[4]>0)) && (tokens[4]>0 implies annotated0) ) || !annotated4 )

ltl p5 { always ( start implies (u0 && u1 && u2 && u3 ) ) }
 
////////////////////////
// properties checked by sucessfull complition of the simulation: 
// 7) all images are removed once annotated / no annotation left in the cache
// 8) all images annotated