The infinite set of all natural numbers.
Infinite sets cannot be enumerated. Hence some operators that require iteration may be unsupported.
The infinite set of all integers.
Infinite sets cannot be enumerated. Hence some operators that require iteration may be unsupported.
The set of all booleans
That is, Set(false, true)
a.eq(b) is true when a and b are equal values of the same type.
It can be used in the infix form as == or as a named operator eq.
a.neq(b) is true when a and b are not equal values of the same type.
It can be used in the infix form as != or as a named operator neq.
p.iff(q) is true when p and q are equal values of the bool type.
This is the logical equivalence operator.
assert(iff(true, true))
assert(iff(false, false))
assert(not(iff(true, false)))
assert(not(iff(false, true)))
p.implies(q) is true when not(p) or q is true.
This is the material implication operator.
assert(true.implies(true))
assert(false.implies(false))
assert(not(true.implies(false)))
assert(not(false.implies(true)))
not(p) is true when p is false.
This is the negation opearator.
s.exists(p) is true when there is an element in s that satisfies p.
This is the existential quantifier.
assert(Set(1, 2, 3).exists(n => n == 2))
assert(not(Set(1, 2, 3).exists(n => n == 4)))
s.forall(p) is true when all elements in s satisfy p.
This is the universal quantifier.
assert(Set(1, 2, 3).forall(n => n > 0))
assert(not(Set(1, 2, 3).forall(n => n > 1)))
e.in(s) is true when the element e is in the set s.
This is the set membership relation.
See also: contains
assert(1.in(Set(1, 2, 3)))
assert(not(4.in(Set(1, 2, 3))))
s.contains(e) is true when the element e is in the set s.
This is the set membership relation.
See also: in
assert(Set(1, 2, 3).contains(1))
assert(not(Set(1, 2, 3).contains(4)))
s1.union(s2) is the set of elements that are in s1 or in s2.
This is the set union operator.
assert(Set(1, 2, 3).union(Set(2, 3, 4)) == Set(1, 2, 3, 4))
s1.intersect(s2) is the set of elements that are in both sets s1 and s2.
This is the set intersection operator.
assert(Set(1, 2, 3).intersect(Set(2, 3, 4)) == Set(2, 3))
s1.exclude(s2) is the set of elements in s1 that are not in s2.
This is the set difference operator.
assert(Set(1, 2, 3).exclude(Set(2, 3, 4)) == Set(1))
s1.subseteq(s2) is true when all elements in s1 are also in s2.
assert(Set(1, 2, 3).subseteq(Set(1, 2, 3, 4)))
assert(not(Set(1, 2, 3).subseteq(Set(1, 2))))
s.filter(p) is the set of elements in s that satisfy p.
assert(Set(1, 2, 3).filter(n => n > 1) == Set(2, 3))
s.map(f) is the set of elements obtained by applying f to
to each element in s. I.e., { f(x) : x \in s}.
assert(Set(1, 2, 3).map(n => n > 1) == Set(false, true, true))
l.fold(z, f) reduces the elements in s using f, starting with z.
I.e., f(...f(f(z, x0), x1)..., xn).
The order in which the elements are combined is unspecified, so the operator must be associative and commutative or else it has undefined behavior.
val sum = Set(1, 2, 3, 4).fold(0, (x, y) => x + y)
assert(sum == 10)
val mul = Set(1, 2, 3, 4).fold(1, (x, y) => x * y)
assert(mul == 24)
s.powerset() is the set of all subsets of s,
including the empty set and the set itself.
assert(Set(1, 2).powerset() == Set(
Set(),
Set(1),
Set(2),
Set(1, 2)
))
s.flatten() is the set of all elements in the sets in s.
assert(Set(Set(1, 2), Set(3, 4)).flatten() == Set(1, 2, 3, 4))
s.allLists() is the set of all lists containing all the elements in s.
assert(Set(1, 2).allLists() == Set(
List(1, 2),
List(2, 1),
))
s.chooseSome() is, deterministically, one element of s.
assert(Set(1, 2, 3).chooseSome() == 1)
assert(Set(1, 2, 3).filter(x => x > 2).chooseSome() == 3)
s.oneOf() is, non-deterministically, one element of s.
nondet x = oneOf(Set(1, 2, 3))
assert(x.in(Set(1, 2, 3)))
s.isFinite() is true when s is a finite set
assert(Set(1, 2, 3).isFinite())
assert(!Nat.isFinite())
s.size() is the cardinality of s.
assert(Set(1, 2, 3).size() == 3)
m.get(k) is the value for k in m.
If k is not in m then the behavior is undefined.
pure val m = Map(1 -> true, 2 -> false)
assert(m.get(1) == true)
m.keys() is the set of keys in the map m.
pure val m = Map(1 -> true, 2 -> false)
assert(m.keys() == Set(1, 2))
s.mapBy(f) is the map from x to f(x) for each element x in s.
pure val m = Set(1, 2, 3).mapBy(x => x * x)
assert(m == Map(1 -> 1, 2 -> 4, 3 -> 9))
s.setToMap() for a set of pairs s is the map
from the first element of each pair to the second.
pure val m = Set((1, true), (2, false)).setToMap()
assert(m == Map(1 -> true, 2 -> false))
keys.setOfMaps(values) is the set of all maps from keys to values.
pure val s = Set(1, 2).setOfMaps(set(true, false))
assert(s == Set(
Map(1 -> true, 2 -> true),
Map(1 -> true, 2 -> false),
Map(1 -> false, 2 -> true),
Map(1 -> false, 2 -> false),
))
m.set(k, v) is the map m but with the key k mapped to v if k.in(keys(m))
If k is not a key in m, this operator has undefined behavior.
pure val m = Map(1 -> true, 2 -> false)
pure val m2 = m.set(2, true)
assert(m == Map(1 -> true, 2 -> false))
assert(m2 == Map(1 -> true, 2 -> true))
m.setBy(k, f) is a map with the same keys as m but with k set to f(m.get(k)).
If k is not present in m, this operator has undefined behavior.
pure val m = Map(1 -> true, 2 -> false)
pure val m2 = m.setBy(2, x => !x)
assert(m == Map(1 -> true, 2 -> false))
assert(m2 == Map(1 -> true, 2 -> true))
m.put(k, v) is the map m but with the key k mapped to v.
pure val m = Map(1 -> true, 2 -> false)
pure val m2 = m.put(2, true)
pure val m3 = m.put(3, true)
assert(m == Map(1 -> true, 2 -> false))
assert(m2 == Map(1 -> true, 2 -> true))
assert(m3 == Map(1 -> true, 2 -> false, 3 -> true))
l.append(e) is the list l with the element e appended.
assert(List(1, 2, 3).append(4) == List(1, 2, 3, 4))
l1.concat(l2) is the list l1 with l2 concatenated at the end.
assert(List(1, 2, 3).append(List(4, 5, 6)) == List(1, 2, 3, 4, 5, 6))
l.head() is the first element of l.
If l is empty, the behavior is undefined.
assert(List(1, 2, 3).head() == 1)
l.tail() is the list l without the first element.
If l is empty, the behavior is undefined.
assert(List(1, 2, 3).tail() == List(2, 3))
l.length() is the length of the list l.
assert(List(1, 2, 3).length() == 3)
l.nth(i) is the i+1th element of the list l.
If i is negative or greater than or equal to l.length(), the behavior is undefined.
assert(List(1, 2, 3).nth(1) == 2)
l.indices() is the set of indices of l.
assert(List(1, 2, 3).indices() == Set(0, 1, 2))
l.replaceAt(i, e) is the list l with the i+1th element replaced by e.
If i is negative or greater than or equal to l.length(), the behavior is undefined.
assert(List(1, 2, 3).replaceAt(1, 4) == List(1, 4, 3))
l.slice(i, j) is the list of elements of l between indices i and j.
i is inclusive and j is exclusive.
The behavior is undefined when:
iis negative or greater than or equal tol.length().jis negative or greater thanl.length().iis greater thanj.
assert(List(1, 2, 3, 4, 5).slice(1, 3) == List(2, 3))
range(i, j) is the list of integers between i and j.
i is inclusive and j is exclusive.
The behavior is undefined when i is greater than j.
assert(range(1, 3) == List(1, 2))
l.select(p) is the list of elements of l that satisfy the predicate p.
Preserves the order of the elements.
assert(List(1, 2, 3).select(x -> x % 2 == 0) == List(2))
l.foldl(z, f) reduces the elements in s using f,
starting with z from the left.
I.e., f(f(f(z, x0), x1)..., xn).
pure val sum = List(1, 2, 3, 4).foldl(0, (x, y) => x + y)
assert(sum == 10)
pure val l = List(1, 2, 3, 4).foldl(List(), (l, e) => l.append(e))
assert(l == List(1, 2, 3, 4))
a.iadd(b) is the integer addition of a and b.
It can be used in the infix form as + or as a named operator iadd.
a.isub(b) is the integer subtraction of b from a.
It can be used in the infix form as - or as a named operator isub.
a.imul(b) is the integer multiplication of a and b.
It can be used in the infix form as * or as a named operator imul.
a.idiv(b) is the integer division of a by b.
It can be used in the infix form as / or as a named operator idiv.
a.imod(b) is the integer modulus of a and b.
It can be used in the infix form as % or as a named operator imod.
a.ipow(b) is the integer exponentiation of a by b.
It can be used in the infix form as ^ or as a named operator ipow.
a.ilt(b) is the integer less than comparison of a and b.
It can be used in the infix form as < or as a named operator ilt.
a.igt(b) is the integer greater than comparison of a and b.
It can be used in the infix form as > or as a named operator igt.
a.ilte(b) is the integer less than or equal to comparison of a and b.
It can be used in the infix form as <= or as a named operator ilte.
a.igte(b) is the integer greater than or equal to comparison of a and b.
It can be used in the infix form as >= or as a named operator igte.
iuminus(a) is -1 * a.
This is the unary minus operator
i.to(j) is the set of integers between i and j.
i is inclusive and j is inclusive.
The behavior is undefined when i is greater than j.
assert(1.to(3) == Set(1, 2, 3))
always(p) is true when p is true for every transition of the system.
var x: int
action Init = x' = 0
action Next = x' = x + 1
temporal Property = always(next(x) > x)
eventually(p) is true when p is true for some transition of the system.
eventually(p) is equivalent to not(always(not(p))).
var x: int
action Init = x' = 0
action Next = x' = x + 1
temporal Property = eventually(x == 10)
next(a) is the value of a in the next state of a transition.
var x: int
action Init = x' = 0
action Next = x' = x + 1
temporal Property = next(x) == x + 1
orKeep(a, v) is true when a is true or the values
for the set of variables v are unchanged.
orKeep(a, v) is equivalent to a or v.map(x => next(x) == x).
This is the stuttering operator.
var x: int
action Init = x' = 0
action Next = x' = x + 1
temporal Spec = Init and always(Next.orKeep(Set(x)))
mustChange(a, v) is true when a is true and the values for the
set of variables v are changed.
mustChange(a, v) is equivalent to a and v.map(x => next(x) != x).
This is the no-stuttering operator.
var x: int
action Init = x' = 0
action Next = any {
x' = x + 1,
x' = x,
}
temporal Spec = Init and always(Next.mustChange(Set(x)))
temporal Property = Spec.implies(always(next(x) > x))
enabled(a) is true when the action a is enabled in the current state.
An action is enabled when all its preconditions are satisfied and it's postcontitions are satisfiable.
var x: int
action Init = x' = 0
action Under10 = all {
x < 10,
x' = x + 1,
}
action Over10 = all {
x >= 10,
x' = x + 1,
}
temporal Property = always(and {
enabled(Under10) iff x < 10,
enabled(Over10) iff x >=10,
})
var x: int
action Init = x' = 0
action impossible = {
nondet i = Set().oneOf()
x' = i
}
temporal Property = always(not(enabled(impossible)))
weakFair(a, v) is true when
eventually(always(a.mustChange(v).enabled())).implies(always(eventually(a.mustChange(v))))
is true.
This is the weak fairness condition.
The weak fairness condition can be expressed in English as (from Specifying Systems):
- It’s always the case that, if A is enabled forever, then an A step eventually occurs.
- A is infinitely often disabled, or infinitely many A steps occur.
- If A is eventually enabled forever, then infinitely many A steps occur.
var x: int
action Init = x' = 0
action Next = any {
x' = x + 1,
x' = x,
}
temporal Property = Next.weakFair(Set(x)).implies(eventually(x == 10))
strongFair(a, v) is true when
always(eventually(a.mustChange(v).enabled())).implies(always(eventually(a.mustChange(v))))
is true.
This is the strong fairness condition.
The strong fairness condition can be expressed in English as (from Specifying Systems):
- A is eventually disabled forever, or infinitely many A steps occur.
- If A is infinitely often enabled, then infinitely many A steps occur.
var x: int
action Init = x' = 0
action cycleTo1 = all { x == 0, x' = 1 },
action cycleTo0 = all { x == 1, x' = 0 },
action breakCycle = all { x == 0, x' = 2 },
action Next = any {
cycleTo1,
cycleTo0,
breakCycle,
x' = x,
}
// Strong fairness can be used to ensure breakCycle happens
temporal Property = breakCycle.strongFair(Set(x)).implies(eventually(x == 2))
assign(n, v) is true when the state variable named n has the value v
in the next state of a transition.
This operator is used to define transitions by specifying how the state variables change
Can be written as n' = v.
var x: int
action Init = x' = 0
// Next defines all transitions from a number to its successor.
action Next = x' = x + 1
ite(c, t, e) is t when c is true and e when c is false.
Can be written as if (c) t else e.
Can be used with actions.
pure val m = if (1 == 2) 3 else 4
assert(m == 4)
var x: int
action a = if (x == 0) x' = 3 else x' = 4
run test = (x' = 0).then(a).then(assert(x == 3))
a.then(b) is true for a step from s1 to s2 if there is a state t such that
a is true for a step from s1 to t and b is true for a step from t to s2.
This is the action composition operator.
var x: int
run test = (x' = 1).then(x' = 2).then(x' = 3).then(assert(x == 3))
Deprecated: use n.reps(A) instead.
a.repeated(n) is the action a repeated n times.
The semantics of this operator is as follows:
- When
n <= 0, this operator is equivalent tounchanged. - When
n = 1,a.repeated(n)is equivalent toa. - When
n > 1,a.repeated(a), is equivalent toa.then(a.repeated(n - 1)).
Note that the operator a.repeated(n) applies a exactly n times (when n is
non-negative). If you want to repeat a from i to j times, you can combine
it with orKeep:
a.repeated(i).then((a.orKeep(vars)).repeated(j - i))
var x: int
run test = (x' = 0).then((x' = x + 1).repeated(3)).then(assert(x == 3))
n.reps(i => A(i)) or n.reps(A) the action A, n times.
The iteration number, starting with 0, is passed as an argument of A.
As actions are usually not parameterized by the iteration number,
the most common form looks like: n.reps(i => A).
The semantics of this operator is as follows:
- When
n <= 0, this operator does not change the state. - When
n = 1,n.reps(A)is equivalent toA(0). - When
n > 1,n.reps(A), is equivalent toA(0).then((n - 1).reps(i => A(1 + i))).
var x: int
run test = (x' = 0).then(3.reps(i => x' = x + 1)).then(assert(x == 3))
a.fail() evaluates to true if and only if action a evaluates to false.
This operator is good for writing tests that expect an action to fail.
assert(p) is an action that is true when p is true.
It does not change the state.
var x: int
run test = (x' = 0).then(3.times(x' = x + 1)).then(assert(x == 3))
var x: int
action Init = x' = 0
action Next = x' = x + 1
run test = Init.then(all { Next, assert(x > 0) })