CODEWITHSUNDEEP
functionreturn-valuealloy
Noah Cabral
Noah Cabral

Reputation: 71

How to return a single value for a function in Alloy?

finding alot of difficulty finidng any good resources on functions in alloy. I have succesfully made a function that returns a set of values (i.e has a "set" return type) but I cannont figure out how to write a function which returns a single value. i. e i have

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 {
     {one t : Time | some f : F | all g : F | f.time = t && gte[f.time,g.time]}
}

The function getTime takes a set of files and returns the most recent file stamp(greatest time attribute of all files in F) however no matter which way I write it I contsantly get the wrong return type (Primitive Boolean) error or some other error. How do I return something of type Time?

Upvotes: 1

Views: 580

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

You get a boolean return type because of the keyword one. This quantifier enforces that true is returned if and only if there is exactly one Time t satisfying the following predicate.

Without any quantifier, the expression in your function would be what we call a set comprehension, that is, a set containing every time atoms satisfying the following predicate will be returned

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

Upvotes: 1

Related Questions