summaryrefslogtreecommitdiff
path: root/abstract/transform.ml
Commit message (Collapse)AuthorAgeFilesLines
* Acceptable heuristic.Alex Auvolat2014-07-111-1/+6
|
* Add heuristic...Alex Auvolat2014-07-101-6/+8
|
* Correct some bugs on clocks.Alex Auvolat2014-07-081-21/+36
|
* Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)Alex Auvolat2014-07-081-60/+62
|
* Cleanup.Alex Auvolat2014-07-081-0/+20
|
* New example ; minor fixes.Alex Auvolat2014-07-041-2/+4
|
* First implementation of resetting transitions.Alex Auvolat2014-07-041-16/+63
|
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-041-110/+125
|
* Simplifications && preparation for restart.Alex Auvolat2014-07-041-8/+14
|
* More verbosity ; adapt rfollow so that it can be provedAlex Auvolat2014-07-021-1/+1
|
* Adapt for real type with Apron ; not very efficient ATM.Alex Auvolat2014-07-011-28/+48
|
* Minor corrections.Alex Auvolat2014-06-261-0/+1
| | | | | | - Use correect clock scope in typing - De-activate multi-valuated domain for enumerate vars + var couples. - Add comment explaining why it doesn't work
* Many things, sorry for the mess.Alex Auvolat2014-06-261-94/+135
| | | | | | | | | | - 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)
* Differentiate pre witin different scopes.Alex Auvolat2014-06-251-0/+2
|
* Implementation of disjunction domain seems to work.Alex Auvolat2014-06-241-7/+7
|
* Not much. Still does not work very well.Alex Auvolat2014-06-201-23/+21
|
* Everything proved !!Alex Auvolat2014-06-191-32/+76
|
* Very buggy disjunction domain !Alex Auvolat2014-06-191-13/+50
|
* Did most of the boring stuff. Now, work on the abstract domain.Alex Auvolat2014-06-191-61/+101
|
* Do some typing ; support multiple pre in abstract interpretation.Alex Auvolat2014-06-191-26/+32
|
* Nice view of guarantees ; add half test, proved.Alex Auvolat2014-06-181-10/+59
|
* Add gilbreath suite ; booleans are not represented in a good way.Alex Auvolat2014-06-181-44/+62
|
* Abstract interpretation gives good results on the limiter example.Alex Auvolat2014-06-181-3/+3
|
* Some abstract interpretation does something now.Alex Auvolat2014-06-171-8/+49
|
* Add bindings to apron. Next : work on abstract interpret.Alex Auvolat2014-06-171-3/+1
|
* Write transformation of program into logical formula.Alex Auvolat2014-06-171-0/+203