Alloy Array Model

Question

I just started learning alloy model language and was trying to write my own array model in Alloy. However, I was unable to extract index from a relation. Here is my sig and fact:

sig Element {}

one sig Array {
  // Map index to element
  IdxEle: Int -> Element,
  // Length of the array.
  length: Int
}

fact Index {
    all r : IdxEle | r.Int >= 0 and r.Int < length
}

The error I was getting was

This must be an integer expression.
Instead, it has the following possible type(s):
{none->none}

I looked over the reference guide but could not find a way to extract the idx field of the relation. Can somebody help me out? Thanks

Answer 1

First, r in your model is of type Array->Int->Element, therefore (Array->Int->Element).Int cannot be computed since the last column in the tuple is of type Element, not Int as you seem to expect. (When you join in Alloy, the last column of the left side must be the same type of the first column of the right side.)

Second, there are easier, more flexible, and more readable ways to express what you want:

sig Element {}

let range[start,end] = {  i : Int | i >= start and i < end }

one sig Array { index : Int -> Element } {
    index.Element = range[ 0, len[this] ]
}

fun len[ array : Array ] : Int { # array.index }

Third ... there is a built in type for you called seq. It has everything you want and more.