diff -r 6c12f5e24e34 -r 0437dbc127b3 src/HOL/HOLCF/IOA/ABP/Check.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/HOLCF/IOA/ABP/Check.ML Sat Nov 27 16:08:10 2010 -0800 @@ -0,0 +1,178 @@ +(* Title: HOLCF/IOA/ABP/Check.ML + Author: Olaf Mueller + +The Model Checker. +*) + +structure Check = +struct + +(* ---------------------------------------------------------------- + P r o t o t y p e M o d e l C h e c k e r + ----------------------------------------------------------------*) + +fun check(extacts,intacts,string_of_a,startsI,string_of_s, + nexts,hom,transA,startsS) = + let fun check_s(s,unchecked,checked) = + let fun check_sa a unchecked = + let fun check_sas t unchecked = + (if member (op =) extacts a then + (if transA(hom s,a,hom t) then ( ) + else (writeln("Error: Mapping of Externals!"); + string_of_s s; writeln""; + string_of_a a; writeln""; + string_of_s t;writeln"";writeln"" )) + else (if hom(s)=hom(t) then ( ) + else (writeln("Error: Mapping of Internals!"); + string_of_s s; writeln""; + string_of_a a; writeln""; + string_of_s t;writeln"";writeln"" )); + if member (op =) checked t then unchecked else insert (op =) t unchecked) + in fold check_sas (nexts s a) unchecked end; + val unchecked' = fold check_sa (extacts @ intacts) unchecked + in (if member (op =) startsI s then + (if member (op =) startsS (hom s) then () + else writeln("Error: At start states!")) + else (); + checks(unchecked',s::checked)) end + and checks([],_) = () + | checks(s::unchecked,checked) = check_s(s,unchecked,checked) + in checks(startsI,[]) end; + + +(* ------------------------------------------------------ + A B P E x a m p l e + -------------------------------------------------------*) + +datatype msg = m | n | l; +datatype act = Next | S_msg of msg | R_msg of msg + | S_pkt of bool * msg | R_pkt of bool * msg + | S_ack of bool | R_ack of bool; + +(* -------------------- Transition relation of Specification -----------*) + +fun transA((u,s),a,(v,t)) = + (case a of + Next => v andalso t = s | + S_msg(q) => u andalso not(v) andalso t = s@[q] | + R_msg(q) => u = v andalso s = (q::t) | + S_pkt(b,q) => false | + R_pkt(b,q) => false | + S_ack(b) => false | + R_ack(b) => false); + + +(* ---------------------- Abstraction function --------------------------*) + +fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p)); + + +(* --------------------- Transition relation of Implementation ----------*) + +fun nexts (s as (env,p,a,q,b,ch1,ch2)) action = + (case action of + Next => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] | + S_msg(mornorl) => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] | + R_msg(mornorl) => if (q<>[] andalso mornorl=hd(q)) + then [(env,p,a,tl(q),b,ch1,ch2)] + else [] | + S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a) + then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl)) + then [s] + else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)]) + else [] | + R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl)) + then (if (h<>b andalso q=[]) + then [(env,p,a,q@[mornorl],not(b),ch1,ch2), + (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)] + else [s,(env,p,a,q,b,tl(ch1),ch2)]) + else [] | + S_ack(h) => if (h=b) + then (if (ch2<>[] andalso h=hd(rev(ch2))) + then [s] + else [s,(env,p,a,q,b,ch1,ch2@[h])]) + else [] | + R_ack(h) => if (ch2<>[] andalso hd(ch2)=h) + then (if h=a + then [(env,tl(p),not(a),q,b,ch1,ch2), + (env,tl(p),not(a),q,b,ch1,tl(ch2))] + else [s,(env,p,a,q,b,ch1,tl(ch2))]) + else []) + + +val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)]; +val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true), + S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false), + S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l), + S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)]; + + +(* ------------------------------------ + Input / Output utilities + ------------------------------------*) + +fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) = + let fun prec x = (Output.raw_stdout ","; pre x) + in + (case lll of + [] => (Output.raw_stdout lpar; Output.raw_stdout rpar) + | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar)) + end; + +fun pr_bool true = Output.raw_stdout "true" +| pr_bool false = Output.raw_stdout "false"; + +fun pr_msg m = Output.raw_stdout "m" +| pr_msg n = Output.raw_stdout "n" +| pr_msg l = Output.raw_stdout "l"; + +fun pr_act a = Output.raw_stdout (case a of + Next => "Next"| + S_msg(ma) => "S_msg(ma)" | + R_msg(ma) => "R_msg(ma)" | + S_pkt(b,ma) => "S_pkt(b,ma)" | + R_pkt(b,ma) => "R_pkt(b,ma)" | + S_ack(b) => "S_ack(b)" | + R_ack(b) => "R_ack(b)"); + +fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">"); + +val pr_bool_list = print_list("[","]",pr_bool); +val pr_msg_list = print_list("[","]",pr_msg); +val pr_pkt_list = print_list("[","]",pr_pkt); + +fun pr_tuple (env,p,a,q,b,ch1,ch2) = + (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p; Output.raw_stdout ", "; + pr_bool a; Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", "; + pr_bool b; Output.raw_stdout ", "; pr_pkt_list ch1; Output.raw_stdout ", "; + pr_bool_list ch2; Output.raw_stdout "}"); + + + +(* --------------------------------- + Main function call + ---------------------------------*) + +(* +check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], + pr_tuple, nexts, hom, transA, [(true,[])]); +*) + + + + + +(* + Little test example + +datatype act = A; +fun transA(s,a,t) = (not(s)=t); +fun hom(i) = i mod 2 = 0; +fun nexts s A = [(s+1) mod 4]; +check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]); + +fun nexts s A = [(s+1) mod 5]; + +*) + +end;