• Ticc
• Input Grammar

Ticc Input Grammar for Ticc 0.20

Keywords

Grammar rules

The following describes the grammar rules of the ticc language.

Note that, in addition to this grammar, the Ticc type checker further limits what inputs can be accepted. This is the same situation as in programming languages: not all that can be parsed constitutes legal input. As an example, the guard of a guarded command (see Guarded Commands for a description) cannot reference primed variables even if there is a grammar rule that allows it. The restrictions on the grammar rules are described in Guarded Commands, Global Structure of Ticc Programs, expressions and Quick Start. Several examples in ticc/examples/tutorial also illustrate the restrictions.

Conventions

• nonterminals are in italics

• tokens are in typewriter face

• The empty string is denoted by <empty>

• A production is written as:

  • nonterminal ::= rule

Input file structure

A file can contain variable, stateset, or module declarations. See Global Structure of Ticc Programs for a description of the overall structure of a Ticc input file. A set of states has a name, and it is defined by a boolean expression (no primed variables allowed). Sets of states declared outside modules can refer only to global variables.

The initial symbol of the grammar is design.

• design ::= varmodlist

  varmodlist ::= <empty> | varmod varmodlist

  varmod ::=
  

  • var varnamelist : vartype
    

  • | statesetd
    | moduledeclaration

  statesetd ::= stateset id : exp

Module declaration

A module declaration consists of a module name, and of a body. The body is a list of variable, invariants, transitions, sets of states, initial conditions, and transitions. These elements can appear in any order.

• moduledeclaration ::= module modname : moddecllist endmodule
  

  modname ::= id

  moddecllist ::=
  

  • vardecl moddecllist
    

  • | stateless moddecllist
    | invariant moddecllist
    | statesetd moddecllist
    | initsetd moddecllist
    | transition moddecllist
    | <empty>;

Variable declarations

Variables can be either of boolean type, or of range type, where the range is [0...n] for some (small ) integer n. Some variables can be declared to be stateless. The module does not track the value of these variables.

• vardecl ::= var varnamelist : vartype

  varnamelist ::=
  

  • varnamelist, varname
    

  • | varname

  varname ::= id

  vartype ::= bool | [ num ... num ]

  stateless ::= stateless varnamelist

Sets of states

A module can have an optional initial condition, defined by initsetd. A module can also declare input and output invariants, which are just boolean expressions (no primed variables allowed). It is possible to use multiple initsetd and invariant formulas in a module; the initial condition, and the invariants, result from conjoining all the given formulas.

A modulo can also declare state sets, via the declaration statesetd. statesetd is defined in the same way as global sets, but can refer also to the local variables of a module.

• initsetd ::= initial : exp

  invariant ::= oinv : exp | iinv : exp

Transitions for Output and Local Actions

A transition can correspond to input, output, or local actions. Each output and local transition is labeled by the name of the action that causes it. Guarded Commands for output and local actions consist of a guard and a command. Follow the above link for more information.

• transition ::=
  

  • output actname : { guardedcmds }
    

  • | local actname : { guardedcmds }
    | input actexp : { globalpart localpart }

  actname ::= id

  guardedcmds ::=
  

  • <empty>

  • | guardedcmd ; guardedcmds
    | guardedcmd

  guardedcmd ::= exp ==> optexp

  optexp ::= <empty> | exp

Transitions for Input Actions

Input transitions can be labeled with actexp (action expression), which can end with *. Such wildcard patterns can match many input actions at once; see wildcard input actions for more information. The guarded commands of input transitions have global and local parts. for more information, see Guarded Commands. The global part is the same as for output and local transitions: The local part has a special syntax, which forces the transition to be deterministic.

• actexp ::= id | wildid

  globalpart ::= <empty> | global : guardedcmds

  localpart ::= <empty> | local : detguardedcmds

  detguardedcmds ::=
  

  • | detguardedcmd
    | detguardedcmds else detguardedcmd

  detguardedcmd ::=
  

  • exp ==> detcmdlist
    

  • | exp ==> detcmdlist;

  detcmdlist ::=
  

  • | detcmd
    | detcmdlist , detcmd

  detcmd ::= nextvar := exp

Expressions

Operators appearing on the same line in the production below, such as | and or, are synonims. See expressions for information on the semantics.

• exp ::= num
  

  • | var
    | var'
    | true
    | false
    | exp = exp
    | exp != exp
    | exp > exp
    | exp < exp
    | exp >= exp
    | exp <= exp
    | exp & exp | exp and exp
    | exp | exp | exp or exp
    | exp -> exp | exp impl exp
    | not exp | ~ exp
    | nondet var'
    | exp + exp
    | exp - exp
    | exp mod exp
    | ( exp )

  ( the | here denotes logical or )

  var ::= id

  id ::= defined by the pattern alpha ( alpha | digit | '_' | '.' )* where alpha is a letter A-Za-z, and digit is a symbol in 0-9.

  wildid ::= defined by the pattern alpha ( alpha | digit | '_' )*'*' where alpha is a letter A-Za-z, and digit is a symbol in 0-9. In other words, this is just like an id, with a star * appended to it.

  num ::= A sequence of at least one digit, i.e. defined by the pattern "digit+".

For the input grammar for previous versions of Ticc, click on Get Info, and look for pages that refer to the older version.