New option to select github version of Z3Added Yojson dependency in lustrevSome progress on Cex generation
missing file
Zustre: timeout and slicing
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
Merge branch 'unstable' 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