summaryrefslogtreecommitdiff
path: root/abstract
Commit message (Collapse)AuthorAgeFilesLines
* First implementation of resetting transitions.Alex Auvolat2014-07-042-27/+80
|
* Use LAST instead of NEXT (only EDD implementation works at the moment)Alex Auvolat2014-07-044-154/+164
|
* Simplifications && preparation for restart.Alex Auvolat2014-07-041-8/+14
|
* 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-022-25/+38
|
* Fix non-termination issue in EDDsAlex Auvolat2014-07-022-75/+90
|
* More verbosity ; adapt rfollow so that it can be provedAlex Auvolat2014-07-023-3/+15
|
* Small changes in Graphwiz export : same vars at same level.Alex Auvolat2014-07-011-0/+11
|
* Adapt for real type with Apron ; not very efficient ATM.Alex Auvolat2014-07-016-74/+104
|
* 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-304-109/+119
|
* More work on EDDs.Alex Auvolat2014-06-272-155/+318
|
* Minor corrections.Alex Auvolat2014-06-262-0/+10
| | | | | | - 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-263-179/+579
| | | | | | | | | | - 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-252-51/+138
|
* Begin implementation of EDD ; SCA implemented.Alex Auvolat2014-06-252-4/+504
|
* Differentiate pre witin different scopes.Alex Auvolat2014-06-251-0/+2
|
* Add command line option : verbose chaotic iterations.Alex Auvolat2014-06-251-12/+17
|
* Implementation of disjunction domain seems to work.Alex Auvolat2014-06-248-531/+590
|
* Not much. Still does not work very well.Alex Auvolat2014-06-206-59/+56
|
* Everything proved !!Alex Auvolat2014-06-193-41/+88
|
* Actually, it works.Alex Auvolat2014-06-192-8/+21
|
* Very buggy disjunction domain !Alex Auvolat2014-06-195-49/+363
|
* Did most of the boring stuff. Now, work on the abstract domain.Alex Auvolat2014-06-195-106/+187
|
* Isolate numerical part of domain. Next: isolate numerical part of equations.Alex Auvolat2014-06-197-51/+124
|
* Do some typing ; support multiple pre in abstract interpretation.Alex Auvolat2014-06-192-92/+51
|
* Presentation changes.Alex Auvolat2014-06-181-15/+26
|
* Nice view of guarantees ; add half test, proved.Alex Auvolat2014-06-184-37/+120
|
* RetabAlex Auvolat2014-06-182-44/+50
|
* Add gilbreath suite ; booleans are not represented in a good way.Alex Auvolat2014-06-185-60/+105
|
* Abstract interpretation gives good results on the limiter example.Alex Auvolat2014-06-184-34/+31
|
* Pretty printing.Alex Auvolat2014-06-188-66/+147
|
* Add intervals domain ; some interesting analysis works.Alex Auvolat2014-06-186-17/+434
|
* Some abstract interpretation does something now.Alex Auvolat2014-06-174-10/+189
|
* Add bindings to apron. Next : work on abstract interpret.Alex Auvolat2014-06-174-3/+183
|
* Write transformation of program into logical formula.Alex Auvolat2014-06-173-25/+389
|
* Add AST for logical formula.Alex Auvolat2014-06-172-0/+80