1 files changed, 552 insertions, 0 deletions
diff --git a/books/workshops/2009/verbeek-schmaltz/verbeek/generic-modules/GeNoC-types.lisp b/books/workshops/2009/verbeek-schmaltz/verbeek/generic-modules/GeNoC-types.lisp
new file mode 100644
index 0000000..081f169
--- /dev/null
+++ b/books/workshops/2009/verbeek-schmaltz/verbeek/generic-modules/GeNoC-types.lisp
@@ -0,0 +1,552 @@
+#|$ACL2s-Preamble$;
+;; Julien Schmaltz
+;; Modified and updated by Amr HELMY 14th august 2007
+;; Definition of the data-types used in GeNoC:
+;; Transactions, missives, travels, results and attempts
+;; June 20th 2005
+;; File: GeNoC-types.lisp
+
+;;Amr helmy
+;;31st october 2007
+
+;; Rev. January 31st by JS (mainly state related functions)
+(begin-book);$ACL2s-Preamble$|#
+
+(in-package "ACL2")
+
+;; book paths on my laptop
+(include-book "data-structures/list-defuns"  :dir :system)
+(include-book "data-structures/list-defthms"  :dir :system)
+;(include-book "textbook/chap11/qsort"  :dir :system)
+
+;;----------------------------------------------|
+;;                                              |
+;;                TRANSACTIONS                  |
+;;                                              |
+;;----------------------------------------------|
+;; A transaction is a tuple t = (id A msg B  flits time)
+;; Accessors are IdT, OrgT, MsgT, destT, FlitT, TimeT
+;; TimeT represent the departure time of the flit
+
+(defun Idt (trans)
+
+   (car trans))
+(defun OrgT (trans) (nth 1 trans))
+(defun MsgT (trans) (nth 2 trans))
+(defun DestT (trans) (nth 3 trans))
+(defun FlitT (trans) (nth 4 trans))
+(defun TimeT (trans) (nth 5 trans))
+
+
+(defun T-ids (Transts)
+  ;; function that grabs the ids of a list of trans.
+  (if (endp Transts)
+      nil
+    (append (list (caar Transts)) (T-ids (cdr Transts)))))
+
+(defun T-msgs (Trs)
+  ;; function that grabs the messages of a list of trans.
+  (if (endp Trs)
+      nil
+    (cons (MsgT (car trs))
+          (T-msgs (cdr Trs)))))
+
+(defun T-orgs (Trs)
+  ;; function that grabs the origins of a list of trans
+  (if (endp Trs)
+      nil
+    (cons (OrgT (car trs))
+          (T-orgs (cdr Trs)))))
+
+(defun T-dests (Trs)
+  ;; function that grabs the destinations of a list of trans
+  (if (endp Trs)
+      nil
+    (cons (DestT (car trs))
+          (T-dests (cdr Trs)))))
+
+;; The following predicate checks that each transaction has
+;; the right number of arguments
+(defun validfield-transactionp (trans)
+  ;; trans = (id A msg B flits time)
+  (and (consp trans)
+       (consp (cdr trans))         ;; (A msg B flits Time)
+       (consp (cddr trans))        ;; (msg B flits Time)
+       (consp (cdddr trans))       ;; (B flits Time)
+       (consp (cddddr trans))                ;; (Flits Time)
+       (consp (cdr (cddddr trans)))  ;(Time)
+       (null (cddr (cddddr trans))))) ;;nil
+
+
+;; The following predicate recognizes a valid list of transactions
+(defun Validfields-T (Transts)
+  (if (endp Transts)
+      t
+    (let ((trans (car Transts)))
+      (and (validfield-transactionp trans)
+           (natp (Idt trans))                       ;; id is a natural
+           (MsgT trans)                             ;; msg /= nil
+           (Natp (FlitT trans))
+           (natp (timeT trans))
+           (not (equal (OrgT trans) (DestT trans))) ;; A /= B
+           (Validfields-T (cdr Transts))))))
+
+;; now we define the predicate that recognizes a valid list of
+;; transactions
+(defun Transactionsp (Transts NodeSet)
+  (let ((T-ids (T-ids Transts)))
+    (and (Validfields-T Transts)
+         (true-listp Transts)
+         (subsetp (T-orgs Transts) NodeSet)
+         ;; the origins are members of the nodeset
+         (subsetp (T-dests Transts) NodeSet)
+         ;; the destinations are members of the nodeset
+         (No-Duplicatesp T-ids))))
+
+;;------------------ end of Transactions ----------------------------------
+
+
+;;-----------------------------------------------|
+;;                                               |
+;;                         MISSIVES              |
+;;                                               |
+;;-----------------------------------------------|
+
+
+;; A missive is a tuple m = (id A frm B Flit Time)
+;; Accessors are IdM, OrgM, FrmM and DestM
+
+(defun IdM (m) (car m))
+(defun OrgM (m) (nth 1 m))
+(defun FrmM (m) (nth 2 m))
+(defun DestM (m) (nth 3 m))
+(defun FlitM (m) (nth 4 m))
+(defun TimeM (m) (nth 5 m))
+
+
+;; We need a function that grabs the ids of a list of missives
+(defun M-ids (M)
+  (if (endp M)
+      nil
+    (append (list (caar M)) (M-ids (cdr M)))))
+
+;; We need a function that grabs the origins of Missives
+(defun M-orgs (M)
+  (if (endp M)
+      nil
+    (append (list (OrgM (car M))) (M-orgs (cdr M)))))
+
+;; The same for the destinations
+(defun M-dests (M)
+  (if (endp M)
+      nil
+    (append (list (DestM (car M))) (M-dests (cdr M)))))
+
+;; We also need a function that grabs the frames of a list of missives
+(defun M-frms (M)
+  (if (endp M)
+      nil
+    (let* ((msv (car M))
+           (m-frm (FrmM msv)))
+      (append (list m-frm) (M-frms (cdr M))))))
+
+
+;; The following predicate checks that each missive has
+;; the right number of arguments
+(defun validfield-missivep (m)
+  ;; m = (id A frm B)
+  (and (consp m)
+       (consp (cdr m))         ;; (A frm B flits time)
+       (consp (cddr m))        ;; (frm B flits time)
+       (consp (cdddr m))       ;; (B flits time)
+       (consp (cddddr m))           ;; (Flits Time)
+       (consp (cdr (cddddr  m))) ;;(time)
+       (null  (cddr  (cddddr  m))))) ;;nil
+
+;; The following predicate recognizes a valid list of missives (partially)
+(defun Validfields-M (M)
+  (if (endp M)
+      t
+    (let ((msv (car M)))
+      (and (validfield-missivep msv)
+           (natp (IdM msv))                     ;; id is a natural
+           (FrmM msv)                           ;; frm /= nil
+           (natp (FlitM msv))
+           (natp (TimeM msv))
+           (not (equal (OrgM msv) (DestM msv))) ;; A /= B
+           (Validfields-M (cdr M))))))
+
+;; now we define the predicate that recognizes a valid list of
+;; missives
+(defun Missivesp (M NodeSet)
+  (let ((M-ids (M-ids M)))
+    (and (Validfields-M M)
+         (subsetp (M-orgs M) NodeSet)    ;;origins subset of nodeset
+         (subsetp (M-dests M) NodeSet)         ;;destinations subset of nodeset
+         (true-listp M)
+         (No-Duplicatesp M-ids))))
+
+;;-------------------- end of Missives -------------------------------------
+
+
+;;------------------------------------------|
+;;                                          |
+;;           TRAVELING MISSIVES             |
+;;                                          |
+;;------------------------------------------|
+
+
+;; A traveling missive is a tuple m = (id A current frm B Flit time)
+;; Accessors are IdTM, OrgTM, curTM, FrmTM and DestTM flitm
+
+(defun IdTM (m) (car m))
+(defun OrgTM (m) (nth 1 m))
+(defun CurTM (m) (nth 2 m))
+(defun FrmTM (m) (nth 3 m))
+(defun DestTM (m) (nth 4 m))
+(defun FlitTM (m) (nth 5 m))
+(defun TimeTM (m) (nth 6 m))
+
+;; We need a function that grabs the ids of a list of missives
+(defun TM-ids (M)
+  (if (endp M)
+      nil
+    (append (list (IdTM (car M))) (TM-ids (cdr M)))))
+
+;; We need a function that grabs the origins of Missives
+(defun TM-orgs (M)
+  (if (endp M)
+      nil
+    (append (list (OrgTM (car M))) (TM-orgs (cdr M)))))
+
+;; The same for the currents
+(defun TM-curs (M)
+  (if (endp M)
+      nil
+    (append (list (CurTM (car M))) (TM-curs (cdr M)))))
+
+;; The same for the destinations
+(defun TM-dests (M)
+  (if (endp M)
+      nil
+    (append (list (DestTM (car M))) (TM-dests (cdr M)))))
+
+;; We also need a function that grabs the frames of a list of missives
+(defun TM-frms (M)
+  ;; grabs the frames of M
+  (if (endp M)
+      nil
+    (let* ((msv (car M))
+           (m-frm (FrmTM msv)))
+      (append (list m-frm) (TM-frms (cdr M))))))
+
+
+;; The following predicate checks that each missive has
+;; the right number of arguments
+(defun validfield-Tmissivep (m)
+  ;; m = (id A current frm B)
+  (and (consp m)
+       (consp (cdr m))         ;; (A current frm B flits time)
+       (consp (cddr m))        ;; (current frm B flits time)
+       (consp (cdddr m))       ;; (frm B flits time)
+       (consp (cddddr m))      ;; (B flits time)
+       (consp (cdr (cddddr  m)));; (flits Time)
+       (consp (cddr (cddddr m))) ;;(time)
+       (null (cdddr (cddddr m)))
+       )) ;;nil
+
+
+
+;; The following predicate recognizes a valid list of missives (partially)
+(defun Validfields-TM (M)
+  (if (endp M)
+      t
+    (let ((msv (car M)))
+      (and (validfield-Tmissivep msv)
+           (natp (IdTM msv))                      ;; id is a natural
+           (FrmTM msv)                            ;; frm /= nil
+           (Natp (FlitTM msv))
+           (natp (TimeTM msv))
+           (not (equal (OrgTM msv) (DestTM msv))) ;; A /= B
+           (not (equal (CurTM msv) (DestTM msv))) ;; current /= B
+           (Validfields-TM (cdr M))))))
+
+;; now we define the predicate that recognizes a valid list of
+;; missives
+(defun TMissivesp (M NodeSet)
+  (let ((M-ids (TM-ids M)))
+    (and (Validfields-TM M)
+         (subsetp (TM-orgs M) NodeSet)                ;;origines subset nodeset
+         (subsetp (TM-curs M) NodeSet)                ;;current subset nodeset
+         (subsetp (TM-dests M) NodeSet)                ;;destination subset nodeset
+         (true-listp M)
+         (No-Duplicatesp M-ids))))
+
+;;-------------------- end of Traveling Missives -------------------------
+
+
+;;------------------------------------------------|
+;;                                                |
+;;                   TRAVELS                      |
+;;                                                |
+;;------------------------------------------------|
+
+;; On ajoute l'origine, car elle va pouvoir ne plus apparaitre dans Routes...
+
+;; A travel is a tuple tr = (id org frm Routes flits time)
+;; Accessors are IdV, OrgV, FrmV, RoutesV and FlitsV
+;; (JS: V comes from the french word for travel, voyage :-)
+
+(defun IdV (tr) (car tr))
+(defun OrgV (m) (nth 1 m))
+(defun FrmV (tr) (nth 2 tr))
+(defun RoutesV (tr) (nth 3 tr))
+(defun FlitV (tr) (nth 4 tr))
+(defun TimeV (tr) (nth 5 tr))
+
+
+;; We need a function that grabs the ids of a list of travels
+(defun V-ids (TrLst)
+  (if (endp TrLst)
+      nil
+    (append (list (caar TrLst)) (V-ids (cdr TrLst)))))
+
+;; We need a function that grabs the orgs of a list of travels
+(defun V-orgs (TrLst)
+  (if (endp TrLst)
+      nil
+    (append (list (OrgV (car TrLst))) (V-orgs (cdr TrLst)))))
+
+
+;; using these functions, we have:
+;; (validfield-route route org dest) implies (validfield-route (cdr route) org dest)
+;; for all routes in routes
+(defun no-consecutive-equals (route)
+  (if (not (and (consp route)
+                (consp (cdr route))))
+    t
+    (and (not (equal (car route) (cadr route)))
+         (no-consecutive-equals (cdr route)))))
+(defun no-hops-equal-to-dest (route dest)
+  (if (not (and (consp route)
+                (consp (cdr route))))
+    t
+    (and (not (equal (car route) dest))
+         (no-hops-equal-to-dest (cdr route) dest))))
+
+;; The following predicate checks that each route of routes
+;; has at least two elements
+(defun validfield-route (routes org nodeset)
+  ;; checks that every route has at least two elements
+  (if (endp routes)
+      t
+    (let ((r (car routes)))
+      (and (consp r)
+           (consp (cdr r))
+           (subsetp r nodeset)
+           (not (equal org (car (last (cdr r))))) ;; (org != dest)
+;           (not (equal (car r) (car (last (cdr r))))) ;; (current != dest)
+           (no-consecutive-equals r)
+           (no-hops-equal-to-dest r (car (last r)))
+;           (or (equal (len r) 2) ;; or len = 2, or next != dest
+;               (not (equal (cadr r) (car (last r)))))
+           (validfield-route (cdr routes) org nodeset)))))
+
+
+;; The following predicate checks that each travel has
+;; the right number of arguments
+(defun validfield-travelp (tr nodeset)
+  ;; tr = (id org frm Routes flits time)
+  (and (consp tr)
+       (consp (cdr tr))          ;; (org frm Routes flits time)
+       (consp (cddr tr))         ;; (frm Routes flits time)
+       (consp (cdddr tr))        ;; (Routes flits time) = ( ((R1) (R2) ...) flits time)
+       (consp (routesv tr))
+       (consp (cddddr tr))       ;;(Flits Time)
+       (consp (cdr (cddddr tr))) ;; (time)
+       (null (cddr (cddddr tr))) ;;nil
+       (member-equal (orgv tr) nodeset)
+       (validfield-route (routesv tr) (orgv tr) nodeset)))
+
+;; The following predicate recognizes a valid list of missives (partially)
+(defun Validfields-TrLst (TrLst nodeset)
+  (if (endp TrLst)
+      t
+    (let ((tr (car TrLst)))
+      (and (validfield-travelp tr nodeset)
+           (natp (IdV tr))                     ;; id is a natural
+           (FrmV tr)                           ;; frm /= nil
+           (natp (FlitV tr))
+           (natp (TimeV tr))
+           (true-listp (RoutesV tr))
+           (Validfields-TrLst (cdr TrLst) nodeset)))))
+
+;; now we define the predicate that recognizes a valid list of
+;; travels
+(defun TrLstp (TrLst nodeset)
+  (let ((V-ids (V-ids TrLst)))
+    (and (Validfields-TrLst TrLst nodeset)
+         (true-listp TrLst)
+         (No-Duplicatesp V-ids))))
+
+(defun V-frms (TrLst)
+  ;; grabs the frames of TrLst
+  (if (endp TrLst)
+      nil
+    (let* ((tr (car Trlst))
+           (v-frm (FrmV tr)))
+      (append (list v-frm) (V-frms (cdr TrLst))))))
+
+;;-------------------- end of Travels -------------------------------------
+
+
+;;---------------------------------------------|
+;;                                             |
+;;                         RESULTS             |
+;;                                             |
+;;---------------------------------------------|
+
+;; A result is a tuple rst = (Id Dest Msg flit Time)
+;; Accessors are IdR, DestR and MsgR
+
+(defun IdR (rst) (car rst))
+(defun DestR (rst) (nth 1 rst))
+(defun MsgR (rst) (nth 2 rst))
+(defun FlitR (rst) (nth 3 rst))
+(defun TimeR (rst) (nth 4 rst))
+
+(defun R-ids (R)
+  ;; function that grabs the ids of a list of results
+  (if (endp R)
+      nil
+    (append (list (caar R)) (R-ids (cdr R)))))
+
+(defun R-dests (Results)
+  ;; function that grabs the destinations of a list of results
+  (if (endp Results)
+      nil
+    (cons (DestR (car Results))
+          (R-dests (cdr Results)))))
+
+(defun R-msgs (Results)
+  ;; function that grabs the messages of a list of results
+  (if (endp Results)
+      nil
+    (cons (MsgR (car results))
+          (R-msgs (cdr Results)))))
+
+
+;; The following predicate checks that each result has
+;; the right number of arguments
+(defun validfield-resultp (rst)
+  ;; tr = (Id Dest Msg)
+  (and (consp rst)
+       (consp (cdr rst))         ;; (Dest Msg Flit time)
+       (consp (cddr rst))        ;; (Msg Flit time)
+       (consp (cdddr rst))                 ;; (flit time)
+       (consp (cddddr rst))                 ;;(time)
+       (null (cdr(cddddr rst)))));; nil
+
+
+;; The following predicate recognizes a valid list of results (partially)
+(defun Validfields-R (R NodeSet)
+  (if (endp R)
+      t
+    (let ((rst (car R)))
+      (and (validfield-resultp rst)
+           (natp (IdR rst))                     ;; id is a natural
+           (MsgR rst)                           ;; msg /= nil
+           (Natp (FlitR rst))
+           (natp (TimeR rst))
+           (member (DestR rst) NodeSet)
+           (Validfields-R (cdr R) NodeSet)))))
+
+;; now we define the predicate that recognizes a valid list of
+;; results
+(defun Resultsp (R NodeSet)
+  (let ((R-ids (R-ids R)))
+    (and (Validfields-R R NodeSet)
+         (true-listp R)
+         (No-Duplicatesp R-ids))))
+
+;;-------------------- end of Results -------------------------------------
+
+;;-----------------------------------------------|
+;;                                               |
+;;                         STATE                 |
+;;                                               |
+;;-----------------------------------------------|
+
+;; a state is a list of the form ( (coor (node_id)) (buffers ...)) where
+;; node_id a an element of NodeSet
+;; we define accessors and predicates defining valid state entries
+
+;; we need accessors to the state elements
+(defun get_coor (st_entry)
+  ;; st_entry =  ( (coor (id)) (buffers ...))
+  ;; this function returns id
+  (cadar st_entry))
+
+
+(defun get_buff (st_entry)
+  ;; st_entry =  ( (coor (id)) (buffers ...))
+  ;; this function returns ...
+  (cadadr st_entry))
+
+
+(defun getcoordinates (ntkstate)
+  (if (endp ntkstate)
+      nil
+    (cons (get_coor (car ntkstate))
+          (getcoordinates (cdr ntkstate)))))
+
+(defun get-buffers (ntkstate)
+  (if (endp ntkstate)
+      nil
+    (cons (get_buff (car ntkstate))
+          (get-buffers (cdr ntkstate)))))
+
+
+(defun validCoord (x)
+  ;; x is (coor (id))
+  (and (equal (car x) 'Coor)
+       (consp x)
+       (consp (cdr x))
+       (null (cddr x))))
+
+(defun ValidBuffer (x)
+  ;; x is (buffers ...)
+  (and (equal (car x) 'Buffers)
+       (consp x)
+       (consp (cdr x))))
+
+(defun ValidCoordlist (x)
+  ;; x is a state = ( ((coor (id)) (buffers ...)) ...)
+  (if (endp x)
+      t
+    (and (Validcoord (caar x))
+         (Validcoordlist (cdr x)))))
+
+(defun ValidbuffersList (x)
+  ;; x is a state = ( ((coor (id)) (buffers ...)) ...)
+  (if (endp x)
+      t
+    (and (ValidBuffer (cadar x))
+         (Validbufferslist (cdr x)))))
+
+;; NOTE: nil is a valid state, so nil is also a valid state element
+
+(defun validstate-entryp (st_entry)
+  (if (endp st_entry)
+      t
+    (and (Validcoord (car st_entry))
+         (Validbuffer (cadr st_entry)))))
+
+
+(defun ValidState (ntkstate)
+  (if (endp ntkstate)
+      t
+    (and ;(consp ntkstate)
+     (Validstate-entryp (car ntkstate))
+     (Validstate (cdr ntkstate)))))#|ACL2s-ToDo-Line|#
+