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