alloy

How do I see the returned value(s) of a function in Alloy?

I'm trying to understand how functions work in Alloy, and an important part of that is testing them. For example I've got this code:

open util/ordering[Time]   // enforces total order on Time

sig Time {}                // instances denote timestamps

sig File {
   time : Time             // every file has exactly one timestamp
}

fun getTime[F : set File] : Time {
    {t : Time | some f : F | all x : F | f.time = t && gte[f.time,x.time]}
}

The getTime function is meant to return the time value of the file(s) with the greatest timestamp, out of the given set of files. I've made the function, and I believe it should work as intended, but I have no clue how to actually test that. I know I can run functions in Alloy, but I can't figure out how to create a sample set of files to use as input. Whenever I do manage to get something to run, nowhere in the resulting visualization does it show what the function outputted.

Solution

  • In the visualization, you can open the "Evaluator" with a button in the toolbar.

    There you can enter stuff like:

    univ

    to get a list of all atoms. And:

    getTime[File$0]

    to evaluate a function.