10000 Getting cardinality from relations · Issue #69 · kenmcmil/ivy · GitHub

More Web Proxy on the site http://driver.im/

Getting cardinality from relations #69

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.

Sign up for GitHub

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

Jump to bottom

Open

jyao15 opened this issue Sep 14, 2022 · 0 comments

jyao15 commented

Consider the following protocol.

type node
relation active(N:node)
type int_t
interpret int_t -> int
individual num_active : int_t

after init {
    active(N) := false;
    num_active := 0;
}

action become_active(n:node) = {
    require ~active(n);
    active(n) := true;
    num_active := num_active + 1;
}

The protocol maintains two invariants

invariant num_active <= COUNT n WHERE active(n) is defined (i.e., total number of nodes)
invariant num_active = COUNT n WHERE active(n) is true (i.e., number of active nodes)

However, I cannot find a way to represent either number in Ivy. Does Ivy support reasoning about cardinality of types/relations?

The text was updated successfully, but these errors were encountered:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

0