src/HOLCF/IOA/ABP/Check.ML
changeset 3072 a31419014be5
child 5963 94709c11601e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed Apr 30 11:24:14 1997 +0200
     1.3 @@ -0,0 +1,176 @@
     1.4 +(*  Title:      HOLCF/IOA/ABP/Check.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1994  TU Muenchen
     1.8 +
     1.9 +The Model Checker
    1.10 +*)
    1.11 +
    1.12 + 
    1.13 +(* ----------------------------------------------------------------
    1.14 +       P r o t o t y p e   M o d e l   C h e c k e r 
    1.15 +   ----------------------------------------------------------------*)
    1.16 +
    1.17 +fun check(extacts,intacts,string_of_a,startsI,string_of_s,
    1.18 +          nexts,hom,transA,startsS) =
    1.19 +  let fun check_s(s,unchecked,checked) =
    1.20 +        let fun check_sa(unchecked,a) =
    1.21 +              let fun check_sas(unchecked,t) =
    1.22 +                    (if a mem extacts then
    1.23 +                          (if transA(hom s,a,hom t) then ( )
    1.24 +                           else (writeln("Error: Mapping of Externals!");
    1.25 +                                 string_of_s s; writeln"";
    1.26 +                                 string_of_a a; writeln"";
    1.27 +                                 string_of_s t;writeln"";writeln"" ))
    1.28 +                     else (if hom(s)=hom(t) then ( )
    1.29 +                           else (writeln("Error: Mapping of Internals!");
    1.30 +                                 string_of_s s; writeln"";
    1.31 +                                 string_of_a a; writeln"";
    1.32 +                                 string_of_s t;writeln"";writeln"" ));
    1.33 +                     if t mem checked then unchecked else t ins unchecked)
    1.34 +              in foldl check_sas (unchecked,nexts s a) end;
    1.35 +              val unchecked' = foldl check_sa (unchecked,extacts @ intacts)
    1.36 +        in    (if s mem startsI then 
    1.37 +                    (if hom(s) mem startsS then ()
    1.38 +                     else writeln("Error: At start states!"))
    1.39 +               else ();  
    1.40 +               checks(unchecked',s::checked)) end
    1.41 +      and checks([],_) = ()
    1.42 +        | checks(s::unchecked,checked) = check_s(s,unchecked,checked)
    1.43 +  in checks(startsI,[]) end;
    1.44 +
    1.45 +
    1.46 +(* ------------------------------------------------------
    1.47 +                 A B P     E x a m p l e
    1.48 +   -------------------------------------------------------*)
    1.49 +
    1.50 +datatype msg = m | n | l;
    1.51 +datatype act = Next | S_msg of msg | R_msg of msg
    1.52 +                    | S_pkt of bool * msg | R_pkt of bool * msg
    1.53 +                    | S_ack of bool | R_ack of bool;
    1.54 +
    1.55 +(* -------------------- Transition relation of Specification -----------*)
    1.56 +
    1.57 +fun transA((u,s),a,(v,t)) = 
    1.58 +    (case a of 
    1.59 +       Next       => v andalso t = s |                         
    1.60 +       S_msg(q)   => u andalso not(v) andalso t = s@[q]   |    
    1.61 +       R_msg(q)   => u = v andalso s = (q::t)  |                    
    1.62 +       S_pkt(b,q) => false |                    
    1.63 +       R_pkt(b,q) => false |                    
    1.64 +       S_ack(b)   => false |                      
    1.65 +       R_ack(b)   => false);
    1.66 +
    1.67 +
    1.68 +(* ---------------------- Abstraction function --------------------------*)
    1.69 +
    1.70 +fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
    1.71 +
    1.72 +
    1.73 +(* --------------------- Transition relation of Implementation ----------*)
    1.74 +
    1.75 +fun nexts (s as (env,p,a,q,b,ch1,ch2)) action =
    1.76 +    (case action of
    1.77 +       Next       => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] |                         
    1.78 +       S_msg(mornorl)   => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] |     
    1.79 +       R_msg(mornorl)   => if (q<>[] andalso mornorl=hd(q)) 
    1.80 +                        then [(env,p,a,tl(q),b,ch1,ch2)]
    1.81 +                        else [] |                    
    1.82 +       S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a)
    1.83 +                        then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl))
    1.84 +                              then [s]
    1.85 +                              else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)])
    1.86 +                        else [] |
    1.87 +       R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl))
    1.88 +                         then (if (h<>b andalso q=[])
    1.89 +                               then [(env,p,a,q@[mornorl],not(b),ch1,ch2),
    1.90 +                                     (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)]
    1.91 +                               else [s,(env,p,a,q,b,tl(ch1),ch2)])
    1.92 +                          else [] | 
    1.93 +       S_ack(h)   => if (h=b)
    1.94 +                        then (if (ch2<>[] andalso h=hd(rev(ch2))) 
    1.95 +                              then [s]
    1.96 +                              else [s,(env,p,a,q,b,ch1,ch2@[h])])
    1.97 +                        else []  |                      
    1.98 +       R_ack(h)   => if (ch2<>[] andalso hd(ch2)=h)
    1.99 +                        then (if h=a
   1.100 +                              then [(env,tl(p),not(a),q,b,ch1,ch2),
   1.101 +                                    (env,tl(p),not(a),q,b,ch1,tl(ch2))]
   1.102 +                              else [s,(env,p,a,q,b,ch1,tl(ch2))]) 
   1.103 +                         else [])
   1.104 +
   1.105 +
   1.106 +val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
   1.107 +val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true),
   1.108 +                  S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false),
   1.109 +                  S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l),
   1.110 +               S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)];
   1.111 +
   1.112 +
   1.113 +(* ------------------------------------
   1.114 +           Input / Output utilities 
   1.115 +   ------------------------------------*)
   1.116 +
   1.117 +fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   1.118 +  let fun prec x = (prs ","; pre x)
   1.119 +  in
   1.120 +    (case lll of
   1.121 +      [] => (prs lpar; prs rpar)
   1.122 +    | x::lll => (prs lpar; pre x; seq prec lll; prs rpar))
   1.123 +   end;
   1.124 +
   1.125 +fun pr_bool true = output(std_out,"true")
   1.126 +|   pr_bool false = output(std_out,"false");
   1.127 +
   1.128 +fun pr_msg m = output(std_out,"m")
   1.129 +|   pr_msg n = output(std_out,"n")
   1.130 +|   pr_msg l = output(std_out,"l");
   1.131 +
   1.132 +fun pr_act a = output(std_out, case a of
   1.133 +      Next => "Next"|                         
   1.134 +      S_msg(ma) => "S_msg(ma)"  |
   1.135 +      R_msg(ma) => "R_msg(ma)"  |
   1.136 +      S_pkt(b,ma) => "S_pkt(b,ma)" |                    
   1.137 +      R_pkt(b,ma) => "R_pkt(b,ma)" |                    
   1.138 +      S_ack(b)   => "S_ack(b)" |                      
   1.139 +      R_ack(b)   => "R_ack(b)");
   1.140 +
   1.141 +fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">");
   1.142 +
   1.143 +val pr_bool_list  = print_list("[","]",pr_bool);
   1.144 +val pr_msg_list   = print_list("[","]",pr_msg);
   1.145 +val pr_pkt_list   = print_list("[","]",pr_pkt);
   1.146 +
   1.147 +fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
   1.148 +        (prs "{"; pr_bool env; prs ", "; pr_msg_list p;  prs ", ";
   1.149 +         pr_bool a;  prs ", "; pr_msg_list q; prs ", ";
   1.150 +         pr_bool b;  prs ", "; pr_pkt_list ch1;  prs ", ";
   1.151 +         pr_bool_list ch2; prs "}");
   1.152 +
   1.153 +
   1.154 +
   1.155 +(* ---------------------------------
   1.156 +         Main function call
   1.157 +   ---------------------------------*)
   1.158 +
   1.159 +(*
   1.160 +check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])], 
   1.161 +      pr_tuple, nexts, hom, transA, [(true,[])]);
   1.162 +*)
   1.163 +
   1.164 +
   1.165 +
   1.166 +
   1.167 +
   1.168 +(*
   1.169 +           Little test example
   1.170 +
   1.171 +datatype act = A;
   1.172 +fun transA(s,a,t) = (not(s)=t);
   1.173 +fun hom(i) = i mod 2 = 0;
   1.174 +fun nexts s A = [(s+1) mod 4];
   1.175 +check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
   1.176 +
   1.177 +fun nexts s A = [(s+1) mod 5];
   1.178 +
   1.179 +*)