blob: f96b28b5b3d95222a1cf2217d5b71f821beaa5cc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
#|$ACL2s-Preamble$;
(begin-book);$ACL2s-Preamble$|#
(in-package "ACL2")
(include-book "make-event/defspec" :dir :system)#|ACL2s-ToDo-Line|#
(include-book "types")
;;
;; Router
;;
(defspec GenericFlowControl
(((flowControl * *) => (mv * *)))
(local (defun FlowControl (node memory)
;; This is the function that performs the flowcontrol in a router. This consists of scheduling the routed input nodes and switching the sheduled msg.
(mv node memory))))
|
