Activity
From 06/18/2019 to 07/17/2019
07/17/2019
- 11:12 PM Revision 72a93147 (lustrec): seal: stateless systems
- 11:10 PM Bug #86 (Closed): lustrev ne se termine pas
- The example was not looping but generating an assert false
commit 72a93147f - 03:41 AM Bug #86 (Closed): lustrev ne se termine pas
- node Abs1_PP(
In1_1 : int;)
returns(
Out1_1 : int; );
var
Abs_1 : int;
let
Abs_1 = (if (In1_1 >= 0) the... - 08:00 PM Bug #88 (New): kind2 output: When for node arguments
- Lustrec syntax:
f(x1 when c, x2 when c, ...)
Kind2 syntax:
(activate f every c)(x1, x2, ...) - 07:58 PM Bug #87 (Closed): kind2 output: merge
- Lustrec syntax:
merge c
(true -> a when true(c))
(false -> b when false(c));
Kind2 syntax:
merge c
(true... - 07:40 PM Revision 1d3f2f66 (lustrec): every in kind2 syntax
- 07:38 PM Bug #82 (Closed): kind2 output for every
- commit 1d3f2f66f
- 07:30 PM Revision ae08b9fc (lustrec): [seal] delt with Merge and when
- [printer] more kind2 syntax
- 07:28 PM Bug #83 (Closed): Kind2 output "bool clock" => "bool"
- commit ae08b9fc9
- 02:16 AM Revision 629392e1 (lustrec): No more when suffix in clocked variables with kind2 option
- 02:13 AM Bug #84 (Closed): kind2 output : "real when true(_isEnabled_clock)" => "real"
- Solved in commit 629392e16f26aaf7d2
07/16/2019
- 11:17 PM Revision 0697ff5b (lustrec): Produce true/false statements as constants
- 11:00 PM Bug #85 (Closed): lustrev failed
- lustrev -verbose 0 -seal -seal-export lustre -d toto2 -node Clock_PP Clock_PP.LUSTREC.lus
Raised by primitive operat... - 10:55 PM Bug #84 (Closed): kind2 output : "real when true(_isEnabled_clock)" => "real"
- Generating MC-DC on the attached file generates a normalized variables with type "real when true(_isEnabled_clock)"....
- 08:24 PM Bug #83 (Closed): Kind2 output "bool clock" => "bool"
- 08:13 PM Bug #82 (Closed): kind2 output for every
- Kind2 syntax for resetting node using EVERY operator is:
(restart <node_name> every <clock>)(<input_1>, <input_2>, ...) - 07:49 PM Bug #68 (Rejected): Error compiling lustresf
- Not enough information
- 07:46 PM Bug #79 (Closed): MCDC Conditions are repeated for variables with one atomic boolean condition
- The issue appears to be solved in Lustrec compiler, version 1.7-1066-lustrec-seal (Xia/Huai-dev)
- 07:43 PM Revision 2200179c (lustrec): removed reload of external modules when checking algebraic loop.
- 07:43 PM Bug #80 (Closed): Import error: node Memory_2047_001 is already defined.
- Algebraic loop in the model. Now the answer is more readable
- 07:40 PM Bug #77 (Closed): lustrec-seal branch failed to compile a valid lustre file (compiled by master branch)
- Solved by commit 2200179cdf52c7509b2
- 07:08 PM Bug #78 (In Progress): Why generate MCDC conditions for constant flows?
- 07:05 PM Bug #78: Why generate MCDC conditions for constant flows?
- I am not sure it is a bug:
- either it is a pure constant like b = true
then a condition if b then e1 else e2 wil... - 06:54 PM Revision 25320f03 (lustrec): scheduling now report unused vars and remove their definition instead of stopping processing.
- 06:53 PM Revision c6c8786b (lustrec): kind2 output for printer. global option available
- 03:38 AM Revision 03c767b1 (lustrec): Seal: solved issue with guards merging
- 01:36 AM Lustrec-Tests Revision 333948c1 (lustrec-tests): add simpler triplex example
07/15/2019
07/13/2019
- 12:45 AM Bug #81 (Closed): Example with Enumeration is not supported by Lustrev
- lustrev failed for model "DaysEnum_PP.LUSTREC"
Raised at file "hashtbl.ml", line 194, characters 13-28
Called from ... - 12:29 AM Bug #80 (Closed): Import error: node Memory_2047_001 is already defined.
- lustrev -seal -seal-export lustre -d bacteriaPopulation_PP -node bacteriaPopulation_PP bacteriaPopulation_PP.LUSTREC...
07/12/2019
- 11:24 PM Revision b8dfc744 (lustrec): valid _verif node for seal-export lustre
- 10:32 PM Revision fbcd3ad1 (lustrec): No space in comments
- 10:24 PM Revision 518951ed (lustrec): Seal export lustre
- 10:24 PM Revision faf2b835 (lustrec): Work in progress: higher level constructs for lustre elements
- 03:05 AM Revision 5b4c0069 (lustrec): Contract printer cocospec
07/11/2019
- 11:25 PM Revision 1561a5bb (lustrec): No space before contract kwd
- 11:23 PM Revision 096f48d5 (lustrec): Printing trailing zeros in real constants
- 11:12 PM Revision 0292f958 (lustrec): Export cocospec contract
- 09:14 PM Revision 3209838a (lustrec): configure.ac
- 09:10 PM Revision 3bd83542 (lustrec): Remove dep
- 09:09 PM Revision 0980686c (lustrec): Seal deps + Z3 pin opam
- 08:59 PM Revision 7a4fd94d (lustrec): Output folder for seal-extract
- 08:41 PM Lustrec-Tests Revision db87e34d (lustrec-tests): Merge branch 'master' of https://cavale.enseeiht.fr/git/lustrec-tests
- 08:40 PM Lustrec-Tests Revision 43460259 (lustrec-tests): New folder for extraction testing
- 08:39 PM Revision 3fd36dc9 (lustrec): Seal-export to a new file
- 07:43 AM Revision d75eb6f1 (lustrec): seal-export: produce the output as well. Could be simpler
- 06:39 AM Revision 81229f63 (lustrec): Seal-extract: first serious version. Guards are gathered as a single expression
07/10/2019
07/09/2019
- 03:02 AM Revision 47851ec2 (lustrec): Working version of seal-extract. Heavy load on z3.
- TODO: improvement through memoization
- 03:02 AM Revision 7659bbb1 (lustrec): Corelang function: push_negations that propagate negations in leafs of the expression
- 12:15 AM Bug #79 (Closed): MCDC Conditions are repeated for variables with one atomic boolean condition
- Compare_1 = (u_1 >= Constant_1);
__cov_0_24 = (u_1 >= Constant_1);
__cov_1_24 = (not ((u_1 >= Const... - 12:13 AM Bug #78 (In Progress): Why generate MCDC conditions for constant flows?
- __test1_PP_1 = (true -> false);
__cov_12_16 = __test1_PP_1;
__cov_13_16 = (not (__test1_PP_1));
...
07/07/2019
- 03:24 AM Revision 7aaacbc9 (lustrec): Better extraction in lustrev-seal
- 03:24 AM Revision 58301109 (lustrec): Zustre: Bug solved in const injection for reals
07/06/2019
- 12:49 AM Revision 2104c80a (lustrec): Addressed a TODO in MCDC Pathconditions: simpler condition for single expression
- 12:04 AM Revision df94cd73 (lustrec): - More systematic translation for mutation
- - copy_var_decl now keeps the generated type
07/05/2019
- 11:15 PM Revision e998fc16 (lustrec): Mutation translates now ids in cocospec import
- 03:07 AM Lustrec-Tests Revision 15c932a9 (lustrec-tests): add ada_diff.py
07/04/2019
- 05:35 PM Revision 67ef9395 (lustrec): minor bugs solved in printer: guarantee vs guarantees in cocospec. Imported node shall not be printed as regular code since it is not part of the grammar yet. Kept them as comment.
- 05:34 PM Revision 3050ca8f (lustrec): keep the open top declaration when loading a module. It may be useful later when producing a lustre file
- 05:33 PM Revision 653b62e0 (lustrec): lustret: do not reload opened modules when generating the mcdc output
- 05:14 PM Lustrec-Tests Revision b745c1a8 (lustrec-tests): Renamed main node as top
- 06:35 AM Revision 8c934ccd (lustrec): lustrev seal: ongoing work on extraction as dynamical system. Still not working yet
- 06:33 AM Revision 6c3f2837 (lustrec): lustrev: removed the check of no dependencies
- 06:32 AM Revision 49d364b8 (lustrec): comestic changes, removing useless logs
- 06:31 AM Revision 7b424fe6 (lustrec): z3 as an optional pacage in configure
- 02:19 AM Lustrec-Tests Revision ea143160 (lustrec-tests): Missing dep for ADA targets
- 01:53 AM Lustrec-Tests Revision 5d9f326b (lustrec-tests): Solving issue in the ADA test cases
- 01:01 AM Revision dc6e8512 (lustrec): Merge branch 'ada' into lustrec-seal
07/01/2019
- 03:14 PM Lustrec-Tests Revision 9bb9b710 (lustrec-tests): rapport de stage modèle word
06/27/2019
- 01:28 PM Lustrec-Tests Revision 7befce21 (lustrec-tests): base3_correct intégré et simulé ous vivado
Also available in: Atom