SEMANTICS OF EXCEPTIONS (complete)

Let G be a goal, and C be a variable.  Then G[C] is defined
recursively as follows:


     if  G = p(X1,...,Xn) but G is not a try
     then  G[C]  =  kill(C) \/ [~kill(C) x p(X1,...,Xn,C)]

     if  G = try(G1,E,A)
     then  G[C]  =  exists C1, new(C1) x G1[C1]
                       [ catch(E,C1) x A[C]  \/  rethrow(E,C1,C)  \/  ~kill(C1) ]

     if G = o(G1)
     then G[C]  =  ?????

     if G = G1 \/ G2
     then G[C]  =  G1[C] \/ G2[C]

     if G = G1 | G2
     then G[C]  =  G1[C] | G2[C]

     if G = G1 x G2
     then G[C]  =  G1[C] x G2[C]


A transaction base is transformed as follows:

(1)  Each rule, p<-G, is replaced by p[C] <- G[C],
     where C is a variable not appearing in the rule.


(2) The following rules are added to the transaction base:

     kill(C) <- event(E,C)

     throw(E,C) <- ins:excep(E,C)

     rethrow(E2,C2,C1) <- o[excep(E1,C2) x not(E1=E2) x del:excep(E1,C2) x ins:excep(E1,C1)]

     catch(E,C) <- o[excep(E,C) x del:excep(E,C)]


(3) For each n-ary base predicate, the following rule is added to the
    transaction base:

	p(X1,...,Xn,C) <- p(X1,...,Xn).

    where X1,...Xn,C are n+1 distinct variables.


(4) The transition oracle contains an update new(C) that creates a new constant symbol, C.





Given a goal, replace every sub-expression, Phi, by

       ~suspend(C) x [kill(C) \/ ~kill(C) x Phi(C)]





                SEMANTICS OF INTERUPTS (complete)

Let G be a goal, and C be a variable.  Then G[C] is defined
recursively as follows:


     if  G = p(X1,...,Xn) but G is not a try
     then  G[C]  =  ~suspend(C) x p(X1,...,Xn,C)

     if  G = try(G1,E,A)
     then  G[C]  =  exists C1, new(C1) x (G1[C1] x ins:end(C1) |  monitor.A(E,C1,C))

     where monitor.A is defined by the following recursive rules:

     monitor.A(E1,C1,C2) <- end(C1) x del:end(C1)

     monitor.A(E1,C1,C2) <- interupt(E,C1) x handle.A(E,E1,C1,C2) x del:interupt(E,C1)
                          x monitor.A(E1,C1,C2)

     handle.A(E,E,C1,C2) <- A[C2]

     handle.A(E,E1,C1,C2) <- not(E=E1) x ins:interupt(E,C2) x ~interupt(E,C2)


     if G = o(G1)
     then G[C]  =  ?????

     if G = G1 \/ G2
     then G[C]  =  G1[C] \/ G2[C]

     if G = G1 | G2
     then G[C]  =  G1[C] | G2[C]

     if G = G1 x G2
     then G[C]  =  G1[C] x G2[C]


A transaction base is transformed as follows:

(1)  Each rule, p<-G, is replaced by p[C] <- G[C],
     where C is a variable not appearing in the rule.


(2) The following rules are added to the transaction base:

     suspend(C) <- interupt(E,C)

     throw(E,C) <- ins:interupt(E,C)

     rethrow(E2,C2,C1) <- o[interupt(E1,C2) x not(E1=E2) x del:interupt(E1,C2) x ins:interupt(E1,C1)]


(3) For each n-ary base predicate, the following rule is added to the
    transaction base:

	p(X1,...,Xn,C) <- p(X1,...,Xn).

    where X1,...Xn,C are n+1 distinct variables.


(4) The transition oracle contains an update new(C) that creates a new constant symbol, C.










                 SEMANTICS OF GENERAL EVENTS (incomplete)


If G is a goal of the form try(G1,E,A), then replace G by the goal
monitor(G1,exception(E),A'), where A' is a new predicate defined by
the following rule:

     A' <- kill x A


Let G be a goal, and C be a variable.  Then G[C] is defined
recursively as follows:


     if  G = p(X1,...,Xn) but G is not a try
     then  G[C]  =  ~suspended(C) x [killed(C)  \/  ~killed(C) x p(X1,...,Xn,C)]


     if  G = monitor(G1,E,A)
     then  G[C]  =  exists C1, new(C1) x (G1[C1] x ins:end(C1) |  monitor.A(E,C1,C))

     where monitor.A is a new predicate defined by the following recursive rules:

     monitor.A(E1,C1,C2) <- end(C1) x del:end(C1)

     monitor.A(E1,C1,C2) <- event(E,C1) x handle.A(E,E1,C1,C2) x del:event(E,C1)
                          x monitor.A(E1,C1,C2)

     handle.A(E,E,C1,C2) <- A[C2]

     handle.A(E,E1,C1,C2) <- not(E=E1) x ins:event(E,C2) x ~event(E,C2)


     if G = o(G1)
     then G[C]  =  ?????

     if G = G1 \/ G2
     then G[C]  =  G1[C] \/ G2[C]

     if G = G1 | G2
     then G[C]  =  G1[C] | G2[C]

     if G = G1 x G2
     then G[C]  =  G1[C] x G2[C]


A transaction base is transformed as follows:


(1)  Each rule, p<-G, is replaced by p[C] <- G[C],
     where C is a variable not appearing in the rule.


(2) The following rules are added to the transaction base:

     kill(C) <- ins:killed(C)

     suspended(C) <- event(E,C)

     throw(E,C) <- ins:event(E,C)

     rethrow(E2,C2,C1) <- o[event(E1,C2) x not(E1=E2) x del:event(E1,C2) x ins:event(E1,C1)]

     catch(E,C) <- o[event(E,C) x del:event(E,C)]


(3) For each n-ary base predicate, the following rule is added to the
    transaction base:

	p(X1,...,Xn,C) <- p(X1,...,Xn).

    where X1,...Xn,C are n+1 distinct variables.


(4) The transition oracle contains an update new(C) that creates a new constant symbol, C.





Given a goal, replace every sub-expression, Phi, by

       ~suspend(C) x [kill(C) \/ ~kill(C) x Phi(C)]