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