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