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

Extend the tool to support the latest functionality of the library #15

Open
3 of 4 tasks
ondrej33 opened this issue Dec 26, 2023 · 1 comment
Open
3 of 4 tasks

Comments

@ondrej33
Copy link
Member

ondrej33 commented Dec 26, 2023

The last few PRs and modifications focused on the library side of the project. However, we should also provide these updates as a part of the model-checking tool. This comes together with a restructuring and refactoring of the code related to the tool.

However, bear in mind there are now also Python bindings, and it is sometimes more practical to use them directly.
Therefore, implement just what really seems to be missing. Also, implement the functionality in a way that some of it can potentially be reused in Python code.

The changes to the tool should reflect the following:

  • Add an option to dump the resulting BDDs to a zip archive.
  • Add an option to evaluate the extended version of HCTL formulae (with wild-card properties and variable domain restrictions). In this mode, the tool must load a "context" for the wild cards, i.e. the raw sets they will evaluate to. This can be done by loading a zip bundle of BDDs. It might be worth it to match the input/output format of the tool as much as possible.
  • Remove the redundant model_format argument and use automatic model parsing as shown in e72a86a
  • Decide on the general form of input loading. Do we want to load different inputs (such as model, properties, etc.) individually, as a single zip, or both?

Better code documentation and refactoring should follow, too.

@ondrej33
Copy link
Member Author

The first three points are addressed by #17. The issue regarding input format remains.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant