-
Notifications
You must be signed in to change notification settings - Fork 7
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
Clock reduction fix #151
Clock reduction fix #151
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good overall!
I left a few comments, but they are quick fixes if you agree.
Nice catch on the change for the ConsistencyExecutor
, it is now instantiated exactly like the DeterminismExecutor
, which is great. When we eventually add the specification
and implementation
executors we should probably introduce a helper function as they will all four will share the exact same instantiation code in extract_system_rep.rs
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Still looks good :)
Before, the clock reduction could not handle queries such as
"refinement: A <= A" -i samples/json/AG
whereA
has unused clocks within it. It would panic, trying to remove clocks on the left side of the expression, tat where actually found on the right side. This PR provides a fix to that.Beyond that, when I created the tests, some other tests were panicking. This was because they expected an
Ok
fromcreate_executable_query
with a failure withing, but clock reduction compiles the system and returns the failure inErr
if one is found. The reason for this is because these tests usedConsistencyExecutor
, which has teh only struct implementingExecutableQuery
that took aSystemRecipe
and compiled the system itself instead of taking aTransitionSystemPtr
.Therefore, I have refactored that, and a helper-function (
json_run_query
) in the tests so we can return the failure when performing clock reduction, instead of when executing the query. This involved a good portion of refactoring (hence the size of the PR), however it is mostly adapting the usage of said helper function