The input languages of ProTL is PrCCSL specifications, i.e., the textual encodings that follow the PrCCSL format. We first describe the character set that are supported in the PrCCSL specifications. Then, how the specifications can be formed by tokens is introduced. Finally, the usage a set of keywords (including declaration, expression and relations) to encode the specifications is demonstrated.

Character Set

A subset of the ASCII character set is utilized in the PrCCSL specifications:

1. Digits: 0,1,2,3,4,5,6,7,8,9.

2. Letters: 'a' -'z' and 'A' -'Z'.

3. Punctuation characters: '+', '*', '=', '#', '(', ')', '.', '[', ']', '-'.

4. Whitespace characters: space, tab, newline, and carriage-return.

5. Line terminators: ';'.

Token

ProTL can recognize various tokens. A summary of token types is provided as follows:

• Integer: A sequence of digits without leading zeros,

Regular Expression: 0|([1-9][0-9]*)

Example: 0, 10, 33

• Double: An integer followed by a decimal point, then followed by a sequence of digits

Regular expression: (Int+).(Int+)

Example: 32.7, 0.001

• Clock: A sequence of characters

Regular expression: (a..z|A..Z|0..9|[|]|_)+

Example: trig, c1, c2, c_3

• Parameter (para): Integers or operations between integers

Regular expression: Int|( Int (+ Int )* ) )

Example: (A+B), 22+13

Syntax of PrCCSL

We introduce the keywords in PrCCSL and their syntax and semantics. Keywords in PrCCSL can be categorized into three types, i.e., clock declaration, expressions and relations.

1. Clock Declaration

• “Clock” declares a new clock. A clock needs to be declared before being used in the PrCCSL expressions or relations. For example, three new clocks named c1, c2 and c3 can be declared as shown as follow:

Clock c1, c2, c3;

• “ClockType” declares a new clock type that can be either dense or discrete. A dense clock represents the continous physical time. A logical clock represents discrete and total order set of event occurrences (often an event occurrence is called tick) based on physical/logical time. A new dense clock type can be defined using DenseClockType as follows:

DenseClockType cost{

reference idealClk, 

factor    10,

offsent   {(event1, 1.8), (event2, 0.2)},

reset     {event3, event4}

};

2. Expressions

• “is” defines a new clock based on expressions.
• “periodicOn” builds a periodic clock that ticks based on a base clock and a period parameter. An example of using periodicOn to define a new clock named c is shown as follows. The instants of c are separated by 50 instants of clock base.

Clock c;

Clock base;

c is periodicOn base period 50;

• “inf” represents the infimum expression, which defines a new clock c that is the slowest clock that is faster than both c1 and c2:

Clock c, c1, c2;

c is c1 inf c2 ;

• “sup” represents supremum expression, which defines the faster clock that is slower than both c1 and c2:

Clock c, c1, c2;

c is c1 sup c2 ;

• “delayFor” results in a clock c by delaying the reference clock ref for a given number of ticks of a base clock base:

Clock c;

Clock base, ref;

c is ref delayFor 50 on base;

• “clockInter” denotes intersection expression, which defines a new clock that ticks if both two reference clocks tick:

Clock c, c1, c2;

c is c1 clockInter c2 ;

• “clockUnion” represents union expression, which defined as a new clock that ticks if when c1 or c2 ticks:

Clock c, c1, c2;

c clockDef c1 clockUnion c2 ;

• “filterBy” filters out undesired instants of clock c1 and leave the desired ticks. For example, c is defined as a clock that ticks from the 2^nd tick of c1, i.e., the 1^st tick of c1 is filtered:

Clock c, c1;

c is c1 filterBy B10(B1);

• ite (if-then-else) represents the conditional clock expression. As shown following code, a conditional clock expression defines a clock that behaves either as a clock c1 or as another clock c2 according to the value of a boolean variable b.

Clock c, c1, c2;

c is if b then c1 else c2;

3. Clock Actions

The clock action relates a logical clock c with a set of oper ations that are performed to change the system behaviors, e.g., assignments, functions/operations on variables.

Clock c;

```C

int a; 

```;

c action {a=1};

4. Probabilistic Clock Actions

Probabilistic clock action is used to describe the situation where an event can be associated with multiple actions under uncertainty, i.e., it is uncertain which action out of a set of actions the system will take when the event occurs.

Clock c;

```C

int a; 

```;

c pAction {(0.10, {a=1}), (0.20, {a=2}), (0.70, a=3)};

5. Clock Relations

• Probabilistic subclock relation (c1 ⊆_0.95 c2 ) specifies that the subclock relation between c1 and c2 must be satised with probability greater than or equal to 95%. p denotes the probability threshold on the relations:

Clock c1, c2;

c1 subclock(p=0.95) c2 ;

• Probabilistic coincidence relation (c1 ≡_0.95 c2) specifies that the coincidence relation between c1 and c2 must be satisfied with proba- bility greater than or equal to 95%:

Clock c1, c2;

c1 coincides(p=0.95) c2 ;

• Probabilistic exclusion (c1#_0.95c2) prevents the instants of two clocks from being coincident:

Clock c1, c2;

c1 excludes(p=0.95) c2 ;

• Probabilistic precedence (c1 ≺_0.95 c2) specifies that c1 must run faster than c2:

Clock c1, c2

c1 precedes(p=0.95) c2 ;

• Probabilistic causality (c1 ≼_0.95 c2) represents a relaxed version of precedence relation, allowing the two clocks to tick at the same time:

Clock c1, c2;

c1 causes(p=0.95) c2 ;

6. N-ary Clock Relation

To describe the complex requirements associated with multiple events, we extend the binary relations into n-ary relations, which allow to de scribe the dependencies among a set of events.

• N-ary coincidence

Clock c1, c2, c3, c4;

coincides(p=0.95, c1, c2, c3, c4);

• N-ary subclock

Clock c1, c2, c3, c4;

subclock(p=0.95, c1, c2, c3, c4);

• N-ary exclusion

Clock c1, c2, c3, c4;

excludes(p=0.95, c1, c2, c3, c4);

• N-ary precedence

Clock c1, c2, c3, c4;

precedes(p=0.95, c1, c2, c3, c4);

• N-ary causality

Clock c1, c2, c3, c4;

causes(p=0.95, c1, c2, c3, c4);

Note that the following keywords should not be used as identifier or names when editing PrCCSL encodings/specifications: Clock, is, DenseClockType, idealClk, IdealClock, factor, offset, reference, reset, coincides, excludes, causes, precedes, periodicOn, period, if, then, else, inf, sup, on, clockInter, clockUnion, delayFor, filterBy.