Frederic G. MARAND b4b3b4e1a5 Lamport PlusCal: 2.1-2.5 Euclid's algorithm.

2025-02-27 16:24:42 +01:00

14 KiB

Raw Permalink Blame History

TLA+ symbols and identifiers

Note that PlusCal allows user-defined operators, so any operator shown as non-native may be introduced by a module if it is part of the user-definable symbols, as defined by Table 4 in the P-syntax manual.

Arrows

Oriented

Single `->`

->
- In [S -> D]: the set of functions from domain S to destination set (codomain) D
<- :
- used in TLA+ only as part of INSTANCE statements with WITH clauses
  - Example: INSTANCE Foo WITH x <- e
- used in TLC Toolbox CFG files to assign values to constants (but doesn't work in TLC CLI)
- used in lectures to represent substitution in expressions, like f WITH v <- e, which substitutes expression e for the symbol v in expression f.
|->, used only as [x |-> y],
- a function mapping a single element x to value y,
- if x is a string, that function is called a record or struct
- if x is a natural, that function is called a sequence or tuple if the domain is finite.
>- and -< : not native TLA+ symbols

Double `=>`

=> : implies
- A => B = B \/ ~A
<=>: logical equivalence, same as = but only applicable to booleans
- A <=> B = (A => B) /\ (B => A)
- A <=> B = (A /\ B) \/ (~A /\ ~B)
>= : greater than or equal operator
<= : less than or equal operator
=< : less than or equal operator
>=<: not part of TLA+

Tilde `~>`

~>: leads to
- TODO
<~: not a native TLA+ symbol

Symmetric

<-> : logical equivalence
- Unlike =, only applies to booleans

No other symmetric arrow is a native TLA+ symbol.

Brackets etc

`[]`: always or functions

Empty: always temporal operator box
- []P means P is true in every state of the system, i.e. it is an invariant
- ~[]P: in EVERY behaviour, there exists at least one state where P is false
- [foo]_bar
  - is shorthand for foo \/ UNCHANGED bar, assuming bar is a sequence, e.g. <<x, y>>
  - which means for foo \/ (x' = x /\ y = y)`
- The combination []<> always eventually can be called repeatedly
  - []<>P means that P will keep becoming true infinitely often.
  - It's like saying "no matter when you look, P will eventually be true again."
  - Meaning at some point in the future, P will become true and remain true forever after.
  - It's like saying "eventually, P will always hold."
Non-empty: functions
- In [S -> D], a set of functions. See Arrows/-->
- In [x |-> y] a specific function. See Arrows/|->
- TODO check: "For any function f = [x ∈ DOMAIN f: x ↦ f[x]]"

`{}`: sets

{} : empty set
{ x1, ... xN } : enumerated set
{ x: y } : a set comprehension. Two kinds have names:
- { expr: x \in S }: a set map, read as "values of expr where x is in S"
- ( x \in S: expr }: a set filter, read as "keys of S where expr holds true"

`<>`: eventually, tuples

<>: eventually temporal operator diamond
- Meaning at some point in the future, P will become true and remain true forever after. It's like saying "eventually, P will always hold."
<>[]: eventually always
- At some point in the future, P will become true and remain true forever after.
- It's like saying "eventually, P will always hold."
<<A>>_v means A is true AND v changes
- Compare to [A]_v meaning A is true OR vdoesn't change
<<a, b, c>> defines a tuple/sequence. Some texts (incorrectly ?) use (a, b, c).

`()`

(a, b, c) : tuple construction is referenced somewhere, but should be <<a, b, c>>
f(x, y, z) : non-niladic function application
- niladic function f application is written f
- that is because a niladic function and its application are actually the same
Expressions grouping for arithmetic
Logical and temporal precedence grouping

Predefined functions and operators, by module

All are pure functions, no mutators.

At least some direct engine support

Naturals

+, -, *, /, ^, %: arithmetic
<, <=, >, >= and less-used =< for <=
Nat : the set of natural integers
- Cannot be enumerated by TLC (in a quantifier or CHOOSE)
- Can be used for membership checking
.. to define "range" sets like 1..3 = {1, 2, 3}
\div: integer floor division: 10 \div 3 = 3

Integers

All of Naturals, plus...
Int : the set of all integers
unary -: negative numbers, like -2

Sequences

Append(S, e): appends element e at the end of sequence S and returns the result
Head(S): first element of S (cf. Lisp CAR)
Len(S): length of sequence
\o: concatenation of two sequences (vs seq + element for Append)
SelectSeq(seq, Op(_)) : filter a sequence using Op
- IsEven(x) == x % 2 = 0 (% has precedence over =)
- SelectSeq(<<1, 2, 3>>, IsEven) = <<2>>
Seq(set): the set of all sequences of set elements (so countable infinite, aleph-null)
- Is actually efficient in TLC, counter-intuitively
- Cannot be enumerated by TLC (in a quantifier or CHOOSE)
- Can be used for membership checking
SubSeq(S, m, n): subsequence of s from m to n, both included
Tail(S): sequence S without first element (cf. Lisp CDR)

Required for PlusCal procedures.

TLC

:> shorthand notation for functions with a singleton domain
- a :> b = [x \in {a} |-> b]
@@: dyadic function merge
- if both operands share the same key use the LEFT one (cf. LearnTLA+ (other sources say the right one)
SortSeq(seq, Op(_, _)) Sorts the sequence with comparator Op.
Any
- Used as x \in Any to get any value x of any type
- Do not use in a spec
- May be useful for modeling properties
Assert(e, t): checks that e is true and returns, or prints t if e if false
JavaTime: The current epoch time.
Permutations(set): all functions acting as permutations of the set
- Permutations(S) == {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}
Print(t, e):
- From one source: prints the value of e with tag t
- From the Standard modules page on LearnTLA: Print(val, out): Prints ToString(val), and evaluates to out as an expression.
- From experience: requires e = TRUE and prints t to output
PrintT(val): Equivalent to Print(val, TRUE).
RandomElement(set): Randomly pulls an element from set. The value can be different on different runs!
SortSetq(seq): Sorts a sequence
TLCEval(v): Evaluates v and caches the result. Can be used to speed up recursive definitions.
TLCGet(val): val can be either an integer or a string.
- If an integer, retrieves the value from the corresponding TLCSet.
- If a string, retrieves statistics from the current model run. The following strings are valid:
  - “queue”
  - “generated”
  - “distinct”
  - "duration”: number of seconds elapsed since the beginning of model checking
  - “level”: the length of the current behavior
    - can be used to bound an unbound model.
  - “diameter”: the length of the longest global behavior
  - “stats”: all of the global stats (everything excluding “level”), as a struct.
TLCSet(i, val): Sets the value for TLCGet(i).
- i must be a positive integer.
- TLCSet can be called multiple times in the same step.
ToString(val): String conversion.

Each TLC worker thread carries a distinct “cache” for the values of TLCGet(i). As such, it’s generally inadvisable to use TLCSet to profile information that lasts beyond a single step.
TLCSet statements evaluated during the initial state, however, will be propagated to all workers.

TLCExt

AssertEq(a, b): Equivalent to a = b, except that if a # b, it also prints the values of a and b.
- This does not terminate model checking!
AssertError(str, exp): True if exp doesn’t throw an error, or if exp throws an error that exactly matches str.
- False otherwise
- This does not terminate model checking!
Trace: Returns the “history” of the current behavior, as a sequence of structs.
TLCModelValue(str): Creates a new model value with name str.
- Can only be used in constant definitions, as part of an ordinary assignment.

CONSTANT Threads <- {
  TLCModelValue(ToString(i)): i \in 1..3
}

assigns the constant Threads a set of model values corresponding to the strings "1", "2", and "3".
This is useful for scenarios where you want to represent distinct entities (like threads) in a model without tying them to specific numeric values.

100% TLA+ user space modules

Bags

Bags defines a special kind of functions, from items to natural values, meant to represent their "count".

IsABag(f)
- IsABag([a |-> 3, b |-> 7]) = TRUE because both 3 and 7 are naturals
- IsABag([a |-> 3, b |-> "B"]) = FALSE because "B" is not a natural
- IsABag([a |-> 3, b |-> -2]) = FALSE because -2 is not a natural
- Any function over the empty set passes IsABag because no elements fail to be naturals
BagToSet(bag) : returns the domain of bag
- equivalent to DOMAIN bag
SetToBag(set) creates a bag with set elements as keys and counts all equal to 1
- equivalent to [x \in set |-> 1]
BagIn(e, bag) : e \in DOMAIN bag
EmptyBag : `<<>>
- Subtlety: any function over the empty set is the EmptyBag
(+): dyadic bag addition merges two bags, adding counts on merged keys
(-): dyadic bag subtraction, subtracting counts on all keys present in the right argument, and dropping all keys with resulting negative or zero counts
BagUnion(set) : bag addition of all members of the set
\sqsubseteq : dyadic operator: true IFF all elements in the right operand have at least as high a count as those in the left operand SubBag(bag) : the set of all subbags of bag as defined by \sqsubseteq
- SubBag(EmptyBag) = {<<>>}
- SubBag([a |-> 2]) = {<<>>, [a -> 1], [a -> 2]}
BagOfAll(Op(_), bag) : mapping of Op over the bag KEYS (not values)
- BagOfAll(LAMBDA x: x^2, <<1, 3, 5>>) = (1 :> 1 @@ 4 :> 3 @@ 9 :> 5)
BagCardinality(bag) : the sum of all counts in the bag
CopiesIn(e, bag) : the count for key e in the bag, 0 if it is absent

FiniteSets

Cardinality(S): number of elements in S
IsFiniteSet(S): is S finite ?

Json

ToJson(val) : convert to a JSON string
- sets and sequences -> JSON arrays
- functions: objects with string keys; converting any non-string source elements to their string representation
JsonSerialize(absoluteFilename, value): convert value to a JSON file
JsonDeserialize(absolutefilename): imports a JSON object from a file

Randomization

Provides pseudo-random subsets, which will prevent TLC from checking all possible states.

This is useful for optimization, but may introduce oversights.

RandomSubset(k, S): random size-k subset of S.
RandomSetOfSubsets(k, n, S): k random subsets of S, where each random subset has on average n elements
- May generate duplicates, so return fewer than k elements,
- May return the empty set
TestRandomSetOfSubsets(k, n, S)
- Calls RandomSetOfSubsets(k, n, S) five times (hardcoded) and returns the number of unique sets each time, as a sequence

Reals

Nothing usable in TLC

Realtime