What’s new in PAT 2.6.0

In this release, Real-Time System module is improved with more timed syntax. Atomic events sequence is supported in CSP and RTS module. For the user interface, PAT provides a better document management menu in the Window toolbar. The simulator’s graph generation is put into an additional thread, which will not hang the user interface. Other updates new examples and bug fixing.

Atomic Sequence

The keyword atomic allows user to define a process which always makes maximum progress if possible. The syntax is atomic{P}, where P is any process definition.

If a sequence of statements is enclosed in parentheses and prefixed with the keyword atomic, this indicates that the sequence is to be executed as one super-step, non-interleaved with other processes. In the interleaving of process executions, no other process can execute statements from the moment that the first statement of an atomic sequence is executed until the last enabled one has completed. The sequence can contain arbitrary process statements, and may be non-deterministic.

Before atomic sequence starts, it competes with other processes. Once atomic sequence starts, it goes into the active state, and it continues to execute until termination or blocked. If any statement within the atomic sequence is blocked (e.g., due to a synchronous channel output event or parallel barrier synchronization), atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence is resumed immediately. If multiple active atomic processes are enabled, then they execute interleavingly. In the following example, process P(or Q) will be blocked by the synchronization channel event once they are in the active states. After the synchronization event, both P and Q are in active states, then the b -> c -> Skip and e -> f -> Skip are executed as there is no atomic.

channel ch 0;
P = atomic { a -> ch!0 -> b -> c -> Skip};
Q = atomic { d -> ch?0 -> e -> f -> Skip};
Sys = P ||| Q;

Note: atomic sequences can be used for state reduction for model checking, especially if the process is composed with other processes in parallel. The number of states may be reduced exponentially. In a way, by using atomic, we may partial order reduction manually (without computational overhead).

Note: atomic sequences inside other atomic sequence has no effect at all.

Note: Atomic sequence is supported in RTS module, all the engaged events in atomic group takes no time.

Syncrhonous Channel in LTL
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)

User Interface Update
1 Tab Management under Window toolbar, which provides similar behaviors like other IDE.
2 The graph generation function in Simulator is moved to an independent thread. The simulator will not hang when u generate a big graph.
3 Open file dialog box will use the default modeling language file type as the default file filter.

Others
1 User manual is updated to latest implementation.
2 Real-Time system example is added.
3 Fix the bugs in latex generation functions and change the “refines”, “refines<F>” and “refines<FD>” symbols in latex