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