• Ticc
• Expressions

Here we describe the meaning of Ticc expressions. For the precise syntax of expressions, and the keywords and symbols, refer to the input grammar. In the next section we discuss how the expressions are created.

Declaration of Types

Ticc has the following types:

• Integer Range, declared as [0..5]. Note that all ranges must start from 0.

• Boolean, declared using the keyword bool.

Constants

• num	non-negative integer constant
  true	Boolean constant true
  false	Boolean constant false

Operators

• &, and	conjunction of two Boolean expressions
  |, or	disjunction of two Boolean expressions
  ->, impl	implication of two Boolean expressions
  ~, not	complementation of a Boolean expression
  =	Equality check of two expressions
  !=	Unequality check of two expressions
  >	Greater than check of two integers
  >=	Greater than check equal of two integers
  <	Less than check of two integers
  <=	Less than equal check of two integers
  mod	Integer modulus of two integers
  +	sum of two integers
  -	subtraction of two integers
  :=	assignment of expression to a primed variable
  nondet	assignment of 'unconstrained' value to a primed variable

Precedence and Associativity of Operators

See this bug.

Expression evaluation and types

The typing rule during expression evaluation are as follows. Read them: they are not what you might expect!

Boolean to integer casts

Boolean "true" and "false" values are cast to the integer value 1 and 0 respectively in numerical expressions.

Casts among range types

In Ticc, the following basic principles apply:

• Expressions are always evaluated in a range that is large enough so that no rollover, or overflow, occurs.

• Negative numbers do not exist, since they are not part of a range type.

Let us illustrate the consequences of these design decisions. Consider the following expression:

 x' = y + z - 3

and assume that the ranges are as follows:

 var x: [0..4]
 var y: [0..5]
 var z: [0..5]

The rules imply the following:

• The sum of y and z is evaluated in a (temporary) range type that is at least [0..10], so that no overflow can occur.

• If the result of the expression is negative, it cannot possibly be equal to x', so the overall expression (which has boolean type) will be false.

For example:

• If x is 4, y is 4, and z is 3, then the expression will be true, as expected. In fact, 4+3 will give 7, and 7-3 = 4: no overflow occurs.

• If x is 1, y is 4, and z is 5, the expression is false, as 4 + 5 - 3 = 6, which is different from 1. Note in particular that rollover does not occur: even though 6 mod 5 = 1, the expression on the right hand side is considered to have value 6, not 1, in spite of the left hand side having range [0..4].

• If y is 1, and z is 1, the expression will be false, since the rhs gives rise to a negative number.

Automatic term reordering

Consider now the following expression:

 x' = y - z + 3

If x is 2, y is 2, and z is 3, then the expression would yield value false, even though 2 = 2 - 3 + 3! In fact, Ticc would evaluate y - z, obtain a negative number, and say that the whole expression is false. To mitigate (but not eliminate) this, after parsing, Ticc tries to reorder the expressions, so that whenever possible, negative results are avoided. For instance, the above expression would be internally transformed into the following expression:

 x' = y + 3 - z

so that a negative result would occur only if the total result is negative. Ticc is somewhat limited in the reorderings it can perform: it can do basic expression simplification, and it reorders the terms of a sum so that positive terms occur before negative terms. If you are interested in knowing what reorderings occurred, you can (better: should) print the modules you parse. Indeed, it is in general a good habit to print the modules after parsing, to check that Ticc has interpreted them correctly.