PSF - Process Specification Formalism

Simanim

Description

Specification

data module Atoms
begin
    exports
    begin
	sorts
	    ATOM
	functions
	    f : -> ATOM
	    g : -> ATOM
	    h : -> ATOM
    end
end Atoms

data module Tool-Types
begin
    exports
    begin
	sorts
	    Tterm
    end
end Tool-Types

data module Tool-ID
begin
    exports
    begin
	functions
	    sim : -> Tterm
	    anim : -> Tterm
    end
    imports
	Tool-Types
end Tool-ID

data module Tool-Messages
begin
    exports
    begin
	functions
	    control-info : -> Tterm
	    control : Tterm # BOOLEAN -> Tterm
	    control : Tterm -> Tterm

	    send-message : -> Tterm

	    reset : -> Tterm
	    quit : -> Tterm
	    controltoanim : -> Tterm
	    controltosim : -> Tterm
	    choose : Tterm -> Tterm
	    choice : Tterm -> Tterm
	    end-of-spec : -> Tterm

	    givecontrol : -> Tterm
	    takecontrol : -> Tterm

	    ack : -> Tterm
	    error : -> Tterm
    end
    imports
	Booleans,
	Tool-Types
end Tool-Messages

data module Tool-data
begin
    exports
    begin
	functions
	    atom : ATOM -> Tterm
	    control-tool : Tterm -> Tterm
	    control-keep : Tterm -> BOOLEAN
	    _|_ : Tterm # Tterm -> Tterm
	    term-atom : Tterm -> BOOLEAN
	    term-list : Tterm -> BOOLEAN
	    left : Tterm -> Tterm
	    right : Tterm -> Tterm
    end
    imports
	Atoms,
	Tool-ID,
	Tool-Messages
    variables
	x : -> Tterm
	y : -> BOOLEAN
	l : -> Tterm
	e : -> Tterm
    equations
    [1] control-tool(control(x, y)) = x
    [2] control-keep(control(x, y)) = y
    [3] term-atom(e) = true when
	    not(term-list(e)) = true
    [4] term-list(l | e) = true
    [5] not(term-list(l)) = true
    [6] left(l | e) = l
    [7] right(l | e) = e
end Tool-data

data module ToolBus-Types
begin
    exports
    begin
	sorts
	    TBterm,
	    TBid
    end
end ToolBus-Types

data module ToolBus-ID
begin
    exports
    begin
	functions
	    SIM : -> TBid
	    ANIM : -> TBid
	    psim : -> TBterm
	    panim : -> TBterm
    end
    imports
	ToolBus-Types
end ToolBus-ID

data module Tool-ToolBus-data
begin
    exports
    begin
	functions
	    tb-term : Tterm -> TBterm
	    conv : Tterm -> TBterm
	    conv : TBterm -> Tterm

	    tool : TBterm -> TBterm
	    get-choice : TBterm -> Tterm

	    is-choose : TBterm -> BOOLEAN
	    is-choice : TBterm -> BOOLEAN
	    is-control : TBterm -> BOOLEAN
	    is-atom : TBterm -> BOOLEAN
    end
    imports
	Tool-data,
	ToolBus-Types
    variables
	t : -> Tterm
	n : -> BOOLEAN
	a : -> ATOM
    equations
    [1] conv(t) = tb-term(t)
    [2] conv(tb-term(t)) = t
    [3] tool(tb-term(control(t, n))) = conv(t)
    [4] tool(tb-term(control(t))) = conv(t)
    [5] get-choice(tb-term(choice(t))) = t

    [6] is-choose(tb-term(choose(t))) = true
    [7] is-choice(tb-term(choice(t))) = true
    [8] is-control(tb-term(control(t, n))) = true
    [9] is-control(tb-term(control(t))) = true
    [10] is-atom(tb-term(atom(a))) = true
end Tool-ToolBus-data

process module Simulator
begin
    exports
    begin
	atoms
	    sim-snd : Tterm
	    sim-rec : Tterm
	processes
	    Simulator
    end
    imports
	Tool-data
    atoms
	sim : Tterm
    processes
	Run : Tterm # BOOLEAN
    sets
	of ATOM
	    A = { f, g, h }
	of Tterm
	    Control-set = { control(c, k) | c in Tterm, k in BOOLEAN }
	of Tterm
	    ATOM-set = { atom(a) | a in ATOM }
    variables
	control : -> Tterm
	keep-control : -> BOOLEAN
    definitions
	Simulator = sum(c in Control-set,
			sim-rec(c) . sim(c) .
			Run(control-tool(c), control-keep(c))
		    )
	Run(control, keep-control) =
		    [ control = sim ] -> (
			sim-rec(send-message) . (
			    (
				sum(a in A, sim(atom(a)) . sim-snd(atom(a)))
			    +   sim(reset) . sim-snd(reset)
			    +   sim(quit) . sim-snd(quit)
			    ) . sim-rec(ack) . sim(ack) .
			    Run(control, keep-control)
			+   [ keep-control = false ] -> (
				sim(controltoanim) . sim-snd(givecontrol) .
				Run(anim, keep-control)
			    )
			)
		    )
		+   [ control = anim ] -> (
			sim-rec(send-message) . (
			    sim-snd(choose(atom(f) | atom(g) | atom(h)))
			+   sim-snd(end-of-spec) . sim-rec(ack) . sim(ack)
			) . (
			    (
				sum(a in ATOM-set, sim-rec(a) . sim(a))
			    +   sim-rec(reset) . sim(reset)
			    +   sim-rec(quit) . sim(quit) . sim-snd(quit)
			    ) . Run(control, keep-control)
			+   sim-rec(takecontrol) . sim(takecontrol) .
			    Run(sim, keep-control)
			)
		    )
end Simulator

process module ToolBus-primitives
begin
    exports
    begin
	atoms
	    tb-snd-msg : TBterm # TBterm
	    tb-rec-msg : TBterm # TBterm
	    tb-comm-msg : TBterm # TBterm

	    tb-snd-eval : TBid # TBterm
	    tb-rec-value : TBid # TBterm
	    tb-snd-do : TBid # TBterm

	    tb-shutdown
    end
    imports
	ToolBus-Types
    communications
	tb-snd-msg(t,m) | tb-rec-msg(t, m) = tb-comm-msg(t, m)
	    for t in TBterm, m in TBterm
end ToolBus-primitives

process module Sim-Interface
begin
    exports
    begin
	atoms
	    simtb-snd : TBterm
	    simtb-rec : TBterm
	processes
	    SimInt
    end
    imports
	Simulator, Tool-ToolBus-data
    atoms
	simint-rec : Tterm
	simint-snd : Tterm
	simint-comm : Tterm
	intsim-comm : Tterm
    processes
	Interface
    sets
	of atoms
	    H = { sim-snd(x), sim-rec(x), simint-rec(x), simint-snd(x)
		    | x in Tterm }
	of Tterm
	    ATOM-set = { atom(a) | a in ATOM }
	of Tterm
	    CHOOSE = { choose(l) | l in Tterm }
    communications
	sim-snd(x) | simint-rec(x) = simint-comm(x) for x in Tterm
	sim-rec(x) | simint-snd(x) = intsim-comm(x) for x in Tterm
    definitions
	Interface =
		    sum(t in TBterm, simtb-rec(t) .
			(
			    [ is-control(t) = true ] -> simint-snd(conv(t))
			+   [ conv(t) = send-message ] -> simint-snd(send-message)
			+   [ is-choice(t) = true ] -> simint-snd(get-choice(t))
			+   [ conv(t) = reset ] -> simint-snd(reset)
			+   [ conv(t) = quit ] -> simint-snd(quit)
			+   [ conv(t) = takecontrol ] -> simint-snd(takecontrol)
			)
		    ) . Interface
		+   sum(a in ATOM-set, simint-rec(a) .
			simtb-snd(conv(a)) . simtb-rec(conv(ack))
		    ) . simint-snd(ack) . Interface
		+   simint-rec(reset) . simtb-snd(conv(reset)) .
		    simtb-rec(conv(ack)) .  simint-snd(ack) . Interface
		+   simint-rec(quit) . simtb-snd(conv(quit))
		+   simint-rec(end-of-spec) . simtb-snd(conv(end-of-spec)) .
		    simtb-rec(conv(ack)) .  simint-snd(ack) . Interface
		+   simint-rec(givecontrol) . simtb-snd(conv(control(anim))) .
		    Interface
		+   sum(c in CHOOSE, simint-rec(c) . simtb-snd(conv(c))) .
		    Interface
	SimInt = encaps(H, Interface || Simulator)
end Sim-Interface

process module Process-Sim
begin
    exports
    begin
	atoms
	    simtb-comm-snd : TBterm
	    simtb-comm-rec : TBterm
	processes
	    Process-Sim
    end
    imports
	ToolBus-primitives,
	ToolBus-ID,
	Sim-Interface
    processes
	TB-Sim : TBterm
    sets
	of atoms
	    H = { tb-snd-eval(tid, t), tb-rec-value(tid, t), tb-snd-do(tid, t),
		    simtb-snd(t), simtb-rec(t) | tid in TBid, t in TBterm }
    communications
	simtb-snd(t) | tb-rec-value(tid, t) = simtb-comm-snd(t)
	    for t in TBterm, tid in TBid
	simtb-rec(t) | tb-snd-eval(tid, t) = simtb-comm-rec(t)
	    for t in TBterm, tid in TBid
	simtb-rec(t) | tb-snd-do(tid, t) = simtb-comm-rec(t)
	    for t in TBterm, tid in TBid
    variables
	t : -> TBterm
    definitions
	Process-Sim =
		encaps(H,
		    SimInt
		||  sum(m in TBterm,
			tb-rec-msg(psim, m) . tb-snd-do(SIM, m) .
			TB-Sim(tool(m))
		    )
		)
	TB-Sim(t) =  (
		[ t = conv(anim) ] -> (
		    tb-snd-eval(SIM, conv(send-message)) .
		    sum(v in TBterm,
			tb-rec-value(SIM, v) . (
			    [ is-choose(v) = true ] -> tb-snd-msg(panim, v)
			+   [ v = conv(end-of-spec) ] -> (
				tb-snd-msg(panim, v) .
				tb-snd-do(SIM, conv(ack))
			    )
			)
		    ) .
		    sum(v in TBterm,
			tb-rec-msg(psim, v) . (
			    [ is-choice(v) = true ] -> tb-snd-do(SIM, v)
			+   [ v = conv(reset) ] -> tb-snd-do(SIM, v)
			+   [ v = conv(quit) ] -> (
				tb-snd-eval(SIM, v) .
				tb-rec-value(SIM, v) .
				tb-shutdown
			    )
			+   [ is-control(v) = true ] -> (
				tb-snd-do(SIM, conv(takecontrol)) .
				TB-Sim(tool(v))
			    )
			)
		    )
		)
	    +   [ t = conv(sim) ] -> (
		    tb-snd-eval(SIM, conv(send-message)) .
		    sum(v in TBterm,
			tb-rec-value(SIM, v) . (
			    (
				[ is-atom(v) = true ] -> tb-snd-msg(panim, v)
			    +   [ v = conv(reset) ] -> tb-snd-msg(panim, v)
			    +   [ v = conv(quit) ] -> tb-shutdown
			    ) .
			    tb-snd-do(SIM, conv(ack))
			+   [ is-control(v) = true ] -> (
				tb-snd-msg(panim, v) .
				TB-Sim(tool(v))
			    )
			)
		    )
		)
	    ) . TB-Sim(t)
end Process-Sim

process module Animation
begin
    exports
    begin
	atoms
	    anim-rec : Tterm
	    anim-snd : Tterm
	processes
	    Animation
    end
    imports
	Tool-data
    atoms
	anim : Tterm
    processes
	Choose : Tterm
	AddChoose : Tterm
	Run : Tterm # BOOLEAN
    sets
	of Tterm
	    ATOM-set = { atom(a) | a in ATOM }
	of Tterm
	    CHOOSE = { choose(l) | l in Tterm }
	of Tterm
	    TOOL = { sim, anim }
	of BOOLEAN
	    CONTROL-INFO = { false, true }
    variables
	l : -> Tterm
	b : -> Tterm
	a : -> ATOM
	control : -> Tterm
	keep-control : -> BOOLEAN
    definitions
	Animation = anim-rec(control-info) .
		    sum(t in TOOL, sum(ci in CONTROL-INFO,
			anim-snd(control(t, ci)) .
			Run(t, ci)
		    ) )
	Run(control, keep-control) =
		    (
			sum(a in ATOM-set, anim-rec(a) . anim(a))
		    +   anim-rec(reset) . anim(reset)
		    +   anim-rec(end-of-spec) . anim(end-of-spec) . (
			    anim(reset) . anim-snd(reset) .
			    Run(control, keep-control)
			+   anim(quit) . anim-snd(quit)
			)
		    +   sum(c in CHOOSE, anim-rec(c) . (
				Choose(c) . Run(control, keep-control)
			    +   anim(reset) . anim-snd(reset) .
				Run(control, keep-control)
			    +   anim(quit) . anim-snd(quit)
			    +   [ keep-control = false ] -> (
				    anim(controltosim) . anim-snd(givecontrol) .
				    Run(sim, keep-control)
				)
			    )
			)
		    ) . (
			anim-snd(ack)
		    +   anim-snd(error)
		    ) . Run(control, keep-control)
		+   anim-rec(takecontrol) . anim(takecontrol) .
		    Run(anim, keep-control)
	Choose(l) =
		    [term-atom(l) = true] -> AddChoose(l)
		+   [term-list(l) = true] -> (
			AddChoose(right(l))
		    +   Choose(left(l))
		    )
	AddChoose(l) = anim(l) . anim-snd(choice(l))
end Animation

process module Anim-Interface
begin
    exports
    begin
	atoms
	    animtb-snd : TBterm
	    animtb-rec : TBterm
	processes
	    AnimInt
    end
    imports
	Animation, Tool-ToolBus-data
    atoms
	animint-rec : Tterm
	animint-snd : Tterm
	animint-comm : Tterm
	intanim-comm : Tterm
    processes
	Interface
    sets
	of atoms
	    H = { anim-snd(x), anim-rec(x), animint-rec(x), animint-snd(x)
		    | x in Tterm }
    communications
	anim-snd(x) | animint-rec(x) = animint-comm(x) for x in Tterm
	anim-rec(x) | animint-snd(x) = intanim-comm(x) for x in Tterm
    definitions
	Interface =
		sum(t in TBterm,
		    animtb-rec(t) . (
			[ conv(t) = control-info ] -> (
			    animint-snd(control-info) .
			    sum(c in Tterm, animint-rec(c) .
				animtb-snd(conv(c)) . Interface
			    )
			)
		    +   [ is-atom(t) = true ] -> animint-snd(conv(t))
		    +   [ conv(t) = reset ] -> animint-snd(reset)
		    +   [ conv(t) = end-of-spec ] -> (
			    animint-snd(end-of-spec) .
			    sum(c in Tterm, animint-rec(c) . (
				    [ is-choice(conv(c)) = true ] -> animtb-snd(conv(c))
				+   [ c = reset ] -> animtb-snd(conv(c))
				+   [ c = quit ] -> animtb-snd(conv(c))
				)
			    ) . Interface
			)
		    +   [ conv(t) = takecontrol ] -> (
			    animint-snd(takecontrol) . Interface
			)
		    +   [ is-choose(t) = true ] -> (
			    animint-snd(conv(t)) .
			    sum(c in Tterm, animint-rec(c) . (
				    [ is-choice(conv(c)) = true ] -> animtb-snd(conv(c))
				+   [ c = reset ] -> animtb-snd(conv(c))
				+   [ c = quit ] -> animtb-snd(conv(c))
				+   [ c = givecontrol ] -> animtb-snd(conv(control(sim)))
				)
			    ) . Interface
			)
		    +   [ is-choice(t) = true ] -> animint-snd(get-choice(t))
		    )
		) . (
		    animint-rec(ack) . animtb-snd(conv(ack))
		+   animint-rec(error) . animtb-snd(conv(error))
		) . Interface
	AnimInt = encaps(H, Animation || Interface)
end Anim-Interface

process module Process-Anim
begin
    exports
    begin
	atoms
	    animtb-comm-snd : TBterm
	    animtb-comm-rec : TBterm
	processes
	    Process-Anim
    end
    imports
	ToolBus-primitives,
	ToolBus-ID,
	Anim-Interface
    processes
	TB-Anim : TBterm
    sets
	of atoms
	    H = { tb-snd-eval(tid, t), tb-rec-value(tid, t), tb-snd-do(tid, t),
		    animtb-snd(t), animtb-rec(t) | tid in TBid, t in TBterm }
    communications
	animtb-snd(t) | tb-rec-value(tid, t) = animtb-comm-snd(t)
	    for t in TBterm, tid in TBid
	animtb-rec(t) | tb-snd-eval(tid, t) = animtb-comm-rec(t)
	    for t in TBterm, tid in TBid
	animtb-rec(t) | tb-snd-do(tid, t) = animtb-comm-rec(t)
	    for t in TBterm, tid in TBid
    variables
	t : -> TBterm
    definitions
	Process-Anim =
		encaps(H,
		    AnimInt
		||  tb-snd-eval(ANIM, conv(control-info)) .
		    sum(v in TBterm,
			tb-rec-value(ANIM, v) . (
			    [ is-control(v) = true ] -> (
				tb-snd-msg(psim, v) .
				TB-Anim(tool(v))
			    )
			+   [ v = conv(error) ] -> tb-shutdown
			)
		    )
		)
	TB-Anim(t) = (
		[ t = conv(anim) ] -> (
		    sum(v in TBterm,
			tb-rec-msg(panim, v) .
			tb-snd-eval(ANIM, v)  -- choose(..) or end-of-spec
		    ) .
		    sum(v in TBterm,
			tb-rec-value(ANIM, v) . (
			    [ is-choice(v) = true ] -> (
				tb-snd-msg(psim, v) .
				tb-snd-eval(ANIM, v) .
				(
				    tb-rec-value(ANIM, conv(ack))
				+   tb-rec-value(ANIM, conv(error)) .
				    tb-shutdown
				)
			    )
			+   [ v = conv(reset) ] -> tb-snd-msg(psim, v)
			+   [ v = conv(quit) ] -> tb-snd-msg(psim, v)
			+   [ is-control(v) = true ] -> (
				tb-snd-msg(psim, v) .
				TB-Anim(tool(v))
			    )
			)
		    )
		)
	    +   [ t = conv(sim) ] -> (
		    sum(v in TBterm,
			tb-rec-msg(panim, v) . (
			    (
				[ is-atom(v) = true ] -> tb-snd-eval(ANIM, v)
			    +   [ v = conv(reset) ] -> tb-snd-eval(ANIM, v)
			    ) . (
				tb-rec-value(ANIM, conv(ack))
			    +   tb-rec-value(ANIM, conv(error)) .
				tb-shutdown
			    )
			+   [ is-control(v) = true ] -> (
				tb-snd-do(ANIM, conv(takecontrol)) .
				TB-Anim(tool(v))
			    )
			)
		    )
		)
	    ) . TB-Anim(t)
end Process-Anim

process module ToolBus-SimAnim
begin
    imports
	ToolBus-primitives,
	Process-Sim,
	Process-Anim
    atoms
	application-shutdown
	tbc-shutdown
	tbc-app-shutdown
	TB-Shutdown
	TB-App-Shutdown
    processes
	ToolBus-SimAnim
	ToolBus-Control
	Application
	Shutdown
    sets
	of atoms
	    H = { tb-snd-msg(t, m), tb-rec-msg(t, m), tbc-shutdown,
		    tbc-app-shutdown, tb-shutdown, application-shutdown
		    | t in TBterm, m in TBterm}
	    P = { TB-Shutdown, TB-App-Shutdown }
    communications
	tb-shutdown | tbc-shutdown = TB-Shutdown
	tbc-app-shutdown | application-shutdown = TB-App-Shutdown
    definitions
	ToolBus-SimAnim =
		    encaps(H, prio(P > atoms, ToolBus-Control || Application))
	ToolBus-Control = tbc-shutdown . tbc-app-shutdown
	Application =
		    disrupt(Process-Sim || Process-Anim, Shutdown)
	Shutdown = application-shutdown
end ToolBus-SimAnim

Compilation

Assuming the specification resides in file simanim, it should be compiled with the command:
% psf -s simanim

Simulation

Compilation gives the file ToolBus-SimAnim.til, which can be simulated with the command:
% sim ToolBus-SimAnim.til
Choose ToolBus-SimAnim as start process.

Animation

With the tool simanim we can combine the simulation with animation. For the animation we use:
Anim::Windows 440 220 -text 45 10

Anim::CreateItem TSIM rect 120 45 44 15 "Process-Sim"
Anim::CreateItem TANIM rect 320 45 44 15 "Process-Anim"
Anim::CreateItem ISIM rect 120 115 44 15 "Interface"
Anim::CreateItem IANIM rect 320 115 44 15 "Interface"
Anim::CreateItem SIM rect 120 185 44 15 "SIM"
Anim::CreateItem ANIM rect 320 185 44 15 "ANIM"

Anim::CreateLine TB \
    pos [expr [Anim::Dim TSIM w,x] - 10] [expr [Anim::Dim TSIM n,y] - 25] \
    pos [expr [Anim::Dim TANIM e,x] + 10] [expr [Anim::Dim TANIM n,y] - 25] \
    pos [expr [Anim::Dim TANIM e,x] + 10] [expr [Anim::Dim TANIM s,y] + 10] \
    pos [expr [Anim::Dim TSIM w,x] - 10] [expr [Anim::Dim TSIM s,y] + 10] \
    pos [expr [Anim::Dim TSIM w,x] - 10] [expr [Anim::Dim TSIM n,y] - 25] \
    -width 1
Anim::Textpos TBH 220 10 n -noreset
Anim::CreateText TBH "ToolBus"

Anim::CreateLine TSIMtoISIM pos [expr [Anim::Dim TSIM x] - 8] \
    [Anim::Dim TSIM s,y] pos [expr [Anim::Dim ISIM x] - 8] [Anim::Dim ISIM n,y] \
    -arrow last
Anim::CreateLine ISIMtoTSIM pos [expr [Anim::Dim ISIM x] + 8] \
    [Anim::Dim ISIM n,y] pos [expr [Anim::Dim TSIM x] + 8] [Anim::Dim TSIM s,y] \
    -arrow last
Anim::CreateLine ISIMtoSIM pos [expr [Anim::Dim ISIM x] - 8] \
    [Anim::Dim ISIM s,y] pos [expr [Anim::Dim SIM x] - 8] [Anim::Dim SIM n,y] \
    -arrow last
Anim::CreateLine SIMtoISIM pos [expr [Anim::Dim SIM x] + 8] \
    [Anim::Dim SIM n,y] pos [expr [Anim::Dim ISIM x] + 8] [Anim::Dim ISIM s,y] \
    -arrow last

Anim::CreateLine TANIMtoIANIM pos [expr [Anim::Dim TANIM x] - 8] \
    [Anim::Dim TANIM s,y] pos [expr [Anim::Dim IANIM x] - 8] \
    [Anim::Dim IANIM n,y] -arrow last
Anim::CreateLine IANIMtoTANIM pos [expr [Anim::Dim IANIM x] + 8] \
    [Anim::Dim IANIM n,y] pos [expr [Anim::Dim TANIM x] + 8] \
    [Anim::Dim TANIM s,y] -arrow last
Anim::CreateLine IANIMtoANIM pos [expr [Anim::Dim IANIM x] - 8] \
    [Anim::Dim IANIM s,y] pos [expr [Anim::Dim ANIM x] - 8] [Anim::Dim ANIM n,y] \
    -arrow last
Anim::CreateLine ANIMtoIANIM pos [expr [Anim::Dim ANIM x] + 8] \
    [Anim::Dim ANIM n,y] pos [expr [Anim::Dim IANIM x] + 8] [Anim::Dim IANIM s,y] \
    -arrow last

Anim::CreateLine TSIMtoTANIM pos [Anim::Dim TSIM e,x] \
    [expr [Anim::Dim TSIM y] + 8] pos [Anim::Dim TANIM w,x] \
    [expr [Anim::Dim TANIM y] + 8] -arrow last
Anim::CreateLine TANIMtoTSIM pos [Anim::Dim TANIM w,x] \
    [expr [Anim::Dim TANIM y] - 8] pos [Anim::Dim TSIM e,x] \
    [expr [Anim::Dim TSIM y] - 8] -arrow last

Anim::TextposItem SIM SIM s n
Anim::TextposItem ANIM ANIM s n

Anim::TextposLine TSIM-ISIM TSIMtoISIM e
Anim::TextposLine ISIM-TSIM ISIMtoTSIM w
Anim::TextposLine ISIM-SIM ISIMtoSIM e
Anim::TextposLine SIM-ISIM SIMtoISIM w

Anim::TextposLine TANIM-IANIM TANIMtoIANIM e
Anim::TextposLine IANIM-TANIM IANIMtoTANIM w
Anim::TextposLine IANIM-ANIM IANIMtoANIM e
Anim::TextposLine ANIM-IANIM ANIMtoIANIM w

Anim::TextposLine TSIM-TANIM TSIMtoTANIM n
Anim::TextposLine TANIM-TSIM TANIMtoTSIM s

proc ANIM_action {atom} {
    if {[regexp {^sim\(control\((.*)\)\)$} $atom match arg1]} {
	Anim::DeleteText ISIM-SIM
	Anim::DeactivateLine ISIMtoSIM
    } elseif {[regexp {^sim\(ack\)$} $atom match]} {
	Anim::DeleteText ISIM-SIM
	Anim::DeactivateLine ISIMtoSIM
    } elseif {[regexp {^sim\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText SIM
	Anim::DeleteText ISIM-SIM
	Anim::CreateText SIM "$arg1"
    } elseif {[regexp {^simint-comm\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText ISIM-SIM
	Anim::DeactivateLine ISIMtoSIM
	Anim::DeleteText SIM
	Anim::CreateText SIM-ISIM "$arg1"
	Anim::ActivateLine SIMtoISIM
    } elseif {[regexp {^intsim-comm\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText TSIM-ISIM
	Anim::DeactivateLine TSIMtoISIM
	Anim::CreateText ISIM-SIM "$arg1"
	Anim::ActivateLine ISIMtoSIM
    } elseif {[regexp {^simtb-comm-snd\(tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::DeleteText SIM-ISIM
	Anim::DeactivateLine SIMtoISIM
	Anim::CreateText ISIM-TSIM "$arg1"
	Anim::ActivateLine ISIMtoTSIM
    } elseif {[regexp {^simtb-comm-rec\(tb-term\((.*)\)\)$} $atom match arg1]} {
	if {! [regexp {^ack$} $arg1 match]} {
	    Anim::DeleteText TANIM-TSIM
	    Anim::DeactivateLine TANIMtoTSIM
	}
	Anim::CreateText TSIM-ISIM "$arg1"
	Anim::ActivateLine TSIMtoISIM
    } elseif {[regexp {^tb-comm-msg\(panim, tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::DeleteText ISIM-TSIM
	Anim::DeactivateLine ISIMtoTSIM
	Anim::CreateText TSIM-TANIM "$arg1"
	Anim::ActivateLine TSIMtoTANIM
    } elseif {[regexp {^tb-comm-msg\(psim, tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::DeleteText IANIM-TANIM
	Anim::DeactivateLine IANIMtoTANIM
	Anim::CreateText TANIM-TSIM "$arg1"
	Anim::ActivateLine TANIMtoTSIM
    } elseif {[regexp {^animtb-comm-rec\(tb-term\((.*)\)\)$} $atom match arg1]} {
	# clean ack from animint
	Anim::DeleteText IANIM-TANIM
	Anim::DeactivateLine IANIMtoTANIM
	Anim::DeleteText TSIM-TANIM
	Anim::DeactivateLine TSIMtoTANIM
	Anim::CreateText TANIM-IANIM "$arg1"
	Anim::ActivateLine TANIMtoIANIM
    } elseif {[regexp {^animtb-comm-snd\(tb-term\((.*)\)\)$} $atom match arg1]} {
	if {[regexp {^control\(.*\)$} $arg1 match]} {
	    Anim::DeleteText TANIM-IANIM
	    Anim::DeactivateLine TANIMtoIANIM
	} else {
	    Anim::DeleteText ANIM-IANIM
	    Anim::DeactivateLine ANIMtoIANIM
	}
	Anim::DeleteText ANIM-IANIM
	Anim::DeactivateLine ANIMtoIANIM
	Anim::CreateText IANIM-TANIM "$arg1"
	Anim::ActivateLine IANIMtoTANIM
    } elseif {[regexp {^intanim-comm\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText TANIM-IANIM
	Anim::DeactivateLine TANIMtoIANIM
	Anim::CreateText IANIM-ANIM "$arg1"
	Anim::ActivateLine IANIMtoANIM
    } elseif {[regexp {^animint-comm\((.*)\)$} $atom match arg1]} {
	# clean after a reset
	Anim::DeleteText IANIM-ANIM
	Anim::DeactivateLine IANIMtoANIM

	Anim::DeleteText ANIM
	Anim::CreateText ANIM-IANIM "$arg1"
	Anim::ActivateLine ANIMtoIANIM
    } elseif {[regexp {^anim\((.*)\)$} $atom match arg1]} {
	Anim::DeleteText IANIM-ANIM
	Anim::DeactivateLine IANIMtoANIM
	Anim::DeleteText ANIM
	Anim::CreateText ANIM "$arg1"
    } elseif {[regexp {^TB-Shutdown$} $atom match]} {
	Anim::DeleteText ISIM-TSIM
	Anim::DeactivateLine ISIMtoTSIM
	Anim::DeleteText IANIM-TANIM
	Anim::DeactivateLine IANIMtoTANIM
    }
}

proc ANIM_choose {atom} {
    if {[regexp {^sim\((.*)\)$} $atom match arg1]} {
	Anim::AddList SIM $match
    } elseif {[regexp {^simint-comm\((.*)\)$} $atom match arg1]} {
	Anim::AddList SIM $match
    } elseif {[regexp {^intsim-comm\((.*)\)$} $atom match arg1]} {
	Anim::AddList ISIM $match
    } elseif {[regexp {^simtb-comm-snd\(tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList ISIM $match
    } elseif {[regexp {^simtb-comm-rec\(tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList TSIM $match
    } elseif {[regexp {^tb-comm-msg\(panim, tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList TSIM $match
    } elseif {[regexp {^tb-comm-msg\(psim, tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList TANIM $match
    } elseif {[regexp {^animtb-comm-rec\(tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList TANIM $match
    } elseif {[regexp {^animtb-comm-snd\(tb-term\((.*)\)\)$} $atom match arg1]} {
	Anim::AddList IANIM $match
    } elseif {[regexp {^intanim-comm\((.*)\)$} $atom match arg1]} {
	Anim::AddList IANIM $match
    } elseif {[regexp {^animint-comm\((.*)\)$} $atom match arg1]} {
	Anim::AddList ANIM $match
    } elseif {[regexp {^anim\((.*)\)$} $atom match arg1]} {
	Anim::AddList ANIM $match
    } elseif {[regexp {^TB-Shutdown|TB-App-Shutdown$} $atom match]} {
	Anim::AddList TSIM $match
    }
}
Assuming the animation resides in file simanim.tcl we can start the animation with the command:
% simanim ToolBus-SimAnim.til simanim.tcl