summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_edd.ml
Commit message (Collapse)AuthorAgeFilesLines
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-041-37/+36
|
* Changes to parser ; EDD optimisations ; test cases.Alex Auvolat2014-07-031-71/+80
|
* New algorithm for variable ordering based on FORCE.Alex Auvolat2014-07-031-8/+85
|
* Add message when a step goes on BOT, ie. contradiction in assumes.Alex Auvolat2014-07-021-12/+21
|
* Fix non-termination issue in EDDsAlex Auvolat2014-07-021-64/+83
|
* More verbosity ; adapt rfollow so that it can be provedAlex Auvolat2014-07-021-1/+11
|
* Small changes in Graphwiz export : same vars at same level.Alex Auvolat2014-07-011-0/+11
|
* Not much : find acceptably good ordering for variables.Alex Auvolat2014-07-011-55/+28
|
* Finish up EDDsAlex Auvolat2014-07-011-43/+98
|
* Implement chaotic iterations on EDDs. Global widening is missing.Alex Auvolat2014-06-301-109/+329
|
* Reached interesting point in BDD implementation.Alex Auvolat2014-06-301-109/+114
|
* More work on EDDs.Alex Auvolat2014-06-271-145/+313
|
* Many things, sorry for the mess.Alex Auvolat2014-06-261-85/+101
| | | | | | | | | | - Implement two new enumeration domains (they don't bring us much) : multi valuation for variables ; multi valuation for variables and pairs of variables (not really sure it works) - Make it so that the number of init/time variables is reduced (do not create new init/time variables on node instanciation, only inside activate blocks and automaton states) - Some work on EDD (it is currently broken and does not compile)
* Implement a few things. Tomorrow: optimizations.Alex Auvolat2014-06-251-36/+119
|
* Begin implementation of EDD ; SCA implemented.Alex Auvolat2014-06-251-0/+500