Manual

User Manual: Pdf

Open the PDF directly: View PDF .
Page Count: 21

Download
Open PDF In Browser	View PDF

PGo Manual
For commit d0241d3

August 25, 2017

1

Introduction

TLA+ is a formal specification language, built on the mathematical concepts of set theory and the temporal logic of
actions. Using the TLC model checker, TLA+ specifications can be checked exhaustively for specific properties, and
the TLA proof system (TLAPS) allows for machine-checked proofs. PlusCal is an algorithm language which can be
translated to TLA+ and uses TLA+ as its expression language. It is easy to specify and verify distributed algorithms
in PlusCal, thanks to its simple constructs for nondeterminism, concurrency primitives, and rich mathematical
constructs. However, PlusCal is not a programming language so it cannot be run, which limits its utility.
PGo aims to correspond a verified PlusCal specification with an executable Go implementation. PGo compiles
an annotated PlusCal specification into a Go program which preserves the semantics of the specification. The main
goal of PGo is to create a compiled Go program which is easy to read and edit. The intended use case for PGo is
for the developer to create and verify a PlusCal spec of the system, compile it with PGo, then edit the compiled
program to fully implement details not included in the specification. Programs compiled by PGo are type safe (they
do not contain type assertions which panic).

2

Using PGo

2.1

Installation

Requirements: Eclipse or Ant 1.9
• Git clone the source at https://bitbucket.org/whiteoutblackout/pgo/
– Option 1: Import as an Eclipse project
– Option 2: Execute ant pgo assuming the project is in the pgo/ directory
Dependencies:
• The Plume options library.
• The TLA+ tools.
• The Go Data Structures library.
PGo was tested on JRE8 and Go 1.8.3.

2.2

Execution

To run PGo, run the Eclipse project or run pgo.sh.
gofolder gofile.

The command-line usage is pgo [options] pcalfile

1

Optional command line arguments:
-h --help= - Print usage information [default false]
-q --logLvlQuiet= - Reduce printing during execution [default false]
-v --logLvlVerbose= - Print detailed information during execution [default false]
-i --infile= - the input pluscal file to transpile [default ]
-o --outfile= - the output file to generate [default ]
-d --outfolder= - the output folder to put additional packages [default ]
--writeAST= - write the AST generated and skip the rest [default false]

2.3

Annotations

PGo requires annotation of the PlusCal source file to properly compile the PlusCal source. Annotations must be
placed in comments within the body of the PlusCal algorithm, but there can be multiple annotations per comment.
Annotations may appear in any part of the comment block containing the PlusCal algorithm. Annotations are of
the form @PGo{  }@PGo.
2.3.1

Annotating types

Many annotations require specifying a type name. PGo uses the following format for type names:
Primitive types
Go type
Annotation keyword
int
int
bool
bool
uint64
uint64
float64
float64
string
string
(void type)
void
Collection types
[]
[]
set with  elements
set[]
map with  keys and  values
map[]
tuple with all elements of type  chan[]
tuple with i th element of type  tuple[,,...]
Type names cannot contain spaces.
2.3.2

TLA+ definitions and constants declared outside of the algorithm block (Required)

The PlusCal algorithm can make use of TLA+ definitions that are found outside the algorithm block. These are
not parsed by PGo and need to be in an annotation for PGo to parse them. Any TLA+ definitions found in define
blocks also need to be annotated. The annotation for a TLA+ definition is of the form def ()?
? == . The definition can be copied almost verbatim from the TLA+, but a parameter
is specified by   so typing information needs to be added to the parameters. The type that the
expression should evaluate to may also be specified, if desired. A TLA+ definition without parameters is compiled
into a variable, and a definition with parameters is compiled into a function.

2

1
2
3
4
5
6
7
8
9

\* outside the algorithm body
foo(i, j) == i + j
bar == {1, 3, 5}
\* ...
\* inside the algorithm body
(*
@PGo{ def foo(i int, j int) int == i + j}@PGo
@PGo{ def bar = {1, 3, 5} }@PGo
*)

PlusCal
1
2
3
4
5

func foo(i int, j int) int {
return i + j
}
var bar pgoutil.Set = pgoutil.NewSet(1, 3, 5)

Compiled Go
There will be constants in PlusCal that are not declared in the PlusCal algorithm (e.g., constant N for model
checking). These variables will need to be specified using PGo annotations either as constants in the compiled Go
program, or command line arguments to the Go program. Constants are specified as const  
 indicating that varname is a Go constant of type  with initial Go value . Command line argument
variables of Go are specified as arg   ()? indicating that variable  is of
type  and is going to be specified through a command line argument to the Go program. If no 
is specified, then the variable will be a positional argument in the order that it appeared in the annotation. If
 is specified, then the variable will be set on the command line using -=.
If a constant is not a primitive type, it cannot be declared as constant or as a command line argument in Go.
The constant can instead be annotated as a TLA+ definition, where the expression is the desired constant value.
This will be compiled to a global variable that is initialized with the given value. PGo provides a compile-time
guarantee that the constant indeed remains constant (it is not assigned to or mutated).
1
2
3
4
5
6
7
8
9
10

\* outside the algorithm body
CONSTANT N, M, ProcSet
\* ...
\* inside the algorithm body
(*
@PGo{ arg N int }@PGo
@PGo{ arg M int PGoFlag }@PGo
@PGo{ def ProcSet set[string] == {"a", "b", "c"} }@PGo
*)
print << N, M >>;

PlusCal

3

1
2
3
4
5
6
7
8
9
10
11

var ProcSet pgoutil.Set = pgoutil.NewSet("a", "b", "c")
var N int
var M int
func main() {
flag.IntVar(&M, "PGoFlag", 0, "")
flag.Parse()
N, _ = strconv.Atoi(flag.Args()[0])
fmt.Printf("%v %v\n", N, M)
}

Compiled Go
$ go run CompiledGo.go -PGoFlag=1 2
2 1
Command-line usage
2.3.3

PlusCal procedure return values (Optional)

PlusCal has no return values, so procedures can only return values by writing to a global variable. PGo requires
the developer to indicate which variable serves this purpose. In PGo, the annotation is of the form ret .
PGo automatically scans all function definitions for the one where the variable is used. Note that using this feature
will remove the specified variable from the global variables. If you rely on global state of the variable for more than
just the function return value, do not specify it as a return value and use the global variable instead.
2.3.4

Variable types (Optional)

PGo will automatically infer types for variables declared in PlusCal. However, you may want to specify the types
rather than using the inferred types (e.g., you want a variable to be a uint64 rather than an int). This is possible
by specifying var  . Annotations are required for variables that involve PlusCal tuples, since
these may compile to slices or tuples depending on context. If no type annotation is provided for a variable, PGo
will indicate the type it inferred in the output Go code.
2.3.5

Function signatures

Similar to specifying variable types. The annotation func ? () ?+ represents
() having a return type of  if specified, and parameters of type , ...
If any types are specified, all return types or parameters must be specified.
1
2
3
4

\* @PGo{ func foo() int string }@PGo
procedure foo(a, b) {
print << a + 1, b >>;
}

PlusCal
1
2
3

func foo(a int, b string) {
fmt.Println("%v %v\n", a + 1, b)
}

Compiled Go
2.3.6

Locking (Optional)

By default, PGo addds locks when compiling a multiprocess PlusCal algorithm. The locking behaviour is described
in more detail in 3.8. The locking annotation is of the form lock [true|false]. PGo adds or omits locks based
on the annotation, overriding the default behaviour.

4

3

Translation

PlusCal has many language constructs that are translated to Go in a non-trivial way. These constructs and their
translations are described in this section. The pgoutil Go helper library, which contains some useful data structures
and helper methods, is also described.

3.1

Variable declarations

In addition to the simple variable declaration var = , PlusCal supports the declaration var \in . This
asserts that the initial value of var is an element of . This is translated into a loop in which each set element
is assigned to var. This is the same as the behaviour of TLC in model-checking mode, and is the most likely use
case.
1
2
3
4
5
6

variables
S = {1, 3};
v \in S;
{
\* algorithm body...
}

PlusCal
1
2
3
4
5
6
7
8
9
10
11

import "pgoutil"
var S pgoutil.Set = pgoutil.NewSet(1, 3) // PGo inferred type set[int]
var v int // PGo inferred type int
func main() {
for v_interface := range S.Iter() {
v = v_interface.(int)
// algorithm body...
}
}

Compiled Go
(The set methods of the pgoutil package are described in 3.4.1.)
If no type annotation was provided for a variable, PGo prints a comment which contains the type that it inferred.
If the variable needs thread-safe access, then PGo will also print the lock group that the variable belongs to (a
description of locking is in 3.8).

3.2

Variable assignment

PlusCal supports multiple variable assignment statements: the statement x := a || y := b evaluates the righthand sides first, then assigns the values to the left-hand sides. A common use is swapping the variables x and y
with the statement x := y || y := x.
Go has a multiple assignment construct, but a PlusCal assignment might not translate to a Go assignment (for
example, assigning a value to a particular map key translates to the Put method). The right-hand sides are first
evaluated and assigned to temporary variables, then assigned to their corresponding variables.
1

1
2
3
4
5
6

x := y || y := x || mapping[i] := a

PlusCal

x_new := y
y_new := x
mapping_new := a
x = x_new
y = y_new
mapping.Put(i, a)

Compiled Go

5

3.3

Macros

PlusCal macros have the same semantics as C/C++ #define directives. PGo expands the PlusCal macro wherever
it occurs.
1
2
3
4
5
6
7
8

1
2
3
4
5
6
7
8
9

variables p = 1, q = 2;
macro add(a, b) {
a := a + b;
}
{
add(p, q);
print p;
}

import "fmt"
var p int = 1
var q int = 2
func main() {
p = p + q
fmt.Println("%v", p)
}

PlusCal
Compiled Go

3.4

Data types

PlusCal supports maps, sets, and tuples, which are implemented in the pgoutil library.
3.4.1

Sets

PlusCal sets are implemented in Go by the pgoutil.Set type. This container is an ordered, thread-safe set which
has methods equivalent to PlusCal set operations.
1
2
3
4
5
6
7
8

1
2
3
4
5
6
7
8
9
10
11
12
13

variables
A = {1, 2, 3};
B = 3 .. 6; \* the set {3, 4, 5, 6}
C = A \union B;
D = SUBSET C; \* powerset of C
{
print A = C;
}

import (
"fmt"
"pgoutil"
)
var
var
var
var

A
B
C
D

pgoutil.Set
pgoutil.Set
pgoutil.Set
pgoutil.Set

=
=
=
=

pgoutil.NewSet(1, 2, 3)
pgoutil.Sequence(3, 6)
A.Union(B)
C.PowerSet()

func main() {
fmt.Printf("%v\n", A.Equal(C))
}

PlusCal also supports the typical mathematical set constructor notations, which are offloaded to library methods:
1
2
3
4
5
6

variables
S = {1, 5, 6};
T = {2, 3};
U = {x \in S : x > 3}; \* equivalent to {5, 6}
V = {x + y : x \in S, y \in T}; \* equivalent to {3, 4, 7, 8, 9}
\* ...

PlusCal

6

1
2
3
4
5
6
7
8
9
10
11

import "pgoutil"
var S pgoutil.Set =
var T pgoutil.Set =
var U pgoutil.Set =
return x > 3
}, S)
var V pgoutil.Set =
return x + y
}, S, T)
// ...

pgoutil.NewSet(1, 5, 6)
pgoutil.NewSet(2, 3)
pgoutil.SetConstructor(func(x int) bool {

pgoutil.SetImage(func(x int, y int) int {

Compiled Go
While not as concise as the PlusCal, the output Go code is still readable.
The Cartesian product operator \X in PlusCal is not associative. For example,
• <<1, 2, 3>> is in Nat \X Nat \X Nat,
• << <<1, 2>>, 3>> is in (Nat \X Nat) \X Nat, and
• <<1, <<2, 3>> >> is in Nat \X (Nat \X Nat),
and none of these are equivalent.
In Go, S.CartesianProduct(T, U, V, ...)
is equivalent to
S \X T \X U \X .... PGo composes these function calls to create the parenthesized expressions above.
1
2
3
4

variables
S = {1, 2, 3};
T = S \X S \X S; \* << 1, 3, 2 >> \in T
U = S \X (S \X S); \* << 1, << 3, 2 >> >> \in U

PlusCal
1
2
3
4
5

import "pgoutil"
var S pgoutil.Set = pgoutil.NewSet(1, 2, 3)
var T pgoutil.Set = S.CartesianProduct(S, S)
var U pgoutil.Set = S.CartesianProduct(S.CartesianProduct(S))

Compiled Go
3.4.2

Maps

PlusCal “functions” are just maps in Go. pgoutil implements an ordered, thread-safe map in Go, which supports
using slices and tuples as keys (unlike the builtin Go map). There are several syntaxes to declare maps, which are
handled by library methods similar to the set methods.
A PlusCal function can be indexed by multiple indices. This is syntactic sugar for a map indexed by a tuple whose
components are the indices.
1
2
3
4

variables
S = {1, 2};
f = [x \in S, y \in S |-> x + y];
a = f[2, 2]; \* a = 4

PlusCal

7

1
2
3
4
5
6
7

import "pgoutil"
var S pgoutil.Set = pgoutil.NewSet(1, 2)
var f pgoutil.Map = pgoutil.MapsTo(func(x int, y int) int {
return x + y
}, S, S)
var a int = f.Get(pgoutil.NewTuple(2, 2))

Compiled Go
(Behind the scenes, the pgoutil.Map uses tuples as keys.)
3.4.3

Tuples

PlusCal tuples are used in several different contexts, so variables involving tuples must be annotated with their
types. Tuples can store homogeneous data, in which case they correspond to Go slices. Tuple components may be
of different types, which correspond to pgoutil.Tuples. Most often in multiprocess algorithms, tuples are used for
communication, in which case pgoutil.Tuples are used. PlusCal tuples are 1-indexed, but Go tuples and slices
are 0-indexed, so 1 is subtracted from all indices in Go.
1
2
3
4
5
6
7
8

(* @PGo{ var slice []string }@PGo
@PGo{ var tup tuple[int,string] }@PGo *)
variables
slice = << "a", "b", "c" >>;
tup = << 1, "a" >>;
{
print slice[2]; \* "b"
}

PlusCal
1
2
3
4
5
6
7
8
9
10
11

import (
"fmt"
"pgoutil"
)
var slice []string = []string{"a", "b", "c"}
var tup pgoutil.Tuple = pgoutil.NewTuple(1, "a")
func main() {
fmt.Printf("%v", slice[2 - 1])
}

Compiled Go

3.5

Predicate operations

PlusCal supports the mathematical quantifiers ∀ and ∃. PGo compiles these to the library methods ForAll and
Exists.
1
2
3
4
5

variables
S = {1,
T = {4,
b1 = \E
b2 = \A

2, 3};
5, 6};
x \in S : x > 2 \* TRUE
x \in S, y \in T : x + y > 6 \* FALSE

PlusCal

8

1
2
3
4
5
6
7
8
9
10

import "pgoutil"
var S pgoutil.Set = pgoutil.NewSet(1, 2,
var T pgoutil.Set = pgoutil.NewSet(4, 5,
var b1 bool = pgoutil.Exists(func(x int)
return x > 2
}, S)
var b2 bool = pgoutil.ForAll(func(x int,
return x + y > 6
}, S, T)

3)
6)
bool {

y int) bool {

Compiled Go
Related is Hilbert’s ε operator (called CHOOSE in PlusCal). In PlusCal, CHOOSE x \in S : P(x) is defined to be
some arbitrary value in S such that P(x) is true. If there is no such x, the expression is unspecified. Furthermore,
CHOOSE is deterministic and always selects the same x given equal sets and equivalent predicates. The Go equivalent
function pgoutil.Choose selects the least element that satisfies the predicate. This guarantees the determinism that
the operator provides, and is the same as TLC’s behaviour. If no element satisfies the predicate P, pgoutil.Choose
panics, similar to TLC returning an error when it encounters unspecified behaviour.
1
2
3
4

variables
S = {1, 2, 3};
a = CHOOSE x \in S : x >= 1
b = CHOOSE y \in S : y < 0 \* TLC error

1
2
3
4
5
6
7
8
9

import "pgoutil"

PlusCal

var S pgoutil.Set = pgoutil.NewSet(1, 2, 3)
var a int = pgoutil.Choose(func(x int) bool {
return x >= 1
}, S).(int) // a == 1
var b int = pgoutil.Choose(func(y int) bool {
return y < 0
}, S).(int) // panic (no element satisfies predicate)

Compiled Go

3.6

With

The PlusCal with statement has the syntax
1
2
3
4
5
6

variables S_1 = {1, 2, 3}, a = "foo";
\* ...
with (x_1 \in S_1, x_2 = a, ...)
{
\* do stuff with the x_i ...
}

PlusCal
This construct selects a random element from each S i and assigns them to the local variables x i. If the syntax
x i = a is used, this simply assigns a to x i. In Go, this translates to

9

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

import (
"math/rand"
"pgoutil"
"time"
)
var S_1 pgoutil.Set = pgoutil.NewSet(1, 2, 3)
var a string = "foo"
// ...
func main() {
rand.Seed(time.Now().UnixNano())
// ...
{
var x_1 int = S_1.ToSlice()[rand.Intn(S_1.Size())].(int)
var x_2 string = a
// ...
// do stuff with the x_i ...
}
}

Compiled Go
In Go the random number generator is seeded with the current Unix time at the beginning of the main function.
The local variables declared by the with and its body are contained in a separate code block, to preserve the
variables’ local scope.

3.7

Processes

The PlusCal algorithm body can either contain statements in a uniprocess algorithm, or process declarations in a multiprocess algorithm. Processes can be declared with the syntax process (Name \in S) or
process (Name = Id). The first construct spawns a set of processes, one for each ID in the set S, and the
second spawns a single process with ID Id. A process can refer to its identifier with the keyword self. In TLC,
multiprocess algorithms are simulated by repeatedly selecting a random process then advancing it one atomic step
(if it does not block).
PGo converts each process body to a function and spawns a goroutine per process. The function takes a single
parameter self, the process ID. There are two semantic considerations: the main goroutine should not exit before
all goroutines finish executing, and the time at which all child goroutines begin executing should be synchronized.
To preserve these semantics, PGo uses a global waitgroup which waits on all goroutines, and each process body
pulls from a dummy channel before beginning execution. When all goroutines have been initialized, the dummy
channel is closed so that the channel pull no longer blocks, allowing for a synchronized start.
The following is a simple example:
1
2
3
4
5
6
7
8
9
10
11
12
13

variables
idSet = {1, 2, 3};
id = "id";
process (PName \in idSet)
variable local;
{
local := self;
}
process (Other = id) {
print self;
}

PlusCal

10

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

import (
"fmt"
"pgoutil"
"sync"
)
var
var
var
var

idSet pgoutil.Set = pgoutil.NewSet(1, 2, 3) // PGo inferred type set[int]
id string = "id" // PGo inferred type string
PGoWait sync.WaitGroup
PGoStart chan bool = make(chan bool)

func PName(self int) {
var local int // PGo inferred type int
defer PGoWait.Done()
<-PGoStart
local = self
}
func Other(self string) {
defer PGoWait.Done()
<-PGoStart
fmt.Printf("%v\n", self)
}
func main() {
// spawn goroutines for PName processes
for procId := range idSet.Iter() {
PGoWait.Add(1)
go PName(procId.(int))
}
PGoWait.Add(1)
close(PGoStart)
PGoWait.Wait()
}

Compiled Go
Note that all processes use the same waitgroup (PGoWait) and dummy channel (PGoStart).

3.8

Labels

In PlusCal, labels are used as targets for goto statements and also to specify atomic operations. If a statement is
labeled, all statements until the next label are considered to be a single atomic operation. In Go, unused labels
cause compile errors so PGo only inserts labels when they are used in goto statements.
To deal with atomicity, PGo divides the global variables into groups and guards each group with a sync.RWMutex.
PGo groups variables by performing a disjoint-set union, merging two variable sets when two variables in them can
be accessed in the same label. The following is a simple example:
1
2
3
4
5
6
7
8

variables a = 0, b = 1, c = 2, d = 3;
process (P \in {1, 2, 3}) {
lab1: a := 1;
b := 2;
lab2: b := 3;
c := 4;
lab3: d := 5;
}

PlusCal

11

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

var
var
var
var
var
var
var

PGoLock []sync.RWMutex = make([]sync.RWMutex, 2)
a int = 0 // PGo inferred type int; Lock group 0
b int = 1 // PGo inferred type int; Lock group 0
c int = 2 // PGo inferred type int; Lock group 0
d int = 3 // PGo inferred type int; Lock group 1
PGoWait sync.WaitGroup
PGoStart chan bool = make(chan bool)

func P(self int) {
defer PGoWait.Done()
<-PGoStart
PGoLock[0].Lock()
a = 1
b = 2
PGoLock[0].Unlock()
PGoLock[0].Lock()
b = 3
c = 4
PGoLock[0].Unlock()
PGoLock[1].Lock()
d = 5
PGoLock[1].Unlock()
}
// ...

Compiled Go
The variable b may be accessed atomically with a (in the label lab1) and also with c (in the label lab2) so all
three of a, b, and c must be grouped together to prevent data races. PGo locks the correct group before each
atomic operation and unlocks it afterwards. Even single operations must use the lock, since there are no atomicity
guarantees for most Go statements. If the atomic operations are specified to be smaller in PlusCal by adding more
labels, PGo will compile smaller variable groups, allowing for more parallelism.
Locking may be turned off with the annotation lock false, and it can similarly be enforced using the annotation
lock true.

3.9

Limitations

Not all PlusCal specifications can be compiled by PGo. This is an overview of some important PlusCal features
that are currently unsupported.
• The await keyword
• The either construct
• Referencing self in a procedure call
• TLA+ features:
– Alignment of boolean operators in bulleted lists determining precedence
– Records (structs)
– Bags (multisets)
– IF ...

THEN ...

– The LET ..

ELSE and CASE expressions

IN construct

– Temporal logic operators
– Recursive definitions
– Operator definition (use definitions with parameters instead)

12

The following are features that may be desirable for a developer working with the compiled program but are not
yet considered by PGo:
• Support for networking
• Interfacing with other programs
• Reading input from sources other than the command line

4

Notes on the Go library

The pgoutil Go package provides some useful data structures and methods that correspond to PlusCal language
features. The data structures are generic and provide no runtime type safety. PGo guarantees at compile-time
that the compiled code does not contain any type assertions that will panic. This section contains some useful
information about these containers for developers wishing to modify and optimize the compiled Go code.

4.1

Maps

The Go library map is mutable, but the PlusCal map is not. An assignment to a component of a PlusCal map does
not change the value of other references to that map:
1
2
3
4
5
6
7
8
9

variables
S = {1, 2, 3};
M = [x \in S |-> 2 * x];
T = {M};
{
print M \in T; \* TRUE
M[2] := 3;
print M \in T; \* FALSE
}

The pgoutil.Map clones any map that is to be inserted into a map or a set. This preserves semantics but may
unnecessarily slow the program, if the map is never mutated. Similarly, since slices are mutable but PlusCal tuples
are immutable, slices are cloned before being used as map keys or values.
The Go map provides three iterators: Keys and Values range over the keys and values stored in the map ordered
by keys, and Iter ranges over KVPairs, which are structs with two fields: Key and Val.
If a PlusCal map is indexed by multiple indices, the Go map internally uses a Tuple of the indices as its key. The
value M[a, b] in PlusCal can be recovered in Go by calling M.Get(pgoutil.NewTuple(a, b)).
The pgoutil.MapsTo method makes extensive use of reflection. Performance-critical sections of the application
should be rewritten to avoid the use of this method. The pgoutil.Map’s comparator function also uses reflection,
which may slow the program especially when using slices or structs as map keys.
The pgoutil package exposes a Map interface. A custom data type which implements pgoutil.Map is interoperable
with the builtin type.

4.2

Sets and predicates

The pgoutil.Set is implemented using the pgoutil.Map as a base, so much of the same semantics apply.
The sets in the Go set library are mutable, whereas TLA+ sets are immutable. However, all operations equivalent
to TLA+ set operations are implemented as methods which do not mutate the Go set. For performance purposes,
sets are not cloned when inserted into a map or a set. The developer modifying the compiled Go program should
exercise caution when making sets of sets or maps with sets if mutating the sets that are inserted. The sets should
be copied with the Clone method before insertion.
Simple optimizations that can be made by the developer when dealing with sets include replacing the PlusCal
S := S \union {elt} with simply adding elt to S and similarly replacing S := S \ {elt} with removing elt
from S. Since this mutates the set, the set must be cloned if it is inserted into a set or used with a map.
Elements inserted into a set must be of the same type; otherwise, the program will panic at runtime. This is the
same behaviour as TLC, which throws an error when one set contains elements of different types. At compile-time,
PGo will throw an error if elements in a set are not of the same type.

13

The SetConstructor and SetImage methods, along with the quantifiers ForAll and Exists and the Choose
method, make use of the reflect package. This drastically improves the readability of the compiled Go program,
but it also incurs a significant performance penalty. Performance-critical sections of the application should be
rewritten to avoid use of these methods.
Since slices are mutable, but PlusCal tuples are immutable, slices are cloned before insertion into a set.
The pgoutil library exposes a Set interface. The developer modifying the Go code may wish to write a custom
set container (say, which is specialized for a specific data type). If this container implements the pgoutil.Set
interface, it is interoperable with the builtin set.

4.3

Tuples

The pgoutil.Tuple implements an immutable tuple type which holds elements of arbitrary type, backed by a slice.
The At and Set tuple methods panic if the index accessed is out of range. The Set and Append tuple methods
create a copy of the tuple, to preserve immutability. (However, the Head and Tail methods do not.)
The pgoutil library exposes a Tuple interface. Any custom container implementing this interface is not interoperable with the builtin tuple.

5
5.1

Example programs
Euclidean algorithm

The Euclidean algorithm is a simple algorithm that computes the greatest common divisor of two integers, and is
a good example PlusCal algorithm.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

------------------------ MODULE Euclid ---------------------------EXTENDS Naturals, TLC
CONSTANT N
(*
--algorithm Euclid {
(* @PGo{ arg N int }@PGo *)
variables u = 24;
v \in 1 .. N;
v_init = v;
{
a: while (u # 0) {
if (u < v) {
u := v || v := u;
};
b: u := u - v;
};
print <<24, v_init, "have gcd", v>>
}
}
*)
===================================================================

PlusCal
1
2
3
4
5
6
7
8
9
10
11

package main
import (
"flag"
"fmt"
"pgoutil"
"strconv"
)
var v int // PGo inferred type int
var u int // PGo inferred type int

14

12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

var v_init int // PGo inferred type int
var N int

func main() {
flag.Parse()
N, _ = strconv.Atoi(flag.Args()[0])
for v_interface := range pgoutil.Sequence(1, N).Iter() {
v = v_interface.(int)
u = 24
v_init = v
for u != 0 {
if u < v {
u_new := v
v_new := u
u = u_new
v = v_new
}
u = u - v
}
fmt.Printf("%v %v %v %v\n", 24, v_init, "have gcd", v)
}
}

Compiled Go
The constant N needs to be annotated since its declaration does not appear in the comment containing the algorithm.
Note the code to swap u and v in lines 26-29 of the Go program.

5.2

N-Queens problem

This PlusCal algorithm computes all possible ways to place n queens on an n × n chessboard such that no two
queens attack each other. It demonstrates the expressive power of PlusCal’s set constructs, as the algorithm is very
concise.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

-------------------------- MODULE QueensPluscal ----------------------------EXTENDS Naturals, Sequences
(***************************************************************************)
(* Formulation of the N-queens problem and an iterative algorithm to solve *)
(* the problem in TLA+. Since there must be exactly one queen in every row *)
(* we represent placements of queens as functions of the form *)
(* queens \in [ 1..N -> 1..N ] *)
(* where queens[i] gives the column of the queen in row i. Note that such *)
(* a function is just a sequence of length N. *)
(* We will also consider partial solutions, also represented as sequences *)
(* of length \leq N. *)
(***************************************************************************)
CONSTANT N \** number of queens and size of the board
ASSUME N \in Nat \ {0}
(* The following predicate determines if queens i and j attack each other
in a placement of queens (represented by a sequence as above). *)
Attacks(queens,i,j) ==
\/ queens[i] = queens[j] \** same column
\/ queens[i] - queens[j] = i - j \** first diagonal
\/ queens[j] - queens[i] = i - j \** second diagonal
(* A placement represents a (partial) solution if no two different queens
attack each other in it. *)
IsSolution(queens) ==

15

27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

\A i \in 1 .. Len(queens)-1 : \A j \in i+1 .. Len(queens) :
~ Attacks(queens,i,j)
(***************************************************************************)
(* We now describe an algorithm that iteratively computes the set of *)
(* solutions of the N-queens problem by successively placing queens. *)
(* The current state of the algorithm is given by two variables: *)
(* - todo contains a set of partial solutions, *)
(* - sols contains the set of full solutions found so far. *)
(* At every step, the algorithm picks some partial solution and computes *)
(* all possible extensions by the next queen. If N queens have been placed *)
(* these extensions are in fact full solutions, otherwise they are added *)
(* to the set todo. *)
(***************************************************************************)
(* --algorithm QueensPluscal
(** @PGo{ arg N int }@PGo
@PGo{ var todo set[[]int] }@PGo
@PGo{ var sols set[[]int] }@PGo
@PGo{ def Attacks(queens []int,i int,j int) ==
\/ queens[i] = queens[j] \** same column
\/ queens[i] - queens[j] = i - j \** first diagonal
\/ queens[j] - queens[i] = i - j \** second diagonal }@PGo
@PGo{ def IsSolution(queens []int) ==
\A i \in 1 .. Len(queens)-1 : \A j \in i+1 .. Len(queens) :
~ Attacks(queens,i,j) }@PGo **)
variables
todo = { << >> };
sols = {};
begin
nxtQ: while todo # {}
do
with queens \in todo,
nxtQ = Len(queens) + 1,
cols = { c \in 1..N : ~ \E i \in 1 .. Len(queens) :
Attacks( Append(queens, c), i, nxtQ ) },
exts = { Append(queens,c) : c \in cols }
do
if (nxtQ = N)
then todo := todo \ {queens}; sols := sols \union exts;
else todo := (todo \ {queens}) \union exts;
end if;
end with;
end while;
end algorithm
*)
=============================================================================

PlusCal
1
2
3
4
5
6
7
8
9
10

package main
import (
"flag"
"math/rand"
"pgoutil"
"strconv"
"time"
)

16

11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

var todo pgoutil.Set = pgoutil.NewSet([]int{})
var sols pgoutil.Set = pgoutil.NewSet()
var N int
func Attacks(queens []int, i int, j int) bool {
return queens[i - 1] == queens[j - 1]
|| queens[i - 1] - queens[j - 1] == i - j
|| queens[j - 1] - queens[i - 1] == i - j
}
func IsSolution(queens []int) bool {
return pgoutil.ForAll(func(i int) bool {
return pgoutil.ForAll(func(j int) bool {
return !Attacks(queens, i, j)
}, pgoutil.Sequence(i + 1, len(queens)))
}, pgoutil.Sequence(1, len(queens) - 1))
}
func main() {
rand.Seed(time.Now().UnixNano())
flag.Parse()
N, _ = strconv.Atoi(flag.Args()[0])
for !pgoutil.NewSet().Equal(todo) {
{
var queens []int // PGo inferred type []int
= todo.ToSlice()[rand.Intn(todo.Size())].([]int)
var nxtQ int = len(queens) + 1 // PGo inferred type int
var cols pgoutil.Set // PGo inferred type set[int]
= pgoutil.SetConstructor(pgoutil.Sequence(1, N), func(c int) bool {
return !pgoutil.Exists(func(i int) bool {
return Attacks(append(queens, c), i, nxtQ)
}, pgoutil.Sequence(1, len(queens)))
})
var exts pgoutil.Set // PGo inferred type set[[]int]
= pgoutil.SetImage(func(c int) []int {
return append(queens, c)
}, cols)
if (nxtQ == N) {
todo = todo.Difference(pgoutil.NewSet(queens))
sols = exts.Union(sols)
} else {
todo = exts.Union((todo.Difference(pgoutil.NewSet(queens))))
}
}
}
}

Compiled Go
(Some lines were broken in order to fit on the page.)
Note that the variables cols and exts do not require a type annotation, though they involve PlusCal tuples, since
PGo can infer their type based on the type of todo.

5.3

Dijkstra’s mutex algorithm

This is a multiprocess algorithm which only allows one process to be in the critical section at one time.
1
2
3
4
5

--------------------------- MODULE DijkstraMutex --------------------------EXTENDS Integers
(***************************************************************************)
(* There is no reason why the processes need to be numbered from 1 to N. *)
(* So, we assume an arbitrary set Proc of process names. *)

17

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

(***************************************************************************)
CONSTANT Proc
(*********
Here is the PlusCal version of this algorithm.
The algorithm was modified from the original by adding the variable temp2,
to avoid a type consistency conflict when temp changes type at Li4a.
(* @PGo{ def Proc == 1 .. 10 }@PGo
@PGo{ lock false }@PGo
*)
--algorithm Mutex
{ variables b = [i \in Proc |-> TRUE], c = [i \in Proc |-> TRUE], k \in Proc;
process (P \in Proc)
variable temp, temp2 ;
{ Li0: while (TRUE)
{ b[self] := FALSE;
Li1: if (k # self) { Li2: c[self] := TRUE;
Li3a: temp := k;
Li3b: if (b[temp]) { Li3c: k := self } ;
Li3d: goto Li1
};
Li4a: c[self] := FALSE;
temp2 := Proc \ {self};
Li4b: while (temp2 # {})
{ with (j \in temp2)
{ temp2 := temp2 \ {j};
if (~c[j]) { goto Li1 }
}
};
cs: skip; \* the critical section
Li5: c[self] := TRUE;
Li6: b[self] := TRUE;
ncs: skip \* non-critical section ("remainder of cycle")
}
}
}
*********)
=============================================================================

PlusCal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

package main
import (
"math/rand"
"pgoutil"
"sync"
"time"
)
var
var
var
var
var
var

Proc pgoutil.Set = pgoutil.Sequence(1, 10)
k int // PGo inferred type int
b pgoutil.Map // PGo inferred type map[int]bool
c pgoutil.Map // PGo inferred type map[int]bool
PGoWait sync.WaitGroup
PGoStart chan bool = make(chan bool)

func P(self int) {
var temp int // PGo inferred type int
var temp2 pgoutil.Set // PGo inferred type set[int]

18

20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

defer PGoWait.Done()
<-PGoStart
for true {
b.Put(self, false)
Li1:
if k != self {
c.Put(self, true)
temp = k
if b.Get(temp).(bool) {
k = self
}
goto Li1
}
c.Put(self, false)
temp2 = Proc.Difference(pgoutil.NewSet(self))
for !pgoutil.NewSet().Equal(temp2) {
{
var j int = temp2.ToSlice()[rand.Intn(temp2.Size())].(int) // PGo inferred type int
temp2 = temp2.Difference(pgoutil.NewSet(j))
if !c.Get(j).(bool) {
goto Li1
}
}
}
// TODO skipped from pluscal
c.Put(self, true)
b.Put(self, true)
// TODO skipped from pluscal
}
}
func main() {
rand.Seed(time.Now().UnixNano())
for k_interface := range Proc.Iter() {
k = k_interface.(int)
b = pgoutil.MapsTo(func(i int) bool {
return true
}, Proc)
c = pgoutil.MapsTo(func(i int) bool {
return true
}, Proc)
for procId := range Proc.Iter() {
PGoWait.Add(1)
go P(procId.(int))
}
close(PGoStart)
PGoWait.Wait()
}
}

Compiled Go
The Go statements used in compilation are atomic on a usual configuration, so locking is turned off.
pgoutil.Map and pgoutil.Set operations are atomic.)
For reference, here is the compiled code when locking is turned on:
1
2
3
4
5
6

package main
import (
"math/rand"
"pgoutil"
"sync"

19

(All

7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68

"time"
)
var
var
var
var
var
var
var

PGoLock []sync.RWMutex = make([]sync.RWMutex, 3)
Proc pgoutil.Set = pgoutil.Sequence(1, 10)
k int // PGo inferred type int; Lock group 2
b pgoutil.Map // PGo inferred type map[int]bool; Lock group 0
c pgoutil.Map // PGo inferred type map[int]bool; Lock group 1
PGoWait sync.WaitGroup
PGoStart chan bool = make(chan bool)

func P(self int) {
var temp int // PGo inferred type int
var temp2 pgoutil.Set // PGo inferred type set[int]
defer PGoWait.Done()
<-PGoStart
for true {
PGoLock[0].Lock()
b.Put(self, false)
PGoLock[0].Unlock()
Li1:
if k != self {
PGoLock[1].Lock()
c.Put(self, true)
PGoLock[1].Unlock()
temp = k
if b.Get(temp).(bool) {
PGoLock[2].Lock()
k = self
PGoLock[2].Unlock()
}
goto Li1
}
PGoLock[1].Lock()
c.Put(self, false)
temp2 = Proc.Difference(pgoutil.NewSet(self))
PGoLock[1].Unlock()
for !pgoutil.NewSet().Equal(temp2) {
{
var j int = temp2.ToSlice()[rand.Intn(temp2.Size())].(int) // PGo inferred type int
temp2 = temp2.Difference(pgoutil.NewSet(j))
if !c.Get(j).(bool) {
goto Li1
}
}
}
// TODO skipped from pluscal
PGoLock[1].Lock()
c.Put(self, true)
PGoLock[1].Unlock()
PGoLock[0].Lock()
b.Put(self, true)
PGoLock[0].Unlock()
// TODO skipped from pluscal
}
}
func main() {
rand.Seed(time.Now().UnixNano())
for k_interface := range Proc.Iter() {
k = k_interface.(int)
b = pgoutil.MapsTo(func(i int) bool {

20

69
70
71
72
73
74
75
76
77
78
79
80
81

return true
}, Proc)
c = pgoutil.MapsTo(func(i int) bool {
return true
}, Proc)
for procId := range Proc.Iter() {
PGoWait.Add(1)
go P(procId.(int))
}
close(PGoStart)
PGoWait.Wait()
}
}

Compiled Go with locks
Note that the loop at line 44 does not require any locking, since it only involves local variables.
The constant Proc is defined to be 1 .. 10 in the annotation. If the process set needs to be changed, only the
annotation needs to be edited.

21



---

Source Exif Data:

File Type                       : PDF
File Type Extension             : pdf
MIME Type                       : application/pdf
PDF Version                     : 1.5
Linearized                      : No
Page Count                      : 21
Page Mode                       : UseOutlines
Author                          : 
Title                           : 
Subject                         : 
Creator                         : LaTeX with hyperref package
Producer                        : pdfTeX-1.40.18
Create Date                     : 2017:08:25 16:08:22-07:00
Modify Date                     : 2017:08:25 16:08:22-07:00
Trapped                         : False
PTEX Fullbanner                 : This is MiKTeX-pdfTeX 2.9.6354 (1.40.18)

EXIF Metadata provided by EXIF.tools