CIF 3

Language tutorial

This tutorial introduces the CIF 3 language. It explains the general idea behind the concepts of the language, and shows how to use them, all by means of examples. The tutorial is focused on giving a short introduction to CIF, and does not cover all details. It is recommended reading for all CIF users.

Introduction

CIF stands for Compositional Interchange Format for hybrid systems. CIF is primarily used to create models of physical systems and their controllers, describing their behavior. However, CIF is a general-purpose modeling language, and can be used to model practically anything, ranging from physical real-world systems to abstract mathematical entities.

CIF supports discrete event models, that are mostly concerned with what happens, and in which order. CIF also supports timed systems, where timing plays and explicit role, and hybrid systems, which combine the discrete events with timing. This makes CIF suitable for modeling of all kinds of systems.

The CIF 3 tooling puts a particular focus on supporting the entire development process of controllers. However, just as the CIF language, the CIF tooling can be applied much more generally. The tooling allows among others specification, supervisory controller synthesis, simulation-based validation and visualization, verification, real-time testing, and code generation.

Lessons

Several lessons are available, grouped into the following categories:

The lessons introduce new concepts, one by one, and are meant to be read in the given order.

Basics

Automata
Explains automata, locations, events, edges, transitions, and more.
Synchronizing events
Explains event synchronization, enabledness, traces, and state spaces.
Non-determinism
Explains multiple causes of non-determinism.
Alphabet
Explains alphabets for both individual automata and entire specifications.
Event declaration placement
Explains the placement of event declarations.
Shorter notations
Explains several shorter notations, including self loops, declaring multiple events with a single declaration, multiple events on an edge, and nameless locations.

Data

Discrete variables
Explains discrete variables, guards, and updates.
Discrete variable value changes
Explains how and when discrete variables can change value.
Location/variable duality (1/2)
Explains the duality between locations and variables using a model of a counter.
Location/variable duality (2/2)
Explains the duality between locations and variables using a model of a lamp.
Global read, local write
Explains the concepts of global read and local write.
Monitoring
Explains monitoring, self loops, and monitor automata.
Old and new values in assignments
Explains old and new values of variables in assignments, multiple assignments, and the order of assignments.
The tau event
Explains the tau event.
Initial values of discrete variables
Explains initialization of discrete variables, including the use of default values and multiple potential initial values.
Initialization predicates
Explains initialization in general, and initialization predicates in particular.
Using locations as variables
Explains the use of locations as variables.
State (exclusion) invariants
Explains state (exclusion) invariants.
State/event exclusion invariants
Explains state/event exclusion invariants.

Types and values

Types, values, and expressions
Explains the concepts of types, values, and expressions, as an introduction for the other lessons in this category.
Values overview
Provides an overview of the available values, and divides them into categories.
Integers
Explains integer types, values, and commonly used expressions.
Integer ranges
Explains integer ranges.
Reals
Explains real types, values, and commonly used expressions.
Booleans
Explains boolean types, values, and commonly used expressions.
Strings
Explains string types, values, and commonly used expressions.
Enumerations
Explains enumeration types, values, and commonly used expressions.
Tuples
Explains tuple types, values, and commonly used expressions.
Lists
Explains list types, values, and commonly used expressions.
Bounded lists and arrays
Explains bounded lists, arrays, and their relations with regular lists.
Sets
Explains set types, values, and commonly used expressions.
Dictionaries
Explains dictionary types, values, and commonly used expressions.
Combining values
Explains how to combine values of different types.

Scalable solutions and reuse (1/2)

Constants
Explains the use of constants.
Algebraic variables
Explains the use of algebraic variables.
Algebraic variables and equations
Explains the use of equations to specify values of algebraic variables.
Type declarations
Explains the use of type declarations.

Time

Timing
Introduces the concept of timing.
Continuous variables
Explains the use of continuous variables.
Continuous variables and equations
Explains the use of equations to specify values of continuous variables.
Equations
Show the use of equations for both continuous and algebraic variables, by means of an example of a non-linear system.
Variables overview
Provides an overview of the different kinds of variables in CIF, and their main differences.
Urgency
Explains the concept of urgency, as well as the different forms of urgency.
Deadlock and livelock
Explains the concepts of deadlock and livelock.

Channel communication

Channels
Explains point-to-point channels and data communication.
Dataless channels
Explains void channels that do not communicate any data.
Combining channel communication with event synchronization
Explains how channel communication can be combined with event synchronization, further restricting the communication.

Functions

Functions
Introduces functions, and explains the different kind of functions.
Internal user-defined functions
Explains internal user-defined functions.
Function statements
Explains the different statements that can be used in internal user-defined functions.
Functions as values
Explains using functions as values, allowing functions to be passed around.

Scalable solutions and reuse (2/2)

Automaton definition/instantiation
Explains using automaton definition and instantiation for reuse.
Parametrized automaton definitions
Explains parametrized automaton definitions.
Automaton definition parameters
Explains the different kinds of parameters of automaton definitions.
Groups
Explains hierarchical structuring using groups.
Group definitions
Explains groups definitions and parametrized group definitions.
Imports
Explains splitting CIF specifications over multiple files using imports.
Imports and libraries
Explains how to create libraries that can be used by multiple CIF specifications using imports, as well as how to use imports to include CIF specifications from other directories.
Imports and groups
Explains how imports and groups interact.
Namespaces
Explains namespaces, and how they can be used together with imports.
Input variables
Explains input variables, how they can be used for coupling with other models and systems, and their relation to imports.

Stochastics

Stochastics
Introduction to stochastic distributions, which allow for sampling, making it possible to produce random values.
Discrete, continuous, and constant distributions
Explains the different categories of stochastic distributions: discrete, continuous, and constant distributions.
Pseudo-randomness
Explains how computers implement stochastics using pseudo-random number generators, and how this affects the use of stochastics in CIF.

Language extensions

Supervisory controller synthesis
Explains how to extend a model to make it suitable for supervisory controller synthesis.
Print output
Explains how to extend a model to include printing of textual output. (This documentation is currently not part of the language tutorial, but of the simulator tool documentation.)
SVG visualization
Explains how to extend a model to couple it to an image for visualization. (This documentation is currently not part of the language tutorial, but of the simulator tool documentation.)
SVG interaction
Explains how to extend a model to couple it to an image for interaction via a visualization. (This documentation is currently not part of the language tutorial, but of the simulator tool documentation.)