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