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 2830 - (view) (download)

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

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