1(* Title: HOL/HOLCF/IOA/ABP/Check.ML 2 Author: Olaf Mueller 3 4The Model Checker. 5*) 6 7structure Check = 8struct 9 10(* ---------------------------------------------------------------- 11 P r o t o t y p e M o d e l C h e c k e r 12 ----------------------------------------------------------------*) 13 14fun check(extacts,intacts,string_of_a,startsI,string_of_s, 15 nexts,hom,transA,startsS) = 16 let fun check_s(s,unchecked,checked) = 17 let fun check_sa a unchecked = 18 let fun check_sas t unchecked = 19 (if member (op =) extacts a then 20 (if transA(hom s,a,hom t) then ( ) 21 else (writeln("Error: Mapping of Externals!"); 22 string_of_s s; writeln""; 23 string_of_a a; writeln""; 24 string_of_s t;writeln"";writeln"" )) 25 else (if hom(s)=hom(t) then ( ) 26 else (writeln("Error: Mapping of Internals!"); 27 string_of_s s; writeln""; 28 string_of_a a; writeln""; 29 string_of_s t;writeln"";writeln"" )); 30 if member (op =) checked t then unchecked else insert (op =) t unchecked) 31 in fold check_sas (nexts s a) unchecked end; 32 val unchecked' = fold check_sa (extacts @ intacts) unchecked 33 in (if member (op =) startsI s then 34 (if member (op =) startsS (hom s) then () 35 else writeln("Error: At start states!")) 36 else (); 37 checks(unchecked',s::checked)) end 38 and checks([],_) = () 39 | checks(s::unchecked,checked) = check_s(s,unchecked,checked) 40 in checks(startsI,[]) end; 41 42 43(* ------------------------------------------------------ 44 A B P E x a m p l e 45 -------------------------------------------------------*) 46 47datatype msg = m | n | l; 48datatype act = Next | S_msg of msg | R_msg of msg 49 | S_pkt of bool * msg | R_pkt of bool * msg 50 | S_ack of bool | R_ack of bool; 51 52(* -------------------- Transition relation of Specification -----------*) 53 54fun transA((u,s),a,(v,t)) = 55 (case a of 56 Next => v andalso t = s | 57 S_msg(q) => u andalso not(v) andalso t = s@[q] | 58 R_msg(q) => u = v andalso s = (q::t) | 59 S_pkt(b,q) => false | 60 R_pkt(b,q) => false | 61 S_ack(b) => false | 62 R_ack(b) => false); 63 64 65(* ---------------------- Abstraction function --------------------------*) 66 67fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p)); 68 69 70(* --------------------- Transition relation of Implementation ----------*) 71 72fun nexts (s as (env,p,a,q,b,ch1,ch2)) action = 73 (case action of 74 Next => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] | 75 S_msg(mornorl) => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] | 76 R_msg(mornorl) => if (q<>[] andalso mornorl=hd(q)) 77 then [(env,p,a,tl(q),b,ch1,ch2)] 78 else [] | 79 S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a) 80 then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl)) 81 then [s] 82 else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)]) 83 else [] | 84 R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl)) 85 then (if (h<>b andalso q=[]) 86 then [(env,p,a,q@[mornorl],not(b),ch1,ch2), 87 (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)] 88 else [s,(env,p,a,q,b,tl(ch1),ch2)]) 89 else [] | 90 S_ack(h) => if (h=b) 91 then (if (ch2<>[] andalso h=hd(rev(ch2))) 92 then [s] 93 else [s,(env,p,a,q,b,ch1,ch2@[h])]) 94 else [] | 95 R_ack(h) => if (ch2<>[] andalso hd(ch2)=h) 96 then (if h=a 97 then [(env,tl(p),not(a),q,b,ch1,ch2), 98 (env,tl(p),not(a),q,b,ch1,tl(ch2))] 99 else [s,(env,p,a,q,b,ch1,tl(ch2))]) 100 else []) 101 102 103val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)]; 104val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true), 105 S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false), 106 S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l), 107 S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)]; 108 109 110(* ------------------------------------ 111 Input / Output utilities 112 ------------------------------------*) 113 114fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) = 115 let fun prec x = (Output.physical_stdout ","; pre x) 116 in 117 (case lll of 118 [] => (Output.physical_stdout lpar; Output.physical_stdout rpar) 119 | x::lll => (Output.physical_stdout lpar; pre x; List.app prec lll; Output.physical_stdout rpar)) 120 end; 121 122fun pr_bool true = Output.physical_stdout "true" 123| pr_bool false = Output.physical_stdout "false"; 124 125fun pr_msg m = Output.physical_stdout "m" 126| pr_msg n = Output.physical_stdout "n" 127| pr_msg l = Output.physical_stdout "l"; 128 129fun pr_act a = Output.physical_stdout (case a of 130 Next => "Next"| 131 S_msg(ma) => "S_msg(ma)" | 132 R_msg(ma) => "R_msg(ma)" | 133 S_pkt(b,ma) => "S_pkt(b,ma)" | 134 R_pkt(b,ma) => "R_pkt(b,ma)" | 135 S_ack(b) => "S_ack(b)" | 136 R_ack(b) => "R_ack(b)"); 137 138fun pr_pkt (b,ma) = (Output.physical_stdout "<"; pr_bool b;Output.physical_stdout ", "; pr_msg ma; Output.physical_stdout ">"); 139 140val pr_bool_list = print_list("[","]",pr_bool); 141val pr_msg_list = print_list("[","]",pr_msg); 142val pr_pkt_list = print_list("[","]",pr_pkt); 143 144fun pr_tuple (env,p,a,q,b,ch1,ch2) = 145 (Output.physical_stdout "{"; pr_bool env; Output.physical_stdout ", "; pr_msg_list p; Output.physical_stdout ", "; 146 pr_bool a; Output.physical_stdout ", "; pr_msg_list q; Output.physical_stdout ", "; 147 pr_bool b; Output.physical_stdout ", "; pr_pkt_list ch1; Output.physical_stdout ", "; 148 pr_bool_list ch2; Output.physical_stdout "}"); 149 150 151 152(* --------------------------------- 153 Main function call 154 ---------------------------------*) 155 156(* 157check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], 158 pr_tuple, nexts, hom, transA, [(true,[])]); 159*) 160 161 162 163 164 165(* 166 Little test example 167 168datatype act = A; 169fun transA(s,a,t) = (not(s)=t); 170fun hom(i) = i mod 2 = 0; 171fun nexts s A = [(s+1) mod 4]; 172check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]); 173 174fun nexts s A = [(s+1) mod 5]; 175 176*) 177 178end; 179