search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
709 stars 124 forks source link

`disj` is ignored for relations #78

Closed hwayne closed 5 years ago

hwayne commented 5 years ago

Spec:

sig Foo {
    foos: Foo -> Foo
}

pred bar[f: Foo] {
    some disj a, b : f.foos { a = b }
}

run {some f: Foo | f.bar}

Expected behavior: predicate should be trivially unsatisfiable.

Actual behavior: Analyzer finds an instance, ignoring the disj.

Notes: Alloy 5. Using e1 != e2 as an additional clause causes the analyzer to behave correctly.

aleksandarmilicevic commented 5 years ago

Not a bug.

The semantics of disj a, b is no a & b (and not a != b). With that in mind, the following is a satisfying instance for your model:

this/Foo={Foo$0}
this/Foo<:foos={}
skolem $f={Foo$0}
skolem $bar_a={}
skolem $bar_b={}

Clearly, both no a & b and a = b are true when both a and b are empty.

hwayne commented 5 years ago

I'm not sure I understand. It gives me the following counterexample:

this/Foo={Foo$0}
this/Foo<:foos={Foo$0->Foo$0->Foo$0}

So foos is nonempty but it still finds a matching example. It also doesn't show $bar_a$ or $bar_b$ in the output. Replacing the disj with some a, b : f.foos { (no a & b) and a = b } causes the same results, though the matching instance is not the first instance (which is empty as expected).