jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity
1042 commits 2 branches 0 tags 6.9 MiB
Commit graph

1042 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nicolas Berthier
4f7413282e Merge branch 'decade' into ctrl-n 2013-11-26 18:03:54 +01:00
Nicolas Berthier
c132b53732 Handle `when' operators in general expressions, in Controllable-Nbac backend. 
- CtrlNbacGen: ignore sub-sampling in general expressions.
 2013-11-26 18:03:07 +01:00
Nicolas Berthier
934c9f9a85 Handle `when' operators for non-Boolean expressions in Controllable-Nbac backend. 2013-11-20 12:13:01 +01:00
Gwenaël Delaval
d27db41485 Version 1.00.03 2013-11-20 10:20:35 +01:00
Nicolas Berthier
808b9772f3 Merge branch 'decade' into ctrl-n 2013-11-20 08:53:00 +01:00
Gwenaël Delaval
71497a82b2 Corrected bug in inline_extvalues 
Inline_extvalues: added local variables of contracts into environments
 2013-11-19 20:39:01 +01:00
Nicolas Berthier
ae6a3aac2e Attractivity property of Controllable-Nbac output; minor refactorings. 2013-11-13 15:35:15 +01:00
Nicolas Berthier
216550c0d1 Fixed warnings & documentation comments. 
- gitignore: ignore files generated by `configure' script.
 2013-11-08 18:51:06 +01:00
Nicolas Berthier
10bdab4dc6 Exclusively use ocamlfind; source documentation generation. 
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
  when `-use-ocamlfind' is passed to ocamlbuild.

- Added some code in `myocamlbuild_config.ml' to be able to generate
  documentation by merging interface and implementation files.
 2013-11-08 15:50:36 +01:00
Nicolas Berthier
8aeab651ce First draft for Controllable-Nbac format generation. 
- CtrlNbac: new module for internal representation and output code for
  Controllable-Nbac format;

- CtrlNbacGen: translation into Controllable-Nbac of Minils nodes
  necessitating controller synthesis; the insertion of calls to
  controllers is not yet done, and the nodes are left unchanged.
 2013-11-08 15:13:39 +01:00
Gwenaël Delaval
106b1339ac Corrected Makefile for binary distribution 2013-11-04 11:52:46 +01:00
Gwenaël Delaval
5b98f9cdf6 Version 1.00.02 
Added CHANGES file
 2013-10-29 19:03:31 +01:00
Gwenal Delaval
13d616c930 Scrollbars on inputs/outputs of hepts 
Allowed shrinking hepts main window and added scrollbars on frames
for inputs and outputs.
 2013-10-29 16:48:34 +01:00
Gwenal Delaval
f5872cbcf4 Change URL for sim2chro in manual 
- change URL for download of sim2chro (towards Lustre v4 distribution)
- added GTKWave in INSTALL
- change font of pdf manual
 2013-10-28 12:19:59 +01:00
Gwenaël Delaval
c0b84bd186 Abstraction of integers for Sigali 
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
 2013-09-06 10:13:08 +02:00
Gwenaël Delaval
f3d34f57d1 Abstraction of integers for Sigali 
Correction of abstraction for Sigali: integer equations comprising no
integer variables should not be abstracted
 2013-09-05 19:03:22 +02:00
Gwenal Delaval
17435fd012 Small changes on manual 2013-09-05 14:35:21 +02:00
Gwenal Delaval
6e791e3199 More permissive syntax (trailing commas/semicols) 
Allowing trailing commas and in parameters declarations
 2013-08-02 14:14:14 +02:00
Gwenal Delaval
bb2c3c4060 Update of manual 
- use of GTKWave
- appendix: interfaces of java 1.4 and 1.5 generated code
 2013-08-02 14:14:14 +02:00
Gwenal Delaval
cd01f82cf6 Graphical simulator: output to GTKWave and TikZ 
Added option -gtkwave, output in VCD (Value Change Dump) format

Button for TikZ (tikz-timing) export.
 2013-08-02 14:14:13 +02:00
Gwenal Delaval
ee7ef158e7 Bug correction: java code generation for "~-." 
Bug correction: handling of unary float "~-."
 2013-08-02 14:14:13 +02:00
Gwenaël Delaval
971f622ea3 Added test of camlp4of in configure script 2013-07-18 11:21:27 +02:00
Gwenaël Delaval
71f7db2d11 Bug correction in Mls_printer and Hept_printer 
Correction of infix operators printing : infix printing only
when two arguments of pervasives infix operators (no assertions
on number of arguments).
 2013-07-10 09:57:19 +02:00
Gwenal Delaval
f696203eb1 Bug in sigalimain 
Bug correction: code generation to sigali for stateless nodes

=> stateless nodes handled like stateful nodes, if not in pervasives.
 2013-07-09 21:16:30 +02:00
Gwenal Delaval
2d150a3a3d Infix operators in printers 
Infix operators handled in Heptagon and Minils printers
 2013-07-09 21:15:31 +02:00
Gwenaël Delaval
7720a632cc Removed bugged local substitutions in Contracts pass 2013-05-17 23:21:43 +02:00
Cédric Pasteur
f5cc4625e0 And don't forget to type the argument of when 2013-05-07 17:13:00 +02:00
Cédric Pasteur
21aae319ee Fixed linear typing of when 
It is always a read. One has to use the 
split operator for sampling linear variables.
 2013-05-07 17:09:58 +02:00
Cédric Pasteur
a00620ca19 Fixed interference of fast memories 
A fast memory should be considered alive during
the whole step function when its clock is false.
 2013-05-06 11:47:05 +02:00
Cédric Pasteur
99dc7820c7 Avoid crash in memalloc 
Check if both variables are optmized
 2013-04-22 18:11:10 +02:00
Nicolas Berthier
8497bafa2e Minor but correction in sigali output. 
- Translation to z3z now evaluates constant expressions instead of
  abstracting them. This non-feature could cause "false" synthesis
  failures due to non-translatable yet constant expressions possibly
  introduced by tomato (or manually), for instance `not false' in node
  `n' bellow:

    node n (a: bool) returns (ok: bool)
      contract assume true enforce ok with ()
    let
      ok = a or not false;
    tel
 2013-04-11 17:30:30 +02:00
Nicolas Berthier
899d33afb6 Corrected a bug in generation of C records. 
Corrected a somewhat unnoticeable but ugly bug in the generation of C
records, that could mess up the field names when they were not
assigned in the same order as in the declaration of the type.
 2013-03-15 09:31:19 +01:00
Nicolas Berthier
9db97de879 Bug correction in `Sigalimain.translate_eq'. 
- In Sigalimain: untranslatable non-boolean expressions should not be
  added as inputs of the controller.

- Avoided some compiler warnings in the same module (with OCaml ≥ 4).
 2013-03-12 16:53:52 +01:00
Gwenal Delaval
9b3ba83bb1 Bug correction in java generation 2013-03-11 16:04:12 +01:00
Gwenaël Delaval
f60b00e9e3 Bug correction in Inline_extvalues 
Added handling of controllable variables in Inline_extvalues
 2013-02-08 14:42:26 +01:00
Gwenal Delaval
3a9b332b9b Heptagon manual: pdf version in repository 
(to avoid laborious recompilations)
 2013-02-05 15:33:45 +01:00
Gwenal Delaval
0b5f92b57e Updated configure script 2013-02-05 15:26:49 +01:00
Gwenaël Delaval
5b1784957f Makefile-distrib update 
Makefile-distrib: include install-sh script in source distribution
(mandatory for autoconf).

Enable simulator by default (for automatic builds on pipol: some ctest
versions does not allow options passing to configure scripts).
 2013-02-04 22:16:10 +01:00
Gwenal Delaval
e7f85d6b25 Configuration for binary release 
- custom bytecode compilation
- added suffix (OS, cpu) in binary distrib
 2013-01-28 15:55:56 +01:00
Gwenal Delaval
2be4e287b9 Take into account the -nosink option in Sigali 
Corrected bug: do not suppress the last state
variable when -nosink is on.
 2013-01-28 15:54:27 +01:00
Gwenaël Delaval
165ff8d7fa configure script: SET_MAKE handling 
Change MAKE=@MAKE@ --> @SET_MAKE@
 2013-01-26 13:28:37 +01:00
Gwenaël Delaval
f2c4507ea4 Bug correction in extern_C example 2013-01-25 15:41:34 +01:00
Gwenaël Delaval
dcfcc0f59c Additional Makefiles for distribution builds 
Makefile-bin: only install target, for binary distribution
Makefile-distrib: two targets, binary-distrib (builds a binary distribution
based on the current configuration) and source-distrib (builds a source distribution)
 2013-01-25 00:36:58 +01:00
Gwenaël Delaval
c39a0e058e INSTALL file for distribution 2013-01-24 23:55:35 +01:00
Gwenaël Delaval
5a9b27d6a9 Correct handling of local assume/enforce of contracts 2012-12-11 08:20:04 +01:00
Gwenaël Delaval
d193d3320b Added example "migration" (Bouhadiba et al, Emsoft 2011) 2012-12-11 08:20:04 +01:00
Gwenal Delaval
ce2e2bdcd0 Added -nbvars option for performance evaluation 2012-11-26 10:05:20 +01:00
Gwenaël Delaval
ef536f412d Added option -nosink (CS optimisation) 
The -nosink option suppress the sink state of sigali equations.

This optimizes the controller synthesis, but work only
when the synthesis objective instantaneoulsy depends only
on the current state (and not on current inputs).
 2012-11-23 12:23:17 +01:00
Gwenaël Delaval
5bdd891105 Handling of controllables in tomato 
Added controllable variables as "inputs" in the
tomato pass.
 2012-11-22 18:52:21 +01:00
Gwenaël Delaval
0e60d2e839 Boolean transformation: added inputs/outputs 
Non transformation of inputs/outputs during
Boolean pass lead to bugs.
 2012-11-22 18:49:12 +01:00