Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /smlnj-lib/trunk/Reactive/machine.sml
ViewVC logotype

Annotation of /smlnj-lib/trunk/Reactive/machine.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2 - (view) (download)
Original Path: sml/trunk/src/smlnj-lib/Reactive/machine.sml

1 : monnier 2 (* machine.sml
2 :     *
3 :     * COPYRIGHT (c) 1997 Bell Labs, Lucent Technologies.
4 :     *
5 :     * This is an implementation of the reactive interpreter instructions,
6 :     * and functions to generate them.
7 :     *)
8 :    
9 :     structure Machine : sig
10 :    
11 :     (* activation return codes *)
12 :     datatype state
13 :     = TERM (* execution of the instruction is complete; activation
14 :     * at future instances has no effect.
15 :     *)
16 :     | STOP (* execution is stopped in this instant, but could
17 :     * progress in the next instant.
18 :     *)
19 :     | SUSP (* exeuction is suspended and must be resumed during this
20 :     * instant.
21 :     *)
22 :    
23 :     type in_signal
24 :     type out_signal
25 :    
26 :     type instant = int
27 :     type signal_state = instant ref
28 :    
29 :     datatype signal = SIG of {
30 :     name : Atom.atom,
31 :     id : int,
32 :     state : signal_state
33 :     }
34 :    
35 :     datatype machine = M of {
36 :     now : instant ref,
37 :     moveFlg : bool ref,
38 :     endOfInstant : bool ref,
39 :     prog : code,
40 :     signals : signal list,
41 :     inputs : signal list,
42 :     outputs : signal list
43 :     }
44 :    
45 :     and code = C of {
46 :     isTerm : unit -> bool,
47 :     terminate : unit -> unit,
48 :     reset : unit -> unit,
49 :     preempt : machine -> unit,
50 :     activation : machine -> state
51 :     }
52 :    
53 :     val runMachine : machine -> bool
54 :     val resetMachine : machine -> unit
55 :     val inputsOf : machine -> in_signal list
56 :     val outputsOf : machine -> out_signal list
57 :    
58 :     val inputSignal : in_signal -> Atom.atom
59 :     val outputSignal : out_signal -> Atom.atom
60 :     val setInSignal : (in_signal * bool) -> unit
61 :     val getInSignal : in_signal -> bool
62 :     val getOutSignal : out_signal -> bool
63 :    
64 :     type config
65 :    
66 :     val || : (code * code) -> code
67 :     val & : (code * code) -> code
68 :     val nothing : code
69 :     val stop : unit -> code
70 :     val suspend : unit -> code
71 :     val action : (machine -> unit) -> code
72 :     val exec : {
73 :     start : machine -> unit,
74 :     stop : machine -> unit,
75 :     done : machine -> bool
76 :     } -> code
77 :     val ifThenElse : ((machine -> bool) * code * code) -> code
78 :     val repeat : (int * code) -> code
79 :     val loop : code -> code
80 :     val close : code -> code
81 :     val emit : signal -> code
82 :     val await : config -> code
83 :     val when : (config * code * code) -> code
84 :     val trapWith : (config * code * code) -> code
85 :    
86 :     end = struct
87 :    
88 :     structure I = Instruction (* for the config type *)
89 :    
90 :     datatype state
91 :     = TERM
92 :     | STOP
93 :     | SUSP
94 :    
95 :     type instant = int
96 :     type signal_state = instant ref
97 :    
98 :     datatype signal = SIG of {
99 :     name : Atom.atom,
100 :     id : int,
101 :     state : signal_state
102 :     }
103 :    
104 :     type config = signal I.config
105 :    
106 :     datatype machine = M of {
107 :     now : instant ref,
108 :     moveFlg : bool ref,
109 :     endOfInstant : bool ref,
110 :     prog : code,
111 :     signals : signal list,
112 :     inputs : signal list,
113 :     outputs : signal list
114 :     }
115 :    
116 :     and code = C of {
117 :     isTerm : unit -> bool,
118 :     terminate : unit -> unit,
119 :     reset : unit -> unit,
120 :     preempt : machine -> unit,
121 :     activation : machine -> state
122 :     }
123 :    
124 :    
125 :     fun now (M{now=t, ...}) = !t
126 :     fun newMove (M{moveFlg, ...}) = moveFlg := true
127 :     fun isEndOfInstant (M{endOfInstant, ...}) = !endOfInstant
128 :    
129 :     datatype presence = PRESENT | ABSENT | UNKNOWN
130 :    
131 :     fun presence (m, SIG{state, ...}) = let
132 :     val ts = !state
133 :     val now = now m
134 :     in
135 :     if (now = ts) then PRESENT
136 :     else if ((now = ~ts) orelse (isEndOfInstant m)) then ABSENT
137 :     else UNKNOWN
138 :     end
139 :    
140 :     fun present (m, SIG{state, ...}) = (now m = !state)
141 :     fun absent (m, SIG{state, ...}) = (now m = ~(!state))
142 :     fun emitSig (m, SIG{state, ...}) = state := now m
143 :     fun emitNot (m, SIG{state, ...}) = state := ~(now m)
144 :    
145 :     datatype in_signal = IN of (machine * signal)
146 :     datatype out_signal = OUT of (machine * signal)
147 :    
148 :     fun inputSignal (IN(_, SIG{name, ...})) = name
149 :     fun outputSignal (OUT(_, SIG{name, ...})) = name
150 :     fun setInSignal (IN(m, s), false) = emitNot(m, s)
151 :     | setInSignal (IN(m, s), true) = emitSig(m, s)
152 :     fun getInSignal (IN(m, s)) = present(m, s)
153 :     fun getOutSignal (OUT(m, s)) = present(m, s)
154 :    
155 :     fun terminate (C{terminate=f, ...}) = f()
156 :     fun isTerm (C{isTerm=f, ...}) = f()
157 :     fun reset (C{reset=f, ...}) = f()
158 :     fun preemption (C{preempt=f, ...}, m) = f m
159 :     fun activation (C{activation=f, ...}, m) = f m
160 :    
161 :     fun activate (i, m) = if (isTerm i)
162 :     then TERM
163 :     else (case activation(i, m)
164 :     of TERM => (terminate i; TERM)
165 :     | res => res
166 :     (* end case *))
167 :    
168 :     fun preempt (i, m) = if (isTerm i)
169 :     then ()
170 :     else (preemption(i, m); terminate i)
171 :    
172 :     (* default instruction methods *)
173 :     fun isTermMeth termFlg () = !termFlg
174 :     fun terminateMeth termFlg () = termFlg := true
175 :     fun resetMeth termFlg () = termFlg := false
176 :    
177 :     fun || (i1, i2) = let
178 :     val termFlg = ref false
179 :     val leftSts = ref SUSP
180 :     val rightSts = ref SUSP
181 :     fun resetMeth () = (
182 :     termFlg := false; leftSts := SUSP; rightSts := SUSP;
183 :     reset i1; reset i2)
184 :     fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
185 :     fun activationMeth m = (
186 :     if (!leftSts = SUSP) then leftSts := activate(i1, m) else ();
187 :     if (!rightSts = SUSP) then rightSts := activate(i2, m) else ();
188 :     case (!leftSts, !rightSts)
189 :     of (TERM, TERM) => TERM
190 :     | (SUSP, _) => SUSP
191 :     | (_, SUSP) => SUSP
192 :     | _ => (leftSts := SUSP; rightSts := SUSP; STOP)
193 :     (* end case *))
194 :     in
195 :     C{ isTerm = isTermMeth termFlg,
196 :     terminate = terminateMeth termFlg,
197 :     reset = resetMeth,
198 :     preempt = preemptMeth,
199 :     activation = activationMeth
200 :     }
201 :     end
202 :    
203 :     fun & (i1, i2) = let
204 :     val termFlg = ref false
205 :     fun resetMeth () = (termFlg := false; reset i1; reset i2)
206 :     fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
207 :     fun activationMeth m =
208 :     if (isTerm i1)
209 :     then activate(i2, m)
210 :     else (case activate(i1, m)
211 :     of TERM => activate(i2, m)
212 :     | res => res
213 :     (* end case *))
214 :     in
215 :     C{ isTerm = isTermMeth termFlg,
216 :     terminate = terminateMeth termFlg,
217 :     reset = resetMeth,
218 :     preempt = preemptMeth,
219 :     activation = activationMeth
220 :     }
221 :     end
222 :    
223 :     val nothing = C{
224 :     isTerm = fn () => true,
225 :     terminate = fn () => (),
226 :     reset = fn () => (),
227 :     preempt = fn _ => (),
228 :     activation = fn _ => TERM
229 :     }
230 :    
231 :     fun stop () = let
232 :     val termFlg = ref false
233 :     in
234 :     C{ isTerm = isTermMeth termFlg,
235 :     terminate = terminateMeth termFlg,
236 :     reset = resetMeth termFlg,
237 :     preempt = fn _ => (),
238 :     activation = fn _ => STOP
239 :     }
240 :     end
241 :    
242 :     fun suspend () = let
243 :     val termFlg = ref false
244 :     in
245 :     C{ isTerm = isTermMeth termFlg,
246 :     terminate = terminateMeth termFlg,
247 :     reset = resetMeth termFlg,
248 :     preempt = fn _ => (),
249 :     activation = fn _ => (termFlg := true; STOP)
250 :     }
251 :     end
252 :    
253 :     fun action f = let
254 :     val termFlg = ref false
255 :     in
256 :     C{ isTerm = isTermMeth termFlg,
257 :     terminate = terminateMeth termFlg,
258 :     reset = resetMeth termFlg,
259 :     preempt = fn _ => (),
260 :     activation = fn m => (f m; TERM)
261 :     }
262 :     end
263 :    
264 :     fun exec {start, stop, done} = let
265 :     val termFlg = ref false
266 :     val running = ref false
267 :     (** NOTE: what if a reset occurs while we are running? We would need to change
268 :     ** the type of resetMeth to take a machine parameter.
269 :     **)
270 :     fun resetMeth () = (termFlg := false)
271 :     fun preemptMeth m = if !running then (running := false; stop m) else ()
272 :     fun activationMeth m = if !running
273 :     then if done m
274 :     then (running := false; TERM)
275 :     else STOP
276 :     else (running := true; start m; SUSP)
277 :     in
278 :     C{ isTerm = isTermMeth termFlg,
279 :     terminate = terminateMeth termFlg,
280 :     reset = resetMeth,
281 :     preempt = preemptMeth,
282 :     activation = activationMeth
283 :     }
284 :     end
285 :    
286 :     fun ifThenElse (pred, i1, i2) = let
287 :     val termFlg = ref false
288 :     val cond = ref NONE
289 :     fun resetMeth () = (
290 :     termFlg := false;
291 :     case !cond
292 :     of (SOME true) => reset i1
293 :     | (SOME false) => reset i2
294 :     | NONE => ()
295 :     (* end case *);
296 :     cond := NONE)
297 :     fun preemptMeth m = (case !cond
298 :     of (SOME true) => preempt(i1, m)
299 :     | (SOME false) => preempt(i2, m)
300 :     | NONE => ()
301 :     (* end case *))
302 :     fun activationMeth m = (case !cond
303 :     of (SOME true) => activate(i1, m)
304 :     | (SOME false) => activate(i2, m)
305 :     | NONE => let
306 :     val b = pred m
307 :     in
308 :     cond := SOME b;
309 :     if b then activate(i1, m) else activate(i2, m)
310 :     end
311 :     (* end case *))
312 :     in
313 :     C{ isTerm = isTermMeth termFlg,
314 :     terminate = terminateMeth termFlg,
315 :     reset = resetMeth,
316 :     preempt = preemptMeth,
317 :     activation = activationMeth
318 :     }
319 :     end
320 :    
321 :     fun repeat (n, i) = let
322 :     val termFlg = ref false
323 :     val counter = ref n
324 :     fun resetMeth () = (termFlg := false; counter := n)
325 :     fun preemptMeth m = preempt(i, m)
326 :     fun activationMeth m =
327 :     if (!counter > 0)
328 :     then (case activate(i, m)
329 :     of TERM => (counter := !counter-1; reset i; TERM)
330 :     | res => res
331 :     (* end case *))
332 :     else TERM
333 :     in
334 :     C{ isTerm = isTermMeth termFlg,
335 :     terminate = terminateMeth termFlg,
336 :     reset = resetMeth,
337 :     preempt = preemptMeth,
338 :     activation = activationMeth
339 :     }
340 :     end
341 :    
342 :     fun loop i = let
343 :     val termFlg = ref false
344 :     val endReached = ref false
345 :     fun resetMeth () = (termFlg := false; endReached := false)
346 :     fun preemptMeth m = preempt (i, m)
347 :     fun activationMeth m = (case activate(i, m)
348 :     of TERM => if (!endReached)
349 :     then (
350 :     (* say(m, "instantaneous loop detected\n"); *)
351 :     STOP)
352 :     else (endReached := true; reset i; TERM)
353 :     | STOP => (endReached := false; STOP)
354 :     | SUSP => SUSP
355 :     (* end case *))
356 :     in
357 :     C{ isTerm = isTermMeth termFlg,
358 :     terminate = terminateMeth termFlg,
359 :     reset = resetMeth,
360 :     preempt = preemptMeth,
361 :     activation = activationMeth
362 :     }
363 :     end
364 :    
365 :     fun close i = let
366 :     val termFlg = ref false
367 :     fun activationMeth m = (case activate(i, m)
368 :     of SUSP => activationMeth m
369 :     | res => res
370 :     (* end case *))
371 :     in
372 :     C{ isTerm = isTermMeth termFlg,
373 :     terminate = terminateMeth termFlg,
374 :     reset = resetMeth termFlg,
375 :     preempt = fn _ => (),
376 :     activation = activationMeth
377 :     }
378 :     end
379 :    
380 :     (** Configuration evaluation **)
381 :     fun fixed (m, c) = let
382 :     fun fix (I.posConfig id) = (presence(m, id) <> UNKNOWN)
383 :     | fix (I.negConfig id) = (presence(m, id) <> UNKNOWN)
384 :     | fix (I.orConfig(c1, c2)) = let
385 :     val b1 = fix c1 and b2 = fix c2
386 :     in
387 :     (b1 andalso evaluate(m, c1)) orelse
388 :     (b2 andalso evaluate(m, c2)) orelse
389 :     (b1 andalso b2)
390 :     end
391 :     | fix (I.andConfig(c1, c2)) = let
392 :     val b1 = fix c1 and b2 = fix c2
393 :     in
394 :     (b1 andalso not(evaluate(m, c1))) orelse
395 :     (b2 andalso not(evaluate(m, c2))) orelse
396 :     (b1 andalso b2)
397 :     end
398 :     in
399 :     fix c
400 :     end
401 :    
402 :     and evaluate (m, c) = let
403 :     fun eval (I.posConfig id) = present(m, id)
404 :     | eval (I.negConfig id) = not(present(m, id))
405 :     | eval (I.orConfig(c1, c2)) = eval c1 orelse eval c2
406 :     | eval (I.andConfig(c1, c2)) = eval c1 andalso eval c2
407 :     in
408 :     eval c
409 :     end
410 :    
411 :     fun fixedEval (m, c) = let
412 :     fun f (I.posConfig id) = (case presence(m, id)
413 :     of UNKNOWN => NONE
414 :     | PRESENT => SOME true
415 :     | ABSENT => SOME false
416 :     (* end case *))
417 :     | f (I.negConfig id) = (case presence(m, id)
418 :     of UNKNOWN => NONE
419 :     | PRESENT => SOME false
420 :     | ABSENT => SOME true
421 :     (* end case *))
422 :     | f (I.andConfig(c1, c2)) = (case (f c1, f c2)
423 :     of (SOME false, _) => SOME false
424 :     | (_, SOME false) => SOME false
425 :     | (SOME true, SOME true) => SOME true
426 :     | _ => NONE
427 :     (* end case *))
428 :     | f (I.orConfig(c1, c2)) = (case (f c1, f c2)
429 :     of (SOME true, _) => SOME true
430 :     | (_, SOME true) => SOME true
431 :     | (SOME false, SOME false) => SOME false
432 :     | _ => NONE
433 :     (* end case *))
434 :     in
435 :     f c
436 :     end
437 :    
438 :     fun emit signal = let
439 :     val termFlg = ref false
440 :     fun activationMeth m = (
441 :     newMove m;
442 :     emitSig(m, signal);
443 :     TERM)
444 :     in
445 :     C{ isTerm = isTermMeth termFlg,
446 :     terminate = terminateMeth termFlg,
447 :     reset = resetMeth termFlg,
448 :     preempt = fn _ => (),
449 :     activation = activationMeth
450 :     }
451 :     end
452 :    
453 :     fun await c = let
454 :     val termFlg = ref false
455 :     fun activationMeth m = (case fixedEval(m, c)
456 :     of NONE => SUSP
457 :     | (SOME true) => STOP
458 :     | (SOME false) => (
459 :     termFlg := true;
460 :     if (isEndOfInstant m) then STOP else TERM)
461 :     (* end case *))
462 :     in
463 :     C{ isTerm = isTermMeth termFlg,
464 :     terminate = terminateMeth termFlg,
465 :     reset = resetMeth termFlg,
466 :     preempt = fn _ => (),
467 :     activation = activationMeth
468 :     }
469 :     end
470 :    
471 :     fun when (c, i1, i2) = let
472 :     val termFlg = ref false
473 :     val value = ref NONE
474 :     fun resetMeth m = (
475 :     termFlg := false;
476 :     reset i1; reset i2;
477 :     value := NONE)
478 :     fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
479 :     fun activationMeth m = (case !value
480 :     of NONE => (case fixedEval(m, c)
481 :     of NONE => SUSP
482 :     | (SOME v) => (
483 :     value := SOME v;
484 :     if (isEndOfInstant m)
485 :     then STOP
486 :     else if v
487 :     then activate(i1, m)
488 :     else activate(i2, m))
489 :     (* end case *))
490 :     | (SOME true) => activate(i1, m)
491 :     | (SOME false) => activate(i2, m)
492 :     (* end case *))
493 :     in
494 :     C{ isTerm = isTermMeth termFlg,
495 :     terminate = terminateMeth termFlg,
496 :     reset = resetMeth,
497 :     preempt = preemptMeth,
498 :     activation = activationMeth
499 :     }
500 :     end
501 :    
502 :     fun trapWith (c, i1, i2) = let
503 :     val termFlg = ref false
504 :     val activeHandle = ref false
505 :     val resumeBody = ref true
506 :     fun resetMeth m = (
507 :     termFlg := false;
508 :     reset i1; reset i2;
509 :     activeHandle := false;
510 :     resumeBody := true)
511 :     fun preemptMeth m = if (! activeHandle)
512 :     then preempt(i2, m)
513 :     else preempt(i1, m)
514 :     fun activationMeth m =
515 :     if (! activeHandle)
516 :     then activate(i2, m)
517 :     else let
518 :     fun chkConfig () = (case fixedEval(m, c)
519 :     of NONE => SUSP
520 :     | (SOME true) => ( (* actual preemption *)
521 :     preempt(i1, m);
522 :     activeHandle := true;
523 :     if (isEndOfInstant m)
524 :     then STOP
525 :     else activate(i2, m))
526 :     | (SOME false) => (
527 :     resumeBody := true;
528 :     STOP)
529 :     (* end case *))
530 :     in
531 :     if (! resumeBody)
532 :     then (case activate(i1, m)
533 :     of STOP => (resumeBody := false; chkConfig())
534 :     | res => res
535 :     (* end case *))
536 :     else chkConfig()
537 :     end
538 :     in
539 :     C{ isTerm = isTermMeth termFlg,
540 :     terminate = terminateMeth termFlg,
541 :     reset = resetMeth,
542 :     preempt = preemptMeth,
543 :     activation = activationMeth
544 :     }
545 :     end
546 :    
547 :     (* run a machine to a stable state; return true if that is a terminal state *)
548 :     fun runMachine (m as M{now, moveFlg, endOfInstant, prog, ...}) = let
549 :     fun untilStop () = (case activate(prog, m)
550 :     of SUSP => (
551 :     if !moveFlg
552 :     then moveFlg := false
553 :     else endOfInstant := true;
554 :     untilStop ())
555 :     | STOP => false
556 :     | TERM => true
557 :     (* end case *))
558 :     in
559 :     endOfInstant := false;
560 :     moveFlg := false;
561 :     untilStop () before now := !now+1
562 :     end
563 :    
564 :     (* reset a machine back to its initial state *)
565 :     fun resetMachine (M{
566 :     now, moveFlg, endOfInstant, prog, signals, inputs, outputs
567 :     }) = let
568 :     fun resetSig (SIG{state, ...}) = state := 0
569 :     in
570 :     now := 1;
571 :     moveFlg := false;
572 :     endOfInstant := false;
573 :     reset prog;
574 :     List.app resetSig signals;
575 :     List.app resetSig inputs;
576 :     List.app resetSig outputs
577 :     end
578 :    
579 :     fun inputsOf (m as M{inputs, ...}) = List.map (fn s => IN(m, s)) inputs
580 :     fun outputsOf (m as M{inputs, ...}) = List.map (fn s => OUT(m, s)) inputs
581 :    
582 :     end;

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0