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 #1221

Merged
merged 26 commits into from
Jul 10, 2024
Merged

Rasi generator #1221

merged 26 commits into from
Jul 10, 2024

Conversation

PBHTasche
Copy link
Contributor

@PBHTasche PBHTasche commented Jul 9, 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

  • Implemented automatic abstraction refinement for RASI generation
  • Implemented --dev-unsafe-optimization flag for improved performance at the cost of usability
  • Implemented text output for RASI generator
  • Enabled splitting RASI by location
  • Fixed some errors in VeSUV transformation
  • Added explicit entry point to VeSUV transformation

PBHTasche added 26 commits May 29, 2024 13:16
@PBHTasche
Made representation of multi-intervals deterministic
97fb61d 
Splitting states into certain components if possible to factor out uncertainties into the state space

Ignore indexed variables with negative index

Created the infrastructure for static scanning for relevant variables
@PBHTasche
Merge dev to rasi_generator
9621b90
@PBHTasche
Fixed missed merge
b8800af
@PBHTasche
Updated RASI generator for new types in node.scala
1fbe4e7
@PBHTasche
Created infrastructure for selecting new variables on the fly
b2de439
@PBHTasche
Improved handling of mutually dependent variable constraints
cf10256
@PBHTasche
Variable selection works in very limited manner
4d117a3
@PBHTasche
Enabled inferrence of min_advance as required variable
104e27a
@PBHTasche
Filter variables based on whether they locally split the state space
aee6772
@PBHTasche
Fixed VeSUV output stage; fixed output for multiple files
67ebc10
@PBHTasche
Added vesuv_entry to VeSUV output
e435b18
@PBHTasche
Started infrastructure for finding objects for each field
e66bcb2
@PBHTasche
Added textual output option for RASI
55b5407
@PBHTasche
Fixed variable naming for RASI output
596f073
@PBHTasche
Replaced 'main' method by vesuv entry point; did some cleanup
d1da31d
@PBHTasche
Fixed treatment of min_advance; fixed error with changing process det…
299da95 
…ection
@PBHTasche
Add option for splitting RASI
4c823fb
@PBHTasche
Merge dev and refactor transSubnodes
07cf0a0
@PBHTasche
Enabled printing multiple RASIs
c329300
@PBHTasche
Modified scheduler event update mechanism
eca0190
@PBHTasche
Remove printing of trivial scales for predicate applications
33e12d6
@PBHTasche
Add handling for member expression
d7d8972
@PBHTasche
Added --dev-unsafe-optimization option to sacrifice usability for per…
a421155 
…formance
@PBHTasche
When splitting RASI, filter by what the process associated with a spl…
806a9f9 
…itting variable can reach
@PBHTasche
Fixed VeSUV transformation with unused methods in the SystemC code
fb1b432
@PBHTasche
Merge dev into rasi_generator
6892187
@pieter-bos pieter-bos merged commit 20bc29f into dev Jul 10, 2024
15 of 19 checks passed
@pieter-bos pieter-bos deleted the rasi_generator branch July 10, 2024 08:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@pieter-bos pieter-bos pieter-bos approved these changes

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