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