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

Revert change in quotient rule #172

Open
magoorden opened this issue May 31, 2023 · 3 comments
Open

Revert change in quotient rule #172

magoorden opened this issue May 31, 2023 · 3 comments

Comments

@magoorden
Copy link

A while ago a 'bug' was fixed in the Reveaal engine for the quotient operator rule 5 where
image was changed into
image. The actual bug was in the theory, so this change needs to be reverted.

The full rule 5 reads now as
Screenshot 2023-05-31 at 14 04 30

@seblund
Copy link
Member

seblund commented May 31, 2023

It was actually never merged into the main branch, as it seemed like we were undecided on the intended behaviour at the time. The changes are in a draft pull request (PR #146), I will link to this issue in the pull request so we can make sure everything is correct before it is eventually merged.

@magoorden
Copy link
Author

This afternoon we (Florian and I) were using the latest release of Ecdar and it did not produce the right guard. Therefore, I assumed that it was in a merge request that was already merged.

@magoorden
Copy link
Author

magoorden commented May 31, 2023

This is the quotient you should eventually get when you do spec \\ administration for the university example from the paper (note that the university example from the paper has an additional edge in the administration than the default one supplied by the examples in the tool).

Screenshot 2023-05-31 at 14 16 20

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

2 participants