Using erlang2trs: some examples

Using the available tool, one can transform some provided examples as follows.

Example 1

Source Erlang code

main -> factorial({atom_s,{atom_s,{atom_s,atom_z}}}).

factorial(X) -> case X of
		  atom_z -> {atom_s,atom_z};
		  {atom_s,Y} -> mult(X,factorial(Y))
	        end.

mult(X,Y) -> case X of
		atom_z -> atom_z;
	        {atom_s,Z} -> sum(Y,mult(Z,Y))
	     end.

sum(X,Y) -> case X of
		atom_z -> Y;
		{atom_s,Z} -> W=sum(Z,Y), {atom_s,W}
	    end.

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | S | Z | T2 Exp Exp


reduce_global current visited = current


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

main = (factorial (T2 S (T2 S (T2 S Z))))
fun1 Z (x:[])  = (T2 S Z)
fun1 (T2 S y) (x:[])  = (mult x (factorial y))
factorial x  = (fun1 x (x:[]))
fun2 Z (x:(y:[]))  = Z
fun2 (T2 S z) (x:(y:[]))  = (sum y (mult z y))
mult x y  = (fun2 x (x:(y:[])))
fun3 Z (x:(y:[]))  = y
fun3 (T2 S z) (x:(y:[]))  = (fun4 (sum z y) (y:(z:[])))
fun4 w (y:(z:[]))  = (T2 S w)
sum x y  = (fun3 x (x:(y:[])))

Example 2

Source Erlang code

main -> Pid = spawn(foo),
        Pid ! atom_hello.

foo -> receive 
         atom_hello -> atom_yes;
         atom_world -> atom_no
       end.

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | Hello | Yes | No | World


reduce_global current visited
    | member current visited  = current
    | isFinal current         = current
    | otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
    | (isDef exp)  = False
    | otherwise    = isFinal xs

isDef x = case x of
               SPAWN _ _ _  -> True
               SEND _ _ _ _ -> True
               AREC _ _ _   -> True
               SELF _ _     -> True
               _            -> False

brec 3 fresh = case fresh of
             Hello -> True
             World -> True
             _ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i Hello m : ss)) visited = reduce_global (s0 : (ss ++ [State i Hello m])) visited
reduce (s0 : (State i Yes m : ss)) visited = reduce_global (s0 : (ss ++ [State i Yes m])) visited
reduce (s0 : (State i No m : ss)) visited = reduce_global (s0 : (ss ++ [State i No m])) visited
reduce (s0 : (State i World m : ss)) visited = reduce_global (s0 : (ss ++ [State i World m])) visited


reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
      if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
                    else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited


reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited


reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 2 e fresh  = e
spawn 1 pid []  = (SEND 2 pid Hello [])
main = (SPAWN 1 foo [])
rec 3 Hello []  = Yes
rec 3 World []  = No
foo = (AREC 3 [] [])

Example 3

Source Erlang code

main -> Ser = spawn(server),
        Cli = spawn(client(Ser)),
        Cli ! atom_start.

server -> receive 
             Pid -> atom_ok
	  end,
          server.

client(Ser) -> S = self,
               receive 
                     X -> Ser ! S
               end,
               client(Ser).

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | Start


reduce_global current visited
    | member current visited  = current
    | isFinal current         = current
    | otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
    | (isDef exp)  = False
    | otherwise    = isFinal xs

isDef x = case x of
               SPAWN _ _ _  -> True
               SEND _ _ _ _ -> True
               AREC _ _ _   -> True
               SELF _ _     -> True
               _            -> False

brec 4 fresh = case fresh of
             pid -> True
             _ -> False

brec 6 fresh = case fresh of
             x -> True
             _ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i Start m : ss)) visited = reduce_global (s0 : (ss ++ [State i Start m])) visited


reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
      if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
                    else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited


reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited


reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited


reduce (s0 : (State i (SELF n args) m : s)) visited = reduce_global (s0 : (s ++ [State i (self n (I i) args) m])) visited


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 3 e fresh  = e
send 7 e (s:(ser:[]))  = (client ser)
spawn 2 cli (ser:[])  = (SEND 3 cli Start [])
spawn 1 ser []  = (SPAWN 2 (client ser) (ser:[]))
main = (SPAWN 1 server [])
rec 4 pid []  = server
rec 6 x (s:(ser:[]))  = (SEND 7 ser s (s:(ser:[])))
server = (AREC 4 [] [])
self 5 s (ser:[])  = (AREC 6 [] (s:(ser:[])))
client ser  = (SELF 5 (ser:[]))

Example 4

Source Erlang code

main -> Pid2 = spawn(proc2),
        Pid1 = spawn(proc1(Pid2)),
        Pid1 ! atom_hello,
        Pid2 ! atom_world.

proc1(Pid) -> receive 
                  X -> Pid ! X
	      end.

proc2 -> receive 
            X -> atom_ok
         end.

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | World | Hello | Ok


reduce_global current visited
    | member current visited  = current
    | isFinal current         = current
    | otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
    | (isDef exp)  = False
    | otherwise    = isFinal xs

isDef x = case x of
               SPAWN _ _ _  -> True
               SEND _ _ _ _ -> True
               AREC _ _ _   -> True
               SELF _ _     -> True
               _            -> False

brec 5 fresh = case fresh of
             x -> True
             _ -> False

brec 7 fresh = case fresh of
             x -> True
             _ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i World m : ss)) visited = reduce_global (s0 : (ss ++ [State i World m])) visited
reduce (s0 : (State i Hello m : ss)) visited = reduce_global (s0 : (ss ++ [State i Hello m])) visited
reduce (s0 : (State i Ok m : ss)) visited = reduce_global (s0 : (ss ++ [State i Ok m])) visited


reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
      if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
                    else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited


reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited


reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 4 e fresh  = e
send 3 e (pid1:(pid2:[]))  = (SEND 4 pid2 World [])
send 6 e fresh  = e
spawn 2 pid1 (pid2:[])  = (SEND 3 pid1 Hello (pid1:(pid2:[])))
spawn 1 pid2 []  = (SPAWN 2 (proc1 pid2) (pid2:[]))
main = (SPAWN 1 proc2 [])
rec 5 x (pid:[])  = (SEND 6 pid x [])
rec 7 x []  = Ok
proc1 pid  = (AREC 5 [] (pid:[]))
proc2 = (AREC 7 [] [])

Example 5

Source Erlang code

main -> Pid = spawn(proc2),
        Pid ! atom_a.

proc2 -> Pid = spawn(proc3),
         receive
            X -> Pid ! X
         end.

proc3 -> receive
            X -> atom_ok
         end.

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | A | Ok


reduce_global current visited
    | member current visited  = current
    | isFinal current         = current
    | otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
    | (isDef exp)  = False
    | otherwise    = isFinal xs

isDef x = case x of
               SPAWN _ _ _  -> True
               SEND _ _ _ _ -> True
               AREC _ _ _   -> True
               SELF _ _     -> True
               _            -> False

brec 4 fresh = case fresh of
             x -> True
             _ -> False

brec 6 fresh = case fresh of
             x -> True
             _ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i A m : ss)) visited = reduce_global (s0 : (ss ++ [State i A m])) visited
reduce (s0 : (State i Ok m : ss)) visited = reduce_global (s0 : (ss ++ [State i Ok m])) visited


reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
      if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
                    else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited


reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited


reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

send 2 e fresh  = e
send 5 e fresh  = e
spawn 1 pid []  = (SEND 2 pid A [])
spawn 3 pid []  = (AREC 4 [] (pid:[]))
main = (SPAWN 1 proc2 [])
rec 4 x (pid:[])  = (SEND 5 pid x [])
rec 6 x []  = Ok
proc2 = (SPAWN 3 proc3 [])
proc3 = (AREC 6 [] [])

Example 6

Source Erlang code

main ->
    Res = spawn(res({atom_a,atom_a})),
    Left = spawn(left(Res)),
    Right = spawn(right(Res)).    

res(State) ->
    receive 
	{atom_c,S} -> S ! State
    end,
    receive 
	{atom_u,NewState} -> res(NewState)
    end.

left(Res) ->
    S = self, 
    Res ! {atom_c,S},
    receive {atom_a,B} ->
	    Res ! {atom_u,{atom_b,B}},
	    Res ! {atom_c,S},
	    left_aux(Res)
    end.

left_aux(Res) ->
    receive {atom_b,atom_a} ->
	    Res ! {atom_u,{atom_b,atom_b}}
    end.


right(Res) ->
    S = self,
    Res ! {atom_c,S},
    receive {A,atom_a} ->
	    Res ! {atom_u,{A,atom_b}},
	    Res ! {atom_c,S},
	    right_aux(Res)
    end.

right_aux(Res) ->
    receive {atom_a,atom_b} ->
	    Res ! {atom_u,{atom_b,atom_b}}
    end.

Transformed Curry program

data State = State Int Exp [Exp]
data Exp = I Int | SPAWN Int Exp [Exp] | SEND Int Exp Exp [Exp] | AREC Int [Exp] [Exp] | SELF Int [Exp]  | A | U | C | B | T2 Exp Exp


reduce_global current visited
    | member current visited  = current
    | isFinal current         = current
    | otherwise               = reduce current (current:visited)

isFinal [] = True
isFinal (State _ exp _:xs)
    | (isDef exp)  = False
    | otherwise    = isFinal xs

isDef x = case x of
               SPAWN _ _ _  -> True
               SEND _ _ _ _ -> True
               AREC _ _ _   -> True
               SELF _ _     -> True
               _            -> False

brec 4 fresh = case fresh of
             (T2 C s) -> True
             _ -> False

brec 6 fresh = case fresh of
             (T2 U newstate) -> True
             _ -> False

brec 9 fresh = case fresh of
             (T2 A b) -> True
             _ -> False

brec 12 fresh = case fresh of
             (T2 B A) -> True
             _ -> False

brec 16 fresh = case fresh of
             (T2 a A) -> True
             _ -> False

brec 19 fresh = case fresh of
             (T2 A B) -> True
             _ -> False

reduce (s0 : (State i (I fresh1) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (I fresh1) m])) visited
reduce (s0 : (State i (T2 fresh1 fresh2) m : ss)) visited = reduce_global (s0 : (ss ++ [State i (T2 fresh1 fresh2) m])) visited
reduce (s0 : (State i A m : ss)) visited = reduce_global (s0 : (ss ++ [State i A m])) visited
reduce (s0 : (State i U m : ss)) visited = reduce_global (s0 : (ss ++ [State i U m])) visited
reduce (s0 : (State i C m : ss)) visited = reduce_global (s0 : (ss ++ [State i C m])) visited
reduce (s0 : (State i B m : ss)) visited = reduce_global (s0 : (ss ++ [State i B m])) visited


reduce (s0 : (State i (AREC n ms2 args) (m:ms)) : s) visited =
      if (brec n m) then reduce_global (s0 : (s ++ [State i (rec n m args) (ms2++ms)])) visited
                    else reduce (s0 : (State i (AREC n (ms2++[m]) args) ms) : s) visited
reduce (s0 : (State i (AREC n ms2 args) []) : s) visited = reduce_global ((s0 : s) ++ [State i (AREC n ms2 args) []]) visited


reduce (State o (I k) l2 : (State i (SPAWN n e args) m : s)) visited = reduce_global ((State o (I (k+1)) l2 : s) ++ [State i (spawn n (I k) args) m, State k e []]) visited


reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (send_msg j e (s ++ [State i (send n e args) m]))) visited
reduce (s0 : (State i (SEND n (I j) e args) m : s)) visited = reduce_global (s0 : (s ++ [State i (SEND n (I j) e args) m])) visited


reduce (s0 : (State i (SELF n args) m : s)) visited = reduce_global (s0 : (s ++ [State i (self n (I i) args) m])) visited


send_msg _ _ [] = []
send_msg j e (State i b m : s)
        | i==j      = State i b (m++[e]) : s
        | otherwise = State i b m : (send_msg j e s)

member _ [] = False
member x (y:ys) = if x==y then True else member x ys


init = reduce_global [State 0 (I 2) [], State 1 main []] []

spawn 3 right fresh  = right
spawn 2 left (res:[])  = (SPAWN 3 (right res) [])
spawn 1 res []  = (SPAWN 2 (left res) (res:[]))
main = (SPAWN 1 (res (T2 A A)) [])
rec 6 (T2 U newstate) []  = (res newstate)
rec 4 (T2 C s) (state:[])  = (SEND 5 s state (s:(state:[])))
rec 9 (T2 A b) (res:(s:[]))  = (SEND 10 res (T2 U (T2 B b)) (b:(res:(s:[]))))
rec 12 (T2 B A) (res:[])  = (SEND 13 res (T2 U (T2 B B)) [])
rec 16 (T2 a A) (res:(s:[]))  = (SEND 17 res (T2 U (T2 a B)) (a:(res:(s:[]))))
rec 19 (T2 A B) (res:[])  = (SEND 20 res (T2 U (T2 B B)) [])
send 5 e (s:(state:[]))  = (AREC 6 [] [])
send 11 e (res:(s:[]))  = (left_aux res)
send 10 e (b:(res:(s:[])))  = (SEND 11 res (T2 C s) (res:(s:[])))
send 8 e (res:(s:[]))  = (AREC 9 [] (res:(s:[])))
send 13 e fresh  = e
send 18 e (res:(s:[]))  = (right_aux res)
send 17 e (a:(res:(s:[])))  = (SEND 18 res (T2 C s) (res:(s:[])))
send 15 e (res:(s:[]))  = (AREC 16 [] (res:(s:[])))
send 20 e fresh  = e
res state  = (AREC 4 [] (state:[]))
self 7 s (res:[])  = (SEND 8 res (T2 C s) (res:(s:[])))
self 14 s (res:[])  = (SEND 15 res (T2 C s) (res:(s:[])))
left res  = (SELF 7 (res:[]))
left_aux res  = (AREC 12 [] (res:[]))
right res  = (SELF 14 (res:[]))
right_aux res  = (AREC 19 [] (res:[]))