//////////////////////////////////////////////////////////////////////////////
// Copyright (c) 2010, 2026 Contributors to the Eclipse Foundation
//
// See the NOTICE file(s) distributed with this work for additional
// information regarding copyright ownership.
//
// This program and the accompanying materials are made available
// under the terms of the MIT License which is available at
// https://opensource.org/licenses/MIT
//
// SPDX-License-Identifier: MIT
//////////////////////////////////////////////////////////////////////////////

include::_part_attributes.asciidoc[]

indexterm:[tutorial,language]

:leveloffset: -2

[[lang-tut-chapter-index]]
== Language tutorial

This tutorial introduces the CIF 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 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.

indexterm:[discrete event system]
indexterm:[timed system]
indexterm:[hybrid system]

CIF supports discrete event models, that are mostly concerned with what happens, and in which order.
CIF also supports timed systems, where timing plays an 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 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.

CIF <<history-chapter-index,originally stood for>> **C**ompositional **I**nterchange **F**ormat for hybrid systems.
As the language has since evolved beyond its original purpose, the name 'CIF' is nowadays only used in its abbreviated form.

=== Lessons

Several lessons are available, grouped into the following categories:

* <<virtual-toc-target\--lang-tut-basics,Basics>>
* <<virtual-toc-target\--lang-tut-data,Data>>
* <<virtual-toc-target\--lang-tut-values,Types and values>>
* <<virtual-toc-target\--lang-tut-reuse1,Scalable solutions and reuse (1/2)>>
* <<virtual-toc-target\--lang-tut-time,Time>>
* <<virtual-toc-target\--lang-tut-channels,Channel communication>>
* <<virtual-toc-target\--lang-tut-functions,Functions>>
* <<virtual-toc-target\--lang-tut-reuse2,Scalable solutions and reuse (2/2)>>
* <<virtual-toc-target\--lang-tut-stochastics,Stochastics>>
* <<virtual-toc-target\--lang-tut-svg,SVG visualization and interaction>>
* <<virtual-toc-target\--lang-tut-text,Text>>
* <<virtual-toc-target\--lang-tut-synthesis,Synthesis>>
* <<virtual-toc-target\--lang-tut-annotations,Annotations>>

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

[[virtual-toc-target--lang-tut-basics]]
*Basics*

<<lang-tut-basics-chapter-automata>>::
Explains automata, locations, events, edges, transitions, and more.

<<lang-tut-basics-chapter-synchronizing-events>>::
Explains event synchronization, enabledness, traces, and state spaces.

<<lang-tut-basics-chapter-non-determinism>>::
Explains multiple causes of non-determinism.

<<lang-tut-basics-chapter-alphabet>>::
Explains alphabets for both individual automata and entire specifications.

<<lang-tut-basics-chapter-event-placement>>::
Explains the placement of event declarations.

<<lang-tut-basics-chapter-shorter-notations>>::
Explains several shorter notations, including self loops, declaring multiple events with a single declaration, multiple events on an edge, and nameless locations.

[[virtual-toc-target--lang-tut-data]]
*Data*

<<lang-tut-data-chapter-discrete-variables>>::
Explains discrete variables, guards, and updates.

<<lang-tut-data-chapter-discvar-change>>::
Explains how and when discrete variables can change value.

<<lang-tut-data-chapter-loc-var-duality1>>::
Explains the duality between locations and variables using a model of a counter.

<<lang-tut-data-chapter-loc-var-duality2>>::
Explains the duality between locations and variables using a model of a lamp.

<<lang-tut-data-chapter-read-write>>::
Explains the concepts of global read and local write.

<<lang-tut-data-chapter-monitoring>>::
Explains monitoring, self loops, and monitor automata.

<<lang-tut-data-chapter-asgn-old-vs-new>>::
Explains old and new values of variables in assignments, multiple assignments, and the order of assignments.

<<lang-tut-data-chapter-tau-event>>::
Explains the `tau` event.

<<lang-tut-data-chapter-discvar-init>>::
Explains initialization of discrete variables, including the use of default values and multiple potential initial values.

<<lang-tut-data-chapter-init-preds>>::
Explains initialization in general, and initialization predicates in particular.

<<lang-tut-data-chapter-locs-as-var>>::
Explains the use of locations as variables.

<<lang-tut-data-chapter-stat-invariants>>::
Explains state (exclusion) invariants.

<<lang-tut-data-chapter-stat-evt-excl-invariants>>::
Explains state/event exclusion invariants.

[[virtual-toc-target--lang-tut-values]]
*Types and values*

<<lang-tut-values-chapter-types-values-exprs>>::
Explains the concepts of types, values, and expressions, as an introduction for the other lessons in this category.

<<lang-tut-values-chapter-overview>>::
Provides an overview of the available values, and divides them into categories.

<<lang-tut-values-chapter-integers>>::
Explains integer types, values, and commonly used expressions.

<<lang-tut-values-chapter-ranged-integers>>::
Explains ranged integers.

<<lang-tut-values-chapter-reals>>::
Explains real types, values, and commonly used expressions.

<<lang-tut-values-chapter-booleans>>::
Explains boolean types, values, and commonly used expressions.

<<lang-tut-values-chapter-strings>>::
Explains string types, values, and commonly used expressions.

<<lang-tut-values-chapter-enumerations>>::
Explains enumeration types, values, and commonly used expressions.

<<lang-tut-values-chapter-tuples>>::
Explains tuple types, values, and commonly used expressions.

<<lang-tut-values-chapter-lists>>::
Explains list types, values, and commonly used expressions.

<<lang-tut-values-chapter-bounded-lists-and-arrays>>::
Explains bounded lists, arrays, and their relations with regular lists.

<<lang-tut-values-chapter-sets>>::
Explains set types, values, and commonly used expressions.

<<lang-tut-values-chapter-dictionaries>>::
Explains dictionary types, values, and commonly used expressions.

<<lang-tut-values-chapter-combining-values>>::
Explains how to combine values of different types.

<<lang-tut-values-chapter-if-and-switch>>::
Explains `if` and `switch` expressions.

[[virtual-toc-target--lang-tut-reuse1]]
*Scalable solutions and reuse (1/2)*

<<lang-tut-reuse1-chapter-constants>>::
Explains the use of constants.

<<lang-tut-reuse1-chapter-algebraic-variables>>::
Explains the use of algebraic variables.

<<lang-tut-reuse1-chapter-algvar-equations>>::
Explains the use of equations to specify values of algebraic variables.

<<lang-tut-reuse1-chapter-type-declarations>>::
Explains the use of type declarations.

[[virtual-toc-target--lang-tut-time]]
*Time*

<<lang-tut-time-chapter-intro>>::
Introduces the concept of timing.

<<lang-tut-time-chapter-continuous-variables>>::
Explains the use of continuous variables.

<<lang-tut-time-chapter-contvar-equations>>::
Explains the use of equations to specify values of continuous variables.

<<lang-tut-time-chapter-equations>>::
Show the use of equations for both continuous and algebraic variables, by means of an example of a link:https://en.wikipedia.org/wiki/Nonlinear_system[non-linear system].

<<lang-tut-time-chapter-var-overview>>::
Provides an overview of the different kinds of variables in CIF, and their main differences.

<<lang-tut-time-chapter-urgency>>::
Explains the concept of urgency, as well as the different forms of urgency.

<<lang-tut-time-chapter-deadlock-livelock>>::
Explains the concepts of deadlock and livelock.

[[virtual-toc-target--lang-tut-channels]]
*Channel communication*

<<lang-tut-channels-chapter-intro>>::
Explains point-to-point channels and data communication.

<<lang-tut-channels-chapter-void>>::
Explains `void` channels that do not communicate any data.

<<lang-tut-channels-chapter-chan-sync-combi>>::
Explains how channel communication can be combined with event synchronization, further restricting the communication.

[[virtual-toc-target--lang-tut-functions]]
*Functions*

<<lang-tut-functions-chapter-intro>>::
Introduces functions, and explains the different kind of functions.

<<lang-tut-functions-chapter-internal-functions>>::
Explains internal user-defined functions.

<<lang-tut-functions-chapter-statements>>::
Explains the different statements that can be used in internal user-defined functions.

<<lang-tut-functions-chapter-functions-as-values>>::
Explains using functions as values, allowing functions to be passed around.

[[virtual-toc-target--lang-tut-reuse2]]
*Scalable solutions and reuse (2/2)*

<<lang-tut-reuse2-chapter-aut-def-inst>>::
Explains using automaton definition and instantiation for reuse.

<<lang-tut-reuse2-chapter-aut-def-params>>::
Explains parametrized automaton definitions.

<<lang-tut-reuse2-chapter-aut-def-param-kinds>>::
Explains the different kinds of parameters of automaton definitions.

<<lang-tut-reuse2-chapter-groups>>::
Explains hierarchical structuring using groups.

<<lang-tut-reuse2-chapter-group-defs>>::
Explains groups definitions and parametrized group definitions.

<<lang-tut-reuse2-chapter-imports>>::
Explains splitting CIF specifications over multiple files using imports.

<<lang-tut-reuse2-chapter-imports-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.

<<lang-tut-reuse2-chapter-imports-groups>>::
Explains how imports and groups interact.

<<lang-tut-reuse2-chapter-namespaces>>::
Explains namespaces, and how they can be used together with imports.

<<lang-tut-reuse2-chapter-input-variables>>::
Explains input variables, how they can be used for coupling with other models and systems, and their relation to imports.

[[virtual-toc-target--lang-tut-stochastics]]
*Stochastics*

<<lang-tut-stochastics-chapter-intro>>::
Introduction to stochastic distributions, which allow for sampling, making it possible to produce random values.

<<lang-tut-stochastics-chapter-discrete-continuous-constant>>::
Explains the different categories of stochastic distributions: discrete, continuous, and constant distributions.

<<lang-tut-stochastics-chapter-pseudo-randomness>>::
Explains how computers implement stochastics using pseudo-random number generators, and how this affects the use of stochastics in CIF.

[[virtual-toc-target--lang-tut-svg]]
*SVG visualization and interaction*

<<lang-tut-svg-chapter-visualization>>::
Introduction to SVG visualization, which allows to connect an image to a CIF model and update the image based on the state of the model.

<<lang-tut-svg-chapter-first-example>>::
A first simple example of SVG visualization.

<<lang-tut-svg-chapter-inkscape>>::
Explains how to use the Inkscape drawing program to edit SVG images.

<<lang-tut-svg-chapter-example-sun-moon>>::
An example of using groups of SVG objects, as well as controlling the visibility of objects based on the current locations of automata.

<<lang-tut-svg-chapter-example-walk>>::
An example of using groups of SVG objects, positioning them, and changing their position using an output mapping, as well as using the `scale` standard library function, text formatting, multiple values in an output mapping, and multiple format specifiers in a format pattern.

<<lang-tut-svg-chapter-example-rate>>::
An example of using literal values in output mappings, as well using simple solution to solve visualization problems.

<<lang-tut-svg-chapter-example-workstation>>::
An example of fixed-value and clock-based object widths, changing the fill color of objects, updating multiple attributes of an SVG object, specifying colors in SVG, and improving scalability by reusing mappings.

<<lang-tut-svg-chapter-example-tank>>::
An example of using the `scale` standard library function, as well as how inverting the y-axis can reduce the number of output mappings.

<<lang-tut-svg-chapter-example-lamps>>::
An example of hierarchical scalability of SVG images by reusing mappings, as well as copying elements and moving them to the desired position.

<<lang-tut-svg-chapter-example-buffers-products>>::
Another example of hierarchical scalability of SVG images by reusing mappings, as well as copying (copied) elements and moving them to the desired position.

<<lang-tut-svg-chapter-interaction>>::
Explains how to extend a model to couple it to an image for interaction via a visualization.

[[virtual-toc-target--lang-tut-text]]
*Text*

<<lang-tut-text-chapter-print>>::
Introduces print output by means of print declarations, which allows to print custom text from the model at runtime, either to the console or to a file.

<<lang-tut-text-chapter-print-examples>>::
Explains print output by means of examples.

<<lang-tut-text-chapter-fmt>>::
Explains text formatting by means of examples.

[[virtual-toc-target--lang-tut-synthesis]]
*Synthesis*

<<lang-tut-synthesis-intro>>::
Introduces supervisory controller synthesis.

<<lang-tut-synthesis-autkind>>::
Explains how to model automata with different automaton kinds.

<<lang-tut-synthesis-invkind>>::
Explains how to model invariants with different invariant kinds.

<<lang-tut-synthesis-evtctrl>>::
Explains the concept of event controllability and how to model events with different controllabilities.

<<lang-tut-synthesis-marked>>::
Explains the concept of marking and how to model marker predicates.

[[virtual-toc-target--lang-tut-annotations]]
*Annotations*

<<lang-tut-annotations>>::
Explains how to annotate elements of the specification with extra information.

<<lang-tut-annotations-controller>>::
Explains how certain tools can add properties of controllers to the specification.

<<lang-tut-annotations-documentation>>::
Explains how to add documentation to elements of a specification.

<<lang-tut-annotations-partial>>::
Explains how a specification can be labeled a 'partial' specification, making the type checker forego certain checks for it that often lead to false positive warnings on libraries.

<<lang-tut-annotations-reachability-requirement>>::
Explains how to add reachability requirements to a specification.

<<lang-tut-annotations-state>>::
Explains how certain tools that generate state spaces may annotate locations of a state space automaton with state information.
