blob: 5c6c5bb6be6ffbe2d09497ef929696d6b0ada92a [file] [log] [blame]
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="generator" content="Asciidoctor 2.0.12">
<meta name="author" content="Copyright (c) 2010, 2021 Contributors to the Eclipse Foundation">
<link rel="icon" type="image/png" href="favicon.png">
<title>CIF documentation (Incubation)</title>
<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700">
<style>
/* Asciidoctor default stylesheet | MIT License | https://asciidoctor.org */
/* Uncomment @import statement to use as custom stylesheet */
/*@import "https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700";*/
article,aside,details,figcaption,figure,footer,header,hgroup,main,nav,section{display:block}
audio,video{display:inline-block}
audio:not([controls]){display:none;height:0}
html{font-family:sans-serif;-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%}
a{background:none}
a:focus{outline:thin dotted}
a:active,a:hover{outline:0}
h1{font-size:2em;margin:.67em 0}
abbr[title]{border-bottom:1px dotted}
b,strong{font-weight:bold}
dfn{font-style:italic}
hr{-moz-box-sizing:content-box;box-sizing:content-box;height:0}
mark{background:#ff0;color:#000}
code,kbd,pre,samp{font-family:monospace;font-size:1em}
pre{white-space:pre-wrap}
q{quotes:"\201C" "\201D" "\2018" "\2019"}
small{font-size:80%}
sub,sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}
sup{top:-.5em}
sub{bottom:-.25em}
img{border:0}
svg:not(:root){overflow:hidden}
figure{margin:0}
fieldset{border:1px solid silver;margin:0 2px;padding:.35em .625em .75em}
legend{border:0;padding:0}
button,input,select,textarea{font-family:inherit;font-size:100%;margin:0}
button,input{line-height:normal}
button,select{text-transform:none}
button,html input[type="button"],input[type="reset"],input[type="submit"]{-webkit-appearance:button;cursor:pointer}
button[disabled],html input[disabled]{cursor:default}
input[type="checkbox"],input[type="radio"]{box-sizing:border-box;padding:0}
button::-moz-focus-inner,input::-moz-focus-inner{border:0;padding:0}
textarea{overflow:auto;vertical-align:top}
table{border-collapse:collapse;border-spacing:0}
*,*::before,*::after{-moz-box-sizing:border-box;-webkit-box-sizing:border-box;box-sizing:border-box}
html,body{font-size:100%}
body{background:#fff;color:rgba(0,0,0,.8);padding:0;margin:0;font-family:"Noto Serif","DejaVu Serif",serif;font-weight:400;font-style:normal;line-height:1;position:relative;cursor:auto;tab-size:4;word-wrap:anywhere;-moz-osx-font-smoothing:grayscale;-webkit-font-smoothing:antialiased}
a:hover{cursor:pointer}
img,object,embed{max-width:100%;height:auto}
object,embed{height:100%}
img{-ms-interpolation-mode:bicubic}
.left{float:left!important}
.right{float:right!important}
.text-left{text-align:left!important}
.text-right{text-align:right!important}
.text-center{text-align:center!important}
.text-justify{text-align:justify!important}
.hide{display:none}
img,object,svg{display:inline-block;vertical-align:middle}
textarea{height:auto;min-height:50px}
select{width:100%}
.subheader,.admonitionblock td.content>.title,.audioblock>.title,.exampleblock>.title,.imageblock>.title,.listingblock>.title,.literalblock>.title,.stemblock>.title,.openblock>.title,.paragraph>.title,.quoteblock>.title,table.tableblock>.title,.verseblock>.title,.videoblock>.title,.dlist>.title,.olist>.title,.ulist>.title,.qlist>.title,.hdlist>.title{line-height:1.45;color:#7a2518;font-weight:400;margin-top:0;margin-bottom:.25em}
div,dl,dt,dd,ul,ol,li,h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6,pre,form,p,blockquote,th,td{margin:0;padding:0}
a{color:#2156a5;text-decoration:underline;line-height:inherit}
a:hover,a:focus{color:#1d4b8f}
a img{border:0}
p{font-family:inherit;font-weight:400;font-size:1em;line-height:1.6;margin-bottom:1.25em;text-rendering:optimizeLegibility}
p aside{font-size:.875em;line-height:1.35;font-style:italic}
h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{font-family:"Open Sans","DejaVu Sans",sans-serif;font-weight:300;font-style:normal;color:#ba3925;text-rendering:optimizeLegibility;margin-top:1em;margin-bottom:.5em;line-height:1.0125em}
h1 small,h2 small,h3 small,#toctitle small,.sidebarblock>.content>.title small,h4 small,h5 small,h6 small{font-size:60%;color:#e99b8f;line-height:0}
h1{font-size:2.125em}
h2{font-size:1.6875em}
h3,#toctitle,.sidebarblock>.content>.title{font-size:1.375em}
h4,h5{font-size:1.125em}
h6{font-size:1em}
hr{border:solid #dddddf;border-width:1px 0 0;clear:both;margin:1.25em 0 1.1875em;height:0}
em,i{font-style:italic;line-height:inherit}
strong,b{font-weight:bold;line-height:inherit}
small{font-size:60%;line-height:inherit}
code{font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;font-weight:400;color:rgba(0,0,0,.9)}
ul,ol,dl{font-size:1em;line-height:1.6;margin-bottom:1.25em;list-style-position:outside;font-family:inherit}
ul,ol{margin-left:1.5em}
ul li ul,ul li ol{margin-left:1.25em;margin-bottom:0;font-size:1em}
ul.square li ul,ul.circle li ul,ul.disc li ul{list-style:inherit}
ul.square{list-style-type:square}
ul.circle{list-style-type:circle}
ul.disc{list-style-type:disc}
ol li ul,ol li ol{margin-left:1.25em;margin-bottom:0}
dl dt{margin-bottom:.3125em;font-weight:bold}
dl dd{margin-bottom:1.25em}
abbr,acronym{text-transform:uppercase;font-size:90%;color:rgba(0,0,0,.8);border-bottom:1px dotted #ddd;cursor:help}
abbr{text-transform:none}
blockquote{margin:0 0 1.25em;padding:.5625em 1.25em 0 1.1875em;border-left:1px solid #ddd}
blockquote cite{display:block;font-size:.9375em;color:rgba(0,0,0,.6)}
blockquote cite::before{content:"\2014 \0020"}
blockquote cite a,blockquote cite a:visited{color:rgba(0,0,0,.6)}
blockquote,blockquote p{line-height:1.6;color:rgba(0,0,0,.85)}
@media screen and (min-width:768px){h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{line-height:1.2}
h1{font-size:2.75em}
h2{font-size:2.3125em}
h3,#toctitle,.sidebarblock>.content>.title{font-size:1.6875em}
h4{font-size:1.4375em}}
table{background:#fff;margin-bottom:1.25em;border:solid 1px #dedede;word-wrap:normal}
table thead,table tfoot{background:#f7f8f7}
table thead tr th,table thead tr td,table tfoot tr th,table tfoot tr td{padding:.5em .625em .625em;font-size:inherit;color:rgba(0,0,0,.8);text-align:left}
table tr th,table tr td{padding:.5625em .625em;font-size:inherit;color:rgba(0,0,0,.8)}
table tr.even,table tr.alt{background:#f8f8f7}
table thead tr th,table tfoot tr th,table tbody tr td,table tr td,table tfoot tr td{line-height:1.6}
h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{line-height:1.2;word-spacing:-.05em}
h1 strong,h2 strong,h3 strong,#toctitle strong,.sidebarblock>.content>.title strong,h4 strong,h5 strong,h6 strong{font-weight:400}
.center{margin-left:auto;margin-right:auto}
.stretch{width:100%}
.clearfix::before,.clearfix::after,.float-group::before,.float-group::after{content:" ";display:table}
.clearfix::after,.float-group::after{clear:both}
:not(pre).nobreak{word-wrap:normal}
:not(pre).nowrap{white-space:nowrap}
:not(pre).pre-wrap{white-space:pre-wrap}
:not(pre):not([class^=L])>code{font-size:.9375em;font-style:normal!important;letter-spacing:0;padding:.1em .5ex;word-spacing:-.15em;background:#f7f7f8;-webkit-border-radius:4px;border-radius:4px;line-height:1.45;text-rendering:optimizeSpeed}
pre{color:rgba(0,0,0,.9);font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;line-height:1.45;text-rendering:optimizeSpeed}
pre code,pre pre{color:inherit;font-size:inherit;line-height:inherit}
pre>code{display:block}
pre.nowrap,pre.nowrap pre{white-space:pre;word-wrap:normal}
em em{font-style:normal}
strong strong{font-weight:400}
.keyseq{color:rgba(51,51,51,.8)}
kbd{font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;display:inline-block;color:rgba(0,0,0,.8);font-size:.65em;line-height:1.45;background:#f7f7f7;border:1px solid #ccc;-webkit-border-radius:3px;border-radius:3px;-webkit-box-shadow:0 1px 0 rgba(0,0,0,.2),0 0 0 .1em white inset;box-shadow:0 1px 0 rgba(0,0,0,.2),0 0 0 .1em #fff inset;margin:0 .15em;padding:.2em .5em;vertical-align:middle;position:relative;top:-.1em;white-space:nowrap}
.keyseq kbd:first-child{margin-left:0}
.keyseq kbd:last-child{margin-right:0}
.menuseq,.menuref{color:#000}
.menuseq b:not(.caret),.menuref{font-weight:inherit}
.menuseq{word-spacing:-.02em}
.menuseq b.caret{font-size:1.25em;line-height:.8}
.menuseq i.caret{font-weight:bold;text-align:center;width:.45em}
b.button::before,b.button::after{position:relative;top:-1px;font-weight:400}
b.button::before{content:"[";padding:0 3px 0 2px}
b.button::after{content:"]";padding:0 2px 0 3px}
p a>code:hover{color:rgba(0,0,0,.9)}
#header,#content,#footnotes,#footer{width:100%;margin-left:auto;margin-right:auto;margin-top:0;margin-bottom:0;max-width:62.5em;*zoom:1;position:relative;padding-left:.9375em;padding-right:.9375em}
#header::before,#header::after,#content::before,#content::after,#footnotes::before,#footnotes::after,#footer::before,#footer::after{content:" ";display:table}
#header::after,#content::after,#footnotes::after,#footer::after{clear:both}
#content{margin-top:1.25em}
#content::before{content:none}
#header>h1:first-child{color:rgba(0,0,0,.85);margin-top:2.25rem;margin-bottom:0}
#header>h1:first-child+#toc{margin-top:8px;border-top:1px solid #dddddf}
#header>h1:only-child,body.toc2 #header>h1:nth-last-child(2){border-bottom:1px solid #dddddf;padding-bottom:8px}
#header .details{border-bottom:1px solid #dddddf;line-height:1.45;padding-top:.25em;padding-bottom:.25em;padding-left:.25em;color:rgba(0,0,0,.6);display:-ms-flexbox;display:-webkit-flex;display:flex;-ms-flex-flow:row wrap;-webkit-flex-flow:row wrap;flex-flow:row wrap}
#header .details span:first-child{margin-left:-.125em}
#header .details span.email a{color:rgba(0,0,0,.85)}
#header .details br{display:none}
#header .details br+span::before{content:"\00a0\2013\00a0"}
#header .details br+span.author::before{content:"\00a0\22c5\00a0";color:rgba(0,0,0,.85)}
#header .details br+span#revremark::before{content:"\00a0|\00a0"}
#header #revnumber{text-transform:capitalize}
#header #revnumber::after{content:"\00a0"}
#content>h1:first-child:not([class]){color:rgba(0,0,0,.85);border-bottom:1px solid #dddddf;padding-bottom:8px;margin-top:0;padding-top:1rem;margin-bottom:1.25rem}
#toc{border-bottom:1px solid #e7e7e9;padding-bottom:.5em}
#toc>ul{margin-left:.125em}
#toc ul.sectlevel0>li>a{font-style:italic}
#toc ul.sectlevel0 ul.sectlevel1{margin:.5em 0}
#toc ul{font-family:"Open Sans","DejaVu Sans",sans-serif;list-style-type:none}
#toc li{line-height:1.3334;margin-top:.3334em}
#toc a{text-decoration:none}
#toc a:active{text-decoration:underline}
#toctitle{color:#7a2518;font-size:1.2em}
@media screen and (min-width:768px){#toctitle{font-size:1.375em}
body.toc2{padding-left:15em;padding-right:0}
#toc.toc2{margin-top:0!important;background:#f8f8f7;position:fixed;width:15em;left:0;top:0;border-right:1px solid #e7e7e9;border-top-width:0!important;border-bottom-width:0!important;z-index:1000;padding:1.25em 1em;height:100%;overflow:auto}
#toc.toc2 #toctitle{margin-top:0;margin-bottom:.8rem;font-size:1.2em}
#toc.toc2>ul{font-size:.9em;margin-bottom:0}
#toc.toc2 ul ul{margin-left:0;padding-left:1em}
#toc.toc2 ul.sectlevel0 ul.sectlevel1{padding-left:0;margin-top:.5em;margin-bottom:.5em}
body.toc2.toc-right{padding-left:0;padding-right:15em}
body.toc2.toc-right #toc.toc2{border-right-width:0;border-left:1px solid #e7e7e9;left:auto;right:0}}
@media screen and (min-width:1280px){body.toc2{padding-left:20em;padding-right:0}
#toc.toc2{width:20em}
#toc.toc2 #toctitle{font-size:1.375em}
#toc.toc2>ul{font-size:.95em}
#toc.toc2 ul ul{padding-left:1.25em}
body.toc2.toc-right{padding-left:0;padding-right:20em}}
#content #toc{border-style:solid;border-width:1px;border-color:#e0e0dc;margin-bottom:1.25em;padding:1.25em;background:#f8f8f7;-webkit-border-radius:4px;border-radius:4px}
#content #toc>:first-child{margin-top:0}
#content #toc>:last-child{margin-bottom:0}
#footer{max-width:none;background:rgba(0,0,0,.8);padding:1.25em}
#footer-text{color:rgba(255,255,255,.8);line-height:1.44}
#content{margin-bottom:.625em}
.sect1{padding-bottom:.625em}
@media screen and (min-width:768px){#content{margin-bottom:1.25em}
.sect1{padding-bottom:1.25em}}
.sect1:last-child{padding-bottom:0}
.sect1+.sect1{border-top:1px solid #e7e7e9}
#content h1>a.anchor,h2>a.anchor,h3>a.anchor,#toctitle>a.anchor,.sidebarblock>.content>.title>a.anchor,h4>a.anchor,h5>a.anchor,h6>a.anchor{position:absolute;z-index:1001;width:1.5ex;margin-left:-1.5ex;display:block;text-decoration:none!important;visibility:hidden;text-align:center;font-weight:400}
#content h1>a.anchor::before,h2>a.anchor::before,h3>a.anchor::before,#toctitle>a.anchor::before,.sidebarblock>.content>.title>a.anchor::before,h4>a.anchor::before,h5>a.anchor::before,h6>a.anchor::before{content:"\00A7";font-size:.85em;display:block;padding-top:.1em}
#content h1:hover>a.anchor,#content h1>a.anchor:hover,h2:hover>a.anchor,h2>a.anchor:hover,h3:hover>a.anchor,#toctitle:hover>a.anchor,.sidebarblock>.content>.title:hover>a.anchor,h3>a.anchor:hover,#toctitle>a.anchor:hover,.sidebarblock>.content>.title>a.anchor:hover,h4:hover>a.anchor,h4>a.anchor:hover,h5:hover>a.anchor,h5>a.anchor:hover,h6:hover>a.anchor,h6>a.anchor:hover{visibility:visible}
#content h1>a.link,h2>a.link,h3>a.link,#toctitle>a.link,.sidebarblock>.content>.title>a.link,h4>a.link,h5>a.link,h6>a.link{color:#ba3925;text-decoration:none}
#content h1>a.link:hover,h2>a.link:hover,h3>a.link:hover,#toctitle>a.link:hover,.sidebarblock>.content>.title>a.link:hover,h4>a.link:hover,h5>a.link:hover,h6>a.link:hover{color:#a53221}
details,.audioblock,.imageblock,.literalblock,.listingblock,.stemblock,.videoblock{margin-bottom:1.25em}
details>summary:first-of-type{cursor:pointer;display:list-item;outline:none;margin-bottom:.75em}
.admonitionblock td.content>.title,.audioblock>.title,.exampleblock>.title,.imageblock>.title,.listingblock>.title,.literalblock>.title,.stemblock>.title,.openblock>.title,.paragraph>.title,.quoteblock>.title,table.tableblock>.title,.verseblock>.title,.videoblock>.title,.dlist>.title,.olist>.title,.ulist>.title,.qlist>.title,.hdlist>.title{text-rendering:optimizeLegibility;text-align:left;font-family:"Noto Serif","DejaVu Serif",serif;font-size:1rem;font-style:italic}
table.tableblock.fit-content>caption.title{white-space:nowrap;width:0}
.paragraph.lead>p,#preamble>.sectionbody>[class="paragraph"]:first-of-type p{font-size:1.21875em;line-height:1.6;color:rgba(0,0,0,.85)}
table.tableblock #preamble>.sectionbody>[class="paragraph"]:first-of-type p{font-size:inherit}
.admonitionblock>table{border-collapse:separate;border:0;background:none;width:100%}
.admonitionblock>table td.icon{text-align:center;width:80px}
.admonitionblock>table td.icon img{max-width:none}
.admonitionblock>table td.icon .title{font-weight:bold;font-family:"Open Sans","DejaVu Sans",sans-serif;text-transform:uppercase}
.admonitionblock>table td.content{padding-left:1.125em;padding-right:1.25em;border-left:1px solid #dddddf;color:rgba(0,0,0,.6);word-wrap:anywhere}
.admonitionblock>table td.content>:last-child>:last-child{margin-bottom:0}
.exampleblock>.content{border-style:solid;border-width:1px;border-color:#e6e6e6;margin-bottom:1.25em;padding:1.25em;background:#fff;-webkit-border-radius:4px;border-radius:4px}
.exampleblock>.content>:first-child{margin-top:0}
.exampleblock>.content>:last-child{margin-bottom:0}
.sidebarblock{border-style:solid;border-width:1px;border-color:#dbdbd6;margin-bottom:1.25em;padding:1.25em;background:#f3f3f2;-webkit-border-radius:4px;border-radius:4px}
.sidebarblock>:first-child{margin-top:0}
.sidebarblock>:last-child{margin-bottom:0}
.sidebarblock>.content>.title{color:#7a2518;margin-top:0;text-align:center}
.exampleblock>.content>:last-child>:last-child,.exampleblock>.content .olist>ol>li:last-child>:last-child,.exampleblock>.content .ulist>ul>li:last-child>:last-child,.exampleblock>.content .qlist>ol>li:last-child>:last-child,.sidebarblock>.content>:last-child>:last-child,.sidebarblock>.content .olist>ol>li:last-child>:last-child,.sidebarblock>.content .ulist>ul>li:last-child>:last-child,.sidebarblock>.content .qlist>ol>li:last-child>:last-child{margin-bottom:0}
.literalblock pre,.listingblock>.content>pre{-webkit-border-radius:4px;border-radius:4px;overflow-x:auto;padding:1em;font-size:.8125em}
@media screen and (min-width:768px){.literalblock pre,.listingblock>.content>pre{font-size:.90625em}}
@media screen and (min-width:1280px){.literalblock pre,.listingblock>.content>pre{font-size:1em}}
.literalblock pre,.listingblock>.content>pre:not(.highlight),.listingblock>.content>pre[class="highlight"],.listingblock>.content>pre[class^="highlight "]{background:#f7f7f8}
.literalblock.output pre{color:#f7f7f8;background:rgba(0,0,0,.9)}
.listingblock>.content{position:relative}
.listingblock code[data-lang]::before{display:none;content:attr(data-lang);position:absolute;font-size:.75em;top:.425rem;right:.5rem;line-height:1;text-transform:uppercase;color:inherit;opacity:.5}
.listingblock:hover code[data-lang]::before{display:block}
.listingblock.terminal pre .command::before{content:attr(data-prompt);padding-right:.5em;color:inherit;opacity:.5}
.listingblock.terminal pre .command:not([data-prompt])::before{content:"$"}
.listingblock pre.highlightjs{padding:0}
.listingblock pre.highlightjs>code{padding:1em;-webkit-border-radius:4px;border-radius:4px}
.listingblock pre.prettyprint{border-width:0}
.prettyprint{background:#f7f7f8}
pre.prettyprint .linenums{line-height:1.45;margin-left:2em}
pre.prettyprint li{background:none;list-style-type:inherit;padding-left:0}
pre.prettyprint li code[data-lang]::before{opacity:1}
pre.prettyprint li:not(:first-child) code[data-lang]::before{display:none}
table.linenotable{border-collapse:separate;border:0;margin-bottom:0;background:none}
table.linenotable td[class]{color:inherit;vertical-align:top;padding:0;line-height:inherit;white-space:normal}
table.linenotable td.code{padding-left:.75em}
table.linenotable td.linenos{border-right:1px solid currentColor;opacity:.35;padding-right:.5em}
pre.pygments .lineno{border-right:1px solid currentColor;opacity:.35;display:inline-block;margin-right:.75em}
pre.pygments .lineno::before{content:"";margin-right:-.125em}
.quoteblock{margin:0 1em 1.25em 1.5em;display:table}
.quoteblock:not(.excerpt)>.title{margin-left:-1.5em;margin-bottom:.75em}
.quoteblock blockquote,.quoteblock p{color:rgba(0,0,0,.85);font-size:1.15rem;line-height:1.75;word-spacing:.1em;letter-spacing:0;font-style:italic;text-align:justify}
.quoteblock blockquote{margin:0;padding:0;border:0}
.quoteblock blockquote::before{content:"\201c";float:left;font-size:2.75em;font-weight:bold;line-height:.6em;margin-left:-.6em;color:#7a2518;text-shadow:0 1px 2px rgba(0,0,0,.1)}
.quoteblock blockquote>.paragraph:last-child p{margin-bottom:0}
.quoteblock .attribution{margin-top:.75em;margin-right:.5ex;text-align:right}
.verseblock{margin:0 1em 1.25em}
.verseblock pre{font-family:"Open Sans","DejaVu Sans",sans;font-size:1.15rem;color:rgba(0,0,0,.85);font-weight:300;text-rendering:optimizeLegibility}
.verseblock pre strong{font-weight:400}
.verseblock .attribution{margin-top:1.25rem;margin-left:.5ex}
.quoteblock .attribution,.verseblock .attribution{font-size:.9375em;line-height:1.45;font-style:italic}
.quoteblock .attribution br,.verseblock .attribution br{display:none}
.quoteblock .attribution cite,.verseblock .attribution cite{display:block;letter-spacing:-.025em;color:rgba(0,0,0,.6)}
.quoteblock.abstract blockquote::before,.quoteblock.excerpt blockquote::before,.quoteblock .quoteblock blockquote::before{display:none}
.quoteblock.abstract blockquote,.quoteblock.abstract p,.quoteblock.excerpt blockquote,.quoteblock.excerpt p,.quoteblock .quoteblock blockquote,.quoteblock .quoteblock p{line-height:1.6;word-spacing:0}
.quoteblock.abstract{margin:0 1em 1.25em;display:block}
.quoteblock.abstract>.title{margin:0 0 .375em;font-size:1.15em;text-align:center}
.quoteblock.excerpt>blockquote,.quoteblock .quoteblock{padding:0 0 .25em 1em;border-left:.25em solid #dddddf}
.quoteblock.excerpt,.quoteblock .quoteblock{margin-left:0}
.quoteblock.excerpt blockquote,.quoteblock.excerpt p,.quoteblock .quoteblock blockquote,.quoteblock .quoteblock p{color:inherit;font-size:1.0625rem}
.quoteblock.excerpt .attribution,.quoteblock .quoteblock .attribution{color:inherit;text-align:left;margin-right:0}
p.tableblock:last-child{margin-bottom:0}
td.tableblock>.content{margin-bottom:1.25em;word-wrap:anywhere}
td.tableblock>.content>:last-child{margin-bottom:-1.25em}
table.tableblock,th.tableblock,td.tableblock{border:0 solid #dedede}
table.grid-all>*>tr>*{border-width:1px}
table.grid-cols>*>tr>*{border-width:0 1px}
table.grid-rows>*>tr>*{border-width:1px 0}
table.frame-all{border-width:1px}
table.frame-ends{border-width:1px 0}
table.frame-sides{border-width:0 1px}
table.frame-none>colgroup+*>:first-child>*,table.frame-sides>colgroup+*>:first-child>*{border-top-width:0}
table.frame-none>:last-child>:last-child>*,table.frame-sides>:last-child>:last-child>*{border-bottom-width:0}
table.frame-none>*>tr>:first-child,table.frame-ends>*>tr>:first-child{border-left-width:0}
table.frame-none>*>tr>:last-child,table.frame-ends>*>tr>:last-child{border-right-width:0}
table.stripes-all tr,table.stripes-odd tr:nth-of-type(odd),table.stripes-even tr:nth-of-type(even),table.stripes-hover tr:hover{background:#f8f8f7}
th.halign-left,td.halign-left{text-align:left}
th.halign-right,td.halign-right{text-align:right}
th.halign-center,td.halign-center{text-align:center}
th.valign-top,td.valign-top{vertical-align:top}
th.valign-bottom,td.valign-bottom{vertical-align:bottom}
th.valign-middle,td.valign-middle{vertical-align:middle}
table thead th,table tfoot th{font-weight:bold}
tbody tr th{background:#f7f8f7}
tbody tr th,tbody tr th p,tfoot tr th,tfoot tr th p{color:rgba(0,0,0,.8);font-weight:bold}
p.tableblock>code:only-child{background:none;padding:0}
p.tableblock{font-size:1em}
ol{margin-left:1.75em}
ul li ol{margin-left:1.5em}
dl dd{margin-left:1.125em}
dl dd:last-child,dl dd:last-child>:last-child{margin-bottom:0}
ol>li p,ul>li p,ul dd,ol dd,.olist .olist,.ulist .ulist,.ulist .olist,.olist .ulist{margin-bottom:.625em}
ul.checklist,ul.none,ol.none,ul.no-bullet,ol.no-bullet,ol.unnumbered,ul.unstyled,ol.unstyled{list-style-type:none}
ul.no-bullet,ol.no-bullet,ol.unnumbered{margin-left:.625em}
ul.unstyled,ol.unstyled{margin-left:0}
ul.checklist{margin-left:.625em}
ul.checklist li>p:first-child>.fa-square-o:first-child,ul.checklist li>p:first-child>.fa-check-square-o:first-child{width:1.25em;font-size:.8em;position:relative;bottom:.125em}
ul.checklist li>p:first-child>input[type="checkbox"]:first-child{margin-right:.25em}
ul.inline{display:-ms-flexbox;display:-webkit-box;display:flex;-ms-flex-flow:row wrap;-webkit-flex-flow:row wrap;flex-flow:row wrap;list-style:none;margin:0 0 .625em -1.25em}
ul.inline>li{margin-left:1.25em}
.unstyled dl dt{font-weight:400;font-style:normal}
ol.arabic{list-style-type:decimal}
ol.decimal{list-style-type:decimal-leading-zero}
ol.loweralpha{list-style-type:lower-alpha}
ol.upperalpha{list-style-type:upper-alpha}
ol.lowerroman{list-style-type:lower-roman}
ol.upperroman{list-style-type:upper-roman}
ol.lowergreek{list-style-type:lower-greek}
.hdlist>table,.colist>table{border:0;background:none}
.hdlist>table>tbody>tr,.colist>table>tbody>tr{background:none}
td.hdlist1,td.hdlist2{vertical-align:top;padding:0 .625em}
td.hdlist1{font-weight:bold;padding-bottom:1.25em}
td.hdlist2{word-wrap:anywhere}
.literalblock+.colist,.listingblock+.colist{margin-top:-.5em}
.colist td:not([class]):first-child{padding:.4em .75em 0;line-height:1;vertical-align:top}
.colist td:not([class]):first-child img{max-width:none}
.colist td:not([class]):last-child{padding:.25em 0}
.thumb,.th{line-height:0;display:inline-block;border:solid 4px #fff;-webkit-box-shadow:0 0 0 1px #ddd;box-shadow:0 0 0 1px #ddd}
.imageblock.left{margin:.25em .625em 1.25em 0}
.imageblock.right{margin:.25em 0 1.25em .625em}
.imageblock>.title{margin-bottom:0}
.imageblock.thumb,.imageblock.th{border-width:6px}
.imageblock.thumb>.title,.imageblock.th>.title{padding:0 .125em}
.image.left,.image.right{margin-top:.25em;margin-bottom:.25em;display:inline-block;line-height:0}
.image.left{margin-right:.625em}
.image.right{margin-left:.625em}
a.image{text-decoration:none;display:inline-block}
a.image object{pointer-events:none}
sup.footnote,sup.footnoteref{font-size:.875em;position:static;vertical-align:super}
sup.footnote a,sup.footnoteref a{text-decoration:none}
sup.footnote a:active,sup.footnoteref a:active{text-decoration:underline}
#footnotes{padding-top:.75em;padding-bottom:.75em;margin-bottom:.625em}
#footnotes hr{width:20%;min-width:6.25em;margin:-.25em 0 .75em;border-width:1px 0 0}
#footnotes .footnote{padding:0 .375em 0 .225em;line-height:1.3334;font-size:.875em;margin-left:1.2em;margin-bottom:.2em}
#footnotes .footnote a:first-of-type{font-weight:bold;text-decoration:none;margin-left:-1.05em}
#footnotes .footnote:last-of-type{margin-bottom:0}
#content #footnotes{margin-top:-.625em;margin-bottom:0;padding:.75em 0}
.gist .file-data>table{border:0;background:#fff;width:100%;margin-bottom:0}
.gist .file-data>table td.line-data{width:99%}
div.unbreakable{page-break-inside:avoid}
.big{font-size:larger}
.small{font-size:smaller}
.underline{text-decoration:underline}
.overline{text-decoration:overline}
.line-through{text-decoration:line-through}
.aqua{color:#00bfbf}
.aqua-background{background:#00fafa}
.black{color:#000}
.black-background{background:#000}
.blue{color:#0000bf}
.blue-background{background:#0000fa}
.fuchsia{color:#bf00bf}
.fuchsia-background{background:#fa00fa}
.gray{color:#606060}
.gray-background{background:#7d7d7d}
.green{color:#006000}
.green-background{background:#007d00}
.lime{color:#00bf00}
.lime-background{background:#00fa00}
.maroon{color:#600000}
.maroon-background{background:#7d0000}
.navy{color:#000060}
.navy-background{background:#00007d}
.olive{color:#606000}
.olive-background{background:#7d7d00}
.purple{color:#600060}
.purple-background{background:#7d007d}
.red{color:#bf0000}
.red-background{background:#fa0000}
.silver{color:#909090}
.silver-background{background:#bcbcbc}
.teal{color:#006060}
.teal-background{background:#007d7d}
.white{color:#bfbfbf}
.white-background{background:#fafafa}
.yellow{color:#bfbf00}
.yellow-background{background:#fafa00}
span.icon>.fa{cursor:default}
a span.icon>.fa{cursor:inherit}
.admonitionblock td.icon [class^="fa icon-"]{font-size:2.5em;text-shadow:1px 1px 2px rgba(0,0,0,.5);cursor:default}
.admonitionblock td.icon .icon-note::before{content:"\f05a";color:#19407c}
.admonitionblock td.icon .icon-tip::before{content:"\f0eb";text-shadow:1px 1px 2px rgba(155,155,0,.8);color:#111}
.admonitionblock td.icon .icon-warning::before{content:"\f071";color:#bf6900}
.admonitionblock td.icon .icon-caution::before{content:"\f06d";color:#bf3400}
.admonitionblock td.icon .icon-important::before{content:"\f06a";color:#bf0000}
.conum[data-value]{display:inline-block;color:#fff!important;background:rgba(0,0,0,.8);-webkit-border-radius:50%;border-radius:50%;text-align:center;font-size:.75em;width:1.67em;height:1.67em;line-height:1.67em;font-family:"Open Sans","DejaVu Sans",sans-serif;font-style:normal;font-weight:bold}
.conum[data-value] *{color:#fff!important}
.conum[data-value]+b{display:none}
.conum[data-value]::after{content:attr(data-value)}
pre .conum[data-value]{position:relative;top:-.125em}
b.conum *{color:inherit!important}
.conum:not([data-value]):empty{display:none}
dt,th.tableblock,td.content,div.footnote{text-rendering:optimizeLegibility}
h1,h2,p,td.content,span.alt{letter-spacing:-.01em}
p strong,td.content strong,div.footnote strong{letter-spacing:-.005em}
p,blockquote,dt,td.content,span.alt{font-size:1.0625rem}
p{margin-bottom:1.25rem}
.sidebarblock p,.sidebarblock dt,.sidebarblock td.content,p.tableblock{font-size:1em}
.exampleblock>.content{background:#fffef7;border-color:#e0e0dc;-webkit-box-shadow:0 1px 4px #e0e0dc;box-shadow:0 1px 4px #e0e0dc}
.print-only{display:none!important}
@page{margin:1.25cm .75cm}
@media print{*{-webkit-box-shadow:none!important;box-shadow:none!important;text-shadow:none!important}
html{font-size:80%}
a{color:inherit!important;text-decoration:underline!important}
a.bare,a[href^="#"],a[href^="mailto:"]{text-decoration:none!important}
a[href^="http:"]:not(.bare)::after,a[href^="https:"]:not(.bare)::after{content:"(" attr(href) ")";display:inline-block;font-size:.875em;padding-left:.25em}
abbr[title]::after{content:" (" attr(title) ")"}
pre,blockquote,tr,img,object,svg{page-break-inside:avoid}
thead{display:table-header-group}
svg{max-width:100%}
p,blockquote,dt,td.content{font-size:1em;orphans:3;widows:3}
h2,h3,#toctitle,.sidebarblock>.content>.title{page-break-after:avoid}
#header,#content,#footnotes,#footer{max-width:none}
#toc,.sidebarblock,.exampleblock>.content{background:none!important}
#toc{border-bottom:1px solid #dddddf!important;padding-bottom:0!important}
body.book #header{text-align:center}
body.book #header>h1:first-child{border:0!important;margin:2.5em 0 1em}
body.book #header .details{border:0!important;display:block;padding:0!important}
body.book #header .details span:first-child{margin-left:0!important}
body.book #header .details br{display:block}
body.book #header .details br+span::before{content:none!important}
body.book #toc{border:0!important;text-align:left!important;padding:0!important;margin:0!important}
body.book #toc,body.book #preamble,body.book h1.sect0,body.book .sect1>h2{page-break-before:always}
.listingblock code[data-lang]::before{display:block}
#footer{padding:0 .9375em}
.hide-on-print{display:none!important}
.print-only{display:block!important}
.hide-for-print{display:none!important}
.show-for-print{display:inherit!important}}
@media print,amzn-kf8{#header>h1:first-child{margin-top:1.25rem}
.sect1{padding:0!important}
.sect1+.sect1{border:0}
#footer{background:none}
#footer-text{color:rgba(0,0,0,.6);font-size:.9em}}
@media amzn-kf8{#header,#content,#footnotes,#footer{padding:0}}
</style>
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/4.7.0/css/font-awesome.min.css">
<!--
Copyright (c) 2010, 2021 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
-->
<style>
.menu, .submenu, .menuitem, .menuref {
background-color: Menu;
}
.button {
border: 1px solid ButtonFace;
/*
Styling too similar to a real button is considered bad practice, see https://github.com/asciidoctor/asciidoctor/issues/1881#issuecomment-250702085
border: 2px outset ButtonFace;
background-color: ButtonFace;
*/
padding-left: 0.5ex;
padding-right: 0.5ex;
font-weight: normal;
font-family: "Segoe UI","Open Sans","DejaVu Sans",sans-serif;
white-space: nowrap;
}
.button:before {
content: none !important;
}
.button:after {
content: none !important;
}
#footer-text, #footer-text a {
color: rgba(255,255,255,.8)
}
</style>
</head>
<body class="book toc2 toc-left">
<div id="header">
<h1>CIF documentation (Incubation)</h1>
<div class="details">
<span id="author" class="author">Copyright (c) 2010, 2021 Contributors to the Eclipse Foundation</span><br>
<span id="revnumber">version 0.1.0.20210318-080652</span>
</div>
<div id="toc" class="toc2">
<div id="toctitle">Table of Contents</div>
<ul class="sectlevel1">
<li><a href="#introduction-chapter-index">Introduction</a></li>
<li><a href="#tut-chapter-index">Language tutorial</a>
<ul class="sectlevel2">
<li><a href="#tut-introduction">Introduction</a></li>
<li><a href="#tut-lessons">Lessons</a></li>
<li><a href="#tut-basics">Basics</a>
<ul class="sectlevel3">
<li><a href="#tut-basics-chapter-automata">Automata</a></li>
<li><a href="#tut-basics-chapter-synchronizing-events">Synchronizing events</a></li>
<li><a href="#tut-basics-chapter-non-determinism">Non-determinism</a></li>
<li><a href="#tut-basics-chapter-alphabet">Alphabet</a></li>
<li><a href="#tut-basics-chapter-event-placement">Event declaration placement</a></li>
<li><a href="#tut-basics-chapter-shorter-notations">Shorter notations</a></li>
</ul>
</li>
<li><a href="#tut-data">Data</a>
<ul class="sectlevel3">
<li><a href="#tut-data-chapter-discrete-variables">Discrete variables</a></li>
<li><a href="#tut-data-chapter-discvar-change">Discrete variable value changes</a></li>
<li><a href="#tut-data-chapter-loc-var-duality1">Location/variable duality (1/2)</a></li>
<li><a href="#tut-data-chapter-loc-var-duality2">Location/variable duality (2/2)</a></li>
<li><a href="#tut-data-chapter-read-write">Global read, local write</a></li>
<li><a href="#tut-data-chapter-monitoring">Monitoring</a></li>
<li><a href="#tut-data-chapter-asgn-old-vs-new">Old and new values in assignments</a></li>
<li><a href="#tut-data-chapter-tau-event">The <code>tau</code> event</a></li>
<li><a href="#tut-data-chapter-discvar-init">Initial values of discrete variables</a></li>
<li><a href="#tut-data-chapter-init-preds">Initialization predicates</a></li>
<li><a href="#tut-data-chapter-locs-as-var">Using locations as variables</a></li>
<li><a href="#tut-data-chapter-stat-invariants">State (exclusion) invariants</a></li>
<li><a href="#tut-data-chapter-stat-evt-excl-invariants">State/event exclusion invariants</a></li>
</ul>
</li>
<li><a href="#tut-types-and-values">Types and values</a>
<ul class="sectlevel3">
<li><a href="#tut-values-chapter-types-values-exprs">Types, values, and expressions</a></li>
<li><a href="#tut-values-chapter-overview">Values overview</a></li>
<li><a href="#tut-values-chapter-integers">Integers</a></li>
<li><a href="#tut-values-chapter-integer-ranges">Integer ranges</a></li>
<li><a href="#tut-values-chapter-reals">Reals</a></li>
<li><a href="#tut-values-chapter-booleans">Booleans</a></li>
<li><a href="#tut-values-chapter-strings">Strings</a></li>
<li><a href="#tut-values-chapter-enumerations">Enumerations</a></li>
<li><a href="#tut-values-chapter-tuples">Tuples</a></li>
<li><a href="#tut-values-chapter-lists">Lists</a></li>
<li><a href="#tut-values-chapter-bounded-lists-and-arrays">Bounded lists and arrays</a></li>
<li><a href="#tut-values-chapter-sets">Sets</a></li>
<li><a href="#tut-values-chapter-dictionaries">Dictionaries</a></li>
<li><a href="#tut-values-chapter-combining-values">Combining values</a></li>
</ul>
</li>
<li><a href="#tut-scalable-solutions-and-reuse-12">Scalable solutions and reuse (1/2)</a>
<ul class="sectlevel3">
<li><a href="#tut-reuse1-chapter-constants">Constants</a></li>
<li><a href="#tut-reuse1-chapter-algebraic-variables">Algebraic variables</a></li>
<li><a href="#tut-reuse1-chapter-algvar-equations">Algebraic variables and equations</a></li>
<li><a href="#tut-reuse1-chapter-type-declarations">Type declarations</a></li>
</ul>
</li>
<li><a href="#tut-time">Time</a>
<ul class="sectlevel3">
<li><a href="#tut-time-chapter-intro">Timing</a></li>
<li><a href="#tut-time-chapter-continuous-variables">Continuous variables</a></li>
<li><a href="#tut-time-chapter-contvar-equations">Continuous variables and equations</a></li>
<li><a href="#tut-time-chapter-equations">Equations</a></li>
<li><a href="#tut-time-chapter-var-overview">Variables overview</a></li>
<li><a href="#tut-time-chapter-urgency">Urgency</a></li>
<li><a href="#tut-time-chapter-deadlock-livelock">Deadlock and livelock</a></li>
</ul>
</li>
<li><a href="#tut-channel-communication">Channel communication</a>
<ul class="sectlevel3">
<li><a href="#tut-channels-chapter-intro">Channels</a></li>
<li><a href="#tut-channels-chapter-void">Dataless channels</a></li>
<li><a href="#tut-channels-chapter-chan-sync-combi">Combining channel communication with event synchronization</a></li>
</ul>
</li>
<li><a href="#tut-functions">Functions</a>
<ul class="sectlevel3">
<li><a href="#tut-functions-chapter-intro">Functions</a></li>
<li><a href="#tut-functions-chapter-internal-functions">Internal user-defined functions</a></li>
<li><a href="#tut-functions-chapter-statements">Function statements</a></li>
<li><a href="#tut-functions-chapter-functions-as-values">Functions as values</a></li>
</ul>
</li>
<li><a href="#tut-scalable-solutions-and-reuse-22">Scalable solutions and reuse (2/2)</a>
<ul class="sectlevel3">
<li><a href="#tut-reuse2-chapter-aut-def-inst">Automaton definition/instantiation</a></li>
<li><a href="#tut-reuse2-chapter-aut-def-params">Parametrized automaton definitions</a></li>
<li><a href="#tut-reuse2-chapter-aut-def-param-kinds">Automaton definition parameters</a></li>
<li><a href="#tut-reuse2-chapter-groups">Groups</a></li>
<li><a href="#tut-reuse2-chapter-group-defs">Group definitions</a></li>
<li><a href="#tut-reuse2-chapter-imports">Imports</a></li>
<li><a href="#tut-reuse2-chapter-imports-libraries">Imports and libraries</a></li>
<li><a href="#tut-reuse2-chapter-imports-groups">Imports and groups</a></li>
<li><a href="#tut-reuse2-chapter-namespaces">Namespaces</a></li>
<li><a href="#tut-reuse2-chapter-input-variables">Input variables</a></li>
</ul>
</li>
<li><a href="#tut-stochastics">Stochastics</a>
<ul class="sectlevel3">
<li><a href="#tut-stochastics-chapter-intro">Stochastics</a></li>
<li><a href="#tut-stochastics-chapter-discrete-continuous-constant">Discrete, continuous, and constant distributions</a></li>
<li><a href="#tut-stochastics-chapter-pseudo-randomness">Pseudo-randomness</a></li>
</ul>
</li>
<li><a href="#tut-language-extensions">Language extensions</a>
<ul class="sectlevel3">
<li><a href="#tut-extensions-chapter-synthesis">Supervisory controller synthesis</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#lang-ref-chapter-index">Language reference</a>
<ul class="sectlevel2">
<li><a href="#lang-ref-syntax-lexical">Lexical syntax</a>
<ul class="sectlevel3">
<li><a href="#lang-ref-keywords">Keywords</a></li>
<li><a href="#lang-ref-terminals">Terminals</a></li>
<li><a href="#lang-ref-whitespace">Whitespace</a></li>
<li><a href="#lang-ref-comments">Comments</a></li>
</ul>
</li>
<li><a href="#lang-ref-syntax-grammar">Grammar</a></li>
</ul>
</li>
<li><a href="#tools-chapter-index">Tools</a>
<ul class="sectlevel2">
<li><a href="#tools-specification-tools">Specification tools</a>
<ul class="sectlevel3">
<li><a href="#tools-chapter-text-editor">CIF text editor</a></li>
<li><a href="#tools-chapter-cif2yed">CIF to yEd transformer</a></li>
</ul>
</li>
<li><a href="#tools-supervisory-controller-synthesis-tools">Supervisory controller synthesis tools</a>
<ul class="sectlevel3">
<li><a href="#tools-chapter-datasynth">Data-based supervisory controller synthesis</a></li>
<li><a href="#tools-eventbased-chapter-index">Event-based synthesis toolset</a></li>
<li><a href="#tools-chapter-cif2supremica">CIF to Supremica transformer</a></li>
</ul>
</li>
<li><a href="#tools-simulation-validation-and-visualization-tools">Simulation, validation, and visualization tools</a>
<ul class="sectlevel3">
<li><a href="#tools-cifsim-chapter-index">CIF simulator</a></li>
<li><a href="#tools-simulation-basics">Simulation basics</a></li>
<li><a href="#tools-simulation-inputoutput">Simulation input/Output</a></li>
<li><a href="#tools-simulation-advanced-topics">Simulation advanced topics</a></li>
<li><a href="#tools-simulation-miscellaneous-topics">Simulation miscellaneous topics</a></li>
<li><a href="#tools-simulation-developer-topics">Simulation developer topics</a></li>
</ul>
</li>
<li><a href="#tools-verification-tools">Verification tools</a>
<ul class="sectlevel3">
<li><a href="#tools-chapter-cif2mcrl2">CIF to mCRL2 transformer</a></li>
<li><a href="#tools-chapter-cif2uppaal">CIF to UPPAAL transformer</a></li>
</ul>
</li>
<li><a href="#tools-real-time-testing-code-generation-and-implementation-tools">Real-time testing, code generation, and implementation tools</a>
<ul class="sectlevel3">
<li><a href="#tools-codegen-chapter-index">CIF code generator</a></li>
<li><a href="#tools-cif2plc-chapter-index">CIF PLC code generator</a></li>
</ul>
</li>
<li><a href="#tools-miscellaneous-tools">Miscellaneous tools</a>
<ul class="sectlevel3">
<li><a href="#tools-cif2cif-chapter-index">CIF to CIF transformer</a></li>
<li><a href="#tools-chapter-mergecif">CIF merger</a></li>
<li><a href="#tools-chapter-event-disabler">CIF event disabler</a></li>
<li><a href="#tools-chapter-cif-explorer">CIF explorer</a></li>
</ul>
</li>
<li><a href="#tools-scripting">Scripting</a>
<ul class="sectlevel3">
<li><a href="#tools-scripting-chapter-intro">Introduction to scripting</a></li>
<li><a href="#tools-scripting-chapter-tools">Overview of scriptable tools</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#examples-chapter-index">CIF examples</a></li>
<li><a href="#release-notes-chapter-index">CIF release notes</a>
<ul class="sectlevel2">
<li><a href="#version-0-1">Version 0.1</a></li>
</ul>
</li>
<li><a href="#dev-chapter-index">Developers</a>
<ul class="sectlevel2">
<li><a href="#dev-lang-modify">CIF language modification</a></li>
</ul>
</li>
<li><a href="#legal-chapter-index">Legal</a></li>
</ul>
</div>
</div>
<div id="content">
<div id="preamble">
<div class="sectionbody">
<div class="paragraph">
<p>CIF is a declarative modeling language for the specification of discrete
event, timed, and hybrid systems as a collection of synchronizing automata.
The CIF tooling supports the entire development process of controllers,
including among others specification, supervisory controller synthesis,
simulation-based validation and visualization, verification, real-time
testing, and code generation.</p>
</div>
<div class="paragraph">
<p>CIF is one of the tools of the Eclipse ESCET&#8482; project. Visit the
<a href="https://eclipse.org/escet">project website</a> for downloads,
installation instructions, source code, general tool usage information,
information on how to contribute, and more.</p>
</div>
<div class="admonitionblock warning">
<table>
<tr>
<td class="icon">
<i class="fa icon-warning" title="Warning"></i>
</td>
<td class="content">
<div class="paragraph">
<p>The Eclipse ESCET project, including the CIF language and toolset,
is currently in the
<a href="https://wiki.eclipse.org/Development_Resources/Process_Guidelines/What_is_Incubation">Incubation Phase</a>.</p>
</div>
<div class="paragraph">
<p><span class="image"><img src="./eclipse-incubation.png" alt="eclipse incubation" width="300"></span></p>
</div>
</td>
</tr>
</table>
</div>
<div class="admonitionblock tip">
<table>
<tr>
<td class="icon">
<i class="fa icon-tip" title="Tip"></i>
</td>
<td class="content">
You can <a href="eclipse-escet-incubation-cif-manual.pdf">download this manual</a>
as a PDF as well.
</td>
</tr>
</table>
</div>
<div class="paragraph">
<p>The documentation consists of:</p>
</div>
<div class="ulist">
<ul>
<li>
<p><a href="#introduction-chapter-index">CIF introduction</a></p>
</li>
<li>
<p><a href="#tut-chapter-index">CIF language tutorial</a></p>
</li>
<li>
<p><a href="#lang-ref-chapter-index">CIF language reference manual</a></p>
</li>
<li>
<p><a href="#tools-chapter-index">CIF tool manual</a></p>
</li>
<li>
<p><a href="#examples-chapter-index">CIF examples</a></p>
</li>
<li>
<p><a href="#release-notes-chapter-index">CIF release notes</a></p>
</li>
<li>
<p><a href="#dev-chapter-index">CIF developers manual</a></p>
</li>
<li>
<p><a href="#legal-chapter-index">Legal information</a></p>
</li>
</ul>
</div>
<div class="paragraph">
<p>A screenshot of the CIF tooling IDE:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./screenshot_ide.png" alt="screenshot ide">
</div>
</div>
</div>
</div>
<div class="sect1">
<h2 id="introduction-chapter-index">Introduction</h2>
<div class="sectionbody">
<div class="paragraph">
<p>The CIF language is a powerful declarative automata-based modeling language
for the specification of discrete event, timed (linear dynamics), hybrid
(piecewise continuous dynamics) systems. It can be seen as a rich state
machine language with the following main features:</p>
</div>
<div class="ulist">
<ul>
<li>
<p>Modular specification with synchronized events and communication between
automata.</p>
</li>
<li>
<p>Many data types are available (booleans, integers, reals, tuples, lists,
arrays, sets, and dictionaries), combined with a powerful expression language
for compact variables updates.</p>
</li>
<li>
<p>Text-based specification of the automata, with many features to simplify
modeling large non-trivial industrial systems.</p>
</li>
<li>
<p>Primitives for supervisory controller synthesis are integrated in the
language.</p>
</li>
</ul>
</div>
<div class="paragraph">
<p>The CIF tooling supports the entire development process of controllers,
including among others specification, supervisory controller synthesis,
simulation-based validation and visualization, verification, real-time
testing, and code generation. Highlights of the CIF tooling include:</p>
</div>
<div class="ulist">
<ul>
<li>
<p>Text-based editor that allows to easily specify and edit models.</p>
</li>
<li>
<p>Feature-rich powerful data-based synthesis tool. A transformation to the
supervisory controller synthesis tool Supremica is also available.</p>
</li>
<li>
<p>A simulator that supports both interactive and automated validation of
specifications. Powerful visualization features allow for interactive
visualization-based validation.</p>
</li>
<li>
<p>Conversion to formal verification tools such as mCRL2 and UPPAAL.</p>
</li>
<li>
<p>Implementation language code generation (PLC languages, Java, C, and
Simulink) for real-time testing and implementation of the designed controller.</p>
</li>
</ul>
</div>
<div class="paragraph">
<p></p>
</div>
</div>
</div>
<div class="sect1">
<h2 id="tut-chapter-index">Language tutorial</h2>
<div class="sectionbody">
<div class="paragraph">
<p>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.</p>
</div>
<div class="sect2">
<h3 id="tut-introduction">Introduction</h3>
<div class="paragraph">
<p>CIF stands for <strong>C</strong>ompositional <strong>I</strong>nterchange <strong>F</strong>ormat 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.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div class="paragraph">
<p>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.</p>
</div>
<div class="paragraph">
<p>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.</p>
</div>
</div>
<div class="sect2">
<h3 id="tut-lessons">Lessons</h3>
<div class="paragraph">
<p>Several lessons are available, grouped into the following categories:</p>
</div>
<div class="ulist">
<ul>
<li>
<p><a href="#lang-tut-basics">Basics</a></p>
</li>
<li>
<p><a href="#lang-tut-data">Data</a></p>
</li>
<li>
<p><a href="#lang-tut-values">Types and values</a></p>
</li>
<li>
<p><a href="#lang-tut-reuse1">Scalable solutions and reuse (1/2)</a></p>
</li>
<li>
<p><a href="#lang-tut-time">Time</a></p>
</li>
<li>
<p><a href="#lang-tut-channels">Channel communication</a></p>
</li>
<li>
<p><a href="#lang-tut-functions">Functions</a></p>
</li>
<li>
<p><a href="#lang-tut-reuse2">Scalable solutions and reuse (2/2)</a></p>
</li>
<li>
<p><a href="#lang-tut-stochastics">Stochastics</a></p>
</li>
<li>
<p><a href="#lang-tut-extensions">Language extensions</a></p>
</li>
</ul>
</div>
<div class="paragraph">
<p>The lessons introduce new concepts, one by one, and are meant to be read in
the given order.</p>
</div>
<div id="lang-tut-basics" class="paragraph">
<p><strong>Basics</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-basics-chapter-automata">Automata</a></dt>
<dd>
<p>Explains automata, locations, events, edges, transitions, and more.</p>
</dd>
<dt class="hdlist1"><a href="#tut-basics-chapter-synchronizing-events">Synchronizing events</a></dt>
<dd>
<p>Explains event synchronization, enabledness, traces, and state spaces.</p>
</dd>
<dt class="hdlist1"><a href="#tut-basics-chapter-non-determinism">Non-determinism</a></dt>
<dd>
<p>Explains multiple causes of non-determinism.</p>
</dd>
<dt class="hdlist1"><a href="#tut-basics-chapter-alphabet">Alphabet</a></dt>
<dd>
<p>Explains alphabets for both individual automata and entire specifications.</p>
</dd>
<dt class="hdlist1"><a href="#tut-basics-chapter-event-placement">Event declaration placement</a></dt>
<dd>
<p>Explains the placement of event declarations.</p>
</dd>
<dt class="hdlist1"><a href="#tut-basics-chapter-shorter-notations">Shorter notations</a></dt>
<dd>
<p>Explains several shorter notations, including self loops, declaring
multiple events with a single declaration, multiple events on an edge, and
nameless locations.</p>
</dd>
</dl>
</div>
<div id="lang-tut-data" class="paragraph">
<p><strong>Data</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-data-chapter-discrete-variables">Discrete variables</a></dt>
<dd>
<p>Explains discrete variables, guards, and updates.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-discvar-change">Discrete variable value changes</a></dt>
<dd>
<p>Explains how and when discrete variables can change value.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-loc-var-duality1">Location/variable duality (1/2)</a></dt>
<dd>
<p>Explains the duality between locations and variables using a model of a
counter.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-loc-var-duality2">Location/variable duality (2/2)</a></dt>
<dd>
<p>Explains the duality between locations and variables using a model of a
lamp.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-read-write">Global read, local write</a></dt>
<dd>
<p>Explains the concepts of global read and local write.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-monitoring">Monitoring</a></dt>
<dd>
<p>Explains monitoring, self loops, and monitor automata.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-asgn-old-vs-new">Old and new values in assignments</a></dt>
<dd>
<p>Explains old and new values of variables in assignments, multiple
assignments, and the order of assignments.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-tau-event">The <code>tau</code> event</a></dt>
<dd>
<p>Explains the <code>tau</code> event.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-discvar-init">Initial values of discrete variables</a></dt>
<dd>
<p>Explains initialization of discrete variables, including the use of default
values and multiple potential initial values.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-init-preds">Initialization predicates</a></dt>
<dd>
<p>Explains initialization in general, and initialization predicates in
particular.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-locs-as-var">Using locations as variables</a></dt>
<dd>
<p>Explains the use of locations as variables.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-stat-invariants">State (exclusion) invariants</a></dt>
<dd>
<p>Explains state (exclusion) invariants.</p>
</dd>
<dt class="hdlist1"><a href="#tut-data-chapter-stat-evt-excl-invariants">State/event exclusion invariants</a></dt>
<dd>
<p>Explains state/event exclusion invariants.</p>
</dd>
</dl>
</div>
<div id="lang-tut-values" class="paragraph">
<p><strong>Types and values</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-values-chapter-types-values-exprs">Types, values, and expressions</a></dt>
<dd>
<p>Explains the concepts of types, values, and expressions, as an introduction
for the other lessons in this category.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-overview">Values overview</a></dt>
<dd>
<p>Provides an overview of the available values, and divides them into
categories.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-integers">Integers</a></dt>
<dd>
<p>Explains integer types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-integer-ranges">Integer ranges</a></dt>
<dd>
<p>Explains integer ranges.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-reals">Reals</a></dt>
<dd>
<p>Explains real types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-booleans">Booleans</a></dt>
<dd>
<p>Explains boolean types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-strings">Strings</a></dt>
<dd>
<p>Explains string types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-enumerations">Enumerations</a></dt>
<dd>
<p>Explains enumeration types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-tuples">Tuples</a></dt>
<dd>
<p>Explains tuple types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-lists">Lists</a></dt>
<dd>
<p>Explains list types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-bounded-lists-and-arrays">Bounded lists and arrays</a></dt>
<dd>
<p>Explains bounded lists, arrays, and their relations with regular lists.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-sets">Sets</a></dt>
<dd>
<p>Explains set types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-dictionaries">Dictionaries</a></dt>
<dd>
<p>Explains dictionary types, values, and commonly used expressions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-values-chapter-combining-values">Combining values</a></dt>
<dd>
<p>Explains how to combine values of different types.</p>
</dd>
</dl>
</div>
<div id="lang-tut-reuse1" class="paragraph">
<p><strong>Scalable solutions and reuse (1/2)</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-reuse1-chapter-constants">Constants</a></dt>
<dd>
<p>Explains the use of constants.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse1-chapter-algebraic-variables">Algebraic variables</a></dt>
<dd>
<p>Explains the use of algebraic variables.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse1-chapter-algvar-equations">Algebraic variables and equations</a></dt>
<dd>
<p>Explains the use of equations to specify values of algebraic variables.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse1-chapter-type-declarations">Type declarations</a></dt>
<dd>
<p>Explains the use of type declarations.</p>
</dd>
</dl>
</div>
<div id="lang-tut-time" class="paragraph">
<p><strong>Time</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-time-chapter-intro">Timing</a></dt>
<dd>
<p>Introduces the concept of timing.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-continuous-variables">Continuous variables</a></dt>
<dd>
<p>Explains the use of continuous variables.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-contvar-equations">Continuous variables and equations</a></dt>
<dd>
<p>Explains the use of equations to specify values of continuous variables.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-equations">Equations</a></dt>
<dd>
<p>Show the use of equations for both continuous and algebraic variables, by
means of an example of a
<a href="http://en.wikipedia.org/wiki/Nonlinear_system&gt;">non-linear system</a>.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-var-overview">Variables overview</a></dt>
<dd>
<p>Provides an overview of the different kinds of variables in CIF, and their
main differences.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-urgency">Urgency</a></dt>
<dd>
<p>Explains the concept of urgency, as well as the different forms of urgency.</p>
</dd>
<dt class="hdlist1"><a href="#tut-time-chapter-deadlock-livelock">Deadlock and livelock</a></dt>
<dd>
<p>Explains the concepts of deadlock and livelock.</p>
</dd>
</dl>
</div>
<div id="lang-tut-channels" class="paragraph">
<p><strong>Channel communication</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-channels-chapter-intro">Channels</a></dt>
<dd>
<p>Explains point-to-point channels and data communication.</p>
</dd>
<dt class="hdlist1"><a href="#tut-channels-chapter-void">Dataless channels</a></dt>
<dd>
<p>Explains <code>void</code> channels that do not communicate any data.</p>
</dd>
<dt class="hdlist1"><a href="#tut-channels-chapter-chan-sync-combi">Combining channel communication with event synchronization</a></dt>
<dd>
<p>Explains how channel communication can be combined with event
synchronization, further restricting the communication.</p>
</dd>
</dl>
</div>
<div id="lang-tut-functions" class="paragraph">
<p><strong>Functions</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-functions-chapter-intro">Functions</a></dt>
<dd>
<p>Introduces functions, and explains the different kind of functions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-functions-chapter-internal-functions">Internal user-defined functions</a></dt>
<dd>
<p>Explains internal user-defined functions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-functions-chapter-statements">Function statements</a></dt>
<dd>
<p>Explains the different statements that can be used in internal user-defined
functions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-functions-chapter-functions-as-values">Functions as values</a></dt>
<dd>
<p>Explains using functions as values, allowing functions to be passed around.</p>
</dd>
</dl>
</div>
<div id="lang-tut-reuse2" class="paragraph">
<p><strong>Scalable solutions and reuse (2/2)</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-aut-def-inst">Automaton definition/instantiation</a></dt>
<dd>
<p>Explains using automaton definition and instantiation for reuse.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-aut-def-params">Parametrized automaton definitions</a></dt>
<dd>
<p>Explains parametrized automaton definitions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-aut-def-param-kinds">Automaton definition parameters</a></dt>
<dd>
<p>Explains the different kinds of parameters of automaton definitions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-groups">Groups</a></dt>
<dd>
<p>Explains hierarchical structuring using groups.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-group-defs">Group definitions</a></dt>
<dd>
<p>Explains groups definitions and parametrized group definitions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-imports">Imports</a></dt>
<dd>
<p>Explains splitting CIF specifications over multiple files using imports.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-imports-libraries">Imports and libraries</a></dt>
<dd>
<p>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.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-imports-groups">Imports and groups</a></dt>
<dd>
<p>Explains how imports and groups interact.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-namespaces">Namespaces</a></dt>
<dd>
<p>Explains namespaces, and how they can be used together with imports.</p>
</dd>
<dt class="hdlist1"><a href="#tut-reuse2-chapter-input-variables">Input variables</a></dt>
<dd>
<p>Explains input variables, how they can be used for coupling with other
models and systems, and their relation to imports.</p>
</dd>
</dl>
</div>
<div id="lang-tut-stochastics" class="paragraph">
<p><strong>Stochastics</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-stochastics-chapter-intro">Stochastics</a></dt>
<dd>
<p>Introduction to stochastic distributions, which allow for sampling, making
it possible to produce random values.</p>
</dd>
<dt class="hdlist1"><a href="#tut-stochastics-chapter-discrete-continuous-constant">Discrete, continuous, and constant distributions</a></dt>
<dd>
<p>Explains the different categories of stochastic distributions: discrete,
continuous, and constant distributions.</p>
</dd>
<dt class="hdlist1"><a href="#tut-stochastics-chapter-pseudo-randomness">Pseudo-randomness</a></dt>
<dd>
<p>Explains how computers implement stochastics using pseudo-random number
generators, and how this affects the use of stochastics in CIF.</p>
</dd>
</dl>
</div>
<div id="lang-tut-extensions" class="paragraph">
<p><strong>Language extensions</strong></p>
</div>
<div class="dlist">
<dl>
<dt class="hdlist1"><a href="#tut-extensions-chapter-synthesis">Supervisory controller synthesis</a></dt>
<dd>
<p>Explains how to extend a model to make it suitable for supervisory
controller synthesis.</p>
</dd>
<dt class="hdlist1"><a href="#tools-cifsim-output-print-chapter-index">Print output</a></dt>
<dd>
<p>Explains how to extend a model to include printing of textual output.</p>
<div class="paragraph">
<p>This documentation is currently not part of the language tutorial,
but of the simulator tool documentation.</p>
</div>
</dd>
<dt class="hdlist1"><a href="#tools-cifsim-output-svgviz-chapter-index">SVG visualization</a></dt>
<dd>
<p>Explains how to extend a model to couple it to an image for visualization.</p>
<div class="paragraph">
<p>This documentation is currently not part of the language tutorial,
but of the simulator tool documentation.</p>
</div>
</dd>
<dt class="hdlist1"><a href="#tools-cifsim-input-svg-chapter-index">SVG interaction</a></dt>
<dd>
<p>Explains how to extend a model to couple it to an image for interaction via
a visualization.</p>
<div class="paragraph">
<p>This documentation is currently not part of the language tutorial,
but of the simulator tool documentation.</p>
</div>
</dd>
</dl>
</div>
</div>
<div class="sect2">
<h3 id="tut-basics">Basics</h3>
<div class="sect3">
<h4 id="tut-basics-chapter-automata">Automata</h4>
<div class="paragraph">
<p>
</p>
</div>
<div class="paragraph">
<p>CIF models consist of <em>components</em>. Each of the components represents the
behavior of a part of the system. Components can be modeled as <em>automata</em>,
which form the basis of CIF. The following CIF <em>specification</em>, or CIF <em>model</em>,
shows a simple automaton:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton lamp:
event turn_on, turn_off;
location on:
initial;
edge turn_off goto off;
location off:
edge turn_on goto on;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The automaton is named <code>lamp</code>, and not surprisingly represents the (discrete)
behavior of a lamp.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div id="lang-tut-basics-automata-events" class="paragraph">
<p>Automaton <code>lamp</code> declares two <em>events</em>, named <code>turn_on</code> and <code>turn_off</code>.
Events model things that can happen in a system. They represent changes. For
instance, the <code>turn_on</code> event indicates that the lamp is being turned on. It
represents the change from the lamp being off to the lamp being on. The event
declaration in the <code>lamp</code> automaton declares two events. The event
declaration only indicates that these events exist, it does not yet indicate
when they can happen, and what the result of them happening is.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div id="lang-tut-basics-automata-location" class="paragraph">
<p>All automata have one or more <em>locations</em>, which represent the mutually
exclusive <em>states</em> of the automaton. The <code>lamp</code> automaton has two
<em>locations</em>, named <code>on</code> and <code>off</code>. Automata have an <em>active</em> or <em>current</em>
location. That is, for every automaton one of its location is the active
location, and the automaton is said to be <em>in</em> that location. For instance,
the <code>lamp</code> automaton is either in its <code>on</code> location, or in its <code>off</code>
location.</p>
</div>
<div class="paragraph">
<p></p>
</div>
<div id="lang-tut-basics-automata-loc-init" class="paragraph">
<p>Initially, the lamp is on, as indicated by the <code>initial</code> keyword in the
<code>on</code> location. That is, the <code>on</code> location is the initial location of the
<code>lamp</code> automaton. The initial location is the active location of the
automaton, at the start of the system.</p>
</div>
<div class="paragraph">
<p></p>
</div>
<div id="lang-tut-basics-edge" class="paragraph">
<p>In each location, an automaton can have different behavior, specified using
<em>edges</em>. An edge indicates how an automaton can change its state, by going from
one location to another. Edges can be associated with events, that indicate
what happened, and thus what caused the state change.</p>
</div>
<div class="paragraph">
<p>The <code>lamp</code> automaton has an edge with the <code>turn_off</code> event, in its <code>on</code>
location, going to the <code>off</code> location. Whenever the lamp is on, the <code>lamp</code>
automaton is in its <code>on</code> location. Whenever the lamp is turned off, the
<code>turn_off</code> event happens. The edge with that event indicates what the
result of that event is, for the <code>on</code> location. In this case the result is
that the lamp will then be off, which is why the edge goes to the <code>off</code>
location.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div id="lang-tut-basics-trans" class="paragraph">
<p>The <code>lamp</code> automaton can go from one location to another, as described by its
edges. This is referred to as 'performing a transition', 'taking a transition',
or 'taking an edge'. The <code>lamp</code> automaton can keep performing <em>transitions</em>.
The lamp can be turned on, off, on again, off again, etc. This can go on
forever.</p>
</div>
</div>
<div class="sect3">
<h4 id="tut-basics-chapter-synchronizing-events">Synchronizing events</h4>
<div class="paragraph">
<p>
The power of events is that they synchronize. To illustrate this, consider
the following CIF specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton producer:
event produce, provide;
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The automaton represents a producer that produces products, to be consumed
by a consumer. The <code>producer</code> automaton starts in its <code>producing</code> location,
in which it produces a product. Once the product has been produced, indicated
by the <code>produce</code> event, the automaton will be in its <code>idle</code> location, where
it waits until it can <code>provide</code> the produced product to the consumer. Once it
has provided the product to the consumer, it will once again be <code>producing</code>
another product. Consider also the following continuation of the above
specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton consumer:
event consume;
location idle:
initial;
edge producer.provide goto consuming;
location consuming:
edge consume goto idle;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This second automaton represents a consumer that consumes products. The
<code>consumer</code> is initially <code>idle</code>, waiting for a product from the producer.
Once the producer has provided a product, the consumer will be <code>consuming</code>.
Once it has consumed the product, as indicated by the occurrence of the
<code>consume</code> event, it will become <code>idle</code> again.</p>
</div>
<div class="paragraph">
<p>The specification has three events, the <code>produce</code> and <code>provide</code> events
declared in the <code>producer</code> automaton, and the <code>consume</code> event declared in
the <code>consumer</code> automaton. The <code>consumer</code> automaton, in its <code>idle</code>
location, has an edge that refers to the <code>provide</code> event declared in the
<code>producer</code> automaton. As such, that edge and the edge in the <code>idle</code>
location of the <code>producer</code> automaton, refer to the same event.</p>
</div>
<div class="paragraph">
<p></p>
</div>
<div class="sect4">
<h5 id="tut-synchronization">Synchronization</h5>
<div class="paragraph">
<p>Events that are used in multiple automata, must <em>synchronize</em>. That is, if
one of those automata performs a transition for that event, the other automata
must also participate by performing a transition for that same event. If one
of the automata that uses the event can not perform a transition in its current
location, none of the automata can perform a transition for that event.</p>
</div>
<div class="paragraph">
<p>Now, lets take a closer look at the behavior of the producer/consumer example.
Initially, the <code>producer</code> automaton is in its <code>producing</code> location, and the
<code>consumer</code> automaton is in its <code>idle</code> location. Since the <code>producer</code> is
the only automaton that uses the <code>produce</code> event, and there is an (outgoing)
edge in its current location for that <code>produce</code> event, the <code>producer</code> can
go to its <code>idle</code> location by means of that event.</p>
</div>
<div class="paragraph">
<p>Both the <code>producer</code> and <code>consumer</code> use the <code>provide</code> event. The
<code>producer</code> has no edge with that event in its <code>producing</code> location, while
the <code>consumer</code> does have an edge for that event in its <code>idle</code> location.
Since events must synchronize, and the <code>producer</code> can not participate, the
event can not occur at this time. This is what we expect, as the <code>producer</code>
has not yet produced a product, and can thus not yet <code>provide</code> it to the
consumer. The <code>consumer</code> will have to remain <code>idle</code> until the <code>producer</code>
has produced a product and is ready to <code>provide</code> it to the <code>consumer</code>.</p>
</div>
<div class="paragraph">
<p>
The <code>producer</code> blocks the <code>provide</code> event in this case, and is said to
<em>disable</em> the event. The event is not blocked by the <code>consumer</code>, and is thus
said to be <em>enabled</em> in the <code>consumer</code> automaton. In the entire
specification, the event is <em>disabled</em> as well, as it is disabled by at least
one of the automata of the specification, and all automata must enable the
event for it to become enabled in the specification.</p>
</div>
<div class="paragraph">
<p>The only behavior that is possible, is for the <code>producer</code> to <code>produce</code> a
product, and go to its <code>idle</code> location. The <code>consumer</code> does not participate
and remains in its <code>idle</code> location. Both automata are then in their <code>idle</code>
location, and both have an edge that enables the <code>provide</code> event. As such,
the <code>provide</code> event is enabled in the specification. As this is the only
possible behavior, a transition for the <code>provide</code> event is performed. This
results in the <code>producer</code> going back to its <code>producing</code> location, while at
the same time the <code>consumer</code> goes to its <code>consuming</code> location.</p>
</div>
<div class="paragraph">
<p>In its <code>producing</code> location, the <code>producer</code> can <code>produce</code> a product.
Furthermore, in its <code>consuming</code> location, the <code>consumer</code> can <code>consume</code> a
product. Two transitions are possible, and CIF does not define which one will
be performed. That is, either one can be performed. No assumptions should be
made either way. In other words, both transitions represent valid behavior, as
described by this specification. Since only one transition can be taken at a
time, there are two possibilities. Either the <code>producer</code> starts to
<code>produce</code> the product first, and the <code>consumer</code> starts to <code>consume</code> after
that, or the other way around.</p>
</div>
</div>
<div class="sect4">
<h5 id="tut-traces-and-state-spaces">Traces and state spaces</h5>
<div class="paragraph">
<p>Once both transitions have been taken, we are essentially in the same situation
as we were after the <code>producer</code> produced a product the first time, as both
automata will be in their <code>idle</code> locations again. The behavior of the
specification then continues to repeat forever. However, for each repetition
different choices in the order of production and consumption can be made.</p>
</div>
<div class="paragraph">
<p>
During a single <em>execution</em> or <em>simulation</em>, choices are made each time that
multiple transitions are possible. The sequence of transitions that are taken
is called a <em>trace</em>. Examples of traces for the producer/consumer example are:</p>
</div>
<div class="ulist">
<ul>
<li>
<p><code>produce</code>
<code>provide</code>
<code>produce</code>
<code>consume</code>
<code>provide</code>
<code>produce</code>
<code>consume</code>
&#8230;&#8203;</p>
</li>
<li>
<p><code>produce</code>
<code>provide</code>
<code>produce</code>
<code>consume</code>
<code>provide</code>
<code>consume</code>
<code>produce</code>
&#8230;&#8203;</p>
</li>
<li>
<p><code>produce</code>
<code>provide</code>
<code>consume</code>
<code>produce</code>
<code>provide</code>
<code>produce</code>
<code>consume</code>
&#8230;&#8203;</p>
</li>
<li>
<p><code>produce</code>
<code>provide</code>
<code>consume</code>
<code>produce</code>
<code>provide</code>
<code>consume</code>
<code>produce</code>
&#8230;&#8203;</p>
</li>
</ul>
</div>
<div class="paragraph">
<p>The traces end with <code>...</code> to indicate that they are partial traces, that go
beyond the part of the trace that is shown. These four traces however, cover
all the possibilities for the first seven transitions.</p>
</div>
<div class="paragraph">
<p>
All possible traces together form the <em>state space</em>, which represents all the
possible behavior of a system. For the producer/consumer example, the state
space is:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./tutorial/basics/producer_consumer_state_space_finite.png" alt="producer consumer state space finite">
</div>
</div>
<div class="paragraph">
<p>Here the circles represent the states of the specification, which are a
combination of the states of the two automata. The labels of the circles
indicate the state, as a combination of the first letters of the locations of
the automata. The initial state is labeled <code>p/i</code>, as initially automaton
<code>producer</code> is in its <code>producing</code> (p) location, and the <code>consumer</code> is in
its <code>idle</code> (i) location. The arrows indicate the transitions, and are labeled
with events. The state space clearly shows the choices, as multiple outgoing
arrows for a single state. It also makes it clear that as we move to the right,
and make choices, we can make different choices for different products.
Since the behavior keeps repeating itself, the state space ends with <code>...</code>
to indicate that only a part of the state space is shown.</p>
</div>
<div class="paragraph">
<p>However, we can also show the entire behavior of the specification. Essential
here is that the state space shown above has duplicate states. That is, several
states have the same label, and allow for the same future behavior. By reusing
states, a finite representation of the state space can be made, which shows the
entire possible infinite behavior of the producer/consumer specification:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./tutorial/basics/producer_consumer_state_space_infinite.png" alt="producer consumer state space infinite">
</div>
</div>
</div>
<div class="sect4">
<h5 id="tut-concluding-remarks">Concluding remarks</h5>
<div class="paragraph">
<p>By using multiple automata, the producer and consumer were modeled
independently, allowing for separation of concerns. This is an important
concept, especially when modeling larger systems. In general, the large system
is decomposed into parts, usually corresponding to physical entities. Each of
the parts of the system can then be modeled in isolation, with little regard
for the other parts.</p>
</div>
<div class="paragraph">
<p>By using synchronizing events, the different automata that model different
parts of a system, can interact. This allows for modeling of the connection
between the different parts of the system, ensuring that together they
represent the behavior of the entire system.</p>
</div>
</div>
</div>
<div class="sect3">
<h4 id="tut-basics-chapter-non-determinism">Non-determinism</h4>
<div class="paragraph">
<p>
Depending on the context in which it is used, non-determinism can mean
different things. One definition is having multiple possible traces through the
state space of a system. Another definition is having multiple possible
transitions for a certain event, for a certain state. Different communities
also use different definitions, and some communities only use one of the
definitions, and use a different name to refer to the other concept.</p>
</div>
<div class="sect4">
<h5 id="tut-non-determinism-between-events">Non-determinism between events</h5>
<div class="paragraph">
<p>One cause of non-determinism is that multiple events are enabled, leading to
multiple possible transitions. In other words, there are multiple possible
traces through the state space. During the lesson on
<a href="#tut-basics-chapter-synchronizing-events">synchronizing events</a>, we already
encountered this form of non-determinism, as transitions for the <code>produce</code> and
<code>consume</code> events could be performed in arbitrary order.</p>
</div>
</div>
<div class="sect4">
<h5 id="tut-non-determinism-for-single-event">Non-determinism for single event</h5>
<div class="paragraph">
<p>Another cause of non-determinism is the presence of multiple outgoing edges of
a single location for the same event. This can lead to multiple possible
transitions for a that event, for a single state. For instance, consider the
following CIF specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton coin:
event toss, land, pick_up;
location hand:
initial;
edge toss goto air;
location air:
edge land goto ground;
location ground:
edge pick_up goto hand;
end
automaton outcome:
location unknown:
initial;
edge coin.land goto heads; // First way to land.
edge coin.land goto tails; // Second way to land.
location heads:
edge pick_up goto unknown;
location tails:
edge pick_up goto unknown;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The <code>coin</code> automaton represents a single coin. Initially, it is in the
<code>hand</code> of a person. That person can <code>toss</code> the coin up into the <code>air</code>,
eventually causing it to fall and <code>land</code> on the <code>ground</code>. It can be picked
up (event <code>pick_up</code>), causing it to once again be in the <code>hand</code> of a
person.</p>
</div>
<div class="paragraph">
<p>The <code>outcome</code> automaton registers the outcome of the
<a href="http://en.wikipedia.org/wiki/Coin_toss">coin toss</a>. Initially,
the outcome is <code>unknown</code>. Whenever the coin is tossed, it lands (event
<code>land</code> from automaton <code>coin</code>) on the ground with either the <code>heads</code> or
<code>tails</code> side up. The <code>unknown</code> location of the <code>outcome</code> automaton has
two edges for the same event. This leads to two possible transitions, one to
the <code>heads</code> location, and one to the <code>tails</code> location. This is a
non-deterministic choice, as the model does not specify which transition is
chosen, or even which choice is more likely.</p>
</div>
<div class="paragraph">
<p>In both the <code>heads</code> and <code>tails</code> locations, the coin can be picked up again,
making the outcome <code>unknown</code>. The coin can be tossed again and again,
repeating the behavior forever. The following figure shows the state space of
this specification:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./tutorial/basics/coin_toss_state_space.png" alt="coin toss state space">
</div>
</div>
<div class="paragraph">
<p>The states are labeled with the first letters of the current locations of the
two automata.</p>
</div>
</div>
</div>
<div class="sect3">
<h4 id="tut-basics-chapter-alphabet">Alphabet</h4>
<div class="paragraph">
<p>
</p>
</div>
<div class="paragraph">
<p>The lesson on <a href="#tut-basics-chapter-synchronizing-events">synchronizing events</a>
described how events that are used in multiple automata exhibit synchronizing
behavior. That is, if the event is used in multiple automata, they must all
enable that event in order for a transition to be possible. If one of them can
not perform the event, the event is disabled, and none of the automata can
perform a transition for that event.</p>
</div>
<div class="paragraph">
<p>Whether an automaton participates in the synchronization for a certain event,
is determined by its <em>alphabet</em>. The alphabet of an automaton is the collection
of events over which it synchronizes.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div class="sect4">
<h5 id="tut-default-and-implicit-alphabets">Default and implicit alphabets</h5>
<div class="paragraph">
<p>By default, the alphabet of an automaton implicitly contains all the events
that occur on the edges of the automaton. For instance, consider the following
CIF specification (the producer/consumer example from the lesson on
<a href="#tut-basics-chapter-synchronizing-events">synchronizing events</a>):</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton producer:
event produce, provide;
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end
automaton consumer:
event consume;
location idle:
initial;
edge producer.provide goto consuming;
location consuming:
edge consume goto idle;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The alphabet of the <code>producer</code> automaton contains the events <code>produce</code> and
<code>provide</code>, as both occur on edges of that automaton. The alphabet of the
<code>consumer</code> automaton contains the events <code>producer.produce</code> and
<code>consume</code>.</p>
</div>
<div class="paragraph">
<p></p>
</div>
</div>
<div class="sect4">
<h5 id="lang-tut-basics-alphabet-explicit">Explicit alphabet</h5>
<div class="paragraph">
<p>It is possible to explicitly specify the alphabet of an automaton, as follows:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">event provide;
automaton producer:
event produce;
alphabet produce, provide; // Alphabet explicitly specified.
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The <code>alphabet</code> keyword is followed by the events that comprise the alphabet
of the automaton, separated by commas. In this case, the alphabet contains
the <code>produce</code> and <code>provide</code> events. Since this explicitly specified
alphabet is exactly the same as the default alphabet, it could just as easily
be omitted.</p>
</div>
<div class="paragraph">
<p></p>
</div>
</div>
<div class="sect4">
<h5 id="tut-non-default-alphabet">Non-default alphabet</h5>
<div class="paragraph">
<p>The alphabet is allowed to be empty, which can be explicitly specified as
follows:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">alphabet; // Empty alphabet. Automaton doesn't synchronize over any events.</code></pre>
</div>
</div>
<div class="paragraph">
<p>
However, the alphabet of an automaton must at least contain the events that
occur on the edges of an automaton. That is, it must at least contain the
default alphabet.</p>
</div>
<div class="paragraph">
<p>
It may however also contain additional events. Since there are no edges for
those additional events, the automaton can never enable those events, and
thus always disables them. If a single automaton disables an event, and since
it must always participate if it has that event in its alphabet, this means
that the event becomes globally disabled in the entire specification. Having
such additional events in the alphabet leads to a warning, to inform about the
potential undesired effects of globally disabling events in this manner.</p>
</div>
<div class="paragraph">
<p></p>
</div>
</div>
<div class="sect4">
<h5 id="tut-implicit-vs-explicit">Implicit vs explicit</h5>
<div class="paragraph">
<p>It should be clear that for most automata, the implicit default alphabet
suffices. There are however reasons for explicitly specifying the default
alphabet. For large automata, it can improve the readability, as the explicit
alphabet makes it easy to determine the alphabet of the automaton, without
having to look at all the edges.</p>
</div>
<div class="paragraph">
<p>The need to explicitly specifying a non-default alphabet rarely occurs.
However, several <a href="#tools-chapter-index">tools</a> generate CIF specifications with
explicit alphabets.</p>
</div>
</div>
</div>
<div class="sect3">
<h4 id="tut-basics-chapter-event-placement">Event declaration placement</h4>
<div class="paragraph">
<p>
Consider the following CIF specification (the producer/consumer example from
the lesson on <a href="#tut-basics-chapter-synchronizing-events">synchronizing events</a>):</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton producer:
event produce, provide;
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end
automaton consumer:
event consume;
location idle:
initial;
edge producer.provide goto consuming;
location consuming:
edge consume goto idle;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The specification could also be specified as follows:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton producer:
event produce, provide, consume; // Declaration of event 'consume' moved.
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end
automaton consumer:
location idle:
initial;
edge producer.provide goto consuming;
location consuming:
edge producer.consume goto idle; // Event 'consume' from 'producer'.
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The <code>consume</code> event is now declared in the <code>producer</code> automaton rather than
the <code>consumer</code> automaton, but the locations and edges have not changed. This
modified specification exhibits the same behavior as the original.</p>
</div>
<div class="paragraph">
<p>It should be clear that while events can be declared in various places, it is
best to declare them where they belong. That is, the <code>consume</code> event is only
used by the <code>consumer</code> automaton, and is thus best declared in that
automaton. Similarly, the <code>produce</code> event is only used by the <code>producer</code>
automaton.</p>
</div>
<div class="paragraph">
<p>The <code>provide</code> event however is used by both automata. In such cases the event
is usually declared where it is initiated. In the example above, the producer
provides the product to the consumer, and not the other way around. Therefore,
the <code>provide</code> event is declared in the <code>producer</code> automaton, rather than in
the <code>consumer</code> automaton.</p>
</div>
<div class="paragraph">
<p>However, the modeler is free to choose the best place to declare the event. If
no choice can be made between the automata, the event can also be declared
outside the automata, as follows:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">event provide; // Event 'provide' now declared outside the automata.
automaton producer:
event produce;
location producing:
initial;
edge produce goto idle;
location idle:
edge provide goto producing;
end
automaton consumer:
event consume;
location idle:
initial;
edge provide goto consuming; // Can directly refer to 'provide' event.
location consuming:
edge consume goto idle;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This specification also has the same behavior. Only the placement of the event
declarations has changed.</p>
</div>
<div class="paragraph">
<p>The place where an event is declared is of no influence to the
implicit (default) <a href="#tut-basics-chapter-alphabet">alphabets</a> of the
automata. The implicit alphabet of an automaton is determined solely based on
the events that occur on the edges of that automaton.</p>
</div>
</div>
<div class="sect3">
<h4 id="tut-basics-chapter-shorter-notations">Shorter notations</h4>
<div class="paragraph">
<p>This lessons explains several short notations, that can be used for easier
modeling, can reduce the size of the specification, and make specifications
easier to read. The following topics are discussed:</p>
</div>
<div class="ulist">
<ul>
<li>
<p><a href="#lang-tut-basics-shorter-notations-self-loop">Self loop</a></p>
</li>
<li>
<p><a href="#lang-tut-basics-shorter-notations-evt-decl-mult">Declaring multiple events with a single declaration</a></p>
</li>
<li>
<p><a href="#lang-tut-basics-shorter-notations-edge-mult-evt">Multiple events on an edge</a></p>
</li>
<li>
<p><a href="#lang-tut-basics-shorter-notations-loc-nameless">Nameless location</a></p>
</li>
</ul>
</div>
<div class="paragraph">
<p>
</p>
</div>
<div class="sect4">
<h5 id="lang-tut-basics-shorter-notations-self-loop">Self loop</h5>
<div class="paragraph">
<p>A self loop is an edge that goes to the location from which it originated.
Consider the following example:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton a:
event e;
location x:
edge e goto x;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The edge in location <code>x</code> of automaton <code>a</code> goes to location <code>x</code>. The
effect of the <code>e</code> event is that automaton <code>a</code> remains in its <code>x</code>
location. A self loop can be used to allow a certain event, essentially
ignoring it for that location.</p>
</div>
<div class="paragraph">
<p>The following short notation can be used for self loops:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton a:
event e;
location x:
edge e; // Goto omitted for self loop.
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The <code>goto</code> part of the edge can be omitted for self loop. This can help make
the model easier to read, as the resulting location does not have to be checked
against the source location of the edge, to see whether they match.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
</div>
<div class="sect4">
<h5 id="lang-tut-basics-shorter-notations-evt-decl-mult">Declaring multiple events with a single declaration</h5>
<div class="paragraph">
<p>Several of the previous lessons already showed that multiple events can be
declared using a single event declaration:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">event a, b, c; // Single declaration declares multiple events.</code></pre>
</div>
</div>
<div class="paragraph">
<p>This is equivalent to using multiple event declarations that each declare a
single event:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">event a; // Multiple declarations each declare a single event.
event b;
event c;</code></pre>
</div>
</div>
<div class="paragraph">
<p>Using a single declaration to declare multiple events can help reduce the
length of a specification.</p>
</div>
<div class="paragraph">
<p>
</p>
</div>
</div>
<div class="sect4">
<h5 id="lang-tut-basics-shorter-notations-edge-mult-evt">Multiple events on an edge</h5>
<div class="paragraph">
<p>Consider the following CIF specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton a:
event e, f;
location loc:
edge e goto loc; // Two edges that only differ in the event.
edge f goto loc;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This can also be written more compactly, as follows:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton a:
event e, f;
location loc:
edge e, f goto loc; // Edge with two events.
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>An edge with two or more events means exactly the same as having individual
edges for the different events. That is, a choice is made between them. It does
<em>not</em> specify that event <code>f</code> can only happen after event <code>e</code> has already
happened. Both automata thus have the exact same behavior.</p>
</div>
<div class="paragraph">
<p></p>
</div>
</div>
<div class="sect4">
<h5 id="lang-tut-basics-shorter-notations-loc-nameless">Nameless location</h5>
<div class="paragraph">
<p>Several of the examples above show automata with a single location. For such
automata, the name of the location is optional:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton a:
event e;
location:
edge e;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>Since the location has no name, there is no way to refer to it in a <code>goto</code>,
and thus only self loop edges can be used. Leaving out the name prevents having
to come up with a dummy name, which can clutter the specification.</p>
</div>
</div>
</div>
</div>
<div class="sect2">
<h3 id="tut-data">Data</h3>
<div class="sect3">
<h4 id="tut-data-chapter-discrete-variables">Discrete variables</h4>
<div class="paragraph">
<p>This lesson introduces discrete variables. Consider the following
specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton counter:
event increment, decrement;
disc int count = 3;
location:
edge decrement when count &gt; 0 do count := count - 1;
edge increment when count &lt; 5 do count := count + 1;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>
The <code>counter</code> automaton can be used to count certain things. The
<code>increment</code> and <code>decrement</code> events are used to change the count. The count
itself is stored in a variable named <code>count</code>. CIF has several different types
of variables. Here, we use a discrete variable, as indicated by the <code>disc</code>
keyword. The variable has an <code>int</code> data type, meaning it can have integer
numbers as its value. It is initialized to value <code>3</code>.</p>
</div>
<div class="paragraph">
<p>
The automaton has two edges, one for the <code>increment</code> event, and one for the
<code>decrement</code> event. The edge for the <code>decrement</code> event has a <em>guard</em> that
indicates under which circumstances the event can take place. The condition is
indicated using the <code>when</code> keyword. In this case, the guard ensures that the
count can only be decremented if it is currently positive. The guard of the
edge for the <code>increment</code> event indicates that the count can only be
incremented as long as it is less than five. In general, a guard must hold in
the source location of the edge, for the edge to be enabled, and a transition
to be possible. If the guard is not specified, it defaults to <code>true</code>, which
always holds and does not restrict the edge in any way.</p>
</div>
<div class="paragraph">
<p>
Both edges also have <em>updates</em>, indicated using the <code>do</code> keyword. Updates can
be used to specify the effect of the transition on variables. In this case, the
updates <em>assign</em> a new value to the <code>count</code> variable that is one less or one
more than the current value. That is the value of the <code>count</code> variable is
decremented or incremented by one.</p>
</div>
<div class="paragraph">
<p>This specification represents a counter that can be repeatedly incremented and
decremented by one, and ensures that the value of variable <code>count</code> is always
at least zero and at most five.</p>
</div>
<div class="paragraph">
<p>The state space of the <code>counter</code> automaton is as follows:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./tutorial/data/counter_state_space.png" alt="counter state space">
</div>
</div>
</div>
<div class="sect3">
<h4 id="tut-data-chapter-discvar-change">Discrete variable value changes</h4>
<div class="paragraph">
<p>
Discrete variables can only change value by explicitly assigning them a new
value in the <code>do</code> part of an edge. If an edge does not assign a value to a
discrete variable, that variable keeps its current value. Consider the
following CIF specification:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton lamp:
event turn_on, turn_off;
disc int count = 0;
location off:
initial;
edge turn_on do count := count + 1 goto on;
location on:
edge turn_off goto off;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This is the same <code>lamp</code> automaton as used in the lesson on
<a href="#tut-basics-chapter-automata">automata</a>, but with a <code>count</code> variable added. This
variable is used to count the number of times that the lamp has been turned on.
The edge for the <code>turn_on</code> event increments the value of the variable by one,
each time the lamp is turned on.</p>
</div>
<div class="paragraph">
<p>The edge for the <code>turn_off</code> event does not assign a value to a variable, so
variable <code>count</code> keeps its value when the lamp is turned off.</p>
</div>
<div class="paragraph">
<p>The state space of this specification is:</p>
</div>
<div class="imageblock">
<div class="content">
<img src="./tutorial/data/discvar_change_state_space.png" alt="discvar change state space">
</div>
</div>
<div class="paragraph">
<p>The states are labeled with the name of the current location of automaton
<code>lamp</code> and the current value of variable <code>count</code>.</p>
</div>
</div>
<div class="sect3">
<h4 id="tut-data-chapter-loc-var-duality1">Location/variable duality (1/2)</h4>
<div class="paragraph">
<p>
The lesson that
<a href="#tut-data-chapter-discrete-variables">introduces discrete variables</a>, uses
an example of a counter. The actual count was modeled using a variable:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton counter:
event increment, decrement;
disc int count = 3;
location:
edge decrement when count &gt; 0 do count := count - 1;
edge increment when count &lt; 5 do count := count + 1;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>It is also possible to use multiple locations instead of a variable:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton counter:
event increment, decrement;
location zero:
edge increment goto one;
location one:
edge decrement goto zero;
edge increment goto two;
location two:
edge decrement goto one;
edge increment goto three;
location three:
initial;
edge decrement goto two;
edge increment goto four;
location four:
edge decrement goto three;
edge increment goto five;
location five:
edge decrement goto four;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This alternate model has the same behavior, in that it models a counter that
can be incremented an decremented in steps of one, and the value is kept at
least zero, and at most five. The variant with the variable however, is shorter
and more intuitive. It is also easier to change to the <code>count &lt; 5</code> guard to
<code>count &lt; 100</code> than it is to add dozens of additional locations and edges. In
this case, using a variable is preferable to using multiple locations.</p>
</div>
</div>
<div class="sect3">
<h4 id="tut-data-chapter-loc-var-duality2">Location/variable duality (2/2)</h4>
<div class="paragraph">
<p>
The lesson that <a href="#tut-basics-chapter-automata">introduces automata</a>, used an
example of a lamp:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton lamp:
event turn_on, turn_off;
location on:
initial;
edge turn_off goto off;
location off:
edge turn_on goto on;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>The automaton uses two locations to keep track of the current state of the
lamp. Instead of two locations, it is also possible to use a variable:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="highlight"><code class="language-cif" data-lang="cif">automaton lamp:
event turn_on, turn_off;
disc bool on = true;
location:
initial;
edge turn_on when not on do on := true;
edge turn_off when on do on := false;
end</code></pre>
</div>
</div>
<div class="paragraph">
<p>This alternate automaton uses a single variable named <code>on</code>. The
<a href="#tut-values-chapter-types-values-exprs">data type</a> of the variable is
<code>bool</code>, which means that the variable can only have one of two possible
values: <code>true</code> or <code>false</code>. If variable <code>on</code> has value <code>true</code>, the lamp
is on, and if it has value <code>false</code> it is off. Initially, the lamp is on, as
the initial value of the variable is <code>true</code>. The automaton has only one
location, with two edges. The first edge indicates that the lamp can be turned
on (event <code>turn_on</code>), only when it is not currently on (guard <code>not on</code>),
and then afterwards is on (variable <code>on</code> becomes <code>true</code>). Similarly, the
second edge indicates that the lamp can be turned off, only when it is
currently on, and then afterwards is on.</p>
</div>