samedi 22 septembre 2018

Alloy Array Model

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

Aucun commentaire:

Enregistrer un commentaire