Synthesizing Functional Reactive Programs

TL;DR

This paper presents a method to synthesize executable functional reactive programs from Temporal Stream Logic specifications, enabling automatic generation of reactive code across software and hardware platforms.

Contribution

It introduces a novel approach to transform Control Flow Models derived from TSL into FRP code, bridging the gap between formal specifications and practical implementations.

Findings

Successful translation of CFMs into FRP code for desktop, web, and hardware applications.

Demonstrated applicability on a real-world kitchen timer example.

Effective integration with existing FRP libraries like Yampa, threepenny-gui, and ClaSH.

Abstract

Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), as synthesized from TSL specifications, can be turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are indeed a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic threepenny-gui library, and to hardware using the Applicative hardware description language ClaSH.

Figures

Tables

Table 1. Table 1 . Synthesis and compilation times for creating the different timer applications from the TSL specification.

Process	Time (sec)
Synthesis $\to$ strix	4.965
Compilation
Desktop $\to$ Yampa	19.403
Web $\to$ threepenny-gui	18.344
Hardware
$\to$ ClaSH	11.218
$\to$ yosys	6.405
$\to$ nextpnr	7.276

Equations

$$\begin{array}[]{l}\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\big{(}\,\text{(}{\text{{event}}}~{}{\text{{click}}}\ \leftrightarrow\ \llbracket\hskip 1.0pt{\text{{count}}}\leftarrowtail\,{\text{{increment}}}~{}{\text{{count}}}\hskip 1.0pt\rrbracket\text{)}\\ \qquad\wedge\ \llbracket\hskip 1.0pt{\text{{screen}}}\leftarrowtail\,{\text{{display}}}~{}{\text{{count}}}\hskip 1.0pt\rrbracket\,\big{)}\end{array}$$

$$Signal\ a::\mbox{$\mathcal{T}\scalebox{0.8}{$\boldsymbol{i}\boldsymbol{m}\boldsymbol{e}$}$}\rightarrow a$$

$$SFInputOutput::SignalInput\to SignalOutput$$

$$\begin{array}[]{rl}\tau_{F}\ \;:=&{\text{{s}}}_{{\text{{i}}}}\quad|\quad{\text{{f}}}~{}\;\tau_{F}^{0}~{}\;\tau_{F}^{1}~{}\;\cdots~{}\;\tau_{F}^{n-1}\\[3.00003pt] \tau_{P}\ \;:=&{\text{{p}}}~{}\;\tau_{F}^{0}~{}\;\tau_{F}^{1}~{}\;\ldots~{}\;\tau_{F}^{n-1}\end{array}$$

$$\phi :={\tau }_P|[[{\text{s}}_{\text{o}}\leftarrowtail {\tau }_F]]|\phi \wedge \phi |\text{leavevmode}to7.41pt\text{vbox}to7.41pt\text{pgfpicture}\text{makeatletter}\text{lower}-1.11943ptto0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{definecolor}pgfstrokecolorrgb\mathrm{0,0,0}\text{pgfsys@color@rgb@stroke}000\text{pgfsys@invoke}\text{pgfsys@color@rgb@fill}000\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.4pt\text{pgfsys@invoke}\text{nullfont}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}to0.0pt\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@beginscope}\text{pgfsys@invoke}\text{pgfsys@setlinewidth}0.51666pt\text{pgfsys@invoke}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@moveto}3.44443pt2.58333pt\text{pgfsys@curveto}3.44443pt4.48566pt1.90233pt6.02776pt0.0pt6.02776pt\text{pgfsys@curveto}-1.90233pt6.02776pt-3.44443pt4.48566pt-3.44443pt2.58333pt\text{pgfsys@curveto}-3.44443pt0.681pt-1.90233pt-0.8611pt0.0pt-0.8611pt\text{pgfsys@curveto}1.90233pt-0.8611pt3.44443pt0.681pt3.44443pt2.58333pt\text{pgfsys@closepath}\text{pgfsys@moveto}0.0pt2.58333pt\text{pgfsys@stroke}\text{pgfsys@invoke}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{pgfsys@discardpath}\text{pgfsys@invoke}\text{lxSVG@closescope}\text{pgfsys@endscope}\text{hss}\text{lxSVG@closescope}\text{endpgfpicture}\phi |\phi U\phi$$

$$\exists \mathcal{M}.\forall \iota .\forall ⟨\cdot ⟩.\mathcal{M}\wr \iota ,\iota {\models }_{⟨\cdot ⟩}\phi$$

$$\begin{array}[]{rcl}\textsc{countup}&:=&\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{countup}}}~{}{\text{{time}}}~{}{\text{{dt}}}\hskip 1.0pt\rrbracket\\[1.99997pt] \textsc{countdown}&:=&\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{countdown}}}~{}{\text{{time}}}~{}{\text{{dt}}}\hskip 1.0pt\rrbracket\\[1.99997pt] \textsc{incmin}&:=&\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{incMinutes}}}~{}{\text{{time}}}\hskip 1.0pt\rrbracket\\[1.99997pt] \textsc{incsec}&:=&\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{incSeconds}}}~{}{\text{{time}}}\hskip 1.0pt\rrbracket\\[1.99997pt] \textsc{idle}&:=&\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{time}}}\hskip 1.0pt\rrbracket\end{array}$$

$$\begin{array}[]{rcl}\textsc{zero}&:=&{\text{{eq}}}~{}{\text{{time}}}~{}{\text{{zero}}}\end{array}$$

$$\!\!\!\begin{array}[]{rcl}\textsc{reset}&:=&{\text{{btnMin}}}\,\wedge\,{\text{{btnSec}}}\\[1.99997pt] \textsc{counting}&:=&\textsc{countup}\,\vee\,\textsc{countdown}\\[3.00003pt] \textsc{anykey}&:=&\textit{press}~{}{\text{{btnMin}}}\,\vee\,\textit{press}~{}{\text{{btnSec}}}\\ &&\quad\vee\;\textit{press}~{}{\text{{btnStartStop}}}\\[1.99997pt] \textsc{start}&:=&\textit{press}~{}{\text{{btnStartStop}}}\\ &&\quad\wedge\,\neg\textit{press}~{}{\text{{btnMin}}}\,\wedge\,\neg\textit{press}~{}{\text{{btnSec}}}\\[1.99997pt] \textsc{start\&min}&:=&\textit{press}~{}{\text{{btnStartStop}}}\,\wedge\,\textit{press}~{}{\text{{btnMin}}}\\ &&\quad\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\text{(}\neg{\text{{btnSec}}}\,\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg{\text{{btnSec}}}\text{)}\\[1.99997pt] \textsc{start\&sec}&:=&\textit{press}~{}{\text{{btnStartStop}}}\,\wedge\,\textit{press}~{}{\text{{btnSec}}}\\ &&\quad\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\text{(}\neg{\text{{btnMin}}}\,\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg{\text{{btnMin}}}\text{)}\end{array}$$

$$\begin{array}[]{rcl}\textit{press}~{}x&:=&\neg\,x\;\wedge\;\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}x\end{array}$$

$$\begin{array}[]{rcl}\psi_{1}&:=&\textsc{reset}\;\leftrightarrow\;\llbracket\hskip 1.0pt{\text{{time}}}\leftarrowtail\,{\text{{zero}}}\hskip 1.0pt\rrbracket\\[1.99997pt] \psi_{2}&:=&\neg\textsc{counting}\,\wedge\,\textit{press}~{}{\text{{btnMin}}}\,\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg{\text{{btnSec}}}\\ &&\quad\leftrightarrow\;\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textsc{incmin}\\[1.99997pt] \psi_{3}&:=&\neg\textsc{counting}\,\wedge\,\textit{press}~{}{\text{{btnSec}}}\,\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg{\text{{btnMin}}}\\ &&\quad\leftrightarrow\;\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textsc{incsec}\\[1.99997pt] \psi_{4}&:=&\textsc{zero}\rightarrow\\ &&\quad\big{(}\text{(}\,\textsc{idle}\,\wedge\,\textsc{start}\\ &&\qquad\quad\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textit{tillAnyInput}~{}\textsc{countup}\text{)}\\[1.00006pt] &&\qquad\qquad\ \ \operatorname{\mathcal{W}}\text{(}\textsc{incmin}\vee\textsc{incsec}\text{)}\big{)}\\[1.99997pt] \psi_{5}&:=&\textsc{incmin}\,\vee\,\textsc{incsec}\rightarrow\\ &&\quad\big{(}\text{(}\neg\textsc{counting}\,\wedge\,\textsc{start}\\ &&\qquad\quad\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textit{tillAnyInput}~{}\textsc{countdown}\text{)}\\ &&\qquad\qquad\ \ \operatorname{\mathcal{W}}\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textsc{zero}\big{)}\\[1.99997pt] \psi_{6}&:=&\textsc{counting}\,\wedge\,\textsc{anykey}\,\wedge\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\neg\textsc{reset}\\ &&\quad\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textit{tillAnyInput}~{}\textsc{idle}\\[1.99997pt] \psi_{7}&:=&\neg\textsc{counting}\wedge(\textsc{start\&min}\,\vee\,\textsc{start\&sec})\\ &&\quad\rightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\textit{tillAnyInput}~{}\textsc{countdown}\\[1.99997pt] \psi_{8}&:=&\text{(}\llbracket\hskip 1.0pt{\text{{beep}}}\leftarrowtail\,{\text{{true}}}\hskip 1.0pt\rrbracket\oplus\llbracket\hskip 1.0pt{\text{{beep}}}\leftarrowtail\,{\text{{false}}}\hskip 1.0pt\rrbracket\text{)}\,\wedge\mbox{\ }\\[1.00006pt] &&\big{(}\!\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\text{(}\textsc{countdown}\,\wedge\,\textsc{zero}\text{)}\,\vee\,\textsc{anykey}\\ &&\quad\ \ \leftrightarrow\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\llbracket\hskip 1.0pt{\text{{beep}}}\leftarrowtail\,{\text{{true}}}\hskip 1.0pt\rrbracket\,\big{)}\\[1.99997pt] \psi_{9}&:=&\llbracket\hskip 1.0pt{\text{{screen}}}\leftarrowtail\,{\text{{display}}}~{}{\text{{time}}}\hskip 1.0pt\rrbracket\par\end{array}$$

$$\begin{array}[]{rcl}\textit{tillAnyInput}~{}x&:=&\text{(}x\,\wedge\,\neg\textsc{anykey}\text{)}\\ &&\quad\ \operatorname{\mathcal{W}}\;\text{(}\textsc{reset}\,\vee\,x\,\wedge\,\textsc{anykey}\text{)}\end{array}$$

$$\delta :(\mathbb{O}\cup \mathbb{C}\cup V)\times \mathbb{N}\to (\mathbb{I}\cup \mathbb{C}\cup V\cup \{\perp \})$$

$$firstf>>>secondg=secondg>>>firstf$$

Full text

An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), as synthesized from TSL specifications, can be turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are indeed a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP.

We demonstrate the effectiveness of our translations on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic threepenny-gui library, and to hardware using the Applicative hardware description language ClaSH.

††copyright: none††conference: ACM SIGPLAN Conference; 2019; ††journalyear: 2019††isbn: 978-x-xxxx-xxxx-x/YY/MM††doi: 10.1145/nnnnnnn.nnnnnnn

1. Introduction

Reactive programs implement a broad class of computer systems whose defining element is the continued interaction between the system and its environment. Their importance can be seen through the wide range of applications, such as embedded devices (Helbling and Guyer, 2016), games (Perez, 2017), robotics (Jing et al., 2016), hardware circuits (Khalimov et al., 2014), GUIs (Czaplicki and Chong, 2013), and interactive multimedia (Santolucito et al., 2015).

Functional Reactive Programming (FRP) is a paradigm for writing programs for reactive systems. The fundamental idea of FRP is to extend the classic building blocks of functional programming with the abstraction of a $signal$ to describe values varying over time. In contrast to sequential programs being executed step by step, FRP programs lead to stream processing networks that manage state and switch between behaviors dependent on the user input. Therefore, FRP programs can be exceptionally efficient. For example, a network controller recently implemented as an FRP program on a multicore processor outperformed all its contemporary competing implementations (Voellmy et al., 2013).

Building a reactive program is a complex process, of which the most difficult part is finding a good and correct high-level design (Piterman et al., 2006). Furthermore, even once this design has been fixed, implementing the system still remains a highly error-prone process (Shan et al., 2016). While FRP helps with the latter problem by using an advanced type system to introduce a clear concept of time, it leaves the challenge of switching between behaviors and managing state efficiently open. The use of temporal logic has been explored to test properties of FRP programs (Perez and Nilsson, 2017), however testing still leaves space for possible errors.

Another solution for solving the design challenge has been proposed with Temporal Stream Logic (Finkbeiner et al., 2019), a specification logic to specify the temporal control flow behavior of a program. The logic enforces a clean separation between control and data transformations, which also can be leveraged in FRP (Elliott and Hudak, 1997). Temporal Stream Logic (TSL) is used in combination with a reactive synthesis engine to automatically create an abstract model of temporal control called a Control Flow Model (CFM), which satisfies the given specification. TSL combines Boolean and temporal operations with predicates ${\text{{p}}}~{}{\text{{s}}}_{{\text{{i}}}}$, evaluated on input signals ${\text{{s}}}_{{\text{{i}}}}$, and updates denoted by $\llbracket\hskip 1.0pt{\text{{s}}}_{{\text{{o}}}}\leftarrowtail\,{\text{{f}}}~{}{\text{{s}}}_{{\text{{i}}}}\hskip 1.0pt\rrbracket$, which map pure functions f to input signals ${\text{{s}}}_{{\text{{i}}}}$ and pipe the result to a signal ${\text{{s}}}_{{\text{{o}}}}$. An example for a TSL specification is given by

[TABLE]

which states that a counter must be incremented whenever there is a click event, while the value of the counter is displayed on a screen.

An implementation that satisfies the specified behavior, built using the FRP library Yampa (Courtney et al., 2003), is shown in Fig. 1. The program implements a button in a GUI which shows a counter value that increments with every click. The Yampa FRP library uses an abstraction called arrows, where the arrows define the structure and connection between functions (Liu and Hudak, 2007). As mentioned before, they can be used to cleanly separate data transformations into pure functions, creating a visually clear separation between the control flow and the data level. In the example program in Fig. 1, this separation is clearly visible. The top half is the “arrow” part of the code, which defines a control flow. The bottom half is the “functional” part of the code, which defines the functions f1 and f2, describing pure data transformations.

In the TSL specification, function applications, like click, increment or display, are not tied to a particular implementation. Instead, the synthesis engine ensures that the specification is satisfied for all possible implementations that may be bound to these placeholders, similar to an unknown polymorphic function that is used as an argument in a functional program. Thus, the implementation of Fig. 1 indeed satisfies the given specification by implementing event with isEvent, increment with (+1), and display with render.

The immediate advantage of synthesis over manual programming is that if the synthesis succeeds, there is a guarantee that the constructed program satisfies the specification. Sometimes, the synthesis does not succeed, and this also leads to interesting results. An example is given by the FRPZoo (Gélineau, 2016) study, which consists of implementations for the same program for 16 different FRP libraries. The program consists of two buttons that can be clicked on by the user: a counter button, which keeps track of the number of clicks, and a toggle button, which turns the counter button on and off. To our surprise, after translating the written-English specification from the FRPZoo website into a formal TSL specification, the synthesis procedure was not able to synthesize a satisfying program. By inspecting the output of the synthesis tool, we noticed that the specification is actually unrealizable. The problem is that the specification requires the counter to be incremented whenever the counter button is clicked and, to be reset to zero whenever the toggle button is clicked. This creates a conflict when both buttons are clicked at the same time. To obtain a solution, we had to add the assumption that both buttons are never pressed simultaneously.

While the work of Finkbeiner et al.  2019 discusses the synthesis process for creating the CFM in detail, it does not elaborate on how a CFM is actually turned into FRP code. In this work we explore this process, and show how Causal Commutative Arrows (CCA) form a foundational abstraction for FRP in the context of program synthesis. From this connection between CCA and a CFM, we then build a system to generate library-independent FRP code across a range of FRP abstractions.

There is no single style of FRP which is generally accepted as canonical. Instead, FRP is realized through a number of libraries, which are based on fundamentally different abstractions, such as Monadic FRP (Ploeg and Claessen, 2015; Apfelmus, 2013; Trinkle, 2017), Arrowized FRP (Courtney et al., 2003; Perez et al., 2016; Winograd-Cort, 2015), and Applicative FRP (Baaij, 2015; Apfelmus, 2012). We show how our system is flexible enough to handle these various abstractions by demonstrating the translation from a CFM to Yampa (Courtney et al., 2003; Perez et al., 2016), threepenny-gui (Apfelmus, 2013), and ClaSH (Baaij, 2015). We do not imagine FRP synthesis as a replacement for FRP libraries, but rather as a complement. Through synthesis and code generation, users can automatically construct FRP programs in these libraries, which provide critical interfaces to input/output domains. Furthermore, we show that TSL synthesis generates code as expressive as CCA. While this power is sufficient for many applications, the FRP libraries still provide an interface to more powerful language abstraction features, in cases the user chooses to use them.

In summary, the paper makes the following contributions:

1. (1)

We describe the process of automatically generating library independent FRP control code from TSL specifications. 2. (2)

We examine the relation between CFMs and CCA, and compare the differences between various FRP abstractions during the translation process. 3. (3)

We demonstrate our translations on a real-world kitchen timer application, build as a desktop application using the Arrowized FRP library Yampa, as a web application using the Monadic library threepenny-gui, and to hardware using the Applicative hardware description language ClaSH. 4. (4)

We provide an open-source tool for the synthesis of FRP programs from TSL specification111https://github.com/reactive-systems/tsltools

2. Preliminaries

We assume time to be discrete and denote it by the set \mathcal{T}\scalebox{0.8}{\boldsymbol{i}\boldsymbol{m}\boldsymbol{e}} of positive integers. A value is an arbitrary object of arbitrary type, where we use $\mathcal{V}$ to denote the set of all values. We consider the Boolean values $\mathcal{B}\subseteq\mathcal{V}$ as a special subset, which are either ${\text{{true}}}\in\mathcal{B}$ or ${\text{{false}}}\in\mathcal{B}$.

A signal s\colon\mbox{\mathcal{T}\scalebox{0.8}{$\boldsymbol{i}\boldsymbol{m}\boldsymbol{e}$}}\rightarrow\mathcal{V} is a function fixing a value at each point in time. The set of all signals is denoted by $\mathcal{S}$, usually partitioned into input signals $\mathcal{I}$ and output signals $\mathcal{O}$.

An $n$-ary function $f\colon\mathcal{V}^{n}\rightarrow\mathcal{V}$ determines a new value from $n$ given values. We denote the set of all functions (of arbitrary arity) by $\mathcal{F}$. Constants are functions of arity zero, while every constant is also a value, i.e, an element of $\mathcal{F}\cap\mathcal{V}$. An $n$-ary predicate $p\colon\mathcal{V}^{n}\rightarrow\mathcal{B}$ checks a truth statement on $n$ given values. The set of all predicates (of arbitrary arity) is denoted by $\mathcal{P}$.

2.1. Functional Reactive Programming

FRP is a programming paradigm that uses the abstractions available in functional programming to create an abstraction of time. The core abstraction in FRP is that of a signal

[TABLE]

which produces values of some arbitrary type $a$ over time. The type $a$ can be an input from the world, such as the current position of the mouse, or an output type, such as some text that should be rendered to the screen. Signals are also used internally to manipulate values over time, for example if the position of the mouse should be rendered to the screen.

Arrows

There are many incarnations of FRP, which use various abstraction to manipulate signals over time. One popular abstraction for FRP is a Monad, but a weaker abstraction called Arrows, is also used in many modern libraries (Perez et al., 2016; Murphy, 2016). The Arrow abstraction describes a computation connecting inputs and outputs in a single type (Hughes, 2000). Hence, an Arrow type also allows us to describe reactive programs that process inputs and produce outputs over time.

Arrowized FRP was introduced to plug a space leak in the original FRP work (Elliott and Hudak, 1997; Liu and Hudak, 2007). By using the Arrow abstraction introduced in (Hughes, 2000), which describes in a single type inputs and outputs, we can also describe reactive programs that process inputs and produce outputs over time. At the top level, an Arrowized FRP program will have the form

[TABLE]

which is a signal function type, parametrized by the type of input from the world and the type of output to the world. The core Arrow operators, shown in Fig. 2, are used to composed multiple arrows into larger programs.

The abstractions used in different implementations of FRP vary in expressive power. Arrowized FRP has a smaller interface than a Monadic FRP (Lindley et al., 2011), which prevents particular constructs that caused the aforementioned space leak. This is also useful when choosing a core language to synthesize, as we will be able to simulate an Arrowized FRP program in most Monadic libraries.

CCA

We target a restricted set of arrows called Causal Commutative Arrows (CCA) (Yallop and Liu, 2016; Liu et al., 2011). Specifically, CCA adds additional laws to arrows that constrain their behavior and the type of state they may retain. Of particular interest to our application is that CCA also introduces a special initialization operator, init. This init operator allows for loopD, which is a loop that includes an initialization, as shown in Fig. 3.

We use CCA as a minimal language for synthesis. Our synthesis is able to support any FRP library which is at least as powerful as CCA. Because CCA is again restricted in its interface, there are more libraries that can simulate CCA FRP than Arrowized FRP in general. This makes our synthesis procedure possible for an even wider range of application scenarios. We revisit the implications of CCA as our choice of computation abstraction in Sec. 4.1.

2.2. Reactive Synthesis

The synthesis of a reactive system concerns the process of automatically generating an implementation from a high level specification. The reactive system acts as a deterministic controller, which reads inputs and produces outputs over an infinite amount of time. In contrast, a specification defines all input/output behavior pairs which are valid, i.e., allowed to be produced by the controller.

In the classical synthesis setting, time is discrete and inputs and outputs are given as vectors of Boolean signals. The standard abstraction treats inputs and outputs as atomic propositions $\mathcal{I}\cup\mathcal{O}$, while their Boolean combinations form an alphabet $\Sigma=2^{\mathcal{I}\cup\mathcal{O}}$ of alphabet symbols.

This fixes the behavior of the system to infinite sequences $\sigma=\sigma_{0}\sigma_{1}\sigma_{2}\ldots$ of alphabet symbols $\sigma_{t}$. At every time $t$ signals appearing in the set $\sigma_{t}$ are enabled (true), while signals not in $\sigma_{t}$ are disabled (false). The set of all such sequences is denoted by $\Sigma^{\omega}$, where the $\omega$-operator induces the infinite concatenation of alphabet symbols of $\Sigma$. A deterministic solution links exactly one output sequence $\beta\in(2^{\mathcal{O}})^{\omega}$ to every possible infinite sequence of inputs $\alpha\in(2^{\mathcal{I}})^{\omega}$, i.e., it is a total function $f\colon(2^{\mathcal{I}})^{\omega}\rightarrow(2^{\mathcal{O}})^{\omega}$. A specification describes an arbitrary relation between input sequences $\alpha\in(2^{\mathcal{I}})^{\omega}$ and output sequences $\beta\in(2^{\mathcal{O}})^{\omega}$.

2.3. Connections between FRP and Reactive Systems

A first inspection reveals that FRP fits into the definition of a reactive system, as given in Section 2.2: an FRP program reads an infinite stream of input signals and finally produces a corresponding infinite output stream. Nevertheless, FRP does not fit into the classical setting used for reactive systems, as the input and output streams in FRP are allowed to have arbitrary types.

To solve this problem, one could restrict FRP to just streams of enumerative types, which could then be reduced to a Boolean representation. However, this would drop the necessity of almost all interesting features of FRP and it is questionable whether this restricted notion of FRP would give any benefits against Mealy/Moore automata or circuits, which are already used for reactive systems. Additionally, it just creates an exponential blowup and does not provide any insights into the core problem.

Hence, it is more reasonable and interesting to ask whether it is possible to natively handle streams of arbitrary type within reactive systems. Recall that FRP includes functional behavior, defined using standard functional paradigms, but also a control structure, defined via arrows and loops. We will target synthesis of the control structure, leaving the functional level synthesis to tools such as Myth (Osera and Zdancewic, 2015; Kuncak et al., 2010) or Synquid (Polikarpova et al., 2016).

2.4. Temporal Stream Logic

We use Temporal Stream Logic (TSL) for the specification of the control flow behavior of functional reactive programs (Finkbeiner et al., 2019). The logic has been especially designed for synthesis and describes control flow properties with respect to their temporal behavior over time. If a TSL specification is realizable it can be turned into a Control Flow Model (CFM), which is an abstract representation of the FRP network covering all possible behavior switches.

Temporal Stream Logic builds on the notion of updates, such as $\llbracket\hskip 1.0pt{\text{{y}}}\leftarrowtail\,{\text{{f}}}~{}{\text{{x}}}\hskip 1.0pt\rrbracket$, which expresses that the result of mapping the pure function f to some input stream x is piped to the output stream y. The execution of an update then is coupled with predicate evaluations guiding the control flow decisions of the network. In combination with Boolean and temporal operators, the logic allows for expressing even complex temporally evolving FRP networks using only a short, but precise description of the temporal behavior.

A useful advantage of TSL in contrast to other specification logics is that function and predicate names, as used by the specification, are only considered as symbolic literals. Therefore, the logic guarantees that synthesized systems satisfy the specified behavior for all possible implementations of these function and predicate literals. The literals are still classified according to their arity, i.e., the number of other function terms they are applied to, as well as by their type: input, output, cell, function or predicate. Thus, they can be considered similar to a function, passed as an argument, of polymorphic type.

However, using TSL also comes with another important advantage. As updates can be considered as pure building blocks lifted to the temporal domain, the synthesis engine guarantees that a created CFM is implementable using a static network. This especially is in contrast to the well-known switch operation used by many FRP libraries, which allows for the creation of dynamically evolving networks. While switch is a very expressive operation in the first place, it also comes with drawbacks. First, dynamically evolving networks cannot provide run-time guarantees for memory requirements in general, while static networks do. Second, the behavior of a dynamically evolving network is hard to grasp in general, which especially makes them unamenable for verification. Third, the use of dynamic networks is out of scope for FRP applications with restricted resources, as for example applications that are executed on embedded devices (Sawada and Watanabe, 2016) or are implemented directly in hardware (Baaij, 2015). Finally, while switch is an expressive operation, it is not necessary for most applications (Winograd-Cort and Hudak, 2014). Thus, by using TSL as a specification language, we can avoid these problems implicitly, as the logic guarantees the creation of a static network.

TSL specifications implicitly induce an architecture as shown in Fig. 4. As a basis, the syntax of TSL uses a term based notion, build from input streams ${\text{{i}}}\in\mathbb{I}$, output streams ${\text{{o}}}\in\mathbb{O}$, memory cells ${\text{{c}}}\in\mathbb{C}$, and function and predicate literals ${\text{{f}}}\in\mathbb{F}$ and ${\text{{p}}}\in\mathbb{P}$ with $\mathbb{P}\subseteq\mathbb{F}$, respectively. The purpose of cells is to memorize data values, output to a cell at time t\in\mbox{\mathcal{T}\scalebox{0.8}{$\boldsymbol{i}\boldsymbol{m}\boldsymbol{e}$}}, to provide them again as inputs at time $t+1$. We differentiate between function terms $\tau_{F}\in\mathcal{T}_{\!F}$ and predicate terms $\tau_{P}\in\mathcal{T}_{\!P}$, build according to the following grammar

[TABLE]

where ${\text{{s}}}_{{\text{{i}}}}\in\mathbb{I}\cup\mathbb{C}$ is either an input stream or a cell. In a TSL formula $\varphi$, predicate and function terms are then combined to updates and with Boolean connectives and temporal operators

[TABLE]

where ${\text{{s}}}_{{\text{{o}}}}\in\mathbb{O}\cup\mathbb{C}$ is either an output signal or a cell.

To give semantics to TSL formulas $\varphi$ a universally quantified assignment function $\langle\cdot\rangle\colon\mathbb{F}\rightarrow\mathcal{F}$ is used, fixing an implementation for each predicate and function literal, as well as input streams $\iota\colon\mathbb{I}\rightarrow\mathcal{S}$. We will only give an intuitive description of the semantics here. For a fully formal definition the interested reader is referred to (Finkbeiner et al., 2019). Intuitively, the semantics of TSL can be summarized as follows:

Predicate terms are evaluated to either true or false, by first selecting implementations for all function and predicate literals according to $\langle\cdot\rangle$, and then applying them to inputs, as given by $\iota$, and cells, using the stored value at the current time $t$. The content of a cell thereby is fixed iteratively by selecting the past values piped into the cell over time. Cells are initialized using a special constant provided as part of $\langle\cdot\rangle$.

Function terms are evaluated similar to predicate terms, except that they can evaluate to any value of arbitrary type.

Updates are used to pipe the result of function term evaluations to output streams or cells. Note that updates, as they appear in a TSL formula, semantically are typed as Boolean expressions. In that sense, update expressions are used in TSL formula to state that a specific flow is used at a specific point in time, where the expression evaluates to true if it is used and to false, otherwise.

The Boolean operators negation [$\neg$] and conjunc-tion [$\wedge$], and the temporal operators next [$\mathop{\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}$] and until [$\hskip 0.6pt\mathop{\operatorname{\mathcal{U}}}\hskip 0.2pt$] have standard semantics. Intuitive behavior for the temporal operators is given in Fig. 5, including also the derived operators release [$\varphi\operatorname{\mathcal{R}}\psi\equiv\neg$(($\neg\psi$)$\operatorname{\mathcal{U}}$($\neg\varphi$))], finally [$\operatorname{\leavevmode\hbox to8.7pt{\vbox to8.7pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.76527pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{6.67358pt}\pgfsys@lineto{8.18053pt}{2.58333pt}\pgfsys@lineto{4.09026pt}{-1.50694pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\equiv\emph{true}\operatorname{\mathcal{U}}\varphi$], always [$\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi\equiv\emph{false}\operatorname{\mathcal{R}}\varphi$], and the weak version of until [$\varphi\operatorname{\mathcal{W}}\psi\equiv(\varphi\operatorname{\mathcal{U}}\psi)\vee(\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\varphi)$].

The synthesis problem of creating a CFM $\mathcal{M}$ satisfying a TSL specification $\varphi$ then is formalized by

[TABLE]

where $\mathcal{M}\!\wr\iota$ denotes the output produced by $\mathcal{M}$ under the input $\iota$. Note that the CFM $\mathcal{M}$ must satisfy the specification for all possibly chosen function and predicate implementations, as selected by $\langle\cdot\rangle$, and all possible inputs $\iota$, which is also the reason for the synthesis problem being undecidable in general.

Theorem 2.1 ((Finkbeiner et al., 2019)).

The synthesis problem of TSL is undecidable.

3. System Design with TSL

We demonstrate the advantages of using TSL as a specification language for the development of FRP applications using the example application of a kitchen timer, as presented in Fig. 6. The timer consists of three buttons, a screen displaying the currently set time and a buzzer to produce an alarm. The button values are provided as Boolean input streams to the system, which deliver true, as long as a button is pressed, and false otherwise. In addition, there is another input stream providing the time passed since the last execution of the network, which is utilized to synchronize the time displayed with the clock of the application framework.

Similar to the button inputs, the system must output a Boolean data stream to control the buzzer, which is turned on whenever the output is true. The second output, the system must provide, delivers the data to be displayed on the screen, where the data type is fixed by the utilized application framework as well.

For our development plan, we consider the following list of requirements to be implemented by the timer:

1. (1)

Whenever the MIN and SEC buttons are pressed simultaneously the timer is reset, meaning the time is set to zero and the system stays idle until the next button gets pressed. 2. (2)

If only the MIN button is pressed and the timer is not currently counting up or down, then the currently set time is increased by one minute. 3. (3)

If only the SEC button is pressed and the timer is not currently counting up or down, then the currently set time is increased by one second. 4. (4)

As long as no time greater than zero has been set and the system is idle: if the START/STOP button is pressed and the timer is not already counting up or down, then the timer starts counting up until it is stopped by any button pressed. 5. (5)

If a time has been set and the START/STOP button is pressed, while the timer is not currently counting up or down, then the timer starts counting down until it is stopped by any button pressed. 6. (6)

The timer can always be stopped by pressing any button while counting up or down. 7. (7)

It is possible to start the timer and to set some time simultaneously. 8. (8)

The buzzer beeps on any button press and after the counter reaches zero while counting down. 9. (9)

The display always shows the time currently set.

While it requires a certain amount of engineering to find the right control behavior, especially for fixing the additional state to manage the different modes, when directly implementing the application on top of an FRP library, it is an easy task to specify the control behavior with TSL. We first fix possible operations on time, which is used as a cell for holding the currently set time.

[TABLE]

The used literals countup, countdown, incMinutes, and incSeconds represent pure functions that update the value of time accordingly, while the input signal dt delivers the time difference since the last execution of the network. By the semantics of TSL it is already ensured that assignments to the same cell are always mutually exclusive, i.e., it can never be the case that time is counting up and the minutes are increased in the same time step.

Next, we fix the properties of the behavior of time that influence the control flow behavior. In our case, we need a predicate to check whether the time currently set is zero or not

[TABLE]

where zero is a constant function of the same type as time. We also fix some sub-properties, that are useful to express conditions regularly appearing in the main specification later. In our case these are

[TABLE]

The literals btnMin, btnSec, and btnStartStop represent the input signals for the three buttons, respectively. The function press is used as a helper function for improved readability and is defined as

[TABLE]

This is all we need to implement the invariants of the aforementioned requirements:

[TABLE]

​​The function tillAnyInput is a helper function to denote that a condition must be satisfied until either the system is reset or any button gets pressed. It is defined as:

[TABLE]

The final specification is given by \varphi=\psi_{\textit{init}}\wedge\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\scalebox{1.3}{\wedge}_{i=1}^{9}\psi_{i}, where $\psi_{\textit{init}}$ adds some remaining initial conditions. The full specification, using our plain text specification format, is also given in Fig. 7. Note that the various $\operatorname{\leavevmode\hbox to7.41pt{\vbox to7.41pt{\pgfpicture\makeatletter\hbox{\hskip 3.70276pt\lower-1.11943pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {{}{}}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@moveto{3.44443pt}{2.58333pt}\pgfsys@curveto{3.44443pt}{4.48566pt}{1.90233pt}{6.02776pt}{0.0pt}{6.02776pt}\pgfsys@curveto{-1.90233pt}{6.02776pt}{-3.44443pt}{4.48566pt}{-3.44443pt}{2.58333pt}\pgfsys@curveto{-3.44443pt}{0.681pt}{-1.90233pt}{-0.8611pt}{0.0pt}{-0.8611pt}\pgfsys@curveto{1.90233pt}{-0.8611pt}{3.44443pt}{0.681pt}{3.44443pt}{2.58333pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{2.58333pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ operations in the formulas $\psi_{i}$ are always necessary, since the “being pressed” condition requires a change of the input, which is only observable by comparing the currently provided value with the previous one.

For the development of such specifications, the designer also gets feedback from the synthesis engine. For example, the condition of $\psi_{2}$ requires btnSec to not being pressed in order to increase the minutes of the counter. Without this condition, the synthesis engine would return an unrealizabilty result, since increasing minutes would conflict with setting the time to zero on a potential reset, which also requires btnMin to be pressed.

After the development of the specification is finished, the synthesis automatically creates a CFM that satisfies the specified control behavior. In the next step the CFM then is specialized towards the specific application context.

4. Code Generation

We present a system for the generation of FRP program code from the output of TSL synthesis. The user initially provides a CFM that was synthesized from a TSL specification over a set of predicate and function terms. The user specifies a target FRP abstraction, and receives an executable Haskell FRP program in the library of their choosing.

Our approach takes a multi-stage approach, whereby the TSL specification is first used to generate a control flow model (CFM). The CFM is an abstract representation of the temporal changes that the FRP program must implement in order to satisfy the TSL specification. In particular, a CFM maps the input signals through various function and predicate terms to the output signals. We only consider valid CFMs, where for every cycle created by mapping an output back to an input, there is at least one cell. A cell is a memory unit with delay, so that at one time step a value may be stored, and at the next that value is retrieved. The concept of a cell is analogous to ArrowLoop (Paterson, 2001), or a register in hardware.

The synthesis from TSL to CFM is the most computationally expensive and may result in an unrealizable result, in which case synthesis terminates with no solution. We omit a detailed description of the generation of the CFM from a TSL specification, and instead direct the reader to related work on this topic (Finkbeiner et al., 2019). Here we focus on how the generality of the CFM is utilized to generate framework-independent FRP code. If a satisfying CFM is found during the first stage, a user specifies a target FRP abstraction (Applicative, Monad, Arrow) that should be used to generate the FRP program code from the CFM.

To clarify the translation process from a CFM to FRP code, we give a formal definition of a CFM. A CFM $\mathcal{M}$ is a tuple $\mathcal{M}=(\mathbb{I},\mathbb{O},\mathbb{C},V,\ell,\delta),$ where $\mathbb{I}$ is a finite set of inputs, $\mathbb{O}$ is a finite set of outputs, $\mathbb{C}$ is a finite set of cells, $V$ is a finite set of vertices, $\ell\colon V\rightarrow(\mathbb{F}\cup\mathbb{L}\cup\mathbb{U})$ assigns a vertex a signal function (either a function ${\text{{f}}}\in\mathbb{F}$, a predicate ${\text{{p}}}\in\mathbb{P}$, a logic operator in $\mathbb{L}$ lifted to the signal level, or a mutex selector $\mathbb{U}$ lifted to the signal level). The set of logic operators are the standard Boolean operators (and, or, not), and the mutex selectors are signal functions pattern matching on one input signal to select among the other input signals for output. Finally, a CFM also contains a dependency relation

[TABLE]

relating every output, cell, and vertex to a set of inputs, cells, or vertices. The dependency relations defines the wiring between signal functions. The selector $n\in\mathbb{N}$ argument allows us to specify a specific connection, since a signal function may have multiple inputs. Outputs and cells ${\text{{s}}}\in\mathbb{O}\cup\mathbb{C}$ always have only a single input signal stream, so the first selector has some non-bottom value ($\delta(s,0)\not\equiv\bot$) and any larger selector is undefined ($\forall m>0.\ \delta({\text{{s}}},m)\equiv\bot$). In contrast, for vertices $x\in V$ the number of input signals $n\in\mathbb{N}$ match the arity of the assigned function or predicate $\ell(x)$. This means $\forall m\in\mathbb{N}.\ \delta(x,m)\equiv\bot\leftrightarrow m>n$. We only consider valid CFMs, where a CFM is valid if it does not contain circular dependencies, i.e., on every cycle induced by $\delta$ there must lie at least a single cell. As an example, a CFM would contain a circular dependency if given $x,y\in V$, $\delta(x,0)=y$ and $\delta(y,0)=x$. Such a CFM, if rendered as an Arrow function, would enter an infinite loop, and in the best case, generate the runtime error <<loop>>.

Given a CFM that satisfies the TSL specification, we next convert it into a template for our FRP program. The CFM is transformed via a syntactic transformation into an FRP program in the abstraction of the user’s choice, as a function that is parameterized over the named function and predicate terms, as shown in Fig. 8. The user then provides implementations of the function and predicate terms that complete the construction of the FRP program based on the generated template.

The CFM transformation is modularized to fit any FRP library that is at least as powerful as CCA (Ploeg and Claessen, 2015; Perez et al., 2016; Murphy, 2016; Patai, 2010; Gélineau, 2016). The key insight is that first-order control along with a loop describes the expressive power of both CCA and the CFM model generated from the techniques of (Finkbeiner et al., 2019). Although many FRP libraries support more powerful operations than CCA, *e.g. *switch in Yampa, we do not need to utilize these in the synthesis procedure, and thus can generalize synthesis to target any FRP library that is at least as expressive as CCA.

Recall that in TSL, output signals can be written at the current time $t$, and be read from at time $t+1$. To implement this in the FRP program, we use the concept of a cell in the CFM. In the translation, we allow a space for the user to provide an implementation of the cell that is specialized to their FRP library of choice. In the case of CCA, this is the loopD combinator. The loopD combinator pipes the output values back to the input to allow them to be read at time $t+1$. Since a system may require output values at time $t=0$, the user must also provide initial values to $\mathbb{O}$.

4.1. Properties of Synthesis

For a full description of the formal properties of TSL synthesis, see the work of (Finkbeiner et al., 2019). In summary the synthesis procedure is sound, but not complete. From a programming languages design perspective, this means that “compilation” (synthesis) of a specification may not terminate, but when it does terminate, it will generate code that satisfies the specification.

In the translation of the CFM, we use Casual Commutative Arrows (CCA) as the target conceptual model for the transformation. One interesting note about this is that CCA does not allow the arrowApply function. The arrowApply (also called switch) function is a higher-order arrow that allows for dynamically replacing an arrow with a new one that arrives on an input wire, enforcing a static structure on the generated program. As one of our target domains is hardware (using ClaSH), this would cause problems, as self-reconfiguring hardware is out-of-scope for this work. The insight provided by prior work on CCA (Liu et al., 2011) found that, in general, the expressive power of higher-order arrows makes automatic optimization more difficult. Furthermore, for most FRP programs, first-order switch is more than enough (Winograd-Cort and Hudak, 2014).

With respect to the synthesis procedure, this is a fundamental restriction related to the specification logic TSL. With TSL, every update term $\llbracket\hskip 1.0ptx\leftarrowtail\,y\hskip 1.0pt\rrbracket$ is lifted to an arrow that updates x with y over time. Since in TSL updates are fixed by the specification, so too must the arrow structure be fixed in synthesis.

Note that having a fixed arrow structure disallows higher-order arrows, but higher-order functions can still be passed along the wires. As an example, we may have a function term app  $\colon\!\!\colon\;$  (a  ->  b)  ->  a  ->   b and signals f  $\colon\!\!\colon\;$  a  ->  b and x  $\colon\!\!\colon\;$  a. A simple specification making use of higher order functions then could state that the system should always apply the incoming higher-order function to the incoming value: $\operatorname{\leavevmode\hbox to6.97pt{\vbox to6.97pt{\pgfpicture\makeatletter\hbox{\hskip 0.25833pt\lower-1.11945pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{ {}{{}}{} {}{} {}{} {}{} {}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.51666pt}\pgfsys@invoke{ }\pgfsys@roundjoin\pgfsys@invoke{ }{}\pgfsys@moveto{0.0pt}{-0.86111pt}\pgfsys@lineto{0.0pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{5.5972pt}\pgfsys@lineto{6.45831pt}{-0.86111pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\,\llbracket\hskip 1.0pt{\text{{x}}}\leftarrowtail\,{\text{{app}}}({\text{{f}}},{\text{{x}}})\hskip 1.0pt\rrbracket$. Recall that, absent any user provided assumptions, the synthesis procedure allows the value of all symbols to change at every time step. Proper reasoning over higher-order functions then requires added assumptions in practice, depending on the specific use case.

Additionally, a key difference between arrows and circuits is that arrows are able to carry state that tracks the application of each arrow block. By using CCA, a user may write TSL specifications about stateful arrows that are still handled correctly by the synthesis procedure. To this end, we only synthesize programs that obey the commutativity law (Liu et al., 2011; Yallop and Liu, 2016), restated below, which ensures that arrows cannot carry state that influences the result of composed computations.

[TABLE]

Imagine an arrow with a global counter to track data of a buffer. Since addition is commutative, this arrow respects the commutativity law. However, non-commutative state is possible as well. For example, when building GUIs with Arrowized FRP (Winograd-Cort, 2015), the position of each new UI element depends on the order of the previously laid out elements. Due to the commutativity of the Boolean operators, the commutativity of CCA is a necessary precondition for synthesis of a TSL specification. Specifically, the commutativity of logical conjunction allows the solution to update signals in any arbitrary order. Thus, the correctness of the TSL synthesis relies on commutativity of composition, which is naturally modeled with CCA’s commutativity law.

4.2. Example: Kitchen Timer

We revisit the Kitchen Timer application introduced in Section 3 to show the concrete code that is generated. From the TSL specification, we first generate a CFM using our TSL synthesis toolchain together with the LTL synthesizer strix (Meyer et al., 2018) [version 18.04]. The resulting CFM utilizes six additionally synthesized cells and consists of 1188 vertices. This CFM is then transformed into a control structure for each of the different application domains. In Fig. 10, we show how the template described in Sec. 4 is specialized to each of the three application domains: the desktop program is built with Yampa [version 0.13] and the web app with threepenny-gui [version 0.8.3.0]. Both have been built using stack222https://www.haskellstack.org on lts-13.17 [ghc-8.6.4]. For building the hardware implementation, we first use the functional hardware description language ClaSH333https://github.com/clash-lang/clash-compiler [commit: fff4606] to generate verilog-code, which then is turned into the blif format using the open synthesis suite yosys444https://github.com/YosysHQ/yosys [commit: 70d0f38]. Afterwards, the generated blif-file is placed using the place-and-route tool nextpnr555https://github.com/YosysHQ/nextpnr [commit: 5344bc3]. The packaged result is then uploaded to an iCEblink40HX1K Evaluation Kit Board from Lattice Semiconductor, featuring an ICE40HX1K FPGA with 100 IO-pins and 1280 logic cells, additionally equipped with the required hardware components. The interfaces to the corresponding timer applications are depicted in Fig. 11. The synthesis and compilation times of the different tools are depicted in Table 1. A video demonstration of the three different timers can also be found at:

[TABLE]

Yampa uses Arrowized FRP which easily fits into the general interface for Arrows that we provide (Fig. 10(b)). Likewise, threepenny-gui uses a Monadic FRP (where the signals themselves are Applicative) which also easily fits into our general interface for Monadic FRP (Fig. 10(a)). Finally, for ClaSH, we use a mostly Applicative interface, that is specialized to handle the peculiarities of hardware (which needs explicit clocks, as opposed to more traditional FRP frameworks). If we wanted to support other libraries with explicit clocks, for example, as presented in (Bärenz and Perez, 2018), we would need a specialized module for this - although the customization is limited mostly to the type signature generation as shown in Fig 10(c).

Each control block requires the user to provide a cell implementation. Both Yampa and ClaSH provide native implementations of the concepts, as shown in Fig 12. Although threepenny-gui does not provide the exact implementation of a cell, as we require in our synthesized control block, it can be easily implemented using the available primitives of the library.

5. Related Works

There are various lines of work that are related to our approach. While we draw inspiration from these research directions, each one, on

5.1. Temporal Types for FRP

FRP is a programming paradigm for computations over time, and, hence, a natural extension is to investigate type systems to be able to reason about time. A correspondence between LTL and FRP in a dependently typed language was discovered simultaneously by (Jeffrey, 2012; Jeltsch, 2012). In this formulation, FRP programs are proofs and LTL propositions are reactive, time-varying types that describe temporal properties of these programs. In establishing the connection between logic and FRP, these LTL types are also used to ensure causality and loop-freeness on the type level.

Dependent LTL types are a useful extension to FRP that provides insight into the underlying model of FRP, but does not lend itself to control flow synthesis. In the work of Jeffery and Jeltsch, the types describe the input/output change over time for each arrow. Using these LTL types, only arrows adhering to sensible temporal orderings (*e.g. *computations only depend on past values) will be well typed. However, as with any other FRP system, the temporal control flow of function applications in the program is fixed by the code. A similar approach was used by (Krishnaswami, 2013) to make a temporal type system that ensures there are no spacetime leaks in an well typed FRP program. Work on reasoning about FRP using temporal logics also includes (Sculthorpe and Nilsson, 2010), although this setting considered dynamic network structure, as allowed by higher-order arrows. Further properties beyond safety have been expressed in FRP, for instance using a type extension to enforce fairness properties (Cave et al., 2014).

In contrast, we use the logic TSL, for a fine-grained description of function application behavior which cannot be expressed within pure LTL. The synthesis procedure of TSL determines a temporal control flow of functions, where the TSL specifications determines the transformations to be applied at each point in time. In addition to the logical specifications, the synthesis is also constrained by the types of functions appearing in the specification. Since the types of all functions are fixed for every time step, the type system can be lifted to the specification. If the specification is well typed, synthesis is guaranteed to yield a well typed program.

One connection to our work however is the implications of the fact that the Curry-Howard correspondence extends to FRP and LTL. In the aforementioned work, LTL propositions are types for FRP programs. If a proof of a TSL proposition can be interpreted as a program, one might expect that there is some corresponding type system to TSL. We leave such explorations to future work.

5.2. Synthesis of Reactive Programs

A distinguishing feature of our approach is the connection to an actual programming paradigm, namely FRP. Most reactive synthesis methods instead target transition systems or related formalisms such as finite state machines. The idea to synthesize programs rather than transition systems was introduced in (Madhusudan, 2011). In his work, an automaton is constructed that works on the syntax tree of the program, which makes it possible to obtain concise representations of the implementations, and to determine how many program variables are needed to realize a particular specification. Unlike our FRP programs, Madhusudan’s programs only support variables on a finite range of instances.

Another related approach is the synthesis of synchronization primitives introduced in (Bloem et al., 2012) for the purpose of allowing sequential programs to be executed in parallel. Similar to our synthesis approach, uninterpreted functions are used to abstract from implementation details. However, both the specification mechanism (the existing program itself is used as the specification) and the type of programs considered are completely different from TSL and FRP.

5.3. Logics for Reactive Programs

Many logics have been proposed to specify properties of reactive programs. Synthesis from Signal Temporal Logic (Raman et al., 2015) focuses on modeling physical phenomena on the value level, introducing continuous time to the model and resolving to a system of equations. The approach allows for some different notion of data embedded into the equations. While more focused on the data level, the handling on continuous time might provide inspiration for future extensions to TSL to more explicitly handle continuous time.

Another logic that has been proposed, Ground Temporal Logic (Cyrluk and Narendran, 1994), is a fragment of First Order Logic equipped with temporal operators, where it is not allowed to use quantification. Satisfiability and validity problems are studied, with the result that only a fragment is decidable. However, specifications expressed in Ground Temporal Logic, as well as their motivations, are completely different from our goals.

5.4. Reasoning-based Program Synthesis

Reasoning-based synthesis (Osera and Zdancewic, 2015; Solar-Lezama, 2013; Kuncak et al., 2010; Vechev et al., 2013) is a major line of work that has been mostly, but not entirely, orthogonal to reactive synthesis. While reactive synthesis has focused on the complex control aspects of reactive systems, deductive and inductive synthesis has been concerned with the data transformation aspects in non-reactive, sequential programs. Our work is most related to Sketching (Solar-Lezama, 2013), since in Sketching the user provides the control structure and synthesizes the transformations while with TSL we synthesize the control structure and leave the transformations to the user.

The advantage of deductive synthesis is that it can handle systems with complex data. Its limitation is that it cannot handle the continuous interaction between the system and its environment, which is typical for many applications, such as for cyber-physical systems. This type of interaction can be handled by reactive synthesis, which is, however, typically limited to finite states and can therefore not be used in applications with complex data types. Abstraction-based approaches can be seen as a link between deductive and reactive synthesis (Dimitrova and Finkbeiner, 2012; Beyene et al., 2014).

Along the lines of standard reactive synthesis, our work is focused on synthesizing control structures. We extend the classic approach by also allowing the user to separately provide implementations of data transformations. This is useful in the case where the value manipulations are unknown or beyond the capability of the synthesis tool. For example, a user may want to synthesize an FRP program that uses closed source libraries, which may not be amenable to deductive synthesis. In this case, the user can only specify that certain functions from that API should be called under certain conditions, but cannot and may not want to reason about their output.

6. Conclusions

In this work we have presented a detailed account of how to transform Control Flow Models into framework-independent FRP code. With this transformation, we utilize TSL synthesis as presented in (Finkbeiner et al., 2019) to build a complete toolchain for synthesizing Functional Reactive Programs.

So far we have used a discrete time model in our formalization, however, the behavior of the kitchen timer is in fact sampling rate independent (Continuous Time FRP). Sampling rate independence is guaranteed in TSL as long as the next operator is not used. However, the relation between TSL with the next operator and Continuous Time FRP still needs to be explored.

In another direction, the usual way in FRP to distinguish between continuous and discrete behaviors is to use signals and events. So far we have embedded all data into signals. It is open to future work how to utilize events natively. Future directions for improvements to usability include integrating FRP synthesis more tightly into the typical programming workflow - for instance by allowing TSL specification to be used inline in code with QuasiQuoters (Mainland, 2007).