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

Rasi generator #1208

Merged
merged 34 commits into from
May 27, 2024
Merged

Rasi generator #1208

merged 34 commits into from
May 27, 2024

Conversation

PBHTasche
Copy link
Contributor

@PBHTasche PBHTasche commented May 24, 2024 •
edited
Loading

Checklist:

  • The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.

PR description

  • Bug fixes and performance optimizations for RASI generator
  • Parameter and path condition tracking
  • Infrastructure for automatic variable selection mechanism
  • Improved documentation

@PBHTasche
Fixed an error in equality handling of unsupported data types
553751c
@PBHTasche
Fixed an error in handling of collection operations
3d5d6c1
@PBHTasche
Added option to track sequence sizes
efc29c1
@PBHTasche
Fixed an error when the set of indexed variables pointing to an updat…
edd4ea7 
…ed collection was empty
@PBHTasche
Added handling of size variables in conditions
a564a1f
@PBHTasche
Fixed a bug where integers that could be unequal would not be conside…
1d79dcf 
…red such
@PBHTasche
Added progress messages to CFG generation
8736870
@PBHTasche
Fixed an error where an empty uncertain sequence would have an empty …
c556cb1 
…length rather than 0
@PBHTasche
Sorted output expressions by variable to make debugging easier
2e9dba4
@PBHTasche
Merge branch 'dev' into rasi_generator
5143b06
@PBHTasche
Added path condition for parameters to enforce constant parameters wi…
4c0598b 
…thin a path
@PBHTasche
Fixed an error where tracked sequence sizes couldn't change in postco…
4891461 
…nditions
@PBHTasche
Removed unjustified knowledge of sequence lengths from state
bf0a9de
@PBHTasche
Started adding infrastructure to keep track of variables influencing …
ea658fa 
…overapproximation
@PBHTasche
Implemented variable annotations to RASI edges
9b2ae10
@PBHTasche
Started implementation of variable selection for assumptions
43755ad
@PBHTasche
Added a filter in assumption handling for states that would be imposs…
5bf6543 
…ible in combination with the concrete state
@PBHTasche
Started implementing variable selection process
56ce836
@PBHTasche
Improved and repaired documentation
c568289
@PBHTasche
Fixed typo
88bb641
@PBHTasche
Simplified implementation of constraint map
80be9fa
@PBHTasche
Added support for equations between simple arithmetic expressions; im…
79c37dd 
…plemented variable selection
@PBHTasche
Fixed some errors in the variable selection
030f95c
@PBHTasche
Fixed atomic step for branches of varying length; ignore object varia…
3376c3c 
…bles for variable selection
@PBHTasche
Filtered out processes that do not affect the tracked variables
7f4d40f
@PBHTasche
Add lock/unlock around fork/join statements in VeSUV scheduler
e95b0cd
@PBHTasche
Extended atomic blocks if no changes to variables have occurred
d0e94ea
@PBHTasche
Fixed an error where exploration would loop indefinitely
280c628
@PBHTasche
Improved path condition generation for tracked variables; removed emp…
69a2253 
…ty intervals from multiintervals
@PBHTasche
Changed comparison of abstract valuations to be more robust
b6c2bc1
@pieter-bos pieter-bos merged commit af4fad7 into dev May 27, 2024
8 of 10 checks passed
@pieter-bos pieter-bos deleted the rasi_generator branch May 27, 2024 12:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@PBHTasche @pieter-bos