%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % @ Author: Amer Tahat PhD Student, Computational Sciences and Engineering, Michigan Technological University. % @ Date: 15 April 2014 %-----This file contains------------------------------------------------------------------------------------------- % 1.A Parametric Coloring Ring Model. % 2. Verification of the weak convergence property of TR(m,n) for any number of processes and colors m,n (m >= 3, n > m). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Coloring_n_m [m:posnat,n:posnat]% m is the colors number, n is the processes number. : THEORY BEGIN ASSUMING n_process_m_colors: ASSUMPTION n > m n_prs_dividedby_m_col: ASSUMPTION m >= 3 IMPORTING sets IMPORTING mod IMPORTING integers IMPORTING epsilons IMPORTING finite_sets ENDASSUMING %-EXAMPLE 1. CASE STUDY (m,n)-CL ---------------------------------------- COLORS : NONEMPTY_TYPE= below[m] CONTAINING 0 IMPORTING finite_sequences[COLORS] STC : NONEMPTY_TYPE = {s:finseq| s`length = n } CONTAINING (# length := n, seq := (LAMBDA (i:below[n]): 0) #) ndx_varb : TYPE+ =[COLORS,below[n]] CONTAINING (0,0) %---BASIC TYPES-- LL: VAR ndx_varb ss: VAR STC is_bad_nbr?(K:ndx_varb,L:ndx_varb):bool= mod(abs(K`2-L`2),n) = 1 and K`1 = L`1 is_nbr?(K:ndx_varb,L:ndx_varb):bool= mod(abs(K`2-L`2),n) <= 1 nbr_v(K:ndx_varb):TYPE+ ={C:ndx_varb|is_nbr?(K,C)} CONTAINING K % NEIGHBORS OF A VARIABLE AT PROCESS J AS A TYPE. nbr_s(K:ndx_varb):set[ndx_varb] ={C:ndx_varb|is_nbr?(K,C)} % NEIGHBORS AS A SET. k:VAR ndx_varb nbr_v_sub_ndx_varb:JUDGEMENT nbr_v(k) subtype_of ndx_varb bad_nbr_v(K:ndx_varb):TYPE ={C:ndx_varb|is_bad_nbr?(K,C)} bad_nbr_s(K:ndx_varb):set[ndx_varb] = {C:ndx_varb|is_bad_nbr?(K,C)} %Auxiliary Function-In the paper this function is called VALPOS- K(s:STC,j:below[n]): ndx_varb= (s`seq(j),j) % Valuation Function-- VAL(L:ndx_varb,s:STC): below[m]= K(s,L`2)`1 IMPORTING Add_Weak_Conv [STC,below[m],ndx_varb, VAL] %--nd-Action Function- nbr_lR(K:ndx_varb): TYPE = {c:ndx_varb|is_nbr?(K,c) and K`2-c`2 /= 0}%left/Right nbr(does not include k it self) nbr_colors(K:ndx_varb):set[COLORS]= {cl:COLORS|Exists(c:nbr_v(K)):c`1=cl } %--DEFINING OTHER FUNCTION: fullset_colors:set[COLORS]= {cl:COLORS|TRUE} other(K:ndx_varb):COLORS = epsilon(difference(fullset_colors,nbr_colors(K)) ) %-- bad/good Locality: nbr_is_bad?(s:STC,j:below[n]):bool = nonempty?(bad_nbr_s(K(s,j))) nbr_is_good?(s:STC,j:below[n]):bool= not nbr_is_bad?(s,j) %--DEF OF LEGT STATE------: is_LEGT?(s:STC):bool= Forall (j:below[n]): nbr_is_good?(s,j) S_ill:TYPE= { s:STC| not is_LEGT?(s)} %--DEF OF ACTION FUNCTION--: action(j:below[n],s:{state:STC|not is_LEGT?(state) and nbr_is_bad?(state,j)},K:ndx_varb,C:bad_nbr_v(K)): STC = TABLE %————–——————————————————-———————————————————————————————————————————————————————————————————————————–——————————--% |[ nbr_is_bad?(s,j) | nbr_is_good?(s,j) ]| %—————————————————————————————————————————————–——–———————————————————————————————————————————————————————————————————————————————---% | not is_LEGT?(s) |(# length := n, seq := (LAMBDA (i:below[n]):IF i= j THEN other(K(s,j)) ELSE s(i) ENDIF) #)| || %——————————————————————————————————————————————————————————————————————————————————————————————————————–————————————————————————–—–-% | is_LEGT?(s) | | || %—————————————————————————————————————————————————————————————————————————-———————————————————————————————————-————————–——————————–-% ENDTABLE %--Auxiliary Transition Function is given by--: TRS_p(j:below[n],s:{state:STC|not is_LEGT?(state) and nbr_is_bad?(state,j)},K:ndx_varb,C:bad_nbr_v(K)): Transition = (s, action(j,s,K,C)) % note that the action function is activated only if there exists a bad_nbr otherwise it's silent. % FOR A PROCESS-----: READ_p(s:STC, j:below[n]): set[ndx_varb]= {L:nbr_v(K(s,j))|TRUE } WRITE_p(s:STC,j:below[n]):set[ndx_varb]= {L:ndx_varb|L = K(s,j)} %-- DELTA_p(s:STC,j:below[n]):set[Transition] = {tr: Transition| Exists (c:bad_nbr_v(K(s,j))): tr = (s,action(j,s,K(s,j),c))} %-- % If s is in I the action is silent thus it's impossible to leave I. %--MAIN DEF OF A PROCESS. PRS_p(s:STC,j:below[n]): p_process = (READ_p(s,j), WRITE_p(s,j),DELTA_p(s,j)) %--FOR A PROTOCOL-----: VARB_prt(s:STC): set[ndx_varb]= {v:ndx_varb | Exists (j:below[n]):member(v, WRITE_p(s,j) )} PROC_prt(s:STC): set[p_process]={p:p_process| Exists (j:below[n]):p = PRS_p(s,j) } DELTA_prt(s:STC):set[Transition]={tr: Transition| Exists (j:below[n]):member(tr,DELTA_p(s,j)) }%restricted as above %- Main Definition TR_m_n Using Add_Weak.pvs frame work---------------------------------------------------------------------------- TR_m_n(s:STC):nd_Protocol = (PROC_prt(s),VARB_prt(s),DELTA_prt(s) ) CL_m_n(s:STC):nd_Protocol = (PROC_prt(s),VARB_prt(s),DELTA_prt(s) ) %- ADD_WEAK LEMMAS USABILITY : II:set[STC] = {s:STC|is_LEGT?(s)} I:VAR StatePred s: VAR STC sl: VAR S_ill % %-----Proof of saftey property "convergence to I after finite steps":----------------------------------------------------------------------------------- % The main idea is to construct a sequence of states that reaches I from any state out-side I. % corrected(s:STC, j:below[n]):COLORS = TABLE %————–——————————————————-————————————————-% |[ nbr_is_good?(s,j) | nbr_is_bad?(s,j) ]| %———————————————————-——————————————————–——————————————————-–% | NOT is_LEGT?(s) | s`seq(j) | other(K(s,j)) || %——————————————————————————————————————————————————————————-% | is_LEGT?(s) | s`seq(j) | || %——————————————————————————————————————————————————————————-% ENDTABLE % This function returns always a COLOR without bad neighbors at process j. It is going to be used to define localCorrectness as seen below. %------------------------------------------------------------------------------------------------------------------——————————————————————–— j:VAR below[n] x:VAR COLORS z:VAR ndx_varb bad_nbr_1: JUDGEMENT bad_nbr_v(z) SUBTYPE_OF nbr_v(z) bad_nbr_2: JUDGEMENT bad_nbr_s(z) HAS_TYPE set[bad_nbr_v(z)] AX_CHOICE:AXIOM nonempty?(bad_nbr_s(K(sl,j))) IMPLIES empty?({C: ndx_varb | is_bad_nbr?((other(K(sl, j)), j), C)}) % equivalently: other (the choice function) can choose from the choice set which does not include the bad col %PATH Construction to I: %——————————————————————- % locallyCorrected(s:STC,j:below[n]): STC = TABLE %---------------------------------------------------------------------------------------------------------------------% | not is_LEGT?(s)|(# length := n, seq := (LAMBDA (i:below[n]):IF i = j THEN corrected(s,j) ELSE s`seq(i) ENDIF)#) || %---------------------------------------------------------------------------------------------------------------------% | is_LEGT?(s) | s || %---------------------------------------------------------------------------------------------------------------------% ENDTABLE % RECURSIVE CORRECTION: corrected_up_to_j(s:STC,j:below[n]):RECURSIVE STC = TABLE %-———————————————————————————————————————————————————————————————————-——-% |[ j=0 | j > 0 ]| %---------------------------------------------------------------------------------------—–-% | not is_LEGT?(s) | locallyCorrected(s,0) | locallyCorrected(corrected_up_to_j(s,j-1),j) || %---------------------------------------------------------------------------–--------------% | is_LEGT?(s) | s | s || %--------------------------------------------------------------------------------------——--% ENDTABLE MEASURE j %-- corrected_color_at_proc_i_has_no_bad_nbr1:lemma nbr_is_good?(locallyCorrected(s,j),j) s_has_all_good_nbr_is_LEGT:lemma (forall (j:below[n]): nbr_is_good?(s,j)) implies is_LEGT?(s) % CONSTRUCTION OF LEGITIMATE STATE OUT OF RECURSIVE CORRECTION: s1:STC induct_corrected_up_to_n_minus_1_is_LEGT:THEOREM Forall (j:below[n]): nbr_is_good?(corrected_up_to_j(s1,j),j) % Applying the the recursion j-times gnerates a state that is correct up to j. % Major safety property: constructed_LEGT:STC = (# length := n, seq := (LAMBDA (j:below[n]): corrected_up_to_j(s1,j)`seq(j))#) % s1, (may /may not be LEGT) % s2=(corrected_up_to_0(s1), s1(1) ,s1(2),...,s1(n-1)) (may /may not be LEGT) % s3=(corrected_up_to_0(s1), corrected_up_to_1(s2) ,s1(2),...,s1(n-1)) (may /may not be LEGT) % : % : % constructed_LEGT (to show this must be LEGT). correcting_recursively_up_to_n_minus_1_constructs_LEGT:THEOREM is_LEGT?(constructed_LEGT) % Sugar: a different name for the above theorem: constructed_is_LEGT:THEOREM is_LEGT?(constructed_LEGT) %--------------------------------------------------------------------------------------------------------------- END Coloring_n_m