We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
Hello, Ivy find a counter-example to the following invariant, which seems strange to me:
#lang ivy1.7 type pair_t = struct { x : bool, y : bool } type index object obj(i:index) = { individual p:pair_t after init { p.x := false; p.y := false; } export action act1 = { require p.x = false; p.y := true; } export action act2 = { require p.y = false; p.x := true; } invariant ~(p.x & p.y) }
The text was updated successfully, but these errors were encountered:
Using isolate obj instead of object obj seems to fix the problem.
isolate obj
object obj
Sorry, something went wrong.
No branches or pull requests
Hello, Ivy find a counter-example to the following invariant, which seems strange to me:
The text was updated successfully, but these errors were encountered: