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
, everyLight
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] }