Commit graph

1120 commits

Author SHA1 Message Date
Gwenaël Delaval
ccc07cc7b9 Unalias missing in obc translation 2012-07-31 15:22:38 +02:00
Gwenaël Delaval
35bea85bf7 Boolean: no transformation on inputs/outputs
Only translate local variables, so as to not
modify node interfaces.
2012-07-26 01:45:38 +02:00
Gwenaël Delaval
72b1bd8de3 Typo in error message 2012-07-26 01:33:32 +02:00
Gwenaël Delaval
90dda27a3a Bug correction in Schedule_interf
Bug due to the fact that a variable can be "defined" and "read"
(in scheduling sense) by the same equation, without being a memory:
e.g., a clock defined as the result of a node application, together
with another result on this same clock.

Bug correction: basically removed the "assert false" on killed_vars,
decr_uses; do not count as "use" the self reads.
2012-07-26 01:29:22 +02:00
Gwenal Delaval
5ed07e1e5a Removed systematic qual. of infix op as pervasives
Bug: every infix operator was systematically qualified
as pervasive.
2012-07-24 17:09:51 +02:00
Gwenal Delaval
5890e3599f Light change in test script 2012-07-23 17:36:04 +02:00
Gwenal Delaval
70cb94d0bd Unroll correction
Order of statement was incorrect
2012-07-23 17:35:20 +02:00
Gwenal Delaval
6011353cec Added test of options
Added script test_option which:
- compile and run without option
- compile with option given as argument, run
- diff on the two outputs, fails if different outputs

config file checks for existence of compiler (fails if not exist)

statics1.ept is a copy of statics.ept ; statics2.ept depends on statics1.ept
instead of statics.ept (so as dependency order => lexical order on file names)
2012-07-19 15:23:40 +02:00
Gwenal Delaval
8b7ad28d6b Some more main in tests 2012-07-18 16:54:44 +02:00
Gwenal Delaval
87f359a6fd Added main to several tests
Added main to tests
Added dependency statics -> statics2 in scripts
2012-07-17 17:57:04 +02:00
Gwenal Delaval
891b1f3ffd Added some main in tests
Goal: run as many nodes as possible
2012-07-16 18:49:08 +02:00
Gwenal Delaval
40cf503149 Correct test scripts config file
Added "mkdir _check_builds" if it does not exist
2012-07-16 18:48:03 +02:00
Gwenal Delaval
295997b866 Config of test scripts
Added option -stdlib towards source library
2012-07-16 16:16:59 +02:00
Gwenal Delaval
9c51b91fd3 Correct ctest configuration
SET_TEST_PROPERTIES does not work with ctest < 2.8.0
2012-07-16 16:12:16 +02:00
Gwenal Delaval
7e90dccc0a Cleared java simulation output 2012-07-16 11:37:50 +02:00
Gwenal Delaval
4c0b1f8431 Corrected ctest configuration file 2012-07-16 11:22:56 +02:00
Gwenal Delaval
89ee2a8fb6 Manual: part on automata
Paragraphs about type of transitions
weak/strong, memoryles/with memory
2012-07-16 09:54:12 +02:00
Gwenaël Delaval
e424667f47 Tests with ctest
Configuration files and scripts to perform tests with ctest
- ctest can be run into the test directory or the root
- the script CTestScript.cmake allows ctest to perform the whole
sequence update/configure/build/test and submit the result to
cdash (http://cdash.inria.fr/CDash/index.php?project=Heptagon)
- gen_ctests is used to generate the file test/CTestTestfile.cmake
2012-07-16 01:03:37 +02:00
Gwenaël Delaval
90e391f4df Modified test t13.ept
Modified test t13.ept so that the output is not always "0"
(useful for further comparisons)
2012-07-16 01:00:09 +02:00
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