← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/readme

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2007/schmaltz/genoc-v1.0/generic-modules/readme
 
1
*****************************************************************************
 
2
*                                                                           *
 
3
*                                                                           *
 
4
*                      GeNoC ACL2 scripts                                   *
 
5
*                                                                           *
 
6
*                       Julien Schmaltz                                     *
 
7
*                                                                           *
 
8
*                         TIMA-VDS                                          *
 
9
*                                                                           *
 
10
*                        29/01/06                                           *
 
11
*****************************************************************************
 
12
 
 
13
 
 
14
1 Structure of the books for GeNoC
 
15
-----------------------------------
 
16
 
 
17
1.1 GeNoC-types 
 
18
--------------
 
19
        
 
20
        This book defines the data types used in GeNoC: transactions, 
 
21
missives, travels, etc. It contains basic functions used to manipulate
 
22
these datatypes. 
 
23
        It does not import any book.
 
24
 
 
25
1.2 GeNoC-misc
 
26
--------------
 
27
 
 
28
        This book imports GeNoC-types.
 
29
        This book contains miscellaneous definitions. For instance, it 
 
30
defines predicates like CorrectRoutep, the filtering operator extrac-sublst,
 
31
some lemmas about subsetp, etc.
 
32
 
 
33
1.3 GeNoC-nodeset
 
34
-----------------
 
35
 
 
36
        This book contains functions about the definition and the validation 
 
37
of the set of the existing nodes of a particular network. 
 
38
        It does not import any book.
 
39
 
 
40
1.4 GeNoC-routing
 
41
-----------------
 
42
 
 
43
        This book imports GeNoC-nodeset and GeNoC-misc.
 
44
        It contains functions about the definition and the validation 
 
45
of the routing algorithm. 
 
46
 
 
47
1.5 GeNoC-scheduling
 
48
--------------------
 
49
 
 
50
        This book imports GeNoC-misc and GeNoC-nodeset.
 
51
        It contains functions about the scheduling policy of GeNoC. It
 
52
also adds some lemmas used in the final proof. These lemmas link 
 
53
functions like extract-sublst, missivesp, etc. They are about NodeSet
 
54
and this is why we need the corresponding book.
 
55
 
 
56
1.7 GeNoC-interfaces
 
57
--------------------
 
58
 
 
59
        This book contains functions about the definition and the validation
 
60
of the interfaces. 
 
61
        It does not import any book.
 
62
 
 
63
1.7 GeNoC
 
64
---------
 
65
        This book imports the previous books. It contains the definition 
 
66
of GeNoC and its proof of correctness. 
 
67
 
 
68
1.8 Global Structure
 
69
--------------------
 
70
 
 
71
        The global "book tree" is the following:
 
72
 
 
73
                                 GeNoC
 
74
                        /         |               \ 
 
75
       GeNoC-scheduling    GeNoC-routing       GeNoC-interfaces
 
76
         |          |      |          |         
 
77
 GeNoC-nodeset     GeNoC-misc     GeNoC-nodeset
 
78
                       |
 
79
                   GeNoC-types
 
80