src/HOLCF/IOA/ABP/Check.ML
author wenzelm
Mon Sep 27 20:26:10 2010 +0200 (2010-09-27)
changeset 39733 6d373e9dcb9d
parent 36692 54b64d4ad524
permissions -rw-r--r--
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
     1 (*  Title:      HOLCF/IOA/ABP/Check.ML
     2     Author:     Olaf Mueller
     3 
     4 The Model Checker.
     5 *)
     6 
     7 structure Check =
     8 struct
     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 
    14 fun 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 
    47 datatype msg = m | n | l;
    48 datatype 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 
    54 fun 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 
    67 fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
    68 
    69 
    70 (* --------------------- Transition relation of Implementation ----------*)
    71 
    72 fun 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 
   103 val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
   104 val 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 
   114 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   115   let fun prec x = (Output.raw_stdout ","; pre x)
   116   in
   117     (case lll of
   118       [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
   119     | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
   120    end;
   121 
   122 fun pr_bool true = Output.raw_stdout "true"
   123 |   pr_bool false = Output.raw_stdout "false";
   124 
   125 fun pr_msg m = Output.raw_stdout "m"
   126 |   pr_msg n = Output.raw_stdout "n"
   127 |   pr_msg l = Output.raw_stdout "l";
   128 
   129 fun pr_act a = Output.raw_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 
   138 fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
   139 
   140 val pr_bool_list  = print_list("[","]",pr_bool);
   141 val pr_msg_list   = print_list("[","]",pr_msg);
   142 val pr_pkt_list   = print_list("[","]",pr_pkt);
   143 
   144 fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
   145         (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
   146          pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
   147          pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
   148          pr_bool_list ch2; Output.raw_stdout "}");
   149 
   150 
   151 
   152 (* ---------------------------------
   153          Main function call
   154    ---------------------------------*)
   155 
   156 (*
   157 check(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 
   168 datatype act = A;
   169 fun transA(s,a,t) = (not(s)=t);
   170 fun hom(i) = i mod 2 = 0;
   171 fun nexts s A = [(s+1) mod 4];
   172 check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
   173 
   174 fun nexts s A = [(s+1) mod 5];
   175 
   176 *)
   177 
   178 end;