Home

A PlusCal User`s Manual

1. CASE p gt 1 e O Pn gt en DD VV Hal re Thus its value equals e if all of the p equal FALSE A LET expression allows you to make definitions local to the expression For example LET zx a b y a b IN IF y gt O THEN 2 y ELSE 2 Y l gt I gt equals IF a b gt 0 THEN a b a b ELSE a b a b Any sequence of TLA definitions can appear between the LET and the IN Section 5 11 on page 55 describes TLA definitions 5 10 Temporal Operators A behavior is a nonempty sequence of states where a state is an assign ment of values to variables A behavior of an algorithm is one that can be generated by executing the algorithm A temporal formula is a predicate on behaviors in other words it is true or false for any nonempty sequence of states An algorithm satisfies a temporal formula F iff F is true of all behaviors of the algorithm Temporal formulas cannot appear in a PlusCal algorithm They are used only in the fairness properties assumed of the algorithm s executions and in the properties asserted about the algorithm Section 4 6 on page 38 explains how to assert fairness properties of the algorithm and how to tell TLC to check liveness properties This section defines the TL AT temporal operators that are used to express these fairness and liveness properties 5l The definitions are given for infinite behaviors only They are applied to finite behaviors by considering the
2. gt An assignment statement consists of one or more assignments separated by tokens ending with a semicolon An assignment statement contain ing more than one assignment is called a multiple assignment A multiple assignment is executed by first evaluating the right hand sides of all its as signments and then performing those assignments from left to right For example if i j 3 then executing x i 1 x j 2 sets x 3 to 2 Assignments to the same variable cannot be made in two different as signment statements within the same step In other words in any control path a label must come between two statements that assign to the same variable However assignments to components of the same variable may appear in a single multiple assignment as in x foo 7 13 y 27 x bar x foo 3 2 2 If The if statement has its usual meaning The statement if test t_clause else e_clause is executed by evaluating the expression test and then executing the pos sibly compound statement t_clause or e_clause depending on whether test equals TRUE or FALSE The else clause is optional An if statement must have a non empty then clause An if statement that contains a call 21 return or goto statement or a label within it must be followed by a la beled statement A label on the if statement itself is not considered to be within the statement 3 2 3 Either The either statement has the form eit
3. self if y 0 13 blself FALSE 14 await y 0 goto start y self if x self 17 18 19 skip y 0 b self b self FALSE pie ty while j lt N await b jl jis jet if y self 110 await y 0 goto start Xx The critical section FALSE Figure 2 The fast mutual exclusion algorithm in PlusCal 13 a mathematician I usually call A a function with domain S rather than an array indexed by S However TLAt and PlusCal use programmers square brackets instead of mathematicians parentheses to represent array function application The construct and other TLA notation for functions is explained in Section 5 5 on page 47 The algorithm continues with process Proc 1 N This statement begins a collection named Proc of N processes each process identified by a number in 1 N The statement variable j declares j to be a local variable of these processes meaning that each of the N processes has its own separate variable j A local or global variable z can be initialized by a declaration of the form variable z exp or variable z emp The matching and enclose the code for each process in the collection Proc where self is the identifier of that process in this example a number in 1 N The obvious difference between the original pseudo code for process 7 in Figure 1 and the code for each process self of the P
4. procedure Foo p1 0 p2 a b Like a procedure variable s declaration the initial value declaration of a formal parameter p must be of the form p expression Since a procedure s formal parameters are set equal to the corresponding arguments when the procedure is called their initial values do not affect the execution Those initial values serve only to ensure that the corresponding variables in the TLAT specification always have values of the correct type 37 4 6 Termination Liveness and Fairness We saw in Section 2 5 how to check termination of a uniprocess algorithm Termination is a special case of a general class of properties called liveness properties which assert that something must eventually happen We can use TLC to check more general liveness properties of an algorithm An algorithm satisfies a liveness property only under some assumptions usually fairness assumptions on actions In a PlusCal algorithm there is an action corresponding to each label Execution of that action consists of executing all code from that label to the next An action is enabled iff it can be executed Consider the following code within a process a y 42 Z y 1 b await x gt self x x 1 c An execution of action a consists of executing the assignments to y and z That action is enabled iff control in the process is at a An execution of action b decrements x by 1 It is enabled iff control is at b and the v
5. 24 assertion failure of 24 assignment 20 21 multiple 6 21 to a component 20 assumption fairness 38 atomic action 14 52 atomic operation 52 translation of 61 await PlusCal statement 14 23 BEGIN TRANSLATION 8 behavior 51 binary operator defining 55 blocking action 38 BNF grammar 57 body of process 25 book TLAt 1 Boolean operator 44 45 value 44 brackets square 14 in BNF grammar 57 built in operator of TLATt 8 bulleted list 45 c syntax 3 call PlusCal statement 26 as assignment 27 in with statement 24 not allowed in macro body 28 translation 65 Cardinality TL AT operator 47 CASE TLA expression 50 cfg file 68 checking assertion 10 invariant 16 37 termination 11 the algorithm 33 CHOOSE TLA operator 47 command line running translator and TLC from 5 command line running translator from 68 commas used instead of semicolons 7 12 comment in PlusCal algorithm 6 57 nested 6 comparable values 25 component assignment to 20 computational complexity 4 configuration file 68 conjunction A 44 conjunctions bulleted list of 45 CONSTANT TLA statement 7 35 constant operator 70 parameters 35 constant specifying value of 9 constraint 36 constructor set 47 control path 19 data refinement 54 deadlock 40 63 debugging 36 defaultInitValue 37 declaration of 60 define PlusCal statement 29 translation of 60 definition 5
6. 30 must follow goto statement 25 30 return statement 27 30 naming an atomic operation 52 needed at beginning of algorithm body 29 procedure body 17 26 29 process body 26 29 not permitted in with statement 17 24 30 of while statement 17 22 29 rules for 17 29 label translator option 18 67 labelRoot translator option 67 language algorithm 4 language programming 4 leads to gt 54 Len TLA operator 50 for strings 44 lineWidth translator option 68 list 49 liveness 38 53 checking and symmetry 41 local variable declaration 25 of procedure 26 of process 14 macro 28 57 76 call 28 parameter 28 macro PlusCal statement 28 Marzullo Keith 2 meaning reassigning in TLA 20 28 30 31 membership set 46 missing label error message 34 mode model checking 9 model creating in Toolbox 8 model value 35 model checking mode 9 module end of 8 imported 7 name 7 Naturals 7 ThA 7 TLC 7 17 modulus 43 multiple arguments function of 48 multiple assignment 6 21 multiple assignments to variable 21 27 30 not allowed in with 24 multiply defined symbol parsing er ror 20 30 32 multiprocess algorithm 11 execution of 26 multiprocessor computer running TLC on 41 mutual exclusion 16 myspec translator option 68 name of file 7 module 7 process 25 process set 25 63 Nat set of natural numbers 43 natural numbers 7 Naturals mod
7. Expr IW Variable A TLAF identifier that is not a PlusCal reserved word and is not pc stack or self Field A TL AT record component label Name A TLAF identifier that is not a PlusCal reserved word Label A TLA identifier that is not a PlusCal reserved word and is not Done or Error Expr A TLAF expression not containing a PlusCal reserved word or symbol Defs A sequence of TLAT definitions not containing a PlusCal reserved word or symbol TLA expressions and definitions are described in Section 5 A TLA record component label is any sequence of letters digits and _ characters containing at least one non digit and not equal to WF_ or SF_ A TLA identifier is a record component that is not one of the following ASSUME ASSUMPTION AXIOM CASE CHOOSE CONSTANT CONSTANTS DOMAIN ELSE ENABLED EXCEPT EXTENDS IF IN INSTANCE LET LOCAL MODULE OTHER UNION SUBSET THEN THEOREM UNCHANGED VARIABLE VARIABLES WITH The PlusCal reserved words are assert await begin call define do either else elsif end goto if macro or print procedure process return skip then variable variables when while with Some of these are keywords in the p syntax that are not used in the c KK KK syntax The PlusCal reserved symbols are and 59 B The TLA Translation B 1 The FastMutex Algorithm The TLA translation is described with the example algorithm of FastMutex in Figure 2 on page
8. 12 and 13 were all removed even if one of the assignments was to a different element of the array However a single multiple assignment such as x 1 1 x2 2 17 may assign to different components of the same variable e In the c syntax an opening brace cannot be both preceded and fol lowed by a label that is you can t write something like 11 12 The PlusCal translator will tell you if you have violated any of these rules Running it with the label option causes the translator to add any nec essary labels The text of the algorithm in the source file is not changed the translator adds the labels internally The reportLabels translator option is like the label option but it causes the translator to tell you where it added the labels The 1abel option is the default for a uniprocess algorithm if and only if you don t type any labels yourself If the algorithm contains no labels then the translator will add as few labels as possible resulting in an algorithm with the fewest possible steps Using the fewest steps makes model checking as fast as possible 18 3 The Language This section lists the statements and constructs of PlusCal and explains their meanings In doing so it also describes the language s grammar A BNF specification of the grammar appears in Section A on page 57 of the appendix Before getting to the language description we need some definitions A statement sequence is a sequenc
9. 13 I have simplified the translation a bit to make it easier to read but I have not altered its meaning To help you understand the translation of your own algorithm you can try executing the Toolbox s Goto PCal Source command on any region of the translation The translation begins CONSTANT defaultInit Value This declares defaultInit Value to be an unspecified constant By default a Toolbox model makes defaultInit Value a model value The declaration of defaultInit Value is omitted if every variable is explicitly initialized The translation next declares the algorithm s variables and defines vars to be the tuple of all these variables VARIABLES 2 Y b j pc A K vars x y b j pc The variable pc is added to describe the control state If an algorithm contains one or more procedures a variable stack is added to hold the calling stack In addition each formal parameter and local variable of a procedure is be declared to be a variable Had the algorithm contained a define statement the translation would have contained two VARIABLES statements the first declaring the variables z y b and pc and the second declaring the remaining variable j The definitions from the define statement would have been put between the two VARIABLES statements For a multiprocess program the translation next defines the set ProcSet of all process identifiers ProcSet 1 N Next is the definition of the initial predicate Init that sp
10. 36 sequence printed by TLC 36 statement sequence 19 step 19 52 of an algorithm 4 string 44 treatment by TLC 44 strong fairness 38 53 struct 48 subset 46 SUBSET TLAT operator 46 47 symbol symbol ASCII representation 72 typing 6 user definable 71 symmetry set of model values 41 symmetry used by TLC 41 42 syntaxes of PlusCal 3 Tail TLA operator 50 tail recursion 27 temporal formula 51 operator 51 54 71 termination 38 63 checking 11 Termination property defined by translation 11 64 termination translator option 11 39 then clause of if statement 19 then clause of if statement 21 threads running TLC with multiple Al TLAF 4 book 1 definition 55 placement of 16 19 55 module putting algorithm in 7 operator 43 54 tools web page 33 TLC running from command line 5 simulation mode 9 stopping 9 TLC model checker 33 error found by 36 on multiprocessor computer 41 treatment of strings 44 use of symmetry 41 TLC module 7 17 36 needed for assert statement 24 79 needed for print statement 24 Toolbox 5 creating file with 8 evaluating expressions with 43 Goto PCal Source command 34 37 60 translation 60 66 identifiers defined by 30 identifiers renamed by 31 of atomic operation 61 of procedure 65 66 variables declared by 30 translator 8 TLA specification 68 expressions changed by 34 options 67 69 running 33 35 running from co
11. A statement that appears in the body of an algorithm process procedure or macro must be either one of the statements listed below or else a compound statement A compound statement consists of a sequence of statements separated by semicolons with an optional semicolon at the end that is enclosed in braces Each statement s description includes the rules for labels that pertain to it The labeling rules are also all listed in Section 3 7 below 3 2 1 Assignment An assignment is either an assignment to a variable such as y A B or else an assignment to a component such as x fooli 1 y 3 20 If the current value of x is a record with a foo component that is a function array then this assignment sets the component x foo i 1 to the current value of y 3 The value of this assignment is undefined if the value of x is not a record with a foo component or if x foo is not a function Therefore if such an assignment appears in the code then x will usually be initialized to an element of the correct type or to be a member of some set of elements of the correct type For example the declaration variable x bar BOOLEAN foo 1 N gt f on off asserts that initially x is a record with a bar component that is a Boolean equal to TRUE or FALSE and a foo component that is a function with domain 1 N such that x foo i equals either on or ofP for each i in 1 N The symbol gt is typed
12. Name is an arbitrary name that you give to the process e is an expression Changing Name has no effect on the algorithm but changing the process s identifier e can make a difference Different processes must have different identifiers 15 Moreover the identifiers of all processes should have the same type for example they should all be integers or all be strings or all be sets of records The safety property that algorithm FastMutex should satisfy is mutual exclusion meaning that at most one process can be in its critical section at any one time For the PlusCal version this means that no two processes can be at the statement labeled cs An invariant is an assertion that is true in every state that can occur during an execution of the algorithm Mutual exclusion is the invariance of the assertion no two processes are at statement cs We can tell TLC to check that this assertion is an invariant But first we must know how to express the assertion in TLAT The TLA translation introduces a new variable pc whose value is the label of the next statement to be executed For algorithm FastMuter a process with identifier executes the statement labeled 15 next iff peli equals the string I5 For any multiprocess algorithm the value of the variable pc is a function whose domain is the set of process identifiers For a uniprocess algorithm the value of pc is a single string equal to the label of the next statement to be ex
13. begins the algorithm s body Adding or after a label has no effect for a sequential algorithm The termination option discussed in Section 2 5 on page 11 effectively adds a wf option if none of the fairness options described above is specified The liveness properties we want an algorithm to satisfy can be specified as temporal formulas using the TLA temporal operators used to express fairness and liveness are described in Section 5 10 on page 51 Temporal properties are subtle and can be hard to understand Chapter 8 of the TLA book discusses these properties in more detail Here we just describe one particular operator that is quite useful the operator typed gt and pronounced leads to The formula P Q asserts that if P ever becomes true then Q is true then or will be true at some later As an example let s consider algorithm 39 FastMutex in Figure 2 on page 13 We assume that the processes are fair so we add the keyword fair before the process We allow a process to remain forever inside its noncritical section or its critical section We therefore add after the labels ncs and cs The liveness condition the algorithm satisfies is that if some process is trying to enter its critical section then some process not necessarily the same one is or eventually enters its critical section A process i is trying to enter its critical section if pc i is in the set start 11 I10 It s easier
14. behavior s1 5 to be equivalent to the infinite behavior s1 5n 5n 5n Obtained by repeating the last state forever 5 10 1 Fairness An atomic operation of an algorithm consists of all control paths that start at some label l end at a label and do not pass through any label For example this code sequence Li if x 0 y y 1 else L2 await sem gt 0 sem sem 1 L3 contains the atomic operations Li if x 0 y y 1 else L2 L3 and L2 await sem gt 0 sem sem 1 L3 We name an atomic operation by the label that begins it so the second of these atomic operations is called operation L2 In TLAT an action is a formula describing how the state changes More precisely it is a formula that is true or false of a pair of states We say that s tisan A step iff action A is true of the pair s t of states An action A is said to be enabled in a state s iff it is possible to perform an A action in state s that is iff there is some state t such that s t is an A step For each atomic operation L of a PlusCal algorithm the TLAT trans lation defines an action L that represents the operation in other words where s gt t is an L step iff executing operation L in state s can produce state t We call Lan atomic action of the algorithm Appendix Section B on page 60 describes how atomic operations are represented as atomic actions Fairness assumptions about the algorithm are express
15. being reset to 0 then eventually L2 will be executed A process s next state action is defined to be the disjunction of all its atomic actions The most common fairness assumption is weak fairness of each process s next state action For a PlusCal algorithm weak fairness of a process s next state action is equivalent to the conjunction of weak fairness of each of its atomic actions Similarly strong fairness of a process s next state action in a PlusCal algorithm is equivalent to strong fairness of each of its atomic actions An algorithm s next state action is the disjunction of all of its atomic actions Weak fairness of the algorithm s next state action means that the algorithm will not halt if it is possible for some process to perform an action 5 10 2 Liveness The temporal properties that an algorithm should satisfy are expressed with the temporal operators O and which are defined as follows F is true of a behavior o iff the temporal formula F is true for every suffix of In other words OF is true for a behavior 51 s2 iff F is true on the behavior si Si 1 for all i gt 0 Hence if OF is true of then F is true of We usually think of OF as asserting that F is always true 53 OF is true of a behavior o iff the temporal formula F is true of some suffix of Since is a suffix of itself if F is true of t
16. binary infix operators For example the following defines typed to mean addition modulo N a b a b N Table 4 on page 71 lists all user definable operator symbols Table 5 on page 72 lists the non obvious ASCII versions of those symbols Definitions of operators or functions that are used in the PlusCal al gorithm must appear in the module before the BEGIN TRANSLATION line or in a define statement as described in Section 3 6 on page 29 Except for ones in a define statement definitions that use the identifiers declared or defined in the translation must come after the END TRANSLATION line Those identifiers are listed in Section 3 8 on page 30 TL AT does not use a semicolon or any other delimiter to end a definition It s customary to start each definition on a new line but that isn t necessary Two successive definitions can be separated by any kind of space character or characters References 1 Leslie Lamport TLA temporal logic of actions A web page a link to which can be found at URL http lamport org The page can also be found by searching the Web for the 21 letter string formed by concatenating uid and lamporttlahomepage 59 2 Leslie Lamport A fast mutual exclusion algorithm ACM Transactions on Computer Systems 5 1 1 11 February 1987 3 Leslie Lamport Specifying Systems Addison Wesley Boston 2003 Also available on the Web via a link at http lamport org 4
17. model it will add Termination to the Properties part of the What to check section of the Model Overview page This will cause TLC to check that all possible executions terminate The Termination property is included by the Toolbox for all PlusCal algorithms but its box is checked only if the termination property specified for the root module when the model is created If TLC discovers a non terminating execution it will produce an error message indicating that property Termination is violated and the Toolbox s error trace window will show the non terminating trace Section 4 4 on page 36 explains how to interpret the trace 2 6 A Multiprocess Algorithm Algorithm EuclidAlg is a uniprocess algorithm with only a single thread of control We now look at an example of a multiprocess algorithm writ ten in PlusCal The example is the Fast Mutual Exclusion Algorithm 2 The algorithm has N processes numbered from 1 through N Figure 1 on 11 nes noncritical section start b i true x 1 if y 4 0 then b i false await y 0 goto start fi y 1 if x 4 i then b i false for j 1 to N do await b 5 od if y 7 then await y 0 goto start fi fi critical section y 0 b i false goto ncs Figure 1 Process i of the fast mutual exclusion algorithm based on the original description this page is the original description of process number i except with the noncritical
18. or disproved asserts that any even number greater than 2 is the sum of two primes 2 Getting Started I assume here that you ve programmed in an imperative language like Java or Pascal or C I will therefore not bother to explain the meaning of something like a while statement that appears in such languages You can find the meaning of while and all other PlusCal statements in Section 3 The index can help you 2 1 Typing the Algorithm As an example consider the following bit of PlusCal code that describes Euclid s algorithm adapted from a version given by Sedgewick 5 page 8 It sets v to the gcd greatest common divisor of u and v while u 4 0 x is typed or or neq if u lt v u v L Ax swap u and v u u v The and in the if statement are not necessary because the multiple assignment is considered to be a single statement Comments indicate how to type symbols such as 4 that appear in the examples A complete list of the ASCII versions of symbols appears in Table 5 on page 72 You should find this code easy to understand except for the in the if statement on the second line Assignments separated by s rather than by semicolons form a single multiple assignment statement that is exe cuted by first evaluating all the right hand sides then doing the assignments Thus as the comment says the multiple assignment swaps the values of u and v The snippet of algorithm also indica
19. or tuple of identifiers 3 e1 or h may be replaced by a comma separated list of items a a where each a is es or h Table 1 The operators of TLAT 70 IF p THEN ej ELSE 2 e1 if p true else e2 CASE p gt e 0 O Pn gt en Some e such that p true CASE p gt e1 0 O Pn gt en O OTHER gt e Some e such that p true or e if all p are false LET d 2 ey dn 2 en IN e e in the context of the definitions A p the conjunction p A A Pr V p the disjunction pj V V Pn NM Pn V Pn Table 2 Miscellaneous constructs F OF F is eventually true F is always true WF 4 Weak fairness for action A SF A F G Strong fairness for action A F leads to G Table 3 Temporal operators 1 0 41 2 o 3 kad U 1 4 a 0 o DR geo O B O 4 lt LU gt 1 lt 1 gt 1 lt lt z lt gt lt gt amp KK E J c J C D D QQA L 4 HH O lt 2 11 x H y 1 Defined by the Naturals Integers and Reals modules 2 Defined by the Reals module 3 3 Defined by the Sequences module 4 x7 y is printed as x 5 Defined by the Bags module 6 Defined by the TLC module Table 4 User definable operator symbols 71 L IU U L IU IY Y y IV Vogel lt a ETE el A o
20. self Proc self nes self V start self v IL self V 12 self v 13 self V 14 self v 15 self v 16 self V I7 self V 18 self V 19 self v 110 self V cs self V 111 self v 112 self The action Next is defined to be the next state action of the entire algorithm It is the disjunction of the next state actions of all the processes The existential quantification is equivalent to the disjunction Proc 1 V V Proc N Neat VAself 1 N Proc self V Disjunct to prevent deadlock on termination AV self ProcSet pc self Done UNCHANGED vars The last disjunct of Next is added for TLC s benefit TLC has no way of distinguishing deadlock from termination which is simply a desired form of deadlock The translation therefore adds a disjunction to Nezt that allows a terminated algorithm to perform a step that does nothing This transforms termination into an infinite no op loop so it is not reported as deadlock by 63 TLC Since the FastMutex algorithm cannot terminate the disjunct serves no function in this case However the translator is not clever enough to notice that the disjunct is unnecessary The noDoneDisjunct translator option always suppresses this extra disjunct The translator next defines formula Spec to be the complete TLA speci fication of the algorithm The formula will mean nothing to you if you don t know TLA but that doesn t matter You don t need to understand TLA to use P
21. some process has not terminated The usual way for this to happen is for each processes to be waiting either at an await statement whose expression is false or at a statement of the form with x S when S equals the empty set 40 Deadlock is normally an error and is reported by TLC However some times an algorithm is supposed to halt in a state in which not all processes have reached the end of their code To stop TLC from checking for deadlock uncheck the Deadlock box on the Model Overview page 4 7 2 Multithreading TLC can execute with multiple threads to take advantage of a multiprocessor computer You specify the number of threads it should use in the How to run section of the Model Overview page The number you choose should be at most equal to the number of actual processors the computer has Running it with more threads than there are processors can slow TLC down In theory using w processors can speed up TLC s computation of the set of reachable states by a factor of almost w In practice the speedup depends on the quality of the Java runtime s implementation of multithreading TLC s algorithm for checking liveness is single threaded so additional worker threads will not speed up that part of TLC s execution 4 7 3 Symmetry Many algorithms are symmetric in a set of values For example the fast mu tual exclusion algorithm described in Section 2 6 on page 11 is symmetric in the set of process identifiers
22. to a variable x and any other statement that assigns a value to xz A local variable or parameter of a procedure P is set by a call P or return statement in P The implicit labels Done and Error cannot be used as actual labels 3 8 The Translation s Definitions and Declarations This section lists all the identifiers declared and defined in the TL AT trans lation of a PlusCal algorithm You may need to know what those identifiers are when writing invariants and liveness properties to check the algorithm Moreover as explained on page 20 of Section 3 1 TLATt does not allow the assignment of a new meaning to an identifier that already has a meaning Redefining an identifier declared or defined by the translation or using it as a bound variable will cause a multiply defined identifier error when the TLAt module is parsed by the SANY parser which is invoked by the Toolbox The translation of a PlusCal algorithm declares the following TLA variables e Each variable declared either globally or locally within a process or a procedure e pc e stack if the algorithm contains one or more procedures e Each formal parameter of a procedure 30 A multiprocess PlusCal algorithm defines each of the following For a uni process algorithm the self argument is omitted For a multiprocess algorithm the set ProcSet of all process identifiers The tuple vars of all variables The initial predicate Init It contains a
23. 25 name of 25 next state action of 53 set 25 action defined for 31 name of 25 63 variable 14 process PlusCal construct 14 25 ProcSet defined by translation 30 60 program versus algorithm 4 programming language 4 quantification 45 46 quantifier nesting 46 reachable states 10 36 record 48 as function 48 recursion tail 27 recursive definition 55 refinement data 54 refinement interface 54 renaming by translation 31 reportLabels translator option 18 69 reserved words 59 return PlusCal statement 27 as assignment 27 in with statement 24 not allowed in macro body 28 translation 65 rules for labels 17 29 SANY parser finds algorithm errors 33 34 Sedgewick Robert 6 self PlusCal identifier 14 26 27 61 semicolon not used in TLAt definitions 29 55 78 semicolons used instead of commas 7 12 Seq TLA operator 50 sequence 49 50 of statements 19 of states printed by TLC 36 Sequences Module 50 set 46 47 constructor 47 difference 1 46 membership 46 of all 47 power 46 47 process 25 SETL 4 sf translator option 39 64 skip PlusCal statement 14 24 Spec defined by translation 31 64 spec translator option 68 special character in string 44 specification of the algorithm 64 square brackets 14 in BNF grammar 57 stack variable 30 60 65 in define statement 29 value 65 state 36 predicate 54 reachable 10
24. 5 of binary operator 55 74 placement of 16 29 55 definitions overriding 35 definitions overriding 35 difference set 1 46 disjunction V 44 disjunctions bulleted list of 45 division integer 43 do clause of while statement 22 DOMAIN TLA operator 47 domain of a function 47 Done implicit label 16 not usable as label 30 either PlusCal statement 22 when label must follow 22 30 else clause of if statement 21 empty set 46 enabled 38 52 enabling condition 61 end of module 8 END TRANSLATION 8 equivalence 44 error found by TLC 36 found by translator 33 missing label 34 multiply defined symbol 20 30 32 Error implicit label 26 not usable as label 30 Euclid s algorithm 6 eventually 54 EXCEPT TLA construct 49 used in translation 34 61 exclusion mutual 16 execution of multiprocess algorithm 26 existential quantification 45 exponentiation 43 expression changed by translator 34 evaluating with Toolbox 43 not parsed by translator 33 PlusCal 19 43 51 EXTENDS TLA statement 7 factorial definition of 55 failure of assertion 24 fair PlusCal construct for sequential algorithm 39 fair algorithm PlusCal construct 39 fair process PlusCal construct 38 64 fair process PlusCal construct 39 64 fairness 38 52 for non blocking action 38 strong 38 weak 38 FALSE 44 Fast Mutual Exclusion Algorithm 11 FastMute
25. A PlusCal User s Manual C Syntax Version 1 8 Leslie Lamport 21 October 2015 There is also a P Syntax version of this manual See page 3 for a description of the two syntaxes Contents Preface The Two Syntaxes 1 Introduction 2 Getting Started 2 1 2 2 2 3 2 4 2 5 2 6 2 7 3 The 3 1 3 2 3 3 3 4 3 5 3 6 3 7 3 8 Typing the Algorithm aoaaa aaa The TLA Mod le s e oe ia riet A a ad Translating and Executing the Algorithm Checking the Results oaoa aa a Checking Termination a A Multiprocess Algorithm Where Labels Must and Can t Go Language Expressions bit e Bea A ocd Ee et The Statements A See ie wh i 3 2 1 3 2 2 3 2 3 3 2 4 3 2 5 3 2 6 3 2 7 3 2 8 3 2 9 3 2 10 3 2 11 ASSIM sy ick tess sade Aiea ee wa aT al E al okt AD A Either lt REC gee R N ae eed Ee de While 2 an ea Sad ee e Re Gee ea LOG wa ee be Ae a a Ete E PrOCESSESe o Pern sonta ot do De ee Ay Ga ety to e a dois Procedures ro g 4m Ae a RE eS wet be AD en Macros Definitions A es et A PAS ES Labels The Translation s Definitions and Declarations 4 Checking the Algorithm 4 1 Running the Translator 4 2 Specifying the Constants 0 4 AS Consttaints i Sip eke oe Gea ee ae ee NE a 4 4 Understanding TLC s Output 4 5 Invariance Checking o e o 4 6 Termination
26. C Translator Options Some translator options can be specified in the module file with an options statement It has the form PlusCal options list of options where the items in the list may be but need not be separated by commas In the options statement the in the option name may be omitted Any options may be specified in the Toolbox as follows In the Spec Explorer which can be raised from the File menu right click on the specification and select Properties Put the list of options with in the option names and without commas in the PlusCal call arguments field Options That May Appear in an options Statement wf Change all unfair processes to weakly fair fair processes sf Change all unfair processes to strongly fair fair processes wfNext Conjoin to specification Spec weak fairness of the algorithm s entire next state action nof Conjoin no fairness assumption to specification Spec termination If no fairness option is selected it is equivalent to select ing the wf option When it appears in an option statement in a specification s root module it causes new Toolbox models to specify termination checking When used in command line mode see below it adds to the cfg file a command to cause TLC to check for termina tion noDoneDisjunct Suppress the extra disjunct that the translation normally adds to the next state action Next to prevent TLC from thinking that the algorithm has deadlocked
27. C are given We show the typeset versions of all expressions Table 5 on page 72 shows how symbols with no obvious ASCII representation are typed TLA keywords are typed with upper case letters so TRUE is typed as TRUE If you re not sure about the meaning of some construct try it out with the Toolbox You can have the Toolbox print the value of any constant expression by typing it into the Evaluate Constant Expression section of a model s Model Checking Results page This will cause TLC to evaluate the expression and print the result in the Value box You can tell TLC not to do any checking of the specification by selecting No Behavior Spec in the What is the behavior spec section of the Model Overview page This will be the default selection if you create a module with no algorithm and no VARIABLE declaration 5 1 Numbers Non negative integers are typed in the usual way as strings of decimal digits The standard module Naturals defines the following standard operators on integers x exponentiation lt gt lt gt where is subtraction not the unary negation operator The expression a is typed a b The operator is defined so a b is the set of all integers c such that a lt c lt b The modulus operator and the integer division operator are defined so that for any integer a and positive integer b the value of a b is in 0 b 1 and a bx a b a b The Naturals module also d
28. For example Head 3 7 equals 3 Tail s The tail of sequence s which consists of s with its head re moved For example Tail 3 7 a equals 7 a Append s e The sequence obtained by appending element e to the tail of sequence s For example Append 3 7 3 equals 3 7 3 sot The sequence obtained by concatenating the sequences s and t For example 3 7 o 3 equals 3 7 3 Len s The length of sequence s For example Len 3 7 equals 2 5 9 Miscellaneous Constructs An IF expression has the form IF bool THEN t_expr ELSE e_expr If bool equals TRUE then this expression equals t_expr if bool equals FALSE then it equals e_expr The CASE expression CASE p gt i es Pn gt en equals some e for which p equals TRUE If there is no such p then the value of the expression is unspecified and TLC will report an error when evaluating it For example the value of the expression CASE iE 1 N gt a 1EN 2xN gt b e a ifiisinl N 1 e b ifiisin N 1 2 N 50 e either a or b ifi N e unspecified if 2 is not in 1 2x x N and TLC reports an error when evaluating it ur In the third case whether the expression equals a or b it equals the same value every time it is evaluated The CASE expression CASE p gt e O0 O pn gt en O OTHER e is equivalent to
29. J T Schwartz R B Dewar E Schonberg and E Dubinsky Program ming with sets An Introduction to SETL Springer Verlag New York 1986 5 Robert Sedgewick Algorithms Addison Wesley 1988 56 Appendix Section A gives the BNF grammar of PlusCal and Section B describes the TL AT translation of a PlusCal algorithm A The Grammar The algorithm must appear in a file with a TLAt module either outside the module or within a single comment In the latter case it will almost surely be enclosed by and Comments within an algorithm are delimited by Ax or The grammar described here is for an algorithm with every comment removed and replaced by one or more spaces Here is a simplified BNF grammar for the algorithm text It does not express the restrictions on where labels must or may not occur which are explained in Section 3 7 on page 29 It also does not express the restrictions on what statements may occur in the body of a macro namely that a while call return goto or macro call may not appear there The BNF uses the following notations e The square brackets and are BNF grouping symbols but and are literals e a b means a or b e a means 0 or 1 instance of a e a means 0 or more instances of a e a means 1 or more instances of a The grammar is Algorithm algorithm fair algorithm name VarDecls Definitions Macr
30. Liveness and Fairness 4 7 Additional TLC Features e 4 7 1 Deadlock Checking ooa 4 7 2 Multithreading S Syet ts Fees BG A cen 5 TLAt Expressions and Definitions Bil Numbers e e ae ada Ody OTNES lt 2 KRA a Dee A a EE hae ee HG 5 3 Boolean Operators e o BA A O AN oe eee K 0 07 FUNCTIONS sce io a A ad ee Bot SB Recordsi to A Yoh a te eo an ab AS 5 7 The Except Construct 0 0 0 0 0000 2 eee ee 5 8 Tuples and Sequences o 5 9 Miscellaneous Constructs 2 0004 5 10 Temporal Operators 2 0 00 0004 TOL Fairness su a sete Rat plate a Goes Be Ae a 5 102 LIVERESS s a ech ache oc eG he ee eed td 5 10 3 One Algorithm Implementing Another 5 11 TLAT Definitions td aes Sed arb ee le ys References A The Grammar B The TLA Translation B 1 The FastMutex Algorithm B 2 Procedures 00 ee a a a A C Translator Options Useful Tables Index 33 33 35 36 36 37 38 40 40 41 41 43 43 44 44 46 47 48 49 49 50 5l 52 53 54 55 55 57 60 60 65 67 70 73 Preface This is an instruction manual for Version 1 4 of the c syntax version of the PlusCal algorithm language The following section on page 3 explains the difference between this syntax and the alternative p syntax Section 1 explains what an algorithm language is and why you d w
31. This means that given any possible execution of the algorithm permuting the set of identifiers of the processes yields a possible execution Exactly what symmetry means is explained in Section 14 3 4 on page 245 of the TLAT book When assigning a set of model values to a constant we can specify that set to be a symmetry set Model values are explained on page 35 TLC will then speed up its checking of the algorithm by ignoring any new state it finds that is the same as a state it has already found under a permutation of that set of model values TLC can use symmetry only for a set of model values For TLC to take advantage of the symmetry of algorithm FastMutez that algorithm would have to be rewritten to use an arbitrary set of process identifiers instead of the set of numbers 1 NV When we instruct TLC to assume that an algorithm is symmetric it does not check whether the algorithm really is symmetric That s our re sponsibility Do not tell TLC both to assume symmetry and to check liveness The interaction of a symmetry assumption with TLC s algorithm for checking Al liveness is subtle It s hard to determine if liveness checking will produce correct results when symmetry is assumed 42 5 TLA Expressions and Definitions We now describe the TL AT operators with which PlusCal expressions are built They are also listed with brief explanations in Tables 1 3 on pages 70 71 Only TLA operators that can be evaluated by TL
32. You can check that this equals f EXCEPT c f c EXCEPT d f c d EXCEPT llel exp U An EXCEPT expression can have multiple clauses For example the expression f EXCEPT c expl d e exp2 equals the value of f after executing the PlusCal multiple assignment statement Fle exp1 f d e lt exp2 Remember that a multiple assignment is executed by first evaluating all the right hand expressions then performing the assignments from left to right This implies that f EXCEPT c expl d e exp2 is equal to f EXCEPT c exp1 EXCEPT d e exp2 5 8 Tuples and Sequences A finite sequence is what programmers usually call a list In TLAT a sequence of length n is the same as an n tuple which is defined to be a function with domain 1 n Finite sequences are written in angle brackets L T The sequence e1 en is the function s with domain 1 n such that s i equals e for each in 1 n Thus a bc de 3 equals de 49 Sets of tuples can be described with the Cartesian product operator x For example Nat x Int x a b c is the set of all triples z y z such that z Nat y Int and z a b c The standard module Sequences defines the following operators Seq S The set of all sequences of elements of the set S For example 3 7 is an element of Seq Nat Head s The first element of sequence s
33. algorithm It does this by repeatedly finding all states that can be reached with a single step from a reachable state that it has already found starting with all possible initial states It will run forever if there are an infinite number of reachable states Some algorithms have infinitely many reachable states because they have counters or queues that can grow without bound You can limit the reach able states that TLC examines by using a constraint which is an arbitrary Boolean expression If TLC finds a reachable state s that does not satisfy the constraint then it will not look for states that can be reached from s You can specify such a constraint in the State Constraint section of the model s Advanced Options page For example the constraint x lt 17 causes TLC to find only those reachable states that are either initial states or are reachable by a sequence of states all having x less than 17 4 4 Understanding TLC s Output There are two kinds of errors TLC can find i an assert statement is executed when its expression is false or some property that you asked TLC to check is not satisfied or ii the algorithm is trying to evaluate a meaningless expression such as foo bar if foo does not equal a record In the first case TLC tells you which assertion or property is violated In the second it usually reports the stack of nested expressions it was executing when it found the error but in some cases it just prints the unhelpful
34. alue of x is greater than the process s identifier self An action like a that is enabled iff control is at that label is said to be non blocking An action like b that is not non blocking is said to be blocking Fairness for a non blocking action means that the process cannot stop at that action Thus fairness at a means that if control in the process is at a then the process must eventually execute action a There are two kinds of fairness conditions for blocking actions Weak fairness of an action a means that a process cannot halt at a if a remains for ever enabled For example weak fairness of action b means that if x gt self remains true while the process is at b then action b is eventually executed Strong fairness of a means that in addition to a process not being able to halt at a if a remains true forever it can t halt if a keeps being disabled and subsequently enabled For example strong fairness of action b implies that process self cannot halt at b as long as x gt self either remains true or keeps becoming true even if it also keeps becoming false For a non blocking action weak and strong fairness are equivalent so there is only one kind of fairness Writing fair process instead of just process asserts that all actions of the process are by default weakly fair The default fairness condition of an action of the process can be modified by adding of after its label 38 Writing a asserts that action a is str
35. ant to use one Section 2 tells you what you need to know to get started using PlusCal After reading it you ll be able to write and check PlusCal algorithms You can read the other parts of this manual as you need them The table of contents and the index can help you find what you need Pages 70 72 at the end just before the index contain a series of tables that summarize a lot of useful information The rest of the manual is arranged in the order you re likely to want to look at it e Section 3 describes the things you ll find in most programming lan guage manuals like the statements of the language Once you ve started writing PlusCal algorithms you should browse this chapter to learn about features of PlusCal not mentioned in Section 2 e We run programs but we check algorithms Section 2 gets you started using the translator and TLC model checker to check PlusCal algo rithms Section 4 tells you more about the translator and TLC It s mostly about TLC describing some of its additional features and how to use it to debug an algorithm You should go to Section 4 if you don t understand what the translator or TLC is trying to say when it reports an error e Section 5 is mainly about writing PlusCal expressions The expression language of PlusCal is much richer and more powerful than that of any programming language because it is based on mathematics not on programming The ten or so pages about expressions in Section 5 just introdu
36. assert Vi 1 N i self gt pcli 4 cs V is typed NA and gt is typed gt When using an assert we must also import the TLC module in the EXTENDS statement Invariance checking is discussed further in Section 4 5 Section 4 6 de scribes how to check liveness properties which are the generalization of termination 2 7 Where Labels Must and Can t Go The labeling of statements in a PlusCal algorithm is not completely arbitrary but must obey certain rules The complete list of rules is given in Section 3 7 on page 29 Here are the most common rules which apply to the FastMutex algorithm e The code for each process and a uniprocess program must begin with a label e A while statement must be labeled e The do clause of a with statement cannot contain any labeled state ments This rule restricts what can appear within a with statement for example it prohibits nesting a while inside a with These restric tions apply even when you let the translator add labels The complete list of such restrictions is given in Section 3 2 6 on page 23 e An if statement that contains a label within it must be followed by a label For example label 15 of algorithm FastMutex cannot be omitted e In any control path from one label to the next there cannot be two separate assignment statements to the same variable For example this rule would be violated by two assignments to variable b if labels 11
37. asserts that control of process self is at label ncs The action sets pc self to start the UNCHANGED conjunct asserts that the values of all other variables are not changed The evaluation of the while test does not appear explicitly in the action because it equals TRUE The skip statement similarly does not appear because it has no effect The atomic actions corresponding to the statements labeled start and 1 are analogous A start self A pc self start Ab b EXCEPT self TRUE A pe pc EXCEPT self 11 A UNCHANGED zx y J lL self A pelself 11 A x self A pc pc EXCEPT self 12 NA UNCHANGED y b j 61 Action 12 performs the if statement s test and the subsequent transfer of control 12 self A pelself 12 AIF y 40 THEN pc pc EXCEPT self 13 ELSE pc pc EXCEPT self I5 A UNCHANGED 2 y b j The body of the then clause of statement 2 consists of two atomic actions 13 self A pelself 13 A b b EXCEPT self FALSE A pe pc EXCEPT self 14 NA UNCHANGED 2 y j l4 self E A pelself 14 Ay 0 A pc pc EXCEPT self start N UNCHANGED z y b j The expression y 0 of the await statement is an enabling condition of action 14 Recall that this means the action can be executed only when y 0 is true The conjunct pc self 14 is the other enabling c
38. body of a process set self equals the current process s identifier A multiprocess algorithm is executed by repeatedly choosing an arbitrary process and executing one step of that process if that step s execution is possible Execution of the process s next step is impossible if the process has terminated if its next step contains an await statement whose expression equals FALSE or if that step contains a statement of the form await x S and S equals the empty set As explained in Section 2 6 on page 11 fairness conditions may be specified on the choice of which processes steps are to be executed 3 4 Procedures An algorithm may have one or more procedures If it does the algorithm must be in a TLAt module that EXTENDS the Sequences module The algorithm s procedures follow its global variable declarations and define section if any and precede the that begins the body of a uniprocess algorithm or the first process of a multiprocess algorithm A procedure named PName begins procedure PName param paramy where the identifiers param are the formal parameters of the procedure These parameters are treated as variables and may be assigned to As ex plained in Section 4 5 on page 37 there may also be initial value assignments of the parameters The procedure statement is optionally followed by declarations of vari ables local to the procedure These have the same form as the declara tions of global
39. ce the subject You can learn more from the book Specifying Systems referred to here as the TLA book 3 or from any books on the elementary mathematics of sets functions and logic especially ones written by mathematicians and not computer scientists e Section A of the appendix contains a BNF grammar of PlusCal The subjects of Appendix Sections B and C will make no sense to you until you ve read Section 1 Don t forget about the table of contents the tables on pages 70 72 and the index I wish to thank the people who helped make PlusCal possible Keith Marzullo collaborated in the writing of the translator and helped with the design of the PlusCal language Georges Gonthier made many useful sug gestions for the language The Two Syntaxes PlusCal has two separate syntaxes the prolix p syntax and the more com pact c syntax Here is a snippet of code written in the two syntaxes P Syntax C Syntax while x gt 0 do while x gt 0 if y gt O then y y 1 if y gt 0 y y 1 x x 1 x x 1 L else x x 2 else x x 2 end if print y end while print y The additional wordiness of the p syntax makes the meaning of the code clearer and its use of explicit ends instead of s makes it easier to find syntax errors However the c syntax version is shorter and sensible for matting makes the meaning of the code clear enough You may prefer the c syntax version if you re used to programming in a lan
40. conjunct for each variable The conjuncts for global variables precede those for local procedure and process variables The conjuncts for the variables declared in a single variable statement appear in the order in which they are declared This order is significant since the initial value of a variable can depend on the initial values assigned by previous conjuncts The next state action Next and the complete specification Spec For each statement label Lab an action Lab self if the statement is in a procedure or in a process set otherwise an action Lab This action is the TLATt representation of the atomic operation beginning at that label Actions and atomic operations are discussed in Sec tion 5 10 1 on page 52 If the definition is of Lab self then this is the action describing the operation performed by a process self for self in ProcSet For each procedure P an action P self It is the disjunction of all actions in the procedure executed by a process with identifier self in ProcSet For each process set named P an action P self It is the disjunction of all actions not in a procedure that are executed by a process with identifier self in the process set For each single process named P an action P that is the disjunction of all actions not in a procedure that are executed by the process Because TLA does not allow an identifier to be declared or defined multiple times the translation may rename some of these identif
41. e TL AT parser ignores the double quotes and considers to end a comment To keep both the TLAT parser and the PlusCal translator happy you have to write something like this LY x the delimiter A similar trick works for 5 3 Boolean Operators The Boolean values are written TRUE and FALSE The set BOOLEAN contains these two values The five propositional operators on Booleans are A conjunction and typed N implication typed gt V disjunction or typed equivalence typed lt gt negation not typed or Nequiv The four binary operators are defined by the truth tables of Figure 3 on the next page The operator is defined by TRUE FALSE FALSE TRUE 44 F G FAG F G FVG TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE FALSE TRUE FALSE TRUE FALSE TRUE FALSE FALSE TRUE TRUE FALSE FALSE FALSE FALSE FALSE FALSE F G F gt G F G F G TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE FALSE TRUE FALSE FALSE FALSE TRUE TRUE FALSE TRUE FALSE FALSE FALSE TRUE FALSE FALSE TRUE Figure 3 Truth tables for the binary Boolean operators In addition to the usual binary operators A and V TLA also allows a bulleted list notation for conjunctions and disjunctions For example the expression AA AV D VC AD equals AA BV C A D Indentation i
42. e of statements each ended by a semicolon For example the body of a while statement consists of a sequence of state ments If there is an if statement in that sequence of statements then its then clause the statement or the sequence of statements enclosed in braces that follows the if test consists of a separate sequence of statements The statements in the then clause are not part of the sequence that forms the while s body It is the if statement not the statements that occur inside it that is a statement of the while s body A control path is a path through a piece of PlusCal code that represents a syntactically possible execution sequence if we ignore how the statements are executed For example in the code a if FALSE Y goto W b x 73 Chop eB d x 0 there is a control path that goes from the label a to the label c even though no execution can actually follow that path A step is a control path that starts at a label ends at a label and passes through no other labels In the example above there are two steps beginning at label a one that ends at b and one that ends at d Remember that there is an implicit label Done at the end of a uniprocess algorithm and at the end of each process in a multiprocess algorithm An execution of a PlusCal algorithm consists of a sequence of executions of steps Part of a step can never be executed by itself except for a print or assert statement as described below 3 1 Ex
43. ecifies the initial values of all the declared variables Comments indicate if the variables are global or local to a process or procedure Init Global variables Az defaultInit Value Ay 0 60 Ab i 1 N gt FALSE Process Proc Aj lself l N gt XQ A pe self ProcSet nes Observe that the process local variables and the variable pc are made func tions with domain equal to the appropriate set of process identifiers Next come the action definitions As explained in Section 5 10 1 on page 52 a TLA action is a formula describing a pair of states the state before executing the action and the state after executing it In an action unprimed variables refer to their values before executing the action and the primed variables refer to their values after the execution The translation defines an action for each atomic operation of the algo rithm As explained in Section 5 10 1 an atomic operation begins at a label that is used to name the action The first such action definition is generated by statement ncs The definition is parameterized by the identifier self which represents the current process s identifier The EXCEPT construct is explained in Section 5 7 on page 49 nes self A pe self nes A pe pc EXCEPT self start NA UNCHANGED zx y b j The conjunct pc self ncs is an enabling condition meaning that the action can be executed only when it is true It
44. ecuted There is an implicit label Done at the end of every process and at the end of a uniprocess algorithm Since a process of algorithm FastMutex never terminates pc i never equals Done for any process i In algorithm FastMutex a process i is at statement cs iff peli equals cs Mutual exclusion is therefore asserted by the invariance of the predi cate Mutezx defined by D Muter Vig k LANA pe i es A pefk cs The operators like Y gt and A are explained in Section 5 3 on page 44 Section 3 8 on page 30 explains why we could not use the identifier j instead of k in the V expression TLA allows a definition to refer only to variables and operators that have already been defined or declared Since the definition of Mutex uses the variable pc which is declared by the translation of the algorithm this definition must come after the translation in other words after the END TRANSLATION line We tell TLC to check the invariance of Mutex by adding it as an invariant in the What to check section of the Model Overview page We need not have defined Mutex in the module we could instead just use its definition Vi ke1 N 1 k pe i cs A pc k es 16 as the invariant to check The variable pc can be used in the algorithm s expressions We could therefore also check mutual exclusion by replacing the skip statement cs with assert statement in statement cs cs
45. ed with the follow ing fairness assumptions about actions Weak Fairness of an action A means that if it remains continuously pos sible to execute A then A is eventually executed Weak fairness of A is expressed by the temporal formula WF yars A typed WF_vars A where vars is the tuple of all variables of the algorithm This formula 52 asserts of a behavior s1 s2 that if there is some gt 0 such that A is enabled in state s for all j gt i then sj gt s 41 is an A step for some j gt i Strong Fairness of an action A means that if it is repeatedly possible to execute A even if it is repeatedly impossible to execute A then A is eventually executed Strong fairness of A is expressed by the formula SF yars A typed SF_vars A This formula asserts of a be havior 81 52 that if A is enabled in infinitely many states sj then sj gt s 41 is an A step for some j gt 0 Strong fairness of A is stronger than implies weak fairness of A In other words if SF yars A is true of a behavior then WF yars A is also true of o As an example let L2 be the atomic action corresponding to the atomic operation L2 above on the preceding page Weak fairness of L2 means that if the process is at control point L2 and sem remains positive then eventually operation L2 will be executed Strong fairness of L2 means that if the process is at control point L2 and sem keeps being set to a positive value even if it keeps
46. efines Nat to be the set of all natural numbers non negative integers The Integers module defines everything the Naturals module does plus the unary operator and the set Int of all integers You are unlikely to use Nat or Int in an algorithm but you might very well write something like n Int in a type correctness invariant Section 4 5 43 5 2 Strings Strings are enclosed in double quotes so the string abc is typed abc The following pairs of characters are used to represent certain special char acters in strings ye 0 Xt tab f form feed WN n line feed r carriage return A string is defined in TLAT to be a sequence of characters but TLC does not treat them as first class sequences TLC treats strings as a primitive data type except that the operators o concatenation and Len length defined in the standard Sequences module work properly on them for example TLC knows that ab o c equals abc and Len abc equals 3 These operators are described in Section 5 8 on page 49 below Even though sequences in TLA are functions TLC does not regard them as such and it cannot evaluate abc 2 Putting the TLAt comment delimiters and inside strings in a PlusCal algorithm is tricky if the algorithm appears in a comment as it probably does For example suppose your algorithm contains the statement x the delimiter Because this appears inside a comment th
47. ence concatenation 50 for ar 44 always 5 a 53 54 less than 43 x gt A ox less nE or equal 4 subset 4 dE sl 6 e function application 14 47 11 gt 1 An gt en record con structor 48 z S gt e function constructor 12 48 hy S1 An Sn set of records 48 e1 en tuple sequence 49 1 empty set 46 e1 en set 46 SRFINIAA O x e S P x set constructor 47 always An e 1 x S set constructor 47 greater than 43 greater than or equal 43 conjunction 44 set intersection 46 disjunction 44 set union 46 TL AT operator 36 48 in EXCEPT 49 modulus 10 43 TLAF operator 36 48 Y universal quantification 45 3 existential quantification 45 e Hilbert s 47 set membership 46 in with statement 23 in variable initialization 7 M eae 0 IV N action 52 61 atomic 52 blocking 38 corresponding to label 31 38 defined for procedure 31 defined for process set 31 defined for single process 31 enabled 52 next state 31 53 63 non blocking 38 action atomic 14 algorithm beginning of 6 language 4 multiprocess 11 placement of 8 uniprocess 11 versus program 4 53 73 and A 44 angle brackets 49 Append TLA operator 50 array 47 ASCII representation of symbol 72 assert PlusCal statement 10 17
48. ere is some gt 0 such that F is true of 8 j41 for all j gt i s F G is equivalent to O F gt OG 5 10 3 One Algorithm Implementing Another Instead of just checking that an algorithm satisfies certain properties you can check that it implements a complete higher level specification describ ing what the algorithm is supposed to do The TLAt book explains how to write such a specification in TLAF You can also write the specification as a more abstract PlusCal algorithm In that case you will have to show that the algorithm implements its more abstract version under an interface refine ment Interface refinement is explained in Section 10 8 of the TLA book In most cases the interface refinement will be a simple data refinement 54 5 11 TLA Definitions TLA allows you to define operators that take zero or more arguments Ordinary operator definitions have the two forms F expr F p1 Pn 2 expr The symbol 2 is typed The identifier F and the formal pa rameters p must not already have a meaning All identifiers other than the pi that appear in the expression expr must already have a meaning Hence recursive definitions cannot be written in this way TLAT does allow recursive function definitions of the form fle S expr For example you can define the factorial function by fact n Nat IF n 0 THEN 1 ELSE nx fact n 1 TLA also permits definitions of
49. ery d in S For example li 1 2 3 gt 2 x 2 is the function twice with domain 1 2 3 such that twice 1 1 twice 2 4 twice 3 6 Using the operators QQ and gt defined in the TLC module this function can also be written 1 gt 1 2 gt 4 QA 3 gt 6 For any sets and T the expression S T is the set of all functions f with domain S such that f d is in T for all d in S Functions are first class values so f d can be a function For example the function li Nat j E1 N 2x1 j is a function f such that f 3 z equals 6 zx TLA also allows functions of multiple arguments For example i Nat jel1 N gt 2xi j is a function g of two arguments such that g 3 xz equals 6 x A function with multiple arguments is actually a function with a single argument that is a tuple For example g 3 x is shorthand for g 3 x Section 5 8 on the next page discusses tuples 5 6 Records TL AT provides records that are much like the records also called structs of ordinary programming languages If exp is a record valued expression then exp bar is the bar field of that record The expression foo gt 17 bar 1 2 3 equals the record r containing a foo field whose value is 17 and a bar field whose value is the set 1 2 3 This record r is an element of the set foo Nat bar SUBSET 1 13 consisting of all records with a foo field that is an element of the set Nat of natural n
50. expression ended by oe oe 33 The lesson to be learned from this example is that the source of an error can come well before the location where the error is reported If you can t find the cause of an error try narrowing in on it by running the translator with sections of the code commented out You can do this by bracketing the code with and even if it contains comments The second class of error that can be mysterious is one caused by omit ting a needed label This is indicated by an error message like Missing label at the following location Section 3 7 on page 29 gives the rules for where labels are needed If you are mystified by this message it may be because you ve forgotten that call and return statements assign values to a procedure s parameters and local variables As explained above some errors in the algorithm are not found by the translator but by SANY the TLAT parser The error can be either in the part of the module that you wrote or in the part written by the translator The translator does not parse expressions leaving it to SANY to find most errors in the algorithm s expressions Clicking on the error message in the Toolbox jumps to and highlights the error in the translation Executing the Toolbox s Goto PCal Source command jumps to the corresponding region of PlusCal If the source of the problem is not immediately clear you should be able to figure it knowing that the translation copies
51. fg file reportLabels Tells the translator to print the names and locations of all labels it adds Like label it causes the translator to add missing labels debug Runs the translator in debugging mode Currently this does noth ing useful 69 Logic NN SR eee TRUE FALSE BOOLEAN the set TRUE FALSE VreS p Y dreb n Y CHOOSE 1 ES p An z in S satisfying n Sets 4 E UN C set difference e1 En r ES p Set of elements z in S satisfying p Set consisting of elements e le ES Y Set of elements e such that z in S SUBSET S Set of subsets of S UNION Union of all elements of S Functions fle Function application DOMAIN f Domain of function f l l re Sme Function f such that f x e for x S l S gt T Set of functions f with f x T for x S f EXCEPT e1 e2 Function f equal to f except f e1 e2 Records e h The h field of record e hi Si hn Sn Set of all records with h field in S hi gt 1 hn en The record whose h field is e r EXCEPT h el Record 7 equal to r except P h e Tuples efi The it component of tuple e e1 n The n tuple whose h component is es S1Xx x Sn The set of all n tuples with it component in 8 1 S may be replaced by a comma separated list of items v S where v is either a comma separated list or a tuple of identifiers 2 x may be an identifier
52. following a return or any statement other than a return following a call 3 2 7 Skip The statement skip does nothing 3 2 8 Print Execution of the statement print expr is equivalent to skip except it causes TLC to print the current value of expr TLC may print the value even if the step containing the print statement is not executed because of an await statement that appears later in the step An algorithm containing a print statement must be in a module that EXTENDS the TLC module 3 2 9 Assert The statement assert expr is equivalent to skip if expression expr equals TRUE If expr equals false executing the statement causes TLC to produce an error message saying that the assertion failed and giving the location of the assert statement TLC may report a failed assertion even if the step containing the assert statement is not executed because of an await statement that appears later in the step An algorithm containing an assert statement must be in a module that EXTENDS the TLC module 24 3 2 10 Call and Return The call and return statements are described below in Section 3 4 on page 26 3 2 11 Goto Executing the statement goto lab ends the execution of the current step and causes control to go to the state ment labeled lab In any control path a goto must be immediately followed by a label Remember that the control path by definition ignores the mean ing of the goto and continues to what is syntactically t
53. g an expression with bulleted lists of conjuncts or disjuncts Also the translator does not attempt to format the output so the translation is difficult to read This option is mainly of use to peo ple interested in the formal specification of PlusCal However if you suspect that an error is caused by a bug in the translator you might try using this option to see if the error occurs when the translation is performed by the TLA specification Currently there is only a single specification of the translator available called by letting name be PlusCal myspec name Like spec except the translator uses the files names tla and names cfg in the current directory instead of copying them from its own directory writeAST This causes the translator to write the file AST tla as in the spec option but not to perform the translation Options for Command Line Use Only The PlusCal translator can be run outside the Toolbox from a command line It then produces a configuration cfg file that can be used to run TLC from the command line The following options make sense only when the translator is run from a command line 68 unixEOL When you view the files written by the translator in a text editor you may find a M at the end of every line This option will force the translator to use the Unix end of line convention which should remove those Ms help Type a help file instead of doing a translation nocfg Suppress writing of the c
54. guage derived from C such as C C or Java This manual describes the c syntax version A manual for the p syntax version is available from the TLAt tools Web site 1 Introduction PlusCal is an algorithm language An algorithm language is meant for writ ing algorithms not programs Algorithms differ from programs in several ways e Algorithms perform operations on arbitrary mathematical objects such as graphs and vector spaces Programs perform operations on simple objects such as Booleans and integers operations on more com plex data types must be coded using lower level operations such as integer addition and method invocation e A program describes one method of computing a result an algorithm may describe a class of possible computations For example an algo rithm might simply require that a certain operation be performed for all values of i from 1 to N A program specifies in which order those operations are performed e Execution of an algorithm consists of a sequence of steps An algo rithm s computational complexity is the number of steps it takes to compute the result defining a concurrent algorithm requires specify ing what constitutes a single atomic step There is no well defined notion of a step of a program These differences between algorithms and programs are reflected in the fol lowing differences between PlusCal and programming languages e The language of PlusCal expressions is TLAT a high level s
55. hat execution of P calls Q The execution of Q following the last call prints the value of stack and returns The other two procedure executions then return and the algorithm terminates The value of stack is thus printed in an execution of Q inside an execution of P inside an execution of Q Executing the algorithm prints the following value of stack The notation for writing records is explained in Section 5 6 on page 5 6 65 qA gt Mr qui gt 9 qul2 gt 2 pe K LP2 procedure Q pA gt 11 pB gt 12 pu gt 0 pers LQ2 procedure gt P qA gt 13 qui gt 1 qu2 gt 2 pc Done procedure gt Q The value is a sequence of three records one for each procedure being executed The innermost procedure execution produced the first of these records The procedure field shows that the algorithm is executing a call of Q and the pc field shows that this execution will return to the statement labeled LP2 The remaining components show the values of the procedure s parameter qA and its local variables qul and qu2 when the procedure was called The corresponding variables will be restored to those values upon the next return from procedure Q The second record in the sequence stack contains the same information for the call of procedure P Since this was the first call of P in the call stack the parameters pA and pB and the local variable pv contained their initial values 66
56. he next statement It is legal for a goto to jump into the middle of a while or if statement but this sort of trickery should be avoided 3 3 Processes A multiprocess algorithm contains one or more processes A process begins in one of two ways process ProcName IdSet process ProcName Id The first form begins a process set the second an individual process The identifier ProcName is the process or process set s name The elements of the set dSet and the element Id are called process identifiers The process identifiers of different processes in the same algorithm must all be different This means that the semantics of TLA must imply that they are different which intuitively usually means that they must be of the same type For example the semantics of TLAt does not specify whether or not a string may equal a number For execution by TLC this means that all process identifiers must be comparable values as defined on page 264 of the TLA book 3 The name ProcName has no significance changing it does not change the meaning of the process statement in any way The name appears in the TLATt translation and it should be different for different process statements As explained above in Section 2 6 on page 11 the process statement is optionally followed by declarations of local variables The process body is a sequence of statements enclosed by braces Its first statement must be 25 labeled Within the
57. hen so is OF We usually think of OF as asserting that F is eventually true F G asserts of a behavior that if 7 is any suffix of for which F is true then there is a suffix of 7 for which G is true In other words F G asserts that whenever F becomes true G must be true then or at some later point in the execution We usually read gt as leads to Formulas expressing liveness properties are built with these operators and state predicates A state predicate is a formula that is true or false of a state For example the state predicate x gt 0 is true of those states in which the value of x is greater than 0 A state predicate is considered to be the temporal formula that is true of a behavior iff it is true of the first state of If P is a state predicate then OP is true of a behavior iff P is true of the first state of all suffixes of the behavior in other words iff P is true of all states of o Hence the temporal formula OP asserts that P is an invariant of an algorithm The formula OP asserts of a behavior that P is true in some state of o To check that you understand these temporal operators you can verify that e OOF is true of a behavior o iff F is true for infinitely many suffixes of o In particular if P is a state predicate then OOP asserts of o that P is true for infinitely many states of o e OOF is true of a behavior s1 2 iff th
58. her clause or clauses or Clausen where each clause is a possibly compound statement It is executed by nondeterministically choosing any clause that is executable and executing it The either statement can be executed iff at least one of those clauses can be executed If any clause contains a call return or goto statement or a label then the either statement must be followed by a labeled statement The statement if test t_clause else e_clause is equivalent to the following where the await statement is explained in Section 3 2 5 on the next page either await test t clause or await test e_clause T 3 2 4 While The while statement has its usual meaning The statement lb while test body where body is a possibly compound statement is executed like the following if statement where the goto statement is explained in Section 3 2 11 on page 25 lb if test body goto lb A while statement must be labeled However the statement following a while statement need not be labeled even if there is a label in body 22 3 2 5 Await When A step containing the statement await expr can be executed only when the value of the Boolean expression expr is TRUE Although it usually appears at the beginning of a step an await statement can appear anywhere within the step For example the following two pieces of code are equivalent a x yti1 a await y 1 gt 0 await x gt 0 KS y a Lg AA b The ste
59. iers to pro duce a legal TLA specification For example if the PlusCal code declares a variable x and also uses x as a label or if it declares x as a local variable in two different procedures then one of the two x s must be renamed If the translator renames identifiers then it issues a warning and indicates in comments placed right after the BEGIN TRANSLATION line what renam ings have been done 31 Identifiers defined or declared in the translation may not be given new meanings in any TL AT definition that follows the END TRANSLATION line For example if the PlusCal algorithm declares a variable j then a definition that follows the translated algorithm cannot contain the expression Vi j E LN 143 pcli cs A pels es that redeclares the identifier 7 Such a re use of an identifier causes a multiply defined identifier error when the TL AT module is parsed 32 4 Checking the Algorithm Sections 2 3 2 5 above tell you how to use the translator and TLC model checker to check an algorithm This section explains more about the trans lator and TLC Only the commonly used features of TLC are described Consult Chapter 14 of the TLAt book for a more complete description of what TLC can do Also check the document Current Versions of the TLA Tools on the TLA tools web page for recently added features That page can be found from the main TLA web page a link to which is at http lamport
60. in the macro body by the corresponding expression Every instance includes any uses of d as a bound variable as in the expression id 1 N FALSE The substitution of an expression like y 17 for id here will cause a mys terious error when the translation is parsed When using PlusCal obey the TLAt convention of never assigning a new meaning to any identifier that already has a meaning 28 3 6 Definitions An algorithm s expressions can use any operators defined in the TL AT mod ule before the BEGIN TRANSLATION line Since the TLAt declaration of the algorithm s variables follows that line the definitions of those opera tors can t mention any algorithm variables The PlusCal define statement allows you to write TLATt definitions of operators that depend on the algo rithm s global variables For example suppose the algorithm begins algorithm Test variables x 1 N y define zy 2 y x y zx a x y a T The symbol 2 is typed The operators zy and zx can then be used in expressions anywhere in the remainder of the algorithm Observe that there is no semicolon or other separator between the two definitions Section 5 11 on page 55 describes how to write TLAT definitions The variables that may appear within the define statement are the ones declared in the variable statement that immediately precedes it and that follows the algorithm name as well as the variable pc and if there i
61. lusCal If no liveness or termination option is specified the definition of Spec is Spec Init A Ol Next yars Had we used a fair process statement or the wf option to specify weak fairness of the processes actions the definition of Spec would have the ad ditional conjunct V self 1 N WFyars Proc self Had we added after the labels ncs and cs this conjunct would have become V self 1 N WEvars pclself ncs cs A Proc self Adding a after the label 14 would have changed this conjunct to Vself 1 N A WFoars pe self E ncs cs A Proc self A SF vars 14 self If the algorithm had procedures then Proc self would have been defined to be the disjunction only of the atomic actions in the process body For each procedure P called by the process the translation would have defined action P self to be the disjunction of the atomic actions in the body of the procedure and it would have conjoined to Spec the fairness property Vself 1 N WF vars P self Any and label modifiers in the procedure would be handled analogously to the way they are handled in the body of the process Had we specified strong fairness of the process either with a fair process statement or the sf translator option then the translation would have been the same except with WF replaced everywhere by SF and the now redundant conjunct SF yar 14 self eliminated Final
62. lusCal algorithm in Figure 2 is that the angle brackets have been replaced by labels A single step atomic action of a PlusCal algorithm consists of the execution from one label to the next For example the execution of the test y 0 at label 12 is atomic because a single step that begins at 12 ends when control reaches either 13 or 14 In the c syntax any sequence of statements can be enclosed in braces and the label of the first statement can appear either before or after the open ing brace You can therefore enclose atomic actions in braces For example you can write the step beginning at label 17 of algorithm FastMutez as 17 blself FALSE qi pede hs The PlusCal algorithm represents the noncritical and critical sections as atomic skip operations whose execution consists of a single no op step that does nothing The await statement of the original version is repre sented by the PlusCal await statement A step containing a statement await exp can be executed only if the expression exp equals TRUE Think 14 of the processor attempting to execute the entire step The attempt suc ceeds if the await exp statement is executed with exp equal to TRUE In that case the step is actually executed and control advances to the next step If exp equals FALSE then the attempted execution fails and nothing is changed the processor will try to execute the step again later The keyword when is a synonym for await Yo
63. ly the translation defines the temporal formula Termination that asserts the property that the algorithm eventually terminates Tf you are familiar with TLA then you will realize that adding this disjunct does not change the meaning of the specification just the way TLC checks it 64 algorithm Procedures Y procedure P pA 11 pB 12 variables pv 0 L LP1 pv 1 call Q ProcP LP2 return procedure Q qA 13 variables qv1 1 qv2 2 LQ1 if qA Mn qvi 9 call P a b else print stack LQ2 return LM call Q Mn y Figure 4 An algorithm illustrating procedure calls Termination V self ProcSet pc self Done B 2 Procedures The FastMutex algorithm does not show how procedure calls and returns are translated Their translation models a standard implementation using a call stack that is represented by the variable stack For a multiprocess algorithm the value of stack is an array of individual stacks indexed by process identifier You probably don t care exactly how procedure calls and returns are represented in TLAF if you do you can just look at the translation of an algorithm containing them However you may need to understand how to read the value of stack when debugging your algorithm This is explained with the sample algorithm of Figure 4 on this page An execution of the algorithm calls procedure Q The execution of Q calls procedure P and t
64. message null For any error TLC produces an error trace of states reached in the execution up to the point at which the error occurred A state consists of an assignment of values to all the variables TLC shows most values as ordinary TLAT expressions as described in Section 5 However functions are described in terms of the operators and gt that are defined in the TLC module The expression di gt e1 QQ dg gt e QQ QQ dr gt en equals the function f with domain d1 dn such that f d e for each iinl n It can sometimes be quite difficult to figure out the cause of an error from TLC s error message In that case you can debug by inserting print statements in the algorithm You can also use the Print operator in the algorithm s expressions or in the invariants that TLC is checking The op erator Print is defined in the TLC module so Print pval val equals val but TLC prints the value of pval when evaluating it 36 TLC reports the location of an error in the TLA specification and you can usually click on the error message and jump to that location If the location is in the algorithm s translation the Toolbox s Goto PCal Source command will jump to the corresponding part of the PlusCal code 4 5 Invariance Checking The examples in Section 2 explain how to use TLC to check invariance of a formula meaning that the formula is true in all states reached in any execution of the algorithm An i
65. mmand line 5 68 running from Toolbox 8 TRUE 44 tuple 49 type correctness 37 types 5 typing symbols 6 unary minus 43 UNCHANGED TLA operator 61 union U 46 UNION TLAT operator 46 uniprocess algorithm 11 universal quantification 45 unixEOL translator option 69 user definable symbol 71 value Boolean 44 model 35 returned by procedure 27 values comparable 25 variable 59 declared by translation 30 initializing 6 14 26 37 local declaration of 25 multiple assignments to 21 27 30 multiple assignments to not al lowed in with 24 of procedure 26 of process 14 variable PlusCal statement 14 vars defined by translation 31 60 version of PlusCal 1 weak fairness 38 52 web page TLA tools 33 wf translator option 39 64 wfNext translator option 39 when PlusCal statement 15 23 while PlusCal statement 22 may not appear in a with 24 not allowed in macro body 28 with PlusCal statement 15 23 label not permitted in 17 writeAST translator option 68 80
66. mportant example of invariance is type correctness In ordinary typed programming languages type correctness is a syntactic condition Because PlusCal is typeless type correctness is a property of the algorithm asserting that the value of each variable is an element of the proper set For example we say that a variable p has type prime number iff the value of p is always a prime number in other words iff the following formula is an invariant where Nat is the set of natural numbers p ie Nat Wje2 i 1 i j 40 If you don t understand this invariant now you should after reading Sec tion 5 TLC can check if this formula is an invariant Like type checking in ordinary programs checking type correctness is a good way to find simple errors in a PlusCal algorithm For an algorithm to be type correct the initial values of its variables must be of the right type If no initial value is specified for a variable its default initial value is an unspecified constant named defaultInitValue By default the Toolbox s models set it to be a model value see page 35 Since defaultInitValue is unspecified it is not a type correct value for the variable The algorithm will therefore not be type correct unless the variable is properly initialized Among the variables whose type you might want to check are the procedure parameters An algorithm can assign initial values to a procedure s formal parameters as indicated in this example
67. n then replace the print statement in algorithm FuclidAlg by assert v gcd 24 v_ini TLC will print an error message if this statement is executed when v does not equal gcd 24 v_ini For this to work the operator gcd must be defined in the TLA module before the translated algorithm that is before the BEGIN TRANSLATION line You may be able to understand the TLA definition of gcd knowing that e gcd z y is defined to be the largest integer that divides both z and y e An integer p divides an integer q iff if and only if q p equals 0 where q p is the remainder when q is divided by p 10 e The gcd of x and y is at most equal to x or y The standard TLA operators that are used in the definition are briefly explained in Tables 1 and 2 on pages 70 and 71 Here is the definition give it a try gcd x y 2 CHOOSE E 1 2 AT 4 O Ay i 0 AVZE1 2 Azr i 0 Ay j 0 gt 1 gt If you can t understand it now you should be able to after reading Section 5 2 5 Checking Termination To check that algorithm EuclidAlg always terminates we perform the trans lation with the termination option We do this by putting the line PlusCal options termination in the file either in a comment or else before or after the module The can be omitted from an option name when it appears in the options statement This produces the appropriate translation that should ensure termination If we then create a new
68. ne com ments BEGIN TRANSLATION END TRANSLATION If those lines are already present the translator will delete everything be tween them and replace it with the TLAt translation of the algorithm If not the translator will insert the BEGIN END TRANSLATION comment lines immediately after the comment containing the algorithm You can put them elsewhere as you must if the algorithm is outside the module but you shouldn t The module ends with K which is typed as a string of four or more characters You can create the file Euclid tla in your favorite text editor and then open a new specification in the Toolbox with that as its root file How ever you will probably prefer to create the file in the Toolbox as a new specification 2 3 Translating and Executing the Algorithm You run the translator on the Fulcid module with the Translate PlusCal Algorithm command on the Toolbox s File menu or by typing Control T Because this is a uniprocess algorithm that contains no labels the translator will automatically add the necessary labels After translating the algorithm we can execute it by using the New Model command on the Toolbox s TLC Model Checker menu to have it create a new model We must specify the value the model should assign to N We do that in the What is the model section of the model s Model Overview page Let s assign it the ordinary value 3000 Let s now run the TLC model checker on the s
69. o Procedure CompoundStmt fair 1 Process Definitions define Defs 57 Macro macro Name Variable Variable CompoundStmt Procedure procedure Name PVarDecl PVarDecl PVarDecls CompoundStmt Process fair process Name Nin Expr gt VarDecls CompoundStmt VarDecls variable variables VarDecl VarDecl Variable l in Expr PVarDecls variable variables PVarDecl PVarDecl Variable Expr CompoundStmt T Stmt Stmt JA Stmt Label UnlabeledStmt CompoundStmt UnlabeledStmt Assign If While Either With Await Print Assert Skip Return Goto Call MacroCall L Assign LHS Expr LHS Expr I LHS Variable I Expr Ezpr 1 Field If if Expr Stmt else Stmt While while Ezpr Stmt Either either Stmt or Stmt With with Variable Nin Expr 51 Variable Nin Expr Stmt Await await when Expr Print print Expr Assert assert Expr Skip skip 58 Return return Goto goto Label Call call MacroCall MacroCall Name Expr
70. ondition of this action Actions 15 and 16 introduce nothing new and their definitions are omitted here Action 17 shows that the process s local variable j has been turned into an array indexed by self A I7 self A pelself 17 Ab b EXCEPT self FALSE Aj j EXCEPT self 1 A pe pc EXCEPT self 18 A UNCHANGED 2 y Action 8 shows how a while statement whose test is not identically true is translated I8 self A pc self 18 AIF self lt N THEN b j self Aj j EXCEPT self j self 1 A pc pc EXCEPT self 18 ELSE A pc pc EXCEPT self 19 62 A UNCHANGED 7 A UNCHANGED 2 y b Actions 19 cs and 11 are obtained in a similar manner and are omitted Actions 10 and 12 show the translation of an explicit goto and the transfer of control at the end of the while loop 110 self A pc self 110 Ay 0 A pe pc EXCEPT self start N UNCHANGED zx y b j 112 self Apclself 112 A b b EXCEPT self FALSE A pc pc EXCEPT self ncs A UNCHANGED z y J The translation next defines Proc self to be the next state action of process self of process set Proc which is the disjunction of all the atomic actions of the process The name of a process or process set is used only to name the process s next state action A step of the process is one that satisfies formula Proc
71. ongly fair Writing a asserts that action a satisfies no fairness condition Writing fair process process assserts that all actions of the process are strongly fair by default Adding after a label in the process asserts that the action satisfies no fairness condition Adding after a label in a fair process has no effect A process that is not a fair or fair process is called an unfair process and has no fairness assumptions on its actions Adding or after a label in such a process has no effect The following translator options affect fairness assumptions wf Makes any unfair process one not preceded by fair or fair a fair process sf Makes any unfair process one not preceded by fair or fair a fair process nof Makes every process an unfair process In addition to fairness of individual algorithm actions there is also fairness of the entire algorithm This property asserts that the algorithm cannot halt if it has at least one enabled action This property is asserted by beginning the algorithm with fair algorithm or by the wfNext translator option For a uniprocess or sequential algorithm beginning the algorithm with fair algorithm or using the wfNext wf or sf option are equivalent Without another process if control is at a blocking action a that is not enabled then a can never become enabled Weak fairness for a sequential algorithm can also be specified by writing fair or fair before the that
72. org The Toolbox s Help pages also describe many of TLC s features 4 1 Running the Translator Running the translator is simple Section 2 3 on page 8 explains how to doit Section 2 5 on page 11 describes the translator s termination option The other options you are likely to use are ones that specify fairness properties they are described in Section 4 6 on page 38 Appendix Section C on page 67 contains a list of all translator options The one part of using the translator that can be tricky is understanding its messages There are two kinds of translator error messages that can be mysterious The first is one saying that the translator was expecting to find a certain token and didn t For example the missing semicolon at the end of the first line of Li a bte L2 fix c produces the error message Expected but found line column where the line and column numbers indicate the location of the second We might expect the translator to complain when it finds b c followed by L2 since no legal expression can begin b c L2 However the translator does not try to parse expressions It leaves that task to the SANY parser which is called by the Toolbox Instead upon seeing the in the first statement the translator just assumes that everything until the next reserved symbol is part of the assignment statement s expression It discovers that something is wrong when it finds the
73. ot also assign a value to z For a multiprocess algorithm the identifier self in the body of a proce dure equals the process identifier of the process within which the procedure is executing The return statement has no argument A PlusCal procedure does not explicitly return a value A value can be returned by having the procedure set a global variable and having the code immediately following the call read that variable For example in a multiprocess algorithm procedure P might use a global variable rVal to return a value by executing rVal self return From within a process in a process set the code that calls P might look like this call P 17 lab x rVal self For a call from within a single process the code would contain the process s identifier instead of self In any control path a return statement must be immediately followed by a label A call statement must either be followed in the control path by a label or else it must appear immediately before a return statement in a statement sequence When a call P statement is followed immediately by a return the return from procedure P and the return performed by the return statement are both executed as part of a single execution step When these statements are in the recursive procedure P this combining of the two returns is essentially the standard optimization of replacing tail recursion by a loop 27 3 5 Macros A macro is like a procedu
74. p from a to b can be executed only when the current value of y 1 is positive Remember that an entire step must be executed part of a step cannot be executed by itself The keyword when can be used instead of await 3 2 6 With The statement with id S body is executed by executing the possibly compound statement body with iden tifier id equal to a nondeterministically chosen element of S The symbol is typed in Execution is impossible if S is empty This with statement is therefore equivalent to await S 4 1 with id S body The two statements with id expr with id ferpr are equivalent The expression expr equals the set containing a single element equal to expr In general a with statement has the form with id x expr id xezpr body where each may be either or Commas may be used instead of semicolons between the id x expr items This statement is equivalent to with id xexpri with id x expr body 23 The body of a with statement may not contain a label This rule combined with the rules listed in Section 3 7 page 29 for where labels are required implies that the following may not appear within the body of a with state ment e A while statement e Two separate assignment statements that assign values to the same variable A single multiple assignment may assign values to different components of the same variable e Any statement
75. pecifica tion language based on set theory and first order logic 3 TLA is infinitely more expressive than the expression language of any pro gramming language Even the subset of TL AT that can be executed by the TLC model checker is far more expressive than any program ming language e PlusCal provides simple constructs for expressing nondeterminism e PlusCal uses labels to describe the algorithm s steps However you can omit the labels and let the PlusCal translator add them as necessary You are likely to do this only for uniprocess sequential algorithms SETL 4 provides many of the set theoretic primitives of TLAT but it can imple ment higher level operations only by programming them with procedures and it cannot conveniently express nondeterminism where the partitioning of the computation into steps does not affect the values computed For multiprocess concurrent algorithms you will probably want to specify the grain of atomicity explicitly The primary goals of a programming language are efficiency of execution and ease of writing large programs The primary goals of an algorithm language are making algorithms easier to understand and helping to check their correctness Efficiency matters when executing a program that imple ments the algorithm Algorithms are much shorter than programs typically dozens of lines rather than thousands An algorithm language doesn t need complicated concepts like objects or sophis
76. pecification produced by the translation We ll first run it in simulation mode which performs randomly chosen possible executions for this algorithm by randomly choos ing the initial value of N Use the TLC Options section of the Advanced Options model page TLC produces a gush of output like lt lt 24 1005 gt gt lt lt have gcd 3 gt gt lt lt 24 200 gt gt lt lt have gcd 8 gt gt lt lt 24 2717 gt gt lt lt have gcd 1 gt gt lt lt 24 898 gt gt lt lt have gcd 2 gt gt lt lt 24 1809 gt gt that ends only when we stop TLC with the Cancel button on the progress dialog Instead of having TLC randomly generate possible executions we can run it in model checking mode in which it checks all possible executions of the algorithm Go back to the TLC Options section of the Advanced Options page and select Model checking mode To avoid a huge mass of output let s change the model to have it set N to 4 so there are only 4 possible executions of the algorithm Running TLC now produces the following output lt lt 24 1 gt gt lt lt 24 2 gt gt lt lt 24 3 gt gt lt lt 24 4 gt gt lt lt have gcd 4 gt gt lt lt have gcd 3 gt gt lt lt have gcd 2 gt gt lt lt have gcd 1 gt gt 3This large amount of output triggers a Toolbox bug that prevents it from showing the output in the User Output section of the Model Checking Result
77. pressions The expressions in PlusCal algorithms can be any TLAT expressions that do not contain a PlusCal reserved word or symbol such as begin or You can write arbitrary TLAt definitions in the module before the BEGIN TRANSLATION line and use the defined symbols in the algorithm s expres 19 sions Section 5 explains how to write TLA expressions and definitions Table 1 on page 70 and Table 2 on page 71 provide a convenient summary You are probably used to programming languages that allow only simple operators in expressions and allow variables to have only simple values In PlusCal the following statement assigns to x a record whose a component is the set of integers from 1 to N and whose bcd component is the set of all prime numbers less than or equal to N xo la gt 1 N bed gt i 2 N Vje2 Gi 1 i j 0 It may be a while before you learn how to take advantage of PlusCal s powerful expression language TLAT has the general rule that an identifier cannot be assigned a new meaning if it already has a meaning Thus the identifier i cannot be used as a bound variable in an expression like 1 N gt FALSE if it already has a meaning for example if is an algorithm variable As signing a new meaning to a symbol can result in a multiply defined symbol syntax error in the algorithm s TLA translation 3 2 The Statements The examples in Section 2 contain most PlusCal statements
78. r PlusCal algorithm 13 60 field of record 48 file name 7 FiniteSets module 47 formal parameters of a procedure 26 initializing 37 formula temporal 51 function 47 domain of 47 of multiple arguments 48 recursive definition of 55 ecd 6 10 11 Goldbach s conjecture 5 Gonthier Georges 2 goto PlusCal statement 25 not allowed in macro body 28 79 Goto PCal Source Toolbox command 34 37 60 grammar of PlusCal 57 59 greatest common divisor 6 10 11 Head TLA operator 50 Hilbert s e 47 identifier defined by translation 30 process 25 reassigning meaning of 20 28 30 31 renamed by translation 31 if PlusCal statement 21 when label must follow 17 21 30 IF TLAt expression 50 iff if and only if 10 implementing a specification 54 implementing an algorithm 54 implication 44 imported module 7 indentation used to eliminate paren theses 45 infix operator 71 defining 55 Init defined by translation 31 60 initial predicate 31 60 initializing procedure parameter 37 procedure variable 26 variable 6 14 37 Int set of integers 43 integer division 43 Integers module 43 interface refinement 54 intersection N 46 invariant 16 checking 16 37 keywords 59 label 14 59 action corresponding to 31 38 after call statement 27 30 either statement 22 30 if statement 17 21 30 error caused by omitting 34 may not appear in macro body 28
79. r land or lnot or neg E in lt lt lt lt lt leq or lt or lt lt IL lt prec lt preced subseteq C subset C sqsubset E sqsubseteq J gt 5 N cap or intersect m sqcap p or oplus S or ominus or odot e AX or otimes or oslash E NE 3 NEE la Jiu WE WF_v a 3 po cacas 3 1 s is a sequence of characters 2 x and y are any expressions 3 a sequence of four or more or characters L or Mor lt gt or equiv notin gt gt gt geq or gt gg succ succeq supseteq supset sqsupset sqsupseteq lt cup or union sqcup uplus X or times wr propto gn 1 A AA gt gt _v SF SF_v Teo DR iy RAMAS EA 8 e 3 he gt div cdot o or circ bullet star bigcirc sim simeq asymp approx cong doteq xy x 2 xx O XT xO 2 Table 5 The ASCII representations of typeset symbols 72 Index double quote 44 exponentiation 43 PlusCal separator 6 TLA constructor 12 48 set difference 46 Xx end of line comment 6 minus 43 gt negation 44 TLA operator 48 leads to 53 54 integer division 43 plus 43 Cartesian product 50 implies 44 equivalence 44 defined to equal 29 55 integer interval 7 43 multiplication 43 sequ
80. re except that a call of a macro is expanded at translation time You can think of a macro as a procedure that is executed within the step from which it is called A macro definition looks much like a procedure declaration for example macro P s i await s gt i s s i The difference is that the body of the macro may contain no labels no while call return or goto statement It may contain a call of a previ ously defined macro Macro definitions come right after any global variable declarations and define section A macro call is like a procedure call except with the call omitted for example P sem y 17 The translation replaces the macro call with the sequence of statements ob tained from the body of the macro definition by substituting the arguments of the call for the definition s parameters Thus this call of the P macro expands to await sem gt y 17 sem sem y 17 When translating a macro call substitution is syntactic in the sense that the meaning of any symbol in the macro definition other than a parameter is the meaning it has in the context of the call For example if the body of the macro definition contains a symbol q and the macro is called within a with q statement then the q in the macro expansion is the q introduced by the with statement When replacing a macro by its definition the translation replaces every instance of a macro parameter id in an expression with
81. ry value such as 3000 e A model value Making a constant a model value tells TLC to treat it as an uninterpreted symbol that is unequal to any value other than itself e A set of model values For example setting the constant Proc equal to the set p1 p2 p3 of model values tells TLC to let the value of Proc be the set pl p2 p3 where pl p2 and p3 are considered to be model values uninterpreted symbols See the Toolbox help page for more information about model values You can also assign new meanings to defined constants and constant operators for the purpose of model checking For example an algorithm might contain a statement with i Nat where Nat is defined by the standard Naturals module to be the set of all natural numbers TLC cannot check an algorithm that requires it to enu merate an infinite set like Nat However you can use the Definition Override section of the model s Advanced Options page to tell TLC to substitute a finite set of numbers for Nat Definition override can also be used to replace a definition with one that is more easily computed by TLC For example you might replace the definition of gcd on page 11 with an alternative definition that TLC can compute more efficiently You could use gcd in the algorithm because its definition is easy to understand but speed up the checking by having TLC use another definition 35 4 3 Constraints TLC tries to generate all reachable states of the
82. s a pro cedure the variable stack Local process and procedure variables may not appear in the define statement The define statement s definitions need not mention the algorithm s variables You might prefer to put definitions in the define statement even when they don t have to go there However remember that the define statement cannot mention any symbols defined or declared after the END TRANSLATION line and the symbols it defines cannot be used before the BEGIN TRANSLATION line Definitions including ones in a define statement are not expanded in the PlusCal to TLA translation All defined symbols appear in the translation exactly as they appear in the PlusCal code 3 7 Labels Various rules for where labels must or may not appear have been introduced above The complete set of rules are e The first statement in the body of a procedure of a process or of a uniprocess algorithm must be labeled e A while statement must be labeled 29 e A statement S in a statement sequence must be labeled if it is preceded in that sequence by any of the following A call statement if S is not a return A return statement A goto statement An if or either statement that contains a labeled statement a goto a call or a return anywhere within it e A macro body and the do clause of a with statement cannot contain any labeled statements e In any control path a label must come between an assignment
83. s page where it should go You can find the missing output in the TLC Console which you can find with the TLC Model Checker menu TLC has checked the four possible executions producing the eight possible executions of the print statements But it did not perform those execu tions separately Instead TLC found all reachable states using a breadth first search In doing so it performed the four possible first steps before performing any of the four possible last steps If you want sensible output from running TLC in model checking mode you should have the algorithm execute only a single print statement at the end For our example algorithm this requires saving the initial value of v in a separate variable So we modify the algorithm by introducing a new variable v_ini whose initial value is the initial value of v algorithm EuclidAlg 4 variables u 24 v 1 N v_ini v gt while u 0 5 AO ae print lt lt 24 v_ini have gcd v gt gt Translating and running TLC in model checking mode on this algorithm produces the output lt lt 24 4 have gcd 4 gt gt lt lt 24 3 have gcd 3 gt gt lt lt 24 2 have gcd 2 gt gt lt lt 24 1 have gcd 1 gt gt 2 4 Checking the Results We don t have to print the results and examine them by hand to check them We can let TLC do the checking by using an assert statement Suppose we have defined ged z y to be the gcd of x and y We ca
84. s used to eliminate parentheses which can make a complicated formula easier to read The A or V symbols in a bulleted list conjunction or disjunction must line up exactly Universal and existential quantification over sets of values have the fol lowing forms Va E S P x The expression that equals TRUE if P x equals TRUE for all elements x in the set S and equals FALSE if P x equals FALSE for some x in S Thus Yn 1 3 f n gt y is equivalent to CU gt y A CB gt y A CBI gt y Jz S P x The expression that equals TRUE if P x equals TRUE for some z in S and equals FALSE if P x equals FALSE for all x in S Thus 3n 1 3 f n gt y is equivalent to CU gt y v FB gt y v FB gt y 45 In these expressions the bound identifier x may not already be defined or declared and it may not occur in the expression S In the case of S equal to the empty set these definitions become Va P x TRUE Jx P x FALSE for any P TLA allows some obvious abbreviations for nested quantifiers For example VIES yET F means Ve eS Wye T F de yeS F means 11 S 3yES F 5 4 Sets Enumerated finite sets are written in the usual way e1 en being the set containing the elements e1 n For example 1 1 2 2 4 is the set containing the two elements 2 and 4 Remember that an element either is or is not an element of a set it makes no sense to talk about a
85. section and the outer infinite loop made explicit Angle brackets enclose atomic operations steps For example the evaluation of the ex pression y 0 in the first if statement is performed as a single step If that expression equals true the next step of the process sets b i to false The process s next atomic operation is the execution of the await statement which is performed only when y equals 0 The step cannot be performed when y is not equal to 0 The PlusCal version of this algorithm is in Figure 2 on the next page After the algorithm name comes the declaration of the global variables variables x y 0 b i 1 N gt FALSE Here too declarations can be separated by either semicolons or commas and the final semicolon or comma is required The initial value of z doesn t matter and is not specified The declaration of b states that it is initially an array indexed by the set 1 N such that bli equals FALSE for every i in 1 N The symbol gt is typed gt The expression ve S gt vu l equals an array A indexed by the set S such that A v v 1 for every v in S What programmers call an array mathematicians call a function Like 12 algorithm FastMutex variables x y 0 b i 1 N gt FALSE process Proc 1 N variable j E ncs while TRUE 4 start 11 12 15 16 cs 111 112 skip b self The noncritical section TRUE x
86. set containing multiple copies of an element As a special case of this notation is the empty set the set containing no elements TLA provides the following operators on sets membership U union UNION big U C subset N intersection SUBSET power set set difference Here are their definitions ees Equals TRUE if e is an element of the set S and equals FALSE otherwise SOT The set of elements in both S and T SUT The set of elements in S or T or both SCT True iff every element of S is an element of T SASE The set of elements in S that are not in T UNION S The union of the elements of S In other words a value e is an element of UNION iff it is an element of an element of S Mathematicians usually write this as US 46 SUBSET S The set of all subsets of S Mathematicians sometimes call this the power set of S and write it as P S or 2 Mathematicians often describe a set as the set of all such that The following two constructs formalize such a description x S P x The subset of S consisting of all elements z satisfying property P x For example the set of all odd natural numbers can be written n Nat n 2 1 e a x2 S The set of elements of the form e x for all x in the set S For example 2xn 1 n 1 100 is the set 13 5 7 201 In these expressions the bound identifier x may not already be defined or declared and it may not occur in the e
87. tes the two ways comments are writ ten either begun with and ended by the end of the line or enclosed in matching and delimiters Comments can be nested so you can use and to comment out commented code Let s now put this piece of code into a complete algorithm The algo rithm begins algorithm EuclidAlg where we ve given it the name EuclidAlg We next declare the variables u and v and specify their initial values We could omit their initial values and initialize them with assignment statements but it s better to do it this way Just to illustrate the two kinds of initialization we give u the initial value 24 but let the initial value of v be any integer from 1 through some parameter N variables u 24 v 1 N Ax is typed Nin The declaration of v asserts that its initial value is an element of the set 1 N of integers from 1 through N Individual declarations can be sep arated by either semicolons or commas the final semicolon or comma is required in the c syntax We add print statements to print out the initial values of the variables and the final value of v The print statement can print the value of any ar bitrary expression to print multiple values we can either let that expression be a tuple or else use multiple print statements The complete algorithm is as follows where the while loop is the same as above algorithm EuclidAlg variables u 24
88. ticated type systems that were developed for writing large programs It is easy to write a PlusCal algorithm that cannot be executed for example one containing a statement that assigns to x the smallest integer for which Goldbach s conjecture is false if one exists or else the value 0 An unexecutable algorithm can be interesting and may represent a step in the development of a practical algorithm However most PlusCal users will want to execute their algorithms The PlusCal translator compiles a PlusCal algorithm into a TL AT specification If the algorithm manipulates only finite objects in a sensible way then the TLC model checker will probably be able to execute that specification When used in model checking mode TLC will check all possible executions of the algorithm It can also be used in simulation mode to check randomly generated executions The Toolbox You will almost certainly use the PlusCal translator and the TLC model checker with the TLAt Toolbox This manual assumes that s you will be doing However it does not explain in any detail how to use the Toolbox The Toolbox s Help pages explain that See the TLA web site 1 to find out how to obtain the Toolbox The translator and TLC are ordinary Java programs and can be run from a command line See the TLAt Tools page on the TLA web site to find out how to run the translator The TLA book explains how to run TLC 2 Goldbach s conjecture which has not been proved
89. to express this by saying that pc i is not in the set ncs cs 111 112 So the property we want to check is that this condition leads to some process being in its critical section This property is writen as ACG oN pelil ncs cs 11 112 Jicl N peli cs TLC can check this property for three processes N 3 in about a minute The language constructs and translator options described allow you to express all the fairness assumptions about an algorithm that you re likely to need In the unlikely event that you want some other kind of fairness assumption you can write it yourself using the TLA temporal operators described in Section 5 10 on page 51 Liveness checking including termination is slower than invariance check ing and TLC cannot check liveness on as large a model as it can check invariance 4 7 Additional TLC Features 4 7 1 Deadlock Checking An algorithm is deadlocked if it has not terminated but it can take no further step A process has terminated if it has reached the end of its code so control is at the implicit Done label that ends its body The most likely way for a uniprocess algorithm to deadlock is for a procedure call to fall off the end without executing a return statement that is for it to reach the implicit label Error that ends the procedure body A multiprocess algorithm is deadlocked if no process can take a step but
90. u can use await and when interchangeably The original algorithm uses a for loop to test the values of 6 j in in creasing order of 7 The for loop is represented in the PlusCal version by the while loop at label 18 and the assignment statement that precedes it When control in a process is at statement 18 and j lt N then the next step of the process consists of an execution from 18 back to 18 that is a complete execution of the body of the while loop If 7 gt N a step that begins at 18 performs the while test and ends with control at 19 The FastMutex algorithm works if the b j are tested in arbitrary order We can rewrite the algorithm to perform the tests in a nondeterministic order by replacing that PlusCal code with ideal 18 while j 4 1H is the empty set with p j await bpl Xx 7 is logical negation j j p x is set difference If you don t know the meaning of the operator look it up in the index The statement with id S do body sets id to a nondeterministically chosen element of the set S and then exe cutes body In model checking mode TLC will check the algorithm for all possible choices of id Replacing id S with id exp causes the body to be executed with id equal to the current value of exp A multiprocess algorithm can have multiple process sections The statement process Name e begins a single process named Name with identifier e Note that
91. ule 7 43 negation 44 nested comments 6 nested quantifiers 46 Next defined by translation 31 63 next state action of algorithm 31 63 of process 53 noDoneDisjunct translator option 64 67 nof translator option 39 non blocking action 38 nondeterminism in either statement 22 in with statement 23 not expressed with CHOOSE 47 not 44 null TLC error message 36 numbers 43 natural 7 objects 5 operation atomic 52 operator Boolean 44 45 constant 70 infix 71 temporal 71 TLAT 43 54 user definable 71 option statement 11 options translator 67 69 or V 44 or clause of either statement 22 overriding definitions 35 overriding definitions 35 77 p syntax 3 parameter constant 35 declaration of 7 35 of macro 28 of procedure 26 initializing 37 parentheses eliminated by indenta tion 45 path control 19 pc variable 16 30 60 in define statement 29 in expressions 17 value of 16 PlusCal 4 PlusCal expression 19 43 51 grammar 57 59 version 1 power set 46 47 predicate initial 31 60 predicate state 54 print PlusCal statement 7 10 24 debugging with 36 Print TLA operator 36 procedure 26 action defined for 31 call 26 parameter 26 initializing 37 return from 27 returning a value 27 translation of 65 66 procedure PlusCal construct 26 process 25 action defined for 31 body of 25 identifier of 25 individual
92. umbers and a bar field that is an element of the set SUBSET 1 13 of all subsets of the set 1 13 In TL AT a record with fields foo and bar is actually a function whose domain is the set foo bar L The expression exp bar is shorthand for exp bar 48 5 7 The Except Construct TLA provides an EXCEPT construct for describing a function or record that is almost the same as a given function or record You will probably not need to use the EXCEPT construct yourself However it is used extensively in the TLA translation of PlusCal programs so you must know how to interpret it if you want to understand the translation If f is a function then f EXCEPT c exp equals the value of f after executing the PlusCal statement f c exp Thus f EXCEPT c exp is the function g that is the same as f except that g c exp This function can also be written x DOMAIN f gt IF z c THEN exp ELSE f z Similarly if r is a record then r EXCEPT c exp is the record that equals the value of r after executing r c exp In other words it is the record that is the same as r except that its c field equals erp Since a record is a function whose domain is a set of strings r EXCEPT c exp is the 6699 same as r EXCEPT c exp A clause of an EXCEPT construct can be more complicated For example f EXCEPT c d e exp is the value of f after executing the statement f c d e exp
93. variables except that initializations may only have the form variable expression The procedure s local variables are initialized on each entry to the procedure Any variable declarations are followed by the procedure s body which is a sequence of statements enclosed by braces The body must begin with a labeled statement There is an implicit label Error immediately after the body If control ever reaches that point then execution of either the process multiprocess algorithm or the complete algorithm uniprocess algorithm halts A procedure PName can be called by the statement call PName expr exprn 26 Executing this call assigns the current values of the expressions expr to the corresponding parameters param initializes the procedure s local variables and puts control at the beginning of the procedure body A return statement assigns to the parameters and local procedure vari ables their previous values that is the values they had before the procedure was last called and returns control to the point immediately following the call statement The call and return statements are considered to be assignments to the procedure s parameters and local variables In particular they are included in the rule that a variable can be assigned a value by at most one assignment statement in a step For example if x is a local variable of procedure P then a step within the body of P that recursively calls P cann
94. vei N print u v Ax is typed lt lt gt gt while u 0 Linea shore print have gcd v L 2 2 The TLA Module The translated version of the algorithm is put inside a TLAt module The algorithm must go in the same file as the module The module begins MODULE Euclid which is typed as The number of dashes in each doesn t matter as long as there are at least four The module name is arbitrary but a module named Euclid must go in a file named Euclid tla The module next imports two standard TLA modules EXTENDS Naturals TLC The Naturals module defines common operators on natural numbers includ ing subtraction and the operator that appear in the algorithm s expressions The TLC module is needed if the algorithm uses a print state ment The EXTENDS statement must be the first statement in the module Next the module declares the parameter N CONSTANT N Every symbol or identifier that appears in an expression in the algorithm must be either a a built in TLA operator like or b declared or defined in the module or c declared or defined in an imported module The algorithm itself should appear in the module within a single com ment algorithm EuclidAlg It may also be placed before or after the module in file Euclid tla but that s not a good idea The translation is put in the module between the two single li
95. when it terminates label Tells the translator to add missing labels The translator will add the minimum set of labels needed to satisfy the labeling rules given in Section 3 7 on page 29 This is the default for a uniprocess algorithm in which the user has typed no labels labelRoot name If the translator adds missing labels this causes it to use the prefix name for the added labels so the labels will be namel name2 etc The default prefix is Lbl 67 lineWidth The translator tries to perform the translation so lines have this maximum width It will often fail The default value is 78 the minimum value is 60 Options That Can be Specified Using the Spec Explorer spec name This option is used to have the translation performed by ex ecuting a TLA specification instead of by the translator itself It causes the translator to write to the file AST tla in the current direc tory a TLA module that defines ast to equal a TL AT representation of the algorithm s abstract syntax tree AST and fairness to equal the fairness option The current directory is the one from which the translator is run The translator then copies the files name tla and name cfg from its own internal directory to the current directory runs TLC on name tla and uses TLC s output to produce the translation The TLA representation of an algorithm s AST does not capture for matting information so this translation will not work on any algorithm containin
96. xpression S The construct le x x S has the same generalizations as dr S F For example e z y a ES y T is the set of all elements of the form e z y for x in S and y in T The standard module FiniteSets defines Cardinality S to be the cardi nality number of elements in the finite set S The expression CHOOSE x S P x is defined to equal some arbitrarily chosen value z in the set S such that P x equals TRUE If no such g exists then the value of that expression is unspecified and TLC will report an error when evaluating it The CHOOSE operator is known to logicians as Hilbert s e This operator cannot be used to introduce nondeterminism in an algorithm The PlusCal statement n CHOOSE i 1 7 TRUE will assign to n the same value every time it is executed That value is some single unspecified integer in the set 1 7 5 5 Functions What programmers call an array mathematicians call a function Intu itively a function f maps each element d in its domain to the value f d If f is not a function or d is not in the domain of f then the meaning of F d is not specified and TLC will report an error if it tries to evaluate that expression A function is completely specified by its domain and the value of f d for every d in its domain If f is a function then DOMAIN f is its domain The 47 expression x S gt e x equals the function f whose domain is S such that f d e d for ev
97. your expressions pretty much the way you typed them except for the following changes e Some variables are primed e Variables local to a process are turned into functions arrays that take an additional argument For example in algorithm FastMutex of Figure 2 on page 13 each occurrence of the local variable 7 is replaced by j self e An assignment to an element of a function or record variable is rewrit ten as an assignment to the variable using the TLA EXCEPT construct explained in Section 5 7 on page 49 e Variables may be renamed as explained in Section 3 8 on page 30 If the parser complains that an identifier has been multiply defined it may mean that you have redefined or used as a bound variable an identifier that is defined or declared in the algorithm s translation This problem is discussed above in Section 3 8 on page 30 34 Occasionally 1t may be difficult to figure out the cause of a parsing error In that case try inserting a line to prematurely end the module in different places until you find the definition or statement that is causing the error 4 2 Specifying the Constants Most algorithms are written in terms of constant parameters declared in the TLAt module with a CONSTANT statement A model must specify the values of these constants This is done in the What is the model section of the Model Overview page There are three kinds of values you can assign to a constant e An ordina

A PlusCal User`s Manual

Contents

Download Pdf Manuals

Related Search

Related Contents