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(cont