blob: fbdf67153f523c4768f2c651e4456b70b1363c09 (
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
26
27
28
|
#|$ACL2s-Preamble$;
(begin-book);$ACL2s-Preamble$|#
(in-package "ACL2")
(include-book "../../../generic-modules/router")
(include-book "../../datalink/simple/datalink")
(include-book "../../routecontrol/xy/routecontrol")
(include-book "../../flowcontrol/wormhole/flowcontrol")
(defun XY-wormhole-router (node memory)
;; This function represents the router component of a Node.
;; Applies the different processes in a router in the correct order. The RouterControl and FlowControl get as arguments the memory.
;;
;; Arguments:
;; - node : list of ports in a node
;; - memory : the global memory of a node
(mv-let (node memory)
(xy-RouteControl (simple-ProcessInputs node) memory)
(mv-let (node memory)
(wormhole-Flowcontrol node memory)
(mv (simple-ProcessOutputs node) memory))))
(definstance GenericRouter check-compliance-router
:functional-substitution
((router XY-wormhole-router)))
|
