Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for error automata in Automizer #182

Closed
schillic opened this issue May 19, 2017 · 3 comments
Closed

Add support for error automata in Automizer #182

schillic opened this issue May 19, 2017 · 3 comments
Assignees
@Heizmann @schillic
Labels
Automizer feature

Comments

@schillic
Copy link
Member

An error automaton generalizes an error, just as an interpolant automaton generalizes a reason for infeasibility.
By taking the difference of the abstraction and an error automaton we can continue with the analysis "up to this error".

There have already been three commits related to this issue: 1, 2, 3
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - refactoring and cleanup in CEGAR loop
6e0a217
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - added ErrorTraceContainer; corrected analysis result
cb5dfeb
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - report counterexample in all cases (timeout, unknown)
3218086
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - report error trace statistics, e.g., precondition
0dd35f1
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - extracted error automaton construction to class
dab82c9
schillic added a commit that referenced this issue May 20, 2017
@schillic
#182 - first steps for constructing alternative error automaton
1dce583
schillic added a commit that referenced this issue May 22, 2017
@schillic
#182 - corrected automaton predicates; added TODOs
5c2baf6
schillic added a commit that referenced this issue May 22, 2017
@schillic
#182 - added HoareTripleChecker (not working yet)
ecd4b67
schillic added a commit that referenced this issue May 26, 2017
@schillic
#182 - compute internal transitions correctly
ab127c1
Heizmann added a commit that referenced this issue May 29, 2017
@Heizmann
#182 - support for call and return
5b5d11d
schillic added a commit that referenced this issue Jun 1, 2017
@schillic
#182 - pass enhanced error automaton to CEGAR loop
1505645
schillic added a commit that referenced this issue Jun 1, 2017
@schillic
#182 - inline method
f084259
schillic added a commit that referenced this issue Jun 1, 2017
@schillic
#182 - pass predicate unifier directly
7ae3c45
schillic added a commit that referenced this issue Jun 2, 2017
@schillic
#182 - add False predicate/state
658aa79
schillic added a commit that referenced this issue Jun 2, 2017
@schillic
#182 - commented assertions
a623213
schillic added a commit that referenced this issue Jun 2, 2017
@schillic
#182 - do not print output for error automaton
6eb301e
schillic added a commit that referenced this issue Jun 2, 2017
@schillic
#182 - fix: use correct error automaton versions
593c924
schillic added a commit that referenced this issue Jun 2, 2017
@schillic
#182 - StraightLineInterpolantAutomatonBuilder: option to make all st…
f22d5a9 
…ates accepting
schillic added a commit that referenced this issue Jun 5, 2017
@schillic
#182 - log messages
02e0ecb
schillic added a commit that referenced this issue Jun 6, 2017
@schillic
#182 - make all error automaton states initial (except 'False')
5767fce
schillic added a commit that referenced this issue Jun 6, 2017
@schillic
#182 - refactoring/cc fix
ebc50d0
schillic added a commit that referenced this issue Jun 6, 2017
@schillic
#182 - added intersection with SP
8cfaf8a
schillic added a commit that referenced this issue Jun 6, 2017
@schillic
#182 - unify predicates in error automaton
1a34d16
schillic added a commit that referenced this issue Jun 7, 2017
@schillic
#182 - fix: do not add state twice
9f79954
schillic added a commit that referenced this issue Jun 7, 2017
@schillic
#182 - code and debug simplifications
b58d099
schillic added a commit that referenced this issue Jun 27, 2017
@schillic
#182 - allow that error precondition is null
2394bcb
schillic added a commit that referenced this issue Jun 27, 2017
@schillic
#182 - added danger automaton skeleton
33c803b
schillic added a commit that referenced this issue Jun 27, 2017
@schillic
#182 - more danger automaton stuff
5cf4068
schillic added a commit that referenced this issue Jun 27, 2017
@schillic
#182 - removed old TODOs
fc4e057
schillic added a commit that referenced this issue Jun 27, 2017
@schillic
#182 - refactoring of error automata; danger automata statistics
67d1c90
schillic added a commit that referenced this issue Jun 28, 2017
@schillic
#182 - split code into smaller methods
b4fab45
schillic added a commit that referenced this issue Jun 28, 2017
@schillic
#182 - renaming
6c062a8
schillic added a commit that referenced this issue Jun 28, 2017
@schillic
#182 - compute error precondition in danger automaton
a99c0bd
schillic added a commit that referenced this issue Jun 29, 2017
@schillic
#182 - use IsFinite check; log effective automaton enhancement
6d0f1ef
schillic added a commit that referenced this issue Jun 29, 2017
@schillic
#182 - StraightLineAutomaton had wrong number of states
e99a42e
schillic added a commit that referenced this issue Jun 30, 2017
@schillic
#182 - fixed 'missing statistics' error
84b4e00
schillic added a commit that referenced this issue Jun 30, 2017
@schillic
#182 - added aggregated fault localization for all error traces
40888d6
schillic added a commit that referenced this issue Jul 1, 2017
@schillic
#182 - examples
c05a241
schillic added a commit that referenced this issue Jul 1, 2017
@schillic
#182 - report number of statements
b17d9d4
schillic added a commit that referenced this issue Jul 1, 2017
@schillic
#182 - fault localization can publish statistics
df13c66
schillic added a commit that referenced this issue Jul 1, 2017
@schillic
#182 - report fault localization statistics
55872af
schillic added a commit that referenced this issue Jul 2, 2017
@schillic
#182 - initialize enhancement type with 'unknown' (fixes NPE)
1bd74c1
schillic added a commit that referenced this issue Jul 4, 2017
@schillic
#182 - example
9232881
schillic added a commit that referenced this issue Jul 6, 2017
@schillic
#182 - do fault localization in each iteration
7d57fb7
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - report UNSAFE if timeout occurs and error trace was found
1dcbc7a
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - report total number of statements
3094f0c
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - report number of relevant statements
d3c0cb6
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - changed benchmark result order
a2fed38
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - report total fault localization time
a9d4ee2
schillic added a commit that referenced this issue Jul 7, 2017
@schillic
#182 - fix: missing aggregation; add logger output
0ad4ddd
@schillic
Copy link
Member Author

schillic commented Nov 1, 2017

@Heizmann: Can we close this?

@Heizmann
Copy link
Member

Heizmann commented Nov 1, 2017

I don't know.

@schillic
Copy link
Member Author

schillic commented Nov 1, 2017

Then we can :)

@schillic schillic closed this as completed Nov 1, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Heizmann Heizmann

@schillic schillic

Labels
Automizer feature
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@Heizmann @schillic