Real Time features of Ticc

Ticc supports discrete real-time through the use of clock variables.

Clock variables

Local variables can be of type Clock. A clock variable can assume any integral non-negative value. In expressions, clock variables can only be compared to integral constants. So, if x is a clock variable, the following are valid expressions: 

x<3
x=10
x'>5
x':=20 (in the local part of an input rule)

A module is timed if it has at least one clock variable. Clock variables increase their value by 1 when both players choose a special delay action. The delay action is only available to a player if the state obtained by increasing all clocks by 1 satisfies the player's invariant. The delay action is implicitly present in all timed modules, but it is not shown by the Ticc functions that print a module.

All other actions are taken instantaneously (even if taking such actions may "manually" change the value of some clocks).

The non-Zenoness Condition

Players can play in such a way as to stop the progress of time; for instance, by taking an infinite sequence of instantaneous actions. On the other hand, for a timed module to be "correct", it should satisfy the following condition:

A state is well-formed if it satisfies the above condition. For a more detailed description of the non-Zenoness condition, refer to:

Creation of a Symbolic Module

When a timed symbolic module is created with Ticc.mk_sym, both Input and Output invariants are potentially strengthened in order to ensure that only well-formed states are reachable. An on-screen message warns if such strengthening has occurred.

Similarly, the initial condition of the module is strengthened to ensure that it satisfies both invariants. An on-screen message warns if the initial condition has become empty (false) as a result of such strengthening.

Composition

When at least one of the two modules being composed is timed, the input invariant of the composition is strengthened to make sure that only well-formed states are reachable.

Unsupported Features

The following operations fail raising an exception when invoked on timed modules:

Ticc/Real Time (last edited 2007-08-01 05:35:30 by MarcoFaella)