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

Model should consider all type dependencies #1074

Closed
rami3l opened this issue Jun 16, 2022 · 4 comments · Fixed by #1075
Closed

Model should consider all type dependencies #1074

rami3l opened this issue Jun 16, 2022 · 4 comments · Fixed by #1075
Assignees
Labels
model Related to model package (e.g., model verification)

Comments

@rami3l
Copy link
Contributor

rami3l commented Jun 16, 2022

Now it's possible to have manually-generated Models without all the type dependencies in the Model itself.

For example, when [t, v, m] in L161 is changed to [v, m] in the snippet below:

https://github.com/Componolit/RecordFlux/blob/625853660cfa6074d2862be14bd4729cf8855a27/tests/unit/model/model_test.py#L157-L161

AFAIK, omitting dependencies in the Model itself won’t affect its functionality in PyRFLX. However, this might cause problems when exporting such Models, since the exported files will lack necessary type declarations which will affect their validity.

Ideally, when exporting a Model to .rflx files, no manual management of type dependencies should be required, i.e. RecordFlux should be able to automatically find all dependencies and add them to the exported files.

In the example above, that would mean the exported files should always contain [t, v, m] regardless of whether t is actually included in the list, because v and m depends on t.

@treiher
Copy link
Collaborator

treiher commented Jun 16, 2022

I think parsing the generated specification should lead to an identical model. So I would propose to add this automatic dependency resolution to the constructor of Model instead of to the create_specifications method. In your example, when creating a model by Model([v, m]), t will be automatically added to the Model._types. By this, Model([v, m]) and Model([t, v, m]) will lead to the equal model.

@rami3l
Copy link
Contributor Author

rami3l commented Jun 16, 2022

@treiher
Thanks! Indeed, this approach seems more idiomatic to me; however, there are two main concerns that might arise with this proposition:

  • Model._types is a list, and IIRC the order of items counts in that list. If I add t to the list, where should I add it to make the new Model make sense to RecordFlux?
  • Recursively searching for type dependencies could introduce duplicates in the list in no time. Again, how to eliminate duplicates so that the new Model makes sense, and gets generated deterministically?

@treiher
Copy link
Collaborator

treiher commented Jun 16, 2022

  • Model._types is a list, and IIRC the order of items counts in that list. If I add t to the list, where should I add it to make the new Model make sense to RecordFlux?

I think that can be solved algorithmically. When sequentially analyzing the types, the types which are not yet part of the model, but are dependencies, are added in front of the current analyzed type.

  • Recursively searching for type dependencies could introduce duplicates in the list in no time. Again, how to eliminate duplicates so that the new Model makes sense, and gets generated deterministically?

A simple option would be removing duplicates in the resulting list after the dependency resolution. Just keep the first instance of a type - the unique function could be used for that.

@rami3l rami3l changed the title Model.create_specifications should consider all type dependencies Model should consider all type dependencies Jun 16, 2022
@rami3l rami3l added the model Related to model package (e.g., model verification) label Jun 16, 2022
@rami3l
Copy link
Contributor Author

rami3l commented Jun 16, 2022

When sequentially analyzing the types, the types which are not yet part of the model, but are dependencies, are added in front of the current analyzed type.

I think it's probably better not to make the distinction according to whether the type dependency is in the Model._types list or not, since we are deduplicating in the end anyway.

rami3l added a commit that referenced this issue Jun 21, 2022
Apart from the fix for #1074, this commit also includes the following changes:

* Fix `split_disjunctions` in `Validator._create_model`
* (BREAKING) Make `Type.*dependencies` list deps in postorder
* Correct the definition of `Refinement.*dependencies`
rami3l added a commit that referenced this issue Jun 21, 2022
Apart from the fix for #1074, this commit also includes the following changes:

* Fix `split_disjunctions` in `Validator._create_model`
* (BREAKING) Make `Type.*dependencies` list deps in postorder
* Correct the definition of `Refinement.*dependencies`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
model Related to model package (e.g., model verification)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants