Polymorphic empty relation in Alloy?

Question

I run an Alloy command that involves finding witnesses for some existentials, like this one:

pred foo { 
  some x, y : E -> E | 
    baz[x,y] || qux[x,y] 
}

Alloy comes up with a model where foo is true. I look at the model in the Visualizer, and find that y happens to be the empty relation. I want to dig deeper into the model and see whether baz or qux is true. So I fire up the Evaluator window and type baz[$foo_x, ???]. But what can I type for ???? Since y is empty, there is no variable with the name $foo_y. And typing none or {} gives a type-checking error.

Does Alloy provide an empty relation that can be used at any type? Or is there any way to get at the y witness even though it's empty?

A workaround that I've been using: $foo_x - $foo_x gives me the empty relation at the correct type. But it's quite an ugly hack! Is there a more principled way? — John Wickerson

Alcino Cunha Alcino Cunha · Accepted Answer · 2016-01-22T08:11:08

I belive baz[$foo_x, none->none] should work. The relation none has arity 1, and by using cross product you can get empty relations of the desired arity. The explanation for this can be found in the paper "A Type System for Object Models" by Jonathan Edwards, Daniel Jackson and Emina Torlak.

Polymorphic empty relation in Alloy?

1 Answers