Deadlock-freeness

Given P() as a process, the following assertion asks whether P() is deadlock-free or not.

#assert P() deadlockfree;

Where both assert and deadlockfree are reserved keywords. PAT's model checker performs Depth-First-Search or Breath-First-Search algorithm to repeatedly explore unvisited states until a deadlock state (i.e., a state with no further move except for successfully terminated state) is found or all states have been visited.

Divergence-free

Given P() as a process, the following assertion asks whether P() is divergence-free or not.

#assert P() divergencefree;

Where both assert and divergencefree are reserved keywords. Given a process, it may perform internal transitions forever without engaging any useful events, e.g., P = (a -> P) \ {a};,  In this case, P is said to be divergent. Divergent system is usually undesirable.

Deterministic

Given P() as a process, the following assertion asks whether P() is deterministic or not.

#assert P() deterministic;

Where both assert and deterministic are reserved keywords. Given a process, if it is deterministic, then for any state, there is no two out-going transitions leading to different states but with same events. E.g, the following process is not deterministic.

P = a -> Stop [] a -> Skip;

Nonterminating

Given P() as a process, the following assertion asks whether P() is nonterminating or not.

#assert P() nonterminating;

Where both assert and nonterminating are reserved keywords. PAT's model checker performs Depth-First-Search or Breath-First-Search algorithm to repeatedly explore unvisited states until a terminating state (i.e., a state with no further move, including successfully terminated state) is found or all states have been visited. The following process is deadlockfree, but not nonterminating.

P = a -> Skip;

Reachability

Given P() as a process, the following assertion asks whether P() can reach a state at which some given condition is satisfied.

#assert P() reaches cond;

Where both assert and reaches are reserved keywords and cond is a proposition defined as a global definition. For instance, the following code segment asks whether P() can reach a state at which x is negative.

• var x = 0;
• P() = add{x = x + 1;} -> P() [] minus{x = x -1;} -> P();
• #define goal x < 0;
• #assert P() reaches goal;

In order to tell whether the assertion is true or not, PAT's model checker performs a depth-first-search algorithm to repeatedly explore unvisited states until a state at which the condition is true is found or all states have been visited.

To further query about variable values, PAT allows user to find the minimum value or maximum value of some expressions in all reachable traces. The following coin changing example show how to minimize the number of coins during the reachability search.

• var x = 0;
• var weight = 0;
• P() = if(x <= 14)
•    { 
•          coin1{x = x + 1; weight =weight + 1;} -> P() [] coin2{x = x + 2; weight = weight + 1;} -> P() [] coin5{x = x + 5; weight = weight + 1;} -> P()
•       };
• #define goal x == 14;
• #assert P() reaches goal with min(weight);

Linear Temporal Logic (LTL)

In PAT, we support the full set of LTL syntax. Given a process P(), the following assertion asks whether P() satisfies the LTL formula.

#assert P() |= F;

where F is an LTL formula whose syntax is defined as the following rules,

F = e | prop | [] F | <> F | X F | F1 U F2 | F1 R F2

where e is an event, prop is a pre-defined proposition, [] reads as "always" (also can be written as 'G' in PAT), <> reads as "eventually" (also can be written as 'F' in PAT), X reads as "next", U reads as "until" and R reads as "Release" (also can be written as 'V' in PAT).  

An LTL formula can be evaluated over an infinite sequence of truth evaluations and a position on that path. The semantics for the modal operators is given as follows.

Informally, the assertion is true if and only if every execution of the system satisfies the formula. Given an LTL formula, PAT's model checker firstly invokes a procedure to generate a Buchi automaton which is equivalent to the negation of the formula. Then, the Buchi automaton is composed of the internal model of P() so as to determine whether the formula is true for all system executions or not. Refer to [SUNLDP09] for details. For instance, the following assertion asks whether the philosopher can always eventually eat or not (i.e., non-starvation).

#assert Phil() |= []<>eat;

Note: event e can be component event like eat.0. e can also be channel event like "c!3.8" or "c?19". Double quotation marks are needed when writing channel events due to the special characters ! and ?. Synchronous channel events can be written as c.3.8.

#assert Phil() |= []<> eat.0 && "c!3";

Note: In LTL, if there is synchronous channel, its input (?) or output (!) event will be renamed to synchronous event (.) after parsing.
[](c1!2 -> <> c2?3) will be changed to [](c1.2 -> <> c2.3)

Note: when two or more X are used together, leave a space between them. XX will be mis-recognized as a proposition.

Refinement/ Equivalence

In PAT, we support FDR's approach for checking whether an implementation satisfies a specification or not. That is, by the notion of refinement or equivalence. Different from LTL assertions, an assertion for refinement compares the whole behaviors of a given process with another process, e.g., whether there is a subset relationship. There are in total 3 different notions of refinement relationship, which can be written in the following syntax.

• #assert P() refines Q() -whether P() refines Q() in the trace semantics;
• #assert P() refines<F> Q() -whether P() refines Q() in the stable failures semantics;
• #assert P() refines<FD> Q() -whether P() refines Q() in the failures divergence semantics;

PAT's model checker invokes a reachability analysis procedure to repeatedly explore the (synchronization) product of P() and Q() to search for a state at which the refinement relationship does not hold.