(* Auxiliary functions for printing *)

fun  msg2str (Name n) = implode[chr n]
   | msg2str (Rigid n) = implode[chr n]
   | msg2str (Mpair(M,N)) = "<" ^ (msg2str M) ^ "," ^ (msg2str N) ^ ">"
   | msg2str (Enc(M,N)) = "Enc(" ^ (msg2str M) ^ "," ^ (msg2str N) ^")";

fun mmp2str (In(M,N)) = "(" ^ (msg2str M) ^ " , " ^ (msg2str N) ^ ")^i"
  | mmp2str (Out(M,N)) = "(" ^ (msg2str M) ^ " , " ^ (msg2str N) ^ ")^o";

fun mpair2str (M,N) = "(" ^ (msg2str M) ^ " , " ^ (msg2str N) ^ ")";


fun print_cc {bitrace = bt, theory = th} =
   (print "Bitrace = \n" ; print "[ " ;
    map (fn M => print ((mmp2str M) ^ "; ")) bt; print "]\n";
    print "Theory = \n";
    print "{ ";
    map (fn M => print ((mpair2str M) ^ ", ")) th; print "}\n");
    
    
(* Example 1: inconsistent *)

val a = Rigid (ord #"a");
val b = Rigid (ord #"b");
val x = Name (ord #"x");
val k = Rigid (ord #"k");

val bt = rev [Out(a,a), Out(b,b), In(x,x), Out(Enc(x,k), Enc(a,k)), Out(Enc(b,k), Enc(x,k))];
val bt1 = tl bt;
val prob = {bitrace = bt1, theory = reduce (oth_of bt)};
val prob2 = hd (R1reds prob);
val probs = R3reds prob2;
map print_cc probs ;

(* Example 2: consistent*)

val a = Rigid (ord #"a");
val x = Name (ord #"x");
val k = Rigid (ord #"k");
val m = Rigid (ord #"m");
val l = Rigid (ord #"l");
val n = Rigid (ord #"n");

val bt = rev [Out(a,a), In (x,x), Out(Enc(x, k), Enc (x, l)), Out(Enc(m, Enc(a,k)), Enc(n, Enc(a,l)))];
val bt1 = tail bt;
val prob = {bitrace = bt1, theory = reduce (oth_of bt)};

-----------

Output for example 1:

Bitrace = 
[ (Enc(x,k) , Enc(a,k))^o; (x , x)^i; (b , b)^o; (a , a)^o; ]
Theory = 
{ (a , a), (b , b), (Enc(x,k) , Enc(a,k)), (Enc(b,k) , Enc(x,k)), }

--
Bitrace = 
[ (Enc(b,k) , Enc(a,k))^o; (b , b)^i; (b , b)^o; (a , a)^o; ]
Theory = 
{ (Enc(b,k) , Enc(b,k)), (Enc(b,k) , Enc(a,k)), (b , b), (a , a), }

Bitrace = 
[ (Enc(b,k) , Enc(a,k))^o; (b , b)^i; (b , b)^o; (a , a)^o; ]
Theory = 
{ (Enc(b,k) , Enc(b,k)), (Enc(b,k) , Enc(a,k)), (b , b), (a , a), }

Bitrace = 
[ (Enc(a,k) , Enc(a,k))^o; (a , a)^i; (b , b)^o; (a , a)^o; ]
Theory = 
{ (Enc(b,k) , Enc(a,k)), (Enc(a,k) , Enc(a,k)), (b , b), (a , a), }

Bitrace = 
[ (Enc(a,k) , Enc(a,k))^o; (a , a)^i; (b , b)^o; (a , a)^o; ]
Theory = 
{ (Enc(b,k) , Enc(a,k)), (Enc(a,k) , Enc(a,k)), (b , b), (a , a), }