When to use util/ordering instead of temporal logic?

[Alejandro]

Are there problems when util/ordering is a better fit than temporal logic?

Asking this question after finding the following topic:

Solution to farmer puzzle using Alloy 6 temporal primitives

Hello! The current sample model examples/tutorial/farmer.als (link) distributed with Alloy 6 doesn’t use the new temporal primitives (always, eventually, ' etc.). It might be nice to add another version that uses the new functionality, so that users see they don’t need to deal with util/ordering etc. Although there are already nice sample models showing off the temporal primitives, like trash.als, I think the puzzle is well known enough to be more approachable on its own. As such, I have a mo…

And this blog post, where util/ordering is used:

Use Alloy to model and find a solution to the Goat, Cabbage, and Wolf problem

[alcino]

Hi,

Alloy 6 commits on a particular model of time, where traces are infinite sequences of states. I guess the old idiom of using directly util/ordering to explicitly specify traces might still be useful if you need a different model of time, for example, if you really need to model finite traces.

Note that in most cases we can “simulate” finite traces by infinite ones that end with stuttering. For example, most puzzles like the one you mention are in fact easier to specify in Alloy 6 than with the util/ordering idiom, we just have to make sure that when the puzzle is solved stuttering is still possible.

There are also some temporal properties that might be easier to specify with the util/ordering idiom: for example, if you need to determine the set of all values a variable will have in a trace, this set can trivially be determined in the util/ordering idiom, by just composing with the explicit Time (or State signature), while with temporal logic it will be more verbose.

Best,
Alcino