time (legacy)

Automatically imports an ordered Time signature to your spec. This used to be used for modeling time before Alloy 6, but now there is a native feature for it. This module is now deprecated, but you may still see older specifications that use it.

Warning

Time internally uses the ordering module. This means that the signature is forced to be exact.

See also

Module ordering

Macros

let time.dynamic[x]
Arguments:
  • x (sig) – any signature.

Expands to:

x one -> Time

dynamic can be used as part of a signature definition:

open util/time

abstract sig Color {}
            one sig Red, Green, Yellow extends Color {}

sig Light {
  , state: dynamic[Color]
}

At every Time, every Light will have exactly one color.

let time.dynamicSet[x]
Arguments:
  • x (sig) – any signature.

Expands to:

x -> Time

Equivalent to dynamic, except that any number of elements can belong to any given time:

open util/time

sig Keys {}

one sig Keyboard {
  pressed: dynamicSet[Keys]
}