TLA is a logic for describing systems that go from state to state.

You can write properties about states
x = 3

You can write how a system moves from one state to another - transitions - actions x' = x+1

You can use temporal operators
[] (always), <> (eventually), ~> (leads-to), O (next) * actually, not this one... [] x<4
x=2 ~> x=3
O([] x<4)

Actually, there is no Next operator O in TLA, because its inclusion would lead to problems. It is however needed to construct a tableau, which is why we introduced it here.

Conventional model-checkers:

• use a special programming language (PROMELA, SPL)
• write checks as temporal formulas on states

if (x==3) {noncritical; x=1;}
else {critical; x=x+1;}

TLA says:

• It's error-prone to write in a new programming language
• Let us write spec and check in the same language: logic!
• Hence, the need for actions. Compare below.
• but actions are a two-edged sword...

with actions:     without:
 x'=x+1            Exists y: x=y /\ O(x=y+1)
  solvable          unsolvable in general
                    also, O not in TLA

Model: a possible execution trace of Spec
Model-checker: program to verify that all models satisfy Check

(simplistic) Check "always" formulas about states. * surprisingly useful...

(tableau) Check arbitrary temporal formulas about states.

To check "always" formulas about states is easy: just go through every possible state, and see if the formula holds. This is what TLC did, before the project.

Although it sounds simplistic, it is still useful! For example, TLC found some problems in the cache-coherency protocol of an Alpha chip currently in design. Paper available.)

Action tableau: new technique to handle arbitrary TLA formulas

[]<>Enabled(NextUp) => []<>Taken(NextUp)

equivalently, SF(NextUp).

"Strong Fairness". * what is weak fairness?

Strong and weak fairness

s1,s2,s1,s2,... is illegal under SF(Next)

s1,s2,s1,s2,... is legal under WF(Next)

hclock	hmclock	(m) hmclock

[] (tick \/ stutter)

SF(tick)

(In fact TLA always implicitly allows stutter-steps as part of its very syntax).

    Init:  x=1
  NextUp:  x<3  /\  x'=x+1
NextFlip:  x=3  /\  x'=1
LiveSpec:  SF(NextUp)

    Spec:  /\ Init
           /\ [] (NextUp \/ NextFlip \/ stutter)
           /\ LiveSpec

   Check:  /\ (x=3) ~> (x=1)
           /\ SF(NextFlip)
           /\ [] x<4

The user asks: does Spec => Check ?

In answer, we will attempt to find a counter-example.
i.e. a case where Spec and Not(Check) hold.

Existing model-checkers:

• Separate between fairness spec, logic checks
• Logic checks decided using Tableau method

(TLC only checked "always state" properties, before.)

New Technique 1: Action Tableau

• Generalise the Tableau technique to handle actions as well as states
• Work on Action Tableau not yet finished

• Everything else just a special case of action tableau

New Technique 2: Disjunctive Normal Form

• With TLA actions, fairness spec+check can be written in logic
• Disjunctive Normal Form rearranges them into a decidable form
• Succesfully implemented within TLC
• (DNF linear time; same with action tablueau would be exponential)

Turn a temporal formula on states
into a finite-state machine,
which accepts only those execution traces that satisfy the formula.

We want a counter-example to Spec=>Check: = Not(Check)
= Not(x=3 ~> x=1)
= <>(x=3 /\ []x≠1)

Only consider fulfilling cycles. The green cycle is not fulfilling: it makes the promise <>..., but does not deliver.

Do cross-product: state * tableau

Goal: to find cycle* component that

Answer: (1ⁿ2ⁿ3ⁿ)ⁿ3^ω

Goal: to find a component

A strongly connected component in a graph is a maximal subset of nodes and edges such that every node is reachable from every other node.

There are an infinite number of cycles, but they always end up contained within a component. Components completely capture every possible cycle.

There are standard algorithms for finding components. We use Targan [1972]. A neat online reference is by Prof. Eppstein as course-notes for his algorithms class. Once the components are found, we check that they are fair and fulfilling:

An eventually-always formula <>[]a means: remove all edges from the component that do not satisfy a, and find components in what is left.

An always-eventually formula []<>a means: that a must be present somewhere in the component that's left.

(You see why fairness the conditions eventually-always and always-eventually are so significant: they are temporal formulas which have no need of tableaux, because they merely describe properties of the final within-component loop of a cycle.)

Fulfilling: if we have <>p, which promises p, then we need in the component at least one node which either doesn't have <>p, or which does have p. You need to think subtly to figure out why this is correct. Hint: by construction of the tableau, the only way to get from a <>p to something without <>p is by actually fulfilling it! Incidentally, although it is true that Not([]p) promises Not(p), we don't consider it: since our disjunctive normal form pushed all negations inside.

If a component passes all these tests, then it is a valid counter-example and we are finished. If no component passes all tests, then there are no counter-examples.

The reference we used for all this is Temporal Verification of Reactive Systems: Safety by Manna and Pnueli, but we treat eventually-always and always-eventually a little more generally.

Basic idea: put actions into the tableau graph.

Subject of ongoing work.

In fact, can express all of Spec/\-Check as a single formula, in a single action tableau.

Before, we used to cross tableau with state-transition graph of Spec. But now, Spec has been merged into the tableau...

We cross action-tableau with the trivial universal state transition graph (fragment shown in green; needs no explicit storage; every state connects to every other state).

   NextUp:  x<3  /\  x'=x+1
 NextFlip:  x=3  /\  x'=1
NextStutt:  x'=x

  Formula:  /\ x=1
            /\ [] (\/ NextUp
                   \/ NextFlip
                   \/ NextStutt)

Advantages of action-tableaux:

• Unifies fairness-validation with temporal-formula validation.
• Can view other techniques as optimizations, not fundamentals. e.g. generation of state-transition-graph.
• Can use different validation criteria. e.g. Spec_min => Implementation => Spec_max

Optimization to reduce cost for fairness validation.
Express formula in disjunctive normal form. (preserves meaning)
Then look for cycles, as before.

(Sorry! TLC not yet publically released, so no interactive version available.)

tlclive egtalk

TLC Version 1.0 of 3 Jun 1999
Running Random Simulation with seed 7395095282892744306.
 
Found a counter-example!
The counter-example satisfies these parts from the spec:
<>[]- (state:LiveSpec.fair_enabled)
The counter-example satisfies this temporal formula:
<>(LiveCheck.conj0.cause) /\ []-(LiveCheck.conj0.effect)
And these are the states from which counter-example
cycles might be constructed:
* Behaviour-graph-node 5
particle formulas:  []-(state:LiveCheck.conj0.effect), 
State fingerprint: -4900539538744082733
/\ x = 3
Here endeth the counter-example.
 
[and there's a second counter-example...]
 
Finished checking.