summaryrefslogtreecommitdiff
path: root/abstract/abs_interp_edd.ml
Commit message (Collapse)AuthorAgeFilesLines
* Acceptable heuristic.Alex Auvolat2014-07-111-5/+5
|
* Add heuristic...Alex Auvolat2014-07-101-2/+2
|
* Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!Alex Auvolat2014-07-091-11/+17
|
* Add simplification pass && better heuristic for BDDs based on ternaries.Alex Auvolat2014-07-091-0/+31
|
* Correct some bugs on clocks.Alex Auvolat2014-07-081-7/+12
|
* Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)Alex Auvolat2014-07-081-0/+5
|
* Cleanup.Alex Auvolat2014-07-081-239/+17
|
* Implement stand-alone EDDsAlex Auvolat2014-07-081-2/+0
|
* Adapt domain with non-EDD disjunctions ; it doesn't work very well !Alex Auvolat2014-07-041-6/+8
|
* New example ; minor fixes.Alex Auvolat2014-07-041-3/+8
|
* 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