• Ticc
• Quick Start

To use Ticc, first ensure that the executable file ticc is in your path. There are two ways to use Ticc:

Interactive mode

You invoke Ticc in interactive mode simply by typing:

ticc

At the Ocaml prompt, you must type:

open Ticc;;

At this point, the functions in the module Ticc become available at the top level. These functions are documented in the file ticc/doc/api/Ticc.html, and provide you all the functionality of Ticc.

Script file

You can also include the Ocaml commands in a file called example.in (or any other name you wish), and then invoke Ticc to execute the commands in that file:

ticc example.in

Script files for Ticc

You can find several examples of Ticc scripts in Ticc Examples. These scripts are written in OCaml, and follow a very basic format. Here is an example, in which you:

1. Parse the file MyModel.si (the extension .si stands for "Sociable Interfaces""")

2. Create, from the syntactic modules SomeModuleName and SomeOtherModule, two symbolic modules (implemented via MDDs), stored in the Ocaml variables model1 and model2.

3. Compose the two symbolic modules, forming a symbolic module stored in the Ocaml variable composed.

open Ticc;;
parse "MyModel.si";;

let model1 = mk_sym "SomeModuleName";;
let model2 = mk_sym "SomeOtherModule";;

let composed = compose model1 model2;;

Syntactic vs. Symbolic Representations

Ticc represents modules in two different ways internally: abstract syntactic representations, and symbolically (as MDDs). The abstract syntax representation is created when parsing the file containing the ticc program. You must call the mk_sym function to instantiate the symbolic version of a module, which is then used to compose and validate interfaces.

Parsing Multiple Files

The parse function reads in a .si file describing modules and global variables, and places these definitions into a global namespace. Parsing multiple files is an incremental process: declarations are added to the global name space. This means that modules can't have the same name, even if they are in different files. It also means that you don't need to declare global variables in every file; declaring them in the first file is enough. Think of parsing multiple files simply as a convenient way of splitting into smaller parts the parsing of a larger file. If any error occurs during parsing, all the declarations parsed from the current file (the one with the error) will be discarded. This enables you to fix the file, and try to parse it again.