So far we’ve seen the basics of PlusCal as well as how to run a model. We’ve also seen that if our starting variables are specified as belonging to a set, it expands the state space that TLC can search. This takes us most of the way to writing useful specifications. The last step is to add divergent *behaviors*: allow the system to do different things at a given step. In a single process PlusCal algorithm, there are two simple ways to introduce concurrency: a `with`

statement and an `either`

statement.

`either`

looks a lot like a basic if statement. The syntax is as follows:

```
either
skip;
or
skip;
or
skip;
end either;
```

The important thing is that TLC will run *every* branch. When it encounters an either, it creates a separate behavior and executes a different branch for each one. For example, given:

```
variables x = 3, i = 2;
begin
while i > 0 do
either
x := x + 2;
or
x := x * 2;
end either;
i := i - 1;
end while
```

The inner loop will happen twice. Each time the model can either add two or double x, meaning that there’s four possible end results:

graph TD;
A[3] --> B[5]
A --> C[6]
B --> BB[7]
B --> BC[10]
C --> CB[8]
C --> CC[12]

Will the following code pass or fail?

```
either
assert TRUE;
or
assert FALSE;
end either;
```

Fail, as the second branch can fail. Since a spec only passes if every behavior passes, one behavior failing means the entire spec is broken.

`with`

does the same thing, except instead of creating a new behavior for each possible branch, it creates a behavior for each element in the set. In this case, we have three possible behaviors:

```
with a \in {1, 2, 3} do
x := x + a
end with;
```

This creates a separate timeline for each element in the set.

graph LR;
e["end with"];
with ---x1(x+1);
with ---x2(x+2);
with ---x3(x+3);
x1 --- e; x2 --- e; x3 --- e;

*Specify a system with three flags that can be on or off, as well as can change the state of a flag.*

Right now we’re a little limited in what we can practically do, but we can already start constructing simple patterns. Here’s one way to write this in PlusCal:

```
---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables f1 \in BOOLEAN, f2 \in BOOLEAN, f3 \in BOOLEAN
begin
while TRUE do
with f \in {1, 2, 3} do
if f = 1 then
either
f1 := TRUE;
or
f1 := FALSE;
end either;
elsif f = 2 then
either
f2 := TRUE;
or
f2 := FALSE;
end either;
else
either
f3 := TRUE;
or
f3 := FALSE;
end either;
end if;
end with;
end while;
end algorithm; *)
====
```

This isn’t the most optimal way of writing it, but I wanted to showcase both `with`

and `either`

here. You could probably use just the `either`

. `BOOLEAN`

is a TLA+ builtin and is equal to the set `{TRUE, FALSE}`

. As you can see, every step this picks a single flag and either sets it to true or false. Fairly simple, if cumbersome.

How many possible *behaviors* are there after three loops? Keep in mind that distinct behaviors can have the same end state.

There are 8 initial states. On each loop, the model chooses one of three values and takes one of two actions with it, for a total of 6 paths per loop. So after three loops there are 8*6^3 ~ 1800 behaviors. However, there are only 8 possible current states: most of the behaviors lead to a duplicate outcome.

To give a better sense of where we’re going, here’s how we could write it instead, once we’re more comfortable with the language:

```
---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables flags \in [1..3 -> BOOLEAN], next = TRUE;
begin
while next do
with f \in DOMAIN flags, n \in BOOLEAN do
flags[f] := ~flags[f];
next := n;
end with;
end while;
end algorithm; *)
====
```

The `flags \in [1..3 -> BOOLEAN]`

bit is called a function set. We’ll be covering it later.