Süsteemide modelleerimine 2019/20 sügis

PlusCal Syntax

For a complete reference see, the PlusCal Manual. Here is the summary of the language features that I have used in my examples; you should be able understand the structure from the examples, so this page focuses on the detailed constructs.

PlusCal Statements

PlusCal is a small syntactic extension on top of TLA+. All expressions and data structures are from TLA, but we can write it down like an imperative program. The following are the PlusCal constructs we used:

• Assignment:
  • x := y + 1
• Await (When). This adds an enabling condition on the transition. The process waits until it can make a transition. Note that all the following behave exactly the same:
  • await x > 0; x := x - 1
  • when x > 0; x := x - 1
  • x := x - 1; when x >= 0 (condition on post-transition state)
  • x := x - 1; await x >= 0 (same, but somewhat confusing style)
• If-Statements are like conditional statements, i.e., the process always takes a step, but depending on the condition different actions could be taken. It does not wait (block the process) if the condition is not true.
  • if x > 0 then x := 0 else z := 0 end if
  • if x > 0 then x := 0; y := 2 elsif y > 0 then y := 0 else z := 0 end if
• While-Statements and Goto:
  • Loop: while TRUE do x := x + 1 end while
  • Loop: x := x + 1; goto Loop
  • Loop: while x < 10 do x := x + 1 end while
  • Loop: if x < 10 then x := x + 1; goto Loop end if
• Either models non-deterministic choice:
  • either x := 1 or x := 2 or x := 3 end either
  • either when x > 0; y := 1 or when x < 0; y := -1 end either (This will wait if x is zero)
• With lets us consider a range of values. The model checker will consider all possible values from a given set. It can also be used to just give a name to a variable.
  • with z in {1,2,3} do x := z end with
  • with z = x + 1 do y := z * z end with
• Skip does nothing!

TLA+ Expressions: Basic Types

There is basic operations in TLA to work with integers, strings and booleans. Remember that TLA is a logic, so x = y is equality, not assignment. In PlusCal, we initialize variables by giving equations that hold in the initial state, so we also use equality there too, but otherwise we have x := y for assignment and x = y for equality.

• Integers have their usual syntax and arithmetic operations, except division because / is used for other things.
  • x + 1 \div 10
  • x <= 100
• Strings are also just letters within quotation marks as in most programming languages. You don't need to do much with strings. We only use them as identifiers, but operations like Len and concatenation do exist.
• Booleans are obviously very important. This is a logic, after all. Here are the basic operations that you have seen in any other programming language.
  • TRUE and FALSE are capitalized.
  • A /\ B conjunction is true whenever A and B are true.
  • A \/ B disjunction is true whenever A or B (or both) are true.
  • ~A is true when A is not.
  • A => B implication is the same as ~A \/ B.
  • A <=> B equivalence is the same as equality on booleans.

TLA+ data structures

The key data structures (just like in Java) are Set, Map and List. The last two are called functions and sequences in TLA.

• Sets
  • We can build them by listing elements {1,2,3} or giving a range 1..10.
  • There are built-in sets: Int and Nat.
  • Checking membership:
    • 1 \in {1,2,3} checks if en element belongs to a set
    • {1,3,5} \subseteq 1..5 checks inclusion (subset or equal).
  • Standard operations on sets:
    • {1,2,3} \cap {2,3,4} = {2,3} (intersection).
    • {1,2,3} \cup {2,3,4} = {1,2,3,4} (union).
    • 1..5 \ {2,4} = {1,3,5} (set difference, i.e., removes elements).
  • Sets of sets:
    • UNION {{1,2}, {5,6}, 11..14, {20}} = {1,2,5,6,11,12,13,14,20} flattens a set of sets to a single set that contains all elements of each set.
    • SUBSET {1,2,3} = {{}, {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3}} gives all possible subsets.
  • Filter and map:
    • {x \in 0..100 : x < 15 } filters the elements in the set 0..100 that satisfy the property x < 15.
    • {2*x : x \in 1..10} maps the function 2*x to all elements 1..10, so we get the set containing 2, 4, 6, and so on until 20.
• Functions (Map)
  • f = [i \in 1..10 |-> 2*i] builds a function.
  • Get and Put:
    • f[1] = 2 looks up the element in the map.
    • f[5] := 200 updates the map. This is PlusCal syntax, resulting in the same map as before, but with f[5] having a new value, just like in Java.
  • Building and merging maps.
    • f = ("key" :> 10) is the singleton function with f["key"] = 10.
    • (1 :> 100) @@ (2 :> 200) contains the mappings for both 1 and 2.

Predicate and Temporal Logic

...