CODEWITHSUNDEEP
alloy
John Wickerson
John Wickerson

Reputation: 1232

Polymorphic empty relation in Alloy?

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?

Upvotes: 0

Views: 139

Answers (1)

Alcino Cunha
Alcino Cunha

Reputation: 186

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.

Upvotes: 1

Related Questions