Commit Graph

951 Commits

Author SHA1 Message Date
Gwenaël Delaval a15e17c02d Cleared simulation output 2012-07-16 00:58:40 +02:00
Gwenaël Delaval bcfcf8cf39 Added iostream in standard library 2012-07-14 14:35:34 +02:00
Gwenaël Delaval e103d60c26 Removed eprintf in schedule_interf
eprintf -> Interference.print_debug
2012-07-14 14:31:46 +02:00
Gwenal Delaval 2e0abee73c Added web site
First version of web site

URL of on-line web site is http://heptagon.gforge.inria.fr

The script rsyncweb allows to sync between the repository and the online site (by use of rsync)
2012-07-12 16:08:36 +02:00
Gwenal Delaval 11493f3274 Manual
UpDown automaton (figure)

Changes in the structure: contracts within Section "Syntax and informal semantics"
2012-07-05 17:26:29 +02:00
Gwenal Delaval bea0c5ac7c Manual: section on compilation and install
Manual: section on compilation, install, required tools and libraries
2012-07-05 16:14:39 +02:00
Cédric Pasteur 09202bd9ec Remove graphical syntax 2012-07-05 11:59:16 +02:00
Cédric Pasteur 767883d578 Small fixes 2012-07-05 11:46:30 +02:00
Cédric Pasteur 9e17900f13 Small section on linear annotations 2012-07-05 11:19:43 +02:00
Cédric Pasteur a2b694602f Small section on clocks 2012-07-05 10:14:04 +02:00
Cédric Pasteur 03acfc9bea New sections in the manual
arrays, records, parametricity, etc.
2012-07-05 08:51:46 +02:00
Cédric Pasteur 84e502d7a9 Made val optional for functions
external val node f is a little bit too long
2012-07-04 17:26:38 +02:00
Gwenaël Delaval a0e0bd2dcc Radio transmitter example
Radio transmitter example, from Nicolas Berthier's thesis

With controller synthesis

Generic Makefile including controller synthesis handling
2012-06-29 02:28:42 +02:00
Gwenaël Delaval bf03077cd9 Correct output toward hepts 2012-06-29 02:01:49 +02:00
Gwenaël Delaval ef00823cf7 Added Marc as co-author 2012-06-29 01:43:15 +02:00
Gwenaël Delaval c080ad6cf3 Controller call only when controllables
Avoid built of dummy empty controllers
2012-06-29 01:41:13 +02:00
Gwenaël Delaval 58086190eb Headers and license file for GPL
Headers for every source file (excluding examples), mentioning
authors, copyright and license (GPL)

COPYING file with GPLv3 content.
2012-06-27 18:14:29 +02:00
Cédric Pasteur 5e1dad630b Force fby to be scheduled at the end 2012-06-20 17:09:30 +02:00
Cédric Pasteur 7a10ba028a Fixed disjoint clock computation 2012-06-20 17:09:17 +02:00
Cédric Pasteur ffeb81f529 Use idents instead of ivars in scheduling 2012-06-20 16:33:06 +02:00
Cédric Pasteur 8815a2cd03 Better handling of clocks in memalloc
- We can do a better allocation if we take into
account 'when' in extvalues 
(test/good/memalloc_clocks.ept shows the
improvement)
- Fixed a bug with memalloc on records: if we 
translate:
o = { a with .f = u }
to
o = a; o.f = u
then we cannot share u and o.f
2012-06-20 09:17:13 +02:00
Cédric Pasteur ee7d60120b Fixed bug in translation to minils 2012-06-19 15:56:54 +02:00
Cédric Pasteur ed2c08315b Should be affinity, not copy 2012-06-19 09:33:27 +02:00
Gwenal Delaval d36e988fb9 User manual: first version 2012-06-14 23:07:40 +02:00
Gwenal Delaval 502c5e446f Makefile correction (install target)
Makefile correction: install target for simulator
2012-06-13 15:13:53 +02:00
Gwenal Delaval 352bad4735 Correction of Inline pass
- correction of Hept_mapfold : inclusion of mapfold for b_defnames (blocks)
- Inlining : deep replacement of idents
2012-06-13 15:06:05 +02:00
Gwenal Delaval cf22ba3989 Optional block in contracts
Optional let...tel block in contracts
Sink state in sigali
2012-06-07 17:48:31 +02:00
Gwenal Delaval 2bd31db883 Causality and scheduling with contracts
Correction of the causality analysis and scheduling (with interference)
to take contracts into account.
2012-06-07 15:27:07 +02:00
Gwenal Delaval 2956002f85 Correction and simplification of the sigali pass
Added a "Contracts" pass, after inlining, taking care of the
contracts of the nodes called in the body of a node. This pass
"inlines" the code and assume/guarantee parts of these subcontracts.

The "Sigali" pass both generates the sigali ("z3z") code and add the call to
the controller (which is a node generated further by the sigali tool).
Therefore this pass has been included into the mls compiler, and removed
from the targets (a "z3z" dummy target has been kept for backward compatibility
reasons).
2012-06-06 15:59:08 +02:00
Gwenal Delaval 1e46c2a73c Makefile : removed target "all" from target "install"
On some systems, the targets "all" and "install" must be
made with different rights. Then "all" cannot be a dependendy of
"install", especially since ocamlbuild try to read/modify some
files even if there is no compilation to perform.
2012-06-06 15:55:23 +02:00
Gwenal Delaval bb0bc8bfe5 Added local assume/guarantee
Added local assume/guarantee in contracts.

No syntax associated to these local asume/guarantee: internal use only.
2012-05-29 14:14:46 +02:00
Adrien Guatto 8153bc4eb5 Fixed Tomato: did not reconstruct internal clocks of extvalues 2012-03-30 14:47:47 +02:00
Léonard Gérard 61e14546df Interf scheduling tries harder with arrays 2012-03-19 17:45:06 +01:00
Adrien Guatto fc1edf91f0 OOPS forgot compiler_timings 2012-03-07 17:51:06 +01:00
Adrien Guatto 834e16cad5 Fix: replace opt with native in build system 2012-03-07 17:48:30 +01:00
Adrien Guatto e05f3732a0 Timing framework. 2012-03-07 17:48:08 +01:00
Adrien Guatto f09792485e Hept2mls: fixed missing enter_node 2012-03-07 17:48:08 +01:00
Adrien Guatto 9640acb3a4 More efficient ident handling. 2012-03-07 17:48:08 +01:00
Adrien Guatto 6870ea62c9 Inlining: fix issue with nesting of blocks. 2012-03-07 17:48:08 +01:00
Adrien Guatto 3e8e54f42b Perform inlining before causality/init analysis. 2012-03-07 17:48:08 +01:00
Adrien Guatto 44d3a639e5 Internal error for unknown clocks. 2012-03-02 17:12:30 +01:00
Adrien Guatto 3b0ebf2dbf print_ident: use the function from Idents 2012-03-02 17:12:30 +01:00
Adrien Guatto 557d00f501 Inlining: do not forget when, merge or last. 2012-03-02 17:12:30 +01:00
Adrien Guatto ba1b134640 Static evaluation of modulo. 2012-03-02 14:11:19 +01:00
Adrien Guatto 699b3c68e9 Tomato: bug fix, node inputs were not properly considered different. 2012-03-01 14:46:33 +01:00
Léonard Gérard 8a78bc7d7d Add [external] in the signatures. fix callgraph acordingly. 2012-02-21 16:07:29 +01:00
Léonard Gérard c1b8e47ffb Fixed escape of string in java 2012-02-21 14:39:35 +01:00
Adrien Guatto 070d2eab55 Revert "Changed linear typing for merge."
This reverts commit 0abb050a23.
2012-02-14 14:36:47 +01:00
Adrien Guatto fc08800be6 Improved Emacs mode 2012-02-12 01:09:25 +01:00
Adrien Guatto b00eab153c heptc script: compile C code in addition to Java. 2012-02-12 00:11:27 +01:00