Skip to content

Assumption Supported Trace Generation#2

Open
wfishell wants to merge 2 commits into
lou1306:masterfrom
wfishell:master
Open

Assumption Supported Trace Generation#2
wfishell wants to merge 2 commits into
lou1306:masterfrom
wfishell:master

Conversation

@wfishell

Copy link
Copy Markdown

Updates to the driver to support Assumption Based Trace generation. This takes in the assumption LTL formula alongside inputs which are critical to said assumption and generates a input.txt. It also takes in the rest of the atomic propositions and uses flip to generate them.

@wfishell

Copy link
Copy Markdown
Author

Note I need to double check that the output is using the txt driver and flip isn't assiging that as well. Will get to asap

@lou1306

lou1306 commented Sep 22, 2025

Copy link
Copy Markdown
Owner

Thank you for the PR, I appreciated how you reused the tools/hierarchies laying around in Hoax to do something new!

Can you please mark the fields that can take None as a value as Optional[T] instead of just T? That would solve some reports I get from mypy. (If you want to check the mypy results for yourself you can run uv run mypy . from the repo's root directory. Pay no mind to the 3 errors in hoax/hoa.py, it's something I have been trying to fix.)

Also, just a minor detail, but if you rename AssumptionExample.txt to README.md, then Github should automatically render it when you navigate to the examples/LilyDemo directory on a Web browser :)

@wfishell

Copy link
Copy Markdown
Author

Sounds good! Will make those changes. Will probably get to it later tonight if that is ok.

@lou1306

lou1306 commented Sep 22, 2025

Copy link
Copy Markdown
Owner

Of course, take all the time you need 👍🏻

@wfishell

Copy link
Copy Markdown
Author

just added the updates

@wfishell wfishell left a comment

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

Reviewed changes

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

Successfully merging this pull request may close these issues.

2 participants