<div class="notebook"> <div class="nb-cell markdown"> # Probabilistic Computation Tree Logic In this example we want to perform model checking of the Synchronous Leader Election Protocol expressed in Probabilistic Computation Tree Logic (PCTL). This example shows the computation of expectations and the possibility of mixing LPADs and Prolog for drawing diagrams. Given a synchronous ring of N processes the Synchronous Leader Election Protocol is used to elect a leader (a uniquely designated processor) by sending messages around the ring. The protocol proceeds in rounds and is parametrised by a constant K. Each round begins by all processors (independently) choosing a random number (uniformly) from {1,...,K} as an id. The processors then pass their ids around the ring. If there is a unique id, then the processor with the maximum unique id is elected the leader, and otherwise the processors begin a new round. With this program you can - check that the probability of eventually electing a leader is 1 - compute the probability of electing a leader within a certain number of rounds - compute the expected number of rounds to elect a leader - graph the probability of electing a leader within L rounds as a function of L - graph the expected number of rounds to elect a leader as a function of the number of processes or of K ## Full program The full program of this example is </div> <div class="nb-cell program prolog" data-singleline="true"> :- use_module(library(mcintyre)). :- if(current_predicate(use_rendering/1)). :- use_rendering(c3). :- endif. :- dynamic kr/1,num/1. :- mc. :- begin_lpad. % State Formulae models(_S, tt,_Hist,_Limit,_Time). models(S, prop(P),_Hist,_Limit,_Time) :- proposition(P, S). models(S, and(F1, F2),Hist,Limit,Time) :- models(S, F1,Hist,Limit,Time), models(S, F2,Hist,Limit,Time). models(S, or(F1, _F2),Hist,Limit,Time) :- models(S, F1,Hist,Limit,Time). models(S, or(F1, F2),Hist,Limit,Time) :- \+ models(S, F1,Hist,Limit,Time), models(S, F2,Hist,Limit,Time). models(S, not(F), Hist,Limit,Time) :- \+ models(S, F,Hist,Limit,Time). models(S, prob_until(comp(Op, P), F1, F2),Hist,Limit,Time) :- mc_sample(pmodels(S, until(F1, F2),Hist,Limit,Time),20, Q), comp(Q, Op, P). models(S, prob_next(comp(Op, P), F),Hist,Limit,Time) :- mc_sample(pmodels(S, next(F),Hist,Limit,Time),20, Q), comp(Q, Op, P). comp(Q,>,P):- Q>P. comp(Q,>=,P):- Q>=P. comp(Q,<,P):- Q<P. comp(Q,=<,P):- Q=<P. % Path Formulae pmodels(S,F):- pmodels(S,F,[],nolimit,0,_Time). pmodels(S,F,Hist,Limit,Time):- pmodels(S,F,Hist,Limit,Time,_Time). pmodels(S, until(_F1, F2),Hist,Limit,Time,Time) :- models(S, F2,Hist,Limit,Time),!. pmodels(S, until(F1, F2),Hist0,Limit,Time0,Time) :- within_limit(Time0,Limit), models(S, F1,Hist0,Limit,Time0), ctrans(S, _, T, Hist0, Hist),!, Time1 is Time0+1, pmodels(T, until(F1,F2),Hist,Limit,Time1,Time). pmodels(S, next(F), Hist,Limit,Time0,Time) :- within_limit(Time0,Limit), ctrans(S, _, T, Hist, _),!, Time is Time0+1, models(T, F,Hist,Limit,Time). within_limit(_Time,nolimit):-!. within_limit(Time,Limit):- Time<Limit. bounded_eventually(Prop,Rounds):- num(N), B is Rounds*(N+1), eventually(Prop,B,_T). eventually(Prop):- eventually(Prop,_T). eventually(Prop,Rounds):- eventually(Prop,nolimit,T), num(N), Rounds is T/(N+1). eventually(Prop,Limit,T) :- init(S), pctlspec(Prop, F), pmodels(S, F,[],Limit,0,T). pctlspec(X, until(tt, prop(X))). proposition(P, S) :- final(P, S). final(elect, [_|L]) :- num(N), gen_elected_state(N, L). gen_elected_state(J, L) :- (J==0 -> L=[] ; L = [state(3,_,_,_)|Rest], J1 is J-1, gen_elected_state(J1,Rest) ). % transitions % module counter % [read] c<N-1 -> (c'=c+1); % reading trans(counter, counter(C), read, counter(D),_S,H,H) :- num(N), C < N-1, D is C+1. % [read] c=N-1 -> (c'=c); % finished reading trans(counter, counter(C), read, counter(C),_S,H,H) :- num(N), C =:= N-1. % [done] u1 | u2 | u3 | u4 -> (c'=c); % done trans(counter, counter(C), done, counter(C),S,H,H) :- get_processid(P), nonlocal(process(P,_), uniqueid, 1,S). % [retry] !(u1 | u2 | u3 | u4) -> (c'=1); % pick again reset counter trans(counter, counter(_C), retry, counter(1),S,H,H) :- findall(P,get_processid(P),PL), maplist(nl(S),PL). % [loop] s1=3 -> (c'=c); % loop (when finished to avoid deadlocks) trans(counter, counter(C), loop, counter(C),S,H,H) :- nonlocal(process(1,_), state, 3,S). % module process % local state % s1=0 make random choice % s1=1 reading % s1=2 deciding % s1=3 finished % [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) + ...; % pick value trans(process(_N,_Next), state(0,_,_,_), pick, state(1,1,R,R),_S,H,[pick(R)|H]) :- pick(H,R). %read % [read] s1=1 & u1 & !p1=v2 & c<N-1 -> (u1'=true) & (v1'=v2); trans(process(_N,Next), state(1,1,_,P), read, state(1,1,V,P),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C < CN - 1, nonlocal(process(Next,_), value, V,S), P \== V. % [read] s1=1 & u1 & p1=v2 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0); trans(process(_N,Next), state(1,1,_,P), read, state(1,0,V,0),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C < CN - 1, nonlocal(process(Next,_), value, V,S), P == V. % [read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2); trans(process(_N,Next), state(1,0,_,P), read, state(1,0,V,P),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C < CN - 1, nonlocal(process(Next,_), value, V,S). % read and move to decide % [read] s1=1 & u1 & !p1=v2 & c=N-1 -> (s1'=2) & (u1'=true) & (v1'=0) & (p1'=0); trans(process(_N,Next), state(1,1,_,P), read, state(2,1,0,0),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C =:= CN - 1, nonlocal(process(Next,_), value, V,S), P \== V. % [read] s1=1 & u1 & p1=v2 & c=N-1 -> (u1'=false) & (v1'=0) & (p1'=0); trans(process(_N,Next), state(1,1,_,P), read, state(2,0,0,0),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C =:= CN - 1, nonlocal(process(Next,_), value, V,S), P == V. % [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); trans(process(_N,_Next), state(1,0,_,P), read, state(2,0,0,P),S,H,H) :- nonlocal(counter, counter, C,S), num(CN), C =:= CN - 1. % done % [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); trans(process(_N,_Next), state(2,_,_,_), done, state(3,0,0,0),_S,H,H). % retry % [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); trans(process(_N,_Next), state(2,_,_,_), retry, state(0,0,0,0),_S,H,H). % loop (when finished to avoid deadlocks) % [loop] s1=3 -> (s1'=3); trans(process(_N,_Next), state(3,U,V,P), loop, state(3,U,V,P),_S,H,H). pick(H,V):- kr(K), K1 is K-1, PH is 1/K, findall(I,between(0,K1,I),L), foldl(pick_value(H,PH),L,(1,_),(_,V)). pick_value(_H,_PH,_I,(P0,V0),(P0,V0)):- nonvar(V0). pick_value(H,PH,I,(P0,V0),(P1,V1)):- var(V0), PF is PH/P0, (pick_fact(H,V0,PF)-> P1=PF, V1=I ; P1 is P0*(1-PF), V1=V0 ). pick_fact(_,_,P):P. %pick(H,0):0.5; pick(H,1):0.5. ctrans(S, A, T, Hi, Ho) :- config(P), find_matching_trans(P,S,S,[],A,T,Hi,Ho). find_matching_trans([], [], _CS, _PA, A, [], H,H) :- nonvar(A). find_matching_trans([P|Ps], [S|Ss], CS, PA, A, [T|Ts],Hi,Ho) :- pick_trans(P, S, CS, PA, A, T, Hi,H1), find_matching_trans(Ps, Ss, CS, PA, A, Ts,H1,Ho). find_matching_trans([P|Ps], [S|Ss], CS, PA, A, [S|Ts], Hi,Ho) :- % skip current process; but then all transitions enabled in the current % process will be prohibited for selection in later processes. enabled_trans(P,L), (nonvar(A) -> \+ member(A,L); true), append(L, PA, PA1), find_matching_trans(Ps, Ss, CS, PA1, A, Ts, Hi, Ho). pick_trans(P, S, CS, PA, A, T, H0,H) :- etrans(P, S, PA, A, T,CS, H0,H). etrans(P, S, PA, A, T, CS,H0,H) :- trans(P, S, A, T,CS,H0,H), A \= epsilon, \+ member(A, PA). enabled_trans(P, L) :- setof(A, enabled_trans_in_process(P,A), L). enabled_trans_in_process(P,A) :- clause(trans(P,_,A,_,_,_,_),_), A \= epsilon. nonlocal(Proc, Var, Val,CS) :- getpid(Proc, Var, Pid, Idx), nth1(Pid, CS, State), arg(Idx, State, Val). % writeln(nonlocal_read(Proc, State, Var, Val)). getpid(Proc, Var, Pid, Idx) :- config(Config), nth1(Pid, Config, Proc), nonlocal_access(Proc, Var, Idx). get_processid(P):- num(N), between(1,N,P). config([counter| L]) :- findall(P,get_processid(P),PL), maplist(neighbor,PL,L). neighbor(I,process(I,J)) :- num(N), (I<N -> J is I+1 ; J = 1 ). %config([counter, process(1,2), process(2,3), process(3,4), process(4,1)]). init(S) :- config(P), maplist(init_state,P,S). init_state(counter, counter(1)). init_state(process(_,_), state(0,0,0,0)). nonlocal_access(counter, counter, 1). nonlocal_access(process(_,_), state, 1). nonlocal_access(process(_,_), uniqueid, 2). nonlocal_access(process(_,_), value, 3). nl(S,P):- nonlocal(process(P, _), uniqueid, 0,S). num(4). kr(4). :- end_lpad. graph_prob(G):- retract(num(N)), retract(kr(K)), assert(num(4)), assert(kr(2)), findall(L-P, (between(1,6,L),mc_sample(bounded_eventually(elect,L),100,P)),LV), G=c3{data:_{x:x, rows:[x-'Probability of leader elected within L rounds (N=4, K=2)'|LV]},%legend:_{show: false}, axis:_{x:_{min:1,max:6,label:'L',padding:_{bottom:0.0,top:0.0}}, y:_{label:'Probability',padding:_{bottom:0.0,top:0.0}}}}, retract(num(4)), retract(kr(2)), assert(num(N)), assert(kr(K)). graph_exp_rounds_n(G):- retract(num(NI)), retract(kr(KI)), assert(kr(3)), findall(N-E, (between(3,8,N), assert(num(N)), mc_expectation(eventually(elect,T),100,T,E), retract(num(N))), LV), G=c3{data:_{x:x, rows:[x-'Expected rounds to elect a leader (K=3)'|LV]},%legend:_{show: false}, axis:_{x:_{min:3,max:8,label:'N',padding:_{bottom:0.0,top:0.0}}, y:_{label:'Expected rounds',padding:_{bottom:0.0,top:0.0}}}}, retract(kr(3)), assert(num(NI)), assert(kr(KI)). graph_exp_rounds_k(G):- retract(num(NI)), retract(kr(KI)), assert(num(3)), findall(K-E, (between(3,8,K), assert(kr(K)), mc_expectation(eventually(elect,T),500,T,E), retract(kr(K))), LV), G=c3{data:_{x:x, rows:[x-'Expected rounds to elect a leader (N=3)'|LV]},%legend:_{show: false}, axis:_{x:_{min:3,max:8,label:'K',padding:_{bottom:0.0,top:0.0}}, y:_{label:'Expected rounds',padding:_{bottom:0.0,top:0.0}}}}, retract(num(3)), assert(num(NI)), assert(kr(KI)). </div> <div class="nb-cell markdown"> We first consider the problem of computing expectations. We would like to compute the expected number of rounds to elect a leader. We can compute expectations with == mc_expectation(:Query:atom,+N:int,?Arg:var,-Exp:float). == that computes the expected value of =Arg= in =Query= by sampling. It takes =N= samples of =Query= and sums up the value of =Arg= for each sample. The overall sum is divided by =N= to give =Exp=. An example of use of the above predicate is </div> <div class="nb-cell query"> mc_expectation(eventually(elect,T),1000,T,E). </div> <div class="nb-cell markdown"> that returns in E the expected value of rounds necessary to elect a leader computed by taking 1000 samples. </div> <div class="nb-cell markdown"> We can mix LPADs and Prolog for drawing a graph of the expected number of rounds to elect a leader as a funtion of the number of processes when K=3. We use the Prolog code below, that is included in the program above outside `:-begin/end_lpad`: == graph_exp_rounds_n(G):- retract(num(NI)), retract(kr(KI)), assert(kr(3)), findall(N-E, (between(3,8,N), assert(num(N)), mc_expectation(eventually(elect,T),100,T,E), retract(num(N))), LV), G=c3{data:_{x:x, rows:[x-'Expected rounds to elect a leader (K=3)'|LV]},%legend:_{show: false}, axis:_{x:_{min:3,max:8,label:'N',padding:_{bottom:0.0,top:0.0}}, y:_{label:'Expected rounds',padding:_{bottom:0.0,top:0.0}}}}, retract(kr(3)), assert(num(NI)), assert(kr(KI)). == Note that =num/1= and =kr/1= are declared as dynamic at the beginning of the program, so their definition can be changed. =num/1= stores the number of processes N and =kr/1= the value of K. =graph_exp_rounds_n/1= returns a dict that is rendered as a =c3= graph. The predicates performs a findall/3 where it first asserts an increasing value for N, from 3 to 8, and then computes the expected value of the rounds necessary to elect a leader. The resulting data is then inserted in a =c3=dict. Calling graph_exp_rounds_n(G) you get a graph of the expected number of rounds to elect a leader as a funtion of the number of processes when K=3. </div> <div class="nb-cell query"> graph_exp_rounds_n(G). </div> <div class="nb-cell markdown"> -- Complete example: [pctl_slep.pl](example/inference/pctl_slep.pl) - References: - Gorlin, Andrey, C. R. Ramakrishnan, and Scott A. Smolka. _Model checking with probabilistic tabled logic programming_. Theory and Practice of Logic Programming 12.4-5 (2012). - http://www.prismmodelchecker.org/casestudies/synchronous_leader.php </div> <div class="nb-cell markdown"> -- [Back to Tutorial](tutorial/tutorial.swinb) </div> </div>