• Ticc
• Wildcard Input Actions

Starting from Ticc 0.20, it is possible to use wildcard patterns ending with * as names for input actions in a module. This can be used to specify, at once, requirements for many similarly-named actions.

As an example, suppose that three modules, P1, P2, P3, interact with a module Q. Assume that P1 can output action print_color, P2 can output action print_bw, and P3 can output action print_poster. Assume that Q has the same input constraints for these three actions, and performs the same internal transitions when receiving the actions. Then, rather than specifying three different input rules in Q, it may be convenient to use just one:

•  input print_* { ... } 

This print_* action is called a wildcard input, and it can match all three output actions print_color, print_bw, and print_poster. An example of use of wildcard actions can be found in the house example.

An extreme case consists in using * to match any input action. For instance, the following states that the environment, whatever it does, can never change the value of the variable x:

•  input * { global: x' = x } 

Thus, the * action offers a quick way of expressing environment constraints that apply to all actions.

Composition in presence of wildcard input actions

The best match is the longest match, preferably without wildcard

The best input match for an action a in a module Q is the action labeling an input transition of Q which:

• has the same name of a, if such an action can be found;

• otherwise, consists of the longest prefix of the name of a, followed by *.

For example, suppose Q has actions abc, abc*, and abcde labeling input transitions. Then:

• the best input match for a does not exist;

• the best input match for abc is abc;

• the best input match for abcd is abc*;

• the best input match for abcde is abcde;

• the best input match for abcdef is abc*.

The best output match for an action a in module Q is simply an action with the same name of a, if any.

How composition works

The composition of two modules P and Q is formed as follows. (Note: technically, we are giving the rules for the product of P and Q, from which the composition is then automatically derived).

Normalization

First, the modules are normalized, so that if a module contains an output transition for action a, but no best input match for a, then a false input transition is associated with a. This makes it explicit that the module cannot accept a as input.

Synchronization

Then, we compute the actions in the composition of two modules P and Q as follows. For every action a of P:

• If a labels an output transition transP of P:

  • If there is no best input match for a in Q, then we add to the composition an output transition transP labeled by action a. The idea is that the action a is not shared by Q, so that no synchronization between P and Q occurs. In this case, the composition P || Q of P and Q can issue a as output exactly when P and Q can.

  • If there is a best input match for a in Q, and if this best input match labels the (input) transition transQ, then we add to the composition of P and Q the output action, with the same name as a, resulting from the synchronization of transP and transQ. Roughly, this synchronization consits in:

    • checking that transP satisfies the global assumptions of transQ
    • conjoining transP with the local portion of transQ

    For the details, see the FROCOS 05 paper (Postscript PDF).

• If a labels an input transition transP of P (the name of a can be either a string, or a wildcard pattern):

  • If there is no best input match for a in Q, then we add to the composition an input transition transP labeled by action a. Again, the idea is that a is not shared.

  • If there is a best input match for a in Q, and if this best input match labels the (input) transition transQ, then we add to the composition of P and Q an input transition corresponding to the conjunction of transP and transQ, and labeled by a.

Example 1

Before renormalization

After renormalization

Composition

Ticc will also check that this transition occurs only when u = 1 holds.

Example 2

Before renormalization

After renormalization

Composition

Ticc will also check that this transition occurs only when u = 1 holds.