Alloy incorrectly evaluates predicate (I think)

[edmcman]

Above is a snippet from the Evaluator in an Alloy model. Since ran[InitContext$0.initializers].exp includes VarLvalue$0 and check_ctx[Program.global_vars, VarLvalue$0] is false, I believe that means that check_ctx[Program.global_vars, ran[InitContext$0.initializers].exp] should be false as well. If that is not true, please set me straight because I am very confused!

I can provide the model and solution file if this is indeed a bug.

[pkriens]

Well, it depends on check_ctx, doesn't it?

     enum V { A, B }
     pred chk[ vs : set V ] { A + B = vs }

> chk[A+B]
true
> chk[A]
false

So without the model (and preferably simplified) it is hard to see what the problem is.

[edmcman]

I expected my 1st and 4th evaluations to be equivalent for any check_ctx. Maybe this is a traditional PL way of thinking about it, but I was expecting there to be referential transparency. I.e., If foo evaluates to A + B, I should be able to replace foo with A + B in any expression and get the same result (scoping concerns aside). In reality, foo is ran[InitContext$0.initializers].exp and A + B is VarLvalue$0 + VarLvalue$1.

But here is the definition of check_ctx:

pred check_ctx(ctx:Context, e:Expression) {
    some e.var => (e.var in dom[ctx.varmap] and ctx.varmap[e.var] = e.type)
}

And here is Context:

abstract sig Context {
    varmap: VarIdentifier -> lone Type
}

and Expression:

abstract sig Expression extends ASTTree {
    type : Type
}

Obviously I need to do some work to simplify this, but I think that's enough information to see that the second argument is not a set. I also expected that check_ctx would be monotonic with respect to subsets in the second argument; i.e., check_ctx[foo, A] = false implies check_ctx[foo, A + B] = false.

I'll work on simplifying this into a minimal program.

P.S. Thank you for the help!

[pkriens]

The fact that everything in Alloy is a tupleset can be confusing. Especially since some of the constraints in declarations are not enforced or just to warn you. But show your simplified case and I'll take another look.

[edmcman]

Working on the simplified case now.

So does Alloy not have referential transparency?

[pkriens]

I think it has referential transparency. Or at least should have. However, I think the issue here is the cardinality assumption?

[edmcman]

This demonstrates the ultimate problem:

sig A {
    b: Int -> lone Int
}

/*fact {
    A.b in Int -> lone Int
}*/

check {
    A.b in Int -> lone Int
}

Executing "Check check$1"
   Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20
   5899 vars. 771 primary vars. 9766 clauses. 13ms.
   . found. Assertion is invalid. 15ms.

Especially since some of the constraints in declarations are not enforced

This is really terrible! Of course many models will break when functions can be instantiated by any relation! Is it intentional? The "Software Abstraction" book says on page 78:

Multiplicities are just a shorthand, and can be replaced by standard constraints [...] but multiplicities are preferable because they are terser and easier to read.

[pkriens]

I defer to @dnjackson . Already lost too many of these discussions :-)

[pkriens]

You probably also want to look at https://github.com/AlloyTools/org.alloytools.alloy/issues/14

[edmcman]

You probably also want to look at #14

That does seem like a thorny issue.

But I do think my example above is different in that it violates the spec from the book. The quotes I included were specifically about declarations, but not of predicates or functions.

[aleksandarmilicevic]

Especially since some of the constraints in declarations are not enforced

That is absolutely not true for multiplicity constraints on fields. And the answer is just 2 lines away, so there is no point guessing if not sure:

sig A { b: Int -> lone Int }
run { some a: A | some i: Int | #a.b[i] > 1 } for 3 but 3 Int // => No instance found

If foo evaluates to A + B, I should be able to replace foo with A + B in any expression and get the same result

That holds true in Alloy.

I expected my 1st and 4th evaluations to be equivalent for any check_ctx.

And they are. At least from the screenshot you posted, they both evaluate to true.

This demonstrates the ultimate problem:

There is no problem there. The semantics of your sig declaration

sig A { b: Int -> lone Int }

is not

fact { A.b in (Int -> lone Int) }

which is why your check fails; rather, the semantics is

fact { all a: A | a.b in (Int -> lone Int) }

[edmcman]

And they are. At least from the screenshot you posted, they both evaluate to true.

Sorry, I am not sure what I was thinking there. You are right, of course.

There is no problem there. The semantics of your sig declaration

You are right. I convinced myself that this was the underlying problem but it is not. Let me try again to minimize the issue I am having.

[edmcman]

I think the issue is that I assumed some of my predicates were monotonic but they are not. Sorry for the noise.