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.

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

Move GlassBR Output DDs to IMs #3583

Merged
merged 33 commits into from
Aug 9, 2023
Merged

Conversation

samm82
Copy link
Collaborator

@samm82 samm82 commented Aug 2, 2023

Closes #3569; originated from #3259.

Copy link
Owner

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The code changes seem fine.

However: there's a lot of changes to the generated code (various things are moved around) which doesn't seem as good. So this shouldn't be merged as is, not without some real discussion about why things shifted around so much [it might be fine!]

Also, maybe a master merge is needed too? There are some changes to .json files, but these should all be gone.

@samm82
Copy link
Collaborator Author

samm82 commented Aug 3, 2023

As I made these changes, I tried my best to review the code changes; they seemed to be a logical consequence of the DD -> IM migration, but I figured I'd give @smiths a chance to review these changes before I went any deeper. I agree that a more in-depth investigation is in order, and will get around to it once I'm done the other preliminary work required to add the source information to #3259!

The .json files are still present due to the pending merge of #3553

@samm82
Copy link
Collaborator Author

samm82 commented Aug 6, 2023

I looked into the changes to stable and noticed these groups of changes:

Dependencies

Boiling down the dependencies of the IMs gives the following six groups, where the items in each group can be computed in any order. (Note that "X > _" means that the quantity only depends on values that are input or assumed, and "DD > _" means that the quantity is a DD, not an IM.) Looking at the side "Symbols" bar for Calculations.py and Control.py confirm that this ordering is preserved. (Side note: should we be ordering the IMs like this in the document? Follow up: if we figure out an appropriate ordering automatically when generating code, could this functionality be used to automatically sort the IMs?)

X > AR
X > GTF
X > h
DD > LDF
DD > q

LDF, h > Jtol
q, h, GTF > ~q

AR, ~q > J
AR, Jtol > ~qtol

LDF, J, h, > B
~qtol > NFL

B > Pb
NFL, GTF > LR

Pb, Pbtol > isSafePb
LR, q > isSafeLR

Input Parameters

A trivial change is that quantities that used to be DDs in the set values" step (see the table of required assignments) are no longer stored within inParams (see here) for an example. This affects h, GTF, and AR.

Input Constraints

Since AR is mainly used to calculate other values (i.e., J and $\hat{q}_\text{tol}$ and their dependencies), its constraints are treated as input constraints and can be found in the relevant table. However, now that it is no longer treated like an input when checking the constraints, meaning that its constraint checking code is lost. Obviously losing this is not ideal, so I have some ideas:

  1. Verify it as an output as part of Generate FR(s) for constraint violation #3523. Assuming that output verification happens after all the outputs are calculated, this means that every calculation will be performed even if AR is invalid, which is not ideal. This could potentially be made a future improvement if we go this route.
  2. Add an intermediate verification. This is kind of what is done already, but instead of just having input and output verification, we could add a verification requirement for intermediate values. Hooking this up to code generation could potentially be more involved (and might be another distraction for me), so I'm not sure how practical this is.
  3. Revisit what we really want GlassBR to output. When I initially started Generate “Functional Requirement” for “Output Values”  #3259, I just assumed that the outputs of GlassBR were "correct". Now, I'm realizing that may not be the case. In particular, AR shows up in the Required Assignments table, meaning that it will already get output as part of the FR Output-Values-and-Known-Values (even if this is not actually done yet; see Generate FR for outputting input and known values #3540). If enough quantities are not useful to be "final" outputs of the program (i.e., not part of Output-Values-and-Known-Values), then there may be no need to turn some of these DDs into IMs, including potentially AR! (Note that some DDs had to be moved to IMs so prevent cyclical imports.)

@samm82
Copy link
Collaborator Author

samm82 commented Aug 8, 2023

As an update to my previous comment, we decided to go with option 3 above: reverting the migration of DDs that would already be output by the FR Output-Values-and-Known-Values: AR, GTF, and h. This undid most of the side effects listed above, although the order of LR and Pb swapped for some reason. Most importantly, the constraint checking on AR returned!

@smiths
Copy link
Collaborator

smiths commented Aug 8, 2023

I'm not done reviewing the changes, but I have found something that we should either fix in this PR, or create a separate issue for. The problem actually predates the current changes, but looking at the changes highlights the previous mistake. The change I'd like to see is that the TMs aren't actually used anywhere. We don't have any consistency checks (that was the other potential project for you @samm82!), but if we did they would notice that the TMs aren't actually used for anything. The TMs are generic statements about safety. The corresponding IMs should refer to these TMs. The IMs take the generic safety TMs and refine them into specific safety requirements for GlassBR. The safety-related IMs should refer to their corresponding TMs.

@samm82
Copy link
Collaborator Author

samm82 commented Aug 8, 2023

I think at some point the TMs were referenced, but in a place where really the IMs should have been referenced - I made that switch at some point, but didn't realize it meant that the TMs were no longer used. I think I'll make an issue for it so that it doesn't hold up (a) this PR or (b) my work on testing 😅 unless you think it's the right mix of important and straightforward where I should attempt it in this PR.

@smiths
Copy link
Collaborator

smiths commented Aug 9, 2023

@samm82, yes please create a separate issue about the safety-related TRs not being refined by the IMs.

I like the changes to stable. I'll add my approval, although we should wait for approval from @JacquesCarette before merging.

@JacquesCarette JacquesCarette merged commit 85d5afd into master Aug 9, 2023
5 checks passed
@JacquesCarette JacquesCarette deleted the moveGlassBrOutputDDsToIMs branch August 9, 2023 18:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Move DDs that are outputs to be IMs in GlassBR
4 participants