[seal] delt with Merge and when[printer] more kind2 syntax
Produce true/false statements as constants
scheduling now report unused vars and remove their definition instead of stopping processing.
Seal: solved issue with guards merging
Sorting expressions: less bugs
valid _verif node for seal-export lustre
Seal export lustre
Contract printer cocospec
Export cocospec contract
Output folder for seal-extract
Seal-export to a new file
seal-export: produce the output as well. Could be simpler
Seal-extract: first serious version. Guards are gathered as a single expression
Updated version seal-extract
Working version of seal-extract. Heavy load on z3.TODO: improvement through memoization
Better extraction in lustrev-seal
Zustre: Bug solved in const injection for reals
lustrev seal: ongoing work on extraction as dynamical system. Still not working yet
Minor modif on seal
Reorganizing folders
Some progress on compiling cocospec contract.Contract resolution still need to be done as well as dealing with the machine code level and so on.
Major refreshing of machine generation
Unified compilation of lusi and lus filesDifferent parsers yet but shared process.In case of lusi input the C backend is bypassed since the .h is generated from the lusic and no C code should be generated since it may overwrite existing manually written code...
Fixing issues with changes in machine code
Merge branch 'unstable' into lustrec-seal
Merlin files
First working version of switched system extraction for seal tool
Restructuring code in SEAL
SEAL: compute the projection to switched systems. Some issues with intermediate variables and a better selection of split guard have to be addressed
Preprocess the selected node in seaL BACKEND: focus on memories and perform node slicing.
Merge branch 'vhdl' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
Refactoring of vhdl data types
Added two fresh vars counter and uid.uid is a list of integer denoting the specific instance of a stateful/stateless node.
New option to select github version of Z3Added Yojson dependency in lustrevSome progress on Cex generation
Added support for Process statements, signal assignment, If, Exit and Null sequential statements
Added postprocessing for numeric literals
Ongoing work on json vhdl to vhdl structure conversion
missing file
Zustre: timeout and slicing
Main lustrei
Merge branch 'unstable' of https://cavale.enseeiht.fr/git/lustrec into unstable
zustre progress. Issues with sliced predicates
package z3 to Z3 when using z3 github repo.
Adding input in MAIN fdecl
[lustrev] fixed some issues when calling Z3. Seems working for the moment: basic call to Z3 and sat/unsat result
Some progress on zustre
Try to debug the use of Z3 API. Still having troubles
Zustre: do not declare variables as Fixedpoint relations
Filtering out ERR and MAIN from the forall quantification
Some progress on zustre2
zustre: missing basic ops
Zustre backend
Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal
- Makefile: solved dependency problem when compiling include lusi- Renamed type declarations as lustre_types and machine_code_types
Ongoing work on zustre
ongoing work on zustre backend
- 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.
[lustresf] work in progress. Added global env with initial values
[stateflow] some progress, linking the parsed json to lustrec engine. Some variables are not yet typed. To investigate ...
Merge branch 'unstable-merge' into unstable
[lustresf] add Program constructor in model examples + sf_sem
[JSON] remove pretty-printing functions declarations in cPS_transformer
...
[lustresf] refactoring automata generation using Automata.ml functions
simple conflict when merging unstable and json-parser
[lustresf] Some progress: automaton compiles but not when preprocessed
json-parser: correct parser for regex for real variables with e|E
json-parser: add test for real variable with e|E
json-parser: correct bug on real variables value
json-parser: add string_of_XXX functions for assertions
json-parser: test exception for variables
json-parser: switch arguments for assert_equal (expected/actual)
json-parser: use JSON_parse_error exception
json-parser: more tests with single variables
json-parser: change variables names in tests
json-parser: add test for boolean variable true
json-parser: refactor first test
json-parser: first unit test for JSON parser (variables)
json-parser: clean packages and _tags.in
json-parser: replace assert with exceptions
json-parser: clean files names and directories
json-parser: use Logs and Cmdliner librairies
json-parser: remove Const_bool and use Const_tag
parser-json: clean main program + add pp for vars
parser-json: correct parsing of real constants for variables
parser-json: add variables in parsing
parser-json: final version of parser with new types
TMerge branch 'unstable' into json-parser
bug correction: each var_decl must be unique and not shared as a global var
[lustresf]: tuple of false values for initial state
A fresh option to print with declared types instead of inferred ones
parser-json: first steps to integrate JSON parser
lustresf: Better construction of lustre ast. Still more work to be done.
Moved stateflow tool in src/toolUpdated the makefile to compile lustresfNot working yet