CODEWITHSUNDEEP
alloy
Guillermo Pantaleo
Guillermo Pantaleo

Reputation: 21

consistency check with contradictory facts in Alloy

I do not understand how facts in Alloy work. In this small example there is two contradictory facts, but the predicate testWithoutParameters finds an instance (not expected) unlike the predicate testWithParameters that do not (expected). Both asserts not find counterexamples when they should do it. Where is the error in my interpretation? Deputy code and the output of execution.

sig A{
    aset: set B
}

sig B{
    bset: set B
}

fact Rule_1{
    all a: A |
    #a.aset < 3
}

fact Rule_2{
    all a: A |
    #a.aset > 3
}

pred testWithoutParameters[]{
    all a:A |
    #a.aset = 3
}

pred testWithParameters[a:A, b:B]{
    #a.aset = 3
}

assert test_aset{
    all a:A |
    {
        #a.aset = 3
    }
}

assert testWithoutSense{
    all a: A |
    #a.aset > 3 and #a.aset < 3
}

run testWithParameters for 10
run testWithoutParameters for 10
check test_aset for 10
check testWithoutSense for 10

Executing "Run testWithParameters for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2910 vars. 240 primary vars. 6294 clauses. 14ms. No instance found. Predicate may be inconsistent. 3ms.

Executing "Run testWithoutParameters for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2602 vars. 220 primary vars. 5499 clauses. 14ms. . found. Predicate is consistent. 21ms.

Executing "Check test_aset for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2834 vars. 230 primary vars. 6162 clauses. 14ms. No counterexample found. Assertion may be valid. 3ms.

Executing "Check testWithoutSense for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2844 vars. 230 primary vars. 6191 clauses. 13ms. No counterexample found. Assertion may be valid. 7ms.

4 commands were executed. The results are: #1: No instance found. testWithParameters may be inconsistent. #2: .testWithoutParameters is consistent. #3: No counterexample found. test_aset may be valid. #4: No counterexample found. testWithoutSense may be valid.

Upvotes: 2

Views: 334

Answers (1)

wmeyer
wmeyer

Reputation: 3496

Take a look at the solutions to testWithoutParameters: the set A is always empty. Universally quantified formulas are always true for empty sets, so the contradictions do not matter.

testWithParameters on the other hand contains the implicit fact that there is at least one element in A: the parameter a. But there can be no a that fulfills the contradicting facts, so there is no solution for this predicate.

Edit: No counterexample for testWithoutSense is found for the same underlying reason. Because of the contradicting Facts Rule_1 and Rule_2, your model is always constrained to contain no elements in A. With an empty A, the assertion testWithoutSense is trivially true.

Upvotes: 3

Related Questions