Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools @ 0d79d0f3

# Date Author Comment
0d79d0f3 11/12/2018 02:06 AM Pierre-Loïc Garoche

First working version of switched system extraction for seal tool

a5dc55ca 11/09/2018 07:43 AM Pierre-Loïc Garoche

Restructuring code in SEAL

a742719e 11/08/2018 09:12 AM Pierre-Loïc Garoche

SEAL: compute the projection to switched systems. Some issues with intermediate variables and a better selection of split guard have to be addressed

a703ed0c 11/03/2018 12:03 AM Pierre-Loïc Garoche

Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.

b0c381d0 07/12/2018 04:04 PM Pierre-Loïc Garoche

Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal

fbc571e6 07/04/2018 04:06 PM Arnaud Dieumegard

Refactoring of vhdl data types

7d77632f 06/22/2018 06:24 PM Pierre-Loïc Garoche

Added two fresh vars counter and uid.
uid is a list of integer denoting the specific instance of a stateful/stateless node.

57d61d67 06/22/2018 11:24 AM Pierre-Loïc Garoche

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

fae1790f 06/21/2018 05:42 PM Arnaud Dieumegard

Added support for Process statements, signal assignment, If, Exit and Null sequential statements

d77323b8 06/15/2018 05:45 PM Arnaud Dieumegard

Added postprocessing for numeric literals

55963629 06/12/2018 05:10 PM Arnaud Dieumegard

Ongoing work on json vhdl to vhdl structure conversion

998766b4 06/11/2018 09:37 PM Pierre-Loïc Garoche

missing file

4300981b 06/11/2018 06:44 PM Pierre-Loïc Garoche

Zustre: timeout and slicing

3ca452f3 06/01/2018 04:12 PM Pierre-Loïc Garoche

Main lustrei

885b2896 05/31/2018 02:59 PM Xavier Thirioux

Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable

2f7c9195 05/30/2018 04:02 PM Pierre-Loïc Garoche

zustre progress. Issues with sliced predicates

3d3718ae 05/29/2018 08:59 PM Pierre-Loïc Garoche

package z3 to Z3 when using z3 github repo.

df00d682 05/29/2018 01:49 PM Pierre-Loïc Garoche

Adding input in MAIN fdecl

dbab1fe5 05/29/2018 12:09 AM Pierre-Loïc Garoche

[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result

9f3de818 05/18/2018 08:05 AM Pierre-Loïc Garoche

Some progress on zustre

51ec4e8c 04/18/2018 03:29 AM Pierre-Loïc Garoche

Try to debug the use of Z3 API. Still having troubles

ef609cc9 04/07/2018 12:55 AM Pierre-Loïc Garoche

Zustre: do not declare variables as Fixedpoint relations

8eeec77e 04/06/2018 11:56 PM Pierre-Loïc Garoche

Filtering out ERR and MAIN from the forall quantification

5778dd5e 04/06/2018 11:19 PM Pierre-Loïc Garoche

Some progress on zustre2

46cb4020 04/03/2018 05:02 PM Pierre-Loïc Garoche

zustre: missing basic ops

e4edf171 04/03/2018 04:38 PM Pierre-Loïc Garoche

Zustre backend

e17d3718 04/03/2018 11:28 AM Pierre-Loïc Garoche

Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal

6eda0c25 03/30/2018 11:40 PM Pierre-Loïc Garoche

Merge branch 'unstable' into lustrec-seal

8446bf03 03/30/2018 05:54 PM Pierre-Loïc Garoche

- Makefile: solved dependency problem when compiling include lusi
- Renamed type declarations as lustre_types and machine_code_types

ff2d7a82 03/29/2018 01:41 PM Pierre-Loïc Garoche

Ongoing work on zustre

bc86ee26 03/28/2018 10:41 AM Xavier Thirioux

Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable

c1785a55 03/28/2018 10:35 AM Pierre-Loïc Garoche

ongoing work on zustre backend

ad4774b0 03/15/2018 12:07 AM Pierre-Loïc Garoche

- Normalization parameters (alias and unfold_array) are now provided as parameter
- program type renamed as program_t
- Initiating the lustrev tool with dependencies to z3 and seal.

9c654082 02/13/2018 05:42 PM Pierre-Loïc Garoche

[lustresf] work in progress. Added global env with initial values

51a2c05a 02/01/2018 01:46 PM Xavier Thirioux

Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable

9ae027f8 12/21/2017 12:29 AM Pierre-Loïc Garoche

[stateflow] some progress, linking the parsed json to lustrec engine. Some variables are not yet typed. To investigate ...

e304cd81 12/14/2017 11:24 AM Xavier Thirioux

Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable

61e2b4b7 12/12/2017 03:17 PM Christophe Garion

Merge branch 'unstable-merge' into unstable

b06b7b77 12/12/2017 03:15 PM Christophe Garion

[lustresf] add Program constructor in model examples + sf_sem

b1af4f73 12/12/2017 02:51 PM Christophe Garion

[JSON] remove pretty-printing functions declarations in cPS_transformer

97b1a486 12/12/2017 12:37 PM Xavier Thirioux

Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable

72f666d3 12/12/2017 12:35 PM Xavier Thirioux

...

e0d6f1d1 12/12/2017 12:23 PM Pierre-Loïc Garoche

[lustresf] refactoring automata generation using Automata.ml functions

50ae9ab8 12/12/2017 12:10 PM Christophe Garion

simple conflict when merging unstable and json-parser

2a4992a1 12/12/2017 10:29 AM Pierre-Loïc Garoche

[lustresf] Some progress: automaton compiles but not when preprocessed

050147ec 10/13/2017 02:58 PM Christophe Garion

json-parser: correct parser for regex for real variables with e|E

befd32b5 10/13/2017 02:58 PM Christophe Garion

json-parser: add test for real variable with e|E

d8abc19b 10/13/2017 11:18 AM Christophe Garion

json-parser: correct bug on real variables value

cbfee4a3 10/13/2017 11:16 AM Christophe Garion

json-parser: add string_of_XXX functions for assertions

c3d8313d 10/12/2017 03:36 PM Christophe Garion

json-parser: test exception for variables

89ac5599 10/11/2017 02:26 PM Christophe Garion

json-parser: switch arguments for assert_equal (expected/actual)

0c0b0aff 10/11/2017 02:25 PM Christophe Garion

json-parser: use JSON_parse_error exception

5c0d6e4e 10/10/2017 10:54 PM Christophe Garion

json-parser: more tests with single variables

2b95979d 10/10/2017 05:39 PM Christophe Garion

json-parser: change variables names in tests

0291fcfd 10/10/2017 05:37 PM Christophe Garion

json-parser: add test for boolean variable true

f5c1e4c1 10/10/2017 05:33 PM Christophe Garion

json-parser: refactor first test

550e6a83 10/10/2017 05:30 PM Christophe Garion

json-parser: first unit test for JSON parser (variables)

30fef623 10/10/2017 05:29 PM Christophe Garion

json-parser: clean packages and _tags.in

430dc9ee 10/06/2017 02:57 PM Christophe Garion

json-parser: replace assert with exceptions

921230e6 10/06/2017 02:33 PM Christophe Garion

json-parser: clean files names and directories

5a71ed25 10/06/2017 02:21 PM Christophe Garion

json-parser: use Logs and Cmdliner librairies

bbfbc15a 10/05/2017 02:20 PM Christophe Garion

json-parser: remove Const_bool and use Const_tag

57ecad58 10/03/2017 12:01 PM Christophe Garion

parser-json: clean main program + add pp for vars

37290ede 10/03/2017 10:47 AM Christophe Garion

parser-json: correct parsing of real constants for variables

04396cc7 10/02/2017 05:55 PM Christophe Garion

parser-json: add variables in parsing

eb70bae5 09/26/2017 03:38 PM Christophe Garion

parser-json: final version of parser with new types

15a6823b 09/25/2017 11:15 AM Christophe Garion

TMerge branch 'unstable' into json-parser

68601cf5 09/23/2017 10:26 AM Xavier Thirioux

bug correction: each var_decl must be unique and not shared as a global var

c5d45c13 09/22/2017 05:43 PM Pierre-Loïc Garoche

[lustresf]: tuple of false values for initial state

74ca6b61 09/22/2017 05:38 PM Pierre-Loïc Garoche

A fresh option to print with declared types instead of inferred ones

bad7b67a 09/22/2017 05:20 PM Christophe Garion

parser-json: first steps to integrate JSON parser

69c96b6c 09/22/2017 04:39 PM Pierre-Loïc Garoche

lustresf: Better construction of lustre ast. Still more work to be done.

93119c3f 09/21/2017 01:48 PM Pierre-Loïc Garoche

Moved stateflow tool in src/tool
Updated the makefile to compile lustresf
Not working yet