Spectra: A Specification Language for Reactive Systems

TL;DR

Spectra is a new specification language designed for reactive systems, providing tools for synthesis, execution, and analysis to assist engineers in creating correct and high-quality reactive system specifications.

Contribution

The paper introduces Spectra, a novel specification language for reactive systems, along with a comprehensive toolset for synthesis, execution, and analysis.

Findings

Provides a translation to a kernel language for semantics

Includes a synthesizer for correct-by-construction implementations

Offers analysis tools to improve specification quality

Abstract

Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications. We present the language and give an overview of the tool set.

Figures

Tables

Table 1. Table 1: Overview over keywords and their alternatives (in alphabetical order)

Keyword	Alternative
alw	always
alwEv	alwaysEventually
asm	assumption
env	input
gar	guarantee
H	HISTORICALLY
ini	initially
O	ONCE
S	SINCE
sys	output
Y	PREV

Equations

$$\varphi^{sr}=(\theta^{e}\rightarrow\theta^{s})\wedge(\theta^{e}\rightarrow\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}((\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{H}}\rho^{e})\rightarrow\rho^{s}))\wedge(\theta^{e}\wedge\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}\rho^{e}\rightarrow(\bigwedge_{i\in 1..n}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{GF}}J_{i}^{e}\rightarrow\bigwedge_{j\in 1..m}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{GF}}J_{j}^{s})).$$

$$\texttt{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}} (lifting \& !dropping ->}\\ \texttt{((!dropping {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{U}} (!station \& !dropping)) | {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}} !dropping))}$$

Full text

1 Introduction

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification [30]. Rather than manually constructing an implementation and using model checking to verify it against a specification, synthesis offers an approach where a correct implementation of the system is automatically obtained for a given specification, if such an implementation exists.

As the correct-by-construction promise is attractive, much research effort has been invested and much progress has been achieved over the last two decades on reactive synthesis theory, algorithms, and tools. These include, e.g., the identification of expressive fragments of temporal logics that have efficient, symbolic synthesis solutions [5, 16, 17], various kinds of compositional synthesis [20], controller synthesis for probabilistic systems [7, 19], support for the addition of quantitative criteria [2], bounded synthesis [11], and tools such as RATSY [3] and Slugs [9], to list a few. Still, major challenges remain on the way to bringing the correct-by-construction promise to software engineering practice.

Some of these challenges are at the level of the specification language, i.e., the syntax, semantics, and expressiveness of reactive specifications. First, the language should have features that are specific to its use in the context of reactive synthesis, such as the explicit distinction between system and environment variables, guarantees, and assumptions. Second, careful balance should be found between the language’s usability to engineers, in writing and reading, on the one hand, and its formal expressive power on the other hand. Finally, the language alone may not be enough to address all challenges. Rather, a set of analyses and tools, beyond synthesis itself, specifically tailored for the new language and its use in an end-to-end reactive synthesis environment, is required, for example, in executing the synthesized controllers and in debugging them. In this paper we describe the results of our research efforts over the last three years, to start developing such language and tool set.

Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Beyond the kernel, it includes advanced language features like patterns, monitors, bounded integers, and arithmetic operations. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications, including, e.g., dealing with unrealizable and non-well-separated specifications.

The paper is structured as follows. Sect. 2 provides necessary background on linear temporal logic and its GR(1) fragment, which are required for the formal definition of Spectra semantics. Sect. 3 presents an example Spectra specification of an autonomous forklift robot (first reported in [23]). This specification illustrates many language features of Spectra and serves as a running example throughout the paper. Sect. 4 introduces a small language kernel of Spectra and defines the semantics of a specification as a GR(1) synthesis problem. Sect. 5 covers the language elements Spectra provides and defines their semantics via translations to the kernel. In Sect. 6 we give an overview of Spectra Tools.

2 Background

We provide background on linear temporal logic and synthesis, which is required for the definition of Spectra syntax and semantic. We continue with the notation that we use to define the grammar of Spectra.

2.1 Linear Temporal Logic and Synthesis

We repeat some of the standard definitions of linear temporal logic (LTL), e.g., as found in [5], a modal temporal logic with modalities referring to time. The syntax of LTL formulas is typically defined over a set of atomic propositions $\mathit{AP}$ with the future temporal operators X (next) and U (until).

Definition 1

*The syntax of LTL formulas over $\mathit{AP}$ is

\varphi::=~{}p~{}|~{}\neg\varphi~{}|~{}\varphi\vee\varphi~{}|~{}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\varphi~{}|~{}\varphi\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{U}}\varphi for $p\in\mathit{AP}$.*

For $\Sigma=2^{\mathit{AP}}$, a computation $u=u_{0}u_{1}..\in\Sigma^{\omega}$ is a sequence where $u_{i}$ is the set of atomic propositions that hold at the $i$-th position. For position $i$ we use $u,i\models\varphi$ to denote that $\varphi$ holds at position $i$, inductively defined as:

• •

$u,i\models p$ iff $p\in u_{i}$;

• •

$u,i\models\neg\varphi$ iff $u,i\not\models\varphi$;

• •

$u,i\models\varphi_{1}\vee\varphi_{2}$ iff $u,i\models\varphi_{1}$ or $u,i\models\varphi_{2}$;

• •

u,i\models\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\varphi iff $u,i{+}1\models\varphi$;

• •

u,i\models\varphi_{1}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{U}}\varphi_{2} iff $\exists k\geq i{:~{}}u,k\models\varphi_{2}$ and $\forall j,i\leq j<k{:~{}}u,j\models\varphi_{1}.$

We denote $u,0\models\varphi$ by $u\models\varphi$. We use additional LTL operators F (finally) where \texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}\varphi:=\text{\small{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{true}}}}~{}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{U}}~{}\varphi and G (globally), where \texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}\varphi:=\neg\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}\neg\varphi.

Finally, we also use PastLTL operators Y (previously, dual of X) and S (since, dual of U):

• •

u,i\models\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\varphi iff $i>0\wedge u,(i-1)\models\varphi$;

• •

u,i\models\varphi_{1}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{S}}\varphi_{2} iff $\exists k\leq i{:~{}}u,k\models\varphi_{2}$ and $\forall j,k<j\leq i{:~{}}u,j\models\varphi_{1}.$

We use additional PastLTL operators O (once), where \texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{O}}\varphi:=\text{\small{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{true}}}}~{}\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{S}}~{}\varphi, and H (historically), where \texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{H}}\varphi:=\neg\texttt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{O}}\neg\varphi.

LTL formulas can be used as specifications of reactive systems where atomic propositions are interpreted as environment (input) and system (output) variables. An assignment to all variables is called a state.

A strategy for an LTL specification $\varphi$ prescribes the outputs of a system that from its winning states for all environment choices lead to computations that satisfy $\varphi$. A specification $\varphi$ is called realizable if a strategy exists such that for all initial environment choices the initial states are winning states. The goal of LTL synthesis is, given an LTL specification, to find a strategy that realizes it, if one exists.

2.2 Generalized Reactivity of Rank 1 (GR(1))

GR(1) is a fragment of LTL, which has an efficient symbolic synthesis algorithm [5, 29] and whose expressive power covers most of the well-known LTL specification patterns of Dwyer et al. [8, 22]. GR(1) specifications include assumptions and guarantees about what needs to hold on initial states, on all states (safety), and infinitely often on every run (justice). A GR(1) synthesis problem consists of the following elements [5]:

• •

$\mathcal{X}$ input variables controlled by the environment;

• •

$\mathcal{Y}$ output variables controlled by the system;

• •

$\theta^{e}$ assertion over $\mathcal{X}$ characterizing initial environment states;

• •

$\theta^{s}$ assertion over $\mathcal{X}\cup\mathcal{Y}$ characterizing initial system states;

• •

$\rho^{e}(\mathcal{X},\mathcal{Y},\mathcal{X}^{\prime})$ transition relation of the environment, where $\mathcal{X}^{\prime}$ denotes a primed copy of variables $\mathcal{X}$, i.e., given a current state $\rho^{e}$ restricts the next input;

• •

$\rho^{s}(\mathcal{X},\mathcal{Y},\mathcal{X}^{\prime},\mathcal{Y}^{\prime})$ transition relation of the system, where $\mathcal{X}^{\prime}$ and $\mathcal{X}^{\prime}$ denote primed copies of variables $\mathcal{X}$ and $\mathcal{Y}$, i.e., given a current state and next input $\rho^{s}$ restricts the next output;

• •

$J^{e}_{i\in 1..n}$ justice goals of the environment;

• •

$J^{s}_{j\in 1..m}$ justice goals of the system.

A GR(1) synthesis problem is (strictly111For a comparison of strict realizability and implication realizability see [13, 5].) realizable iff the following LTL formula is realizable:

[TABLE]

Specifications for GR(1) synthesis have to be expressible in the above structure and thus do not cover the complete LTL. Efficient symbolic algorithms for GR(1) realizability checking and controller synthesis have been presented in [5, 29].

GR(1) synthesis has been used and extended in different contexts and for different application domains, including robotics [15, 21], scenario-based specifications [26], aspect languages [25], event-based behavior models [6], hybrid systems [10], and device drivers [34], to name a few.

2.3 Extended Notation for Context-Free Grammars

The Spectra language is defined by a context-free grammar. We now describe the grammar notation that we use throughout this document. An excerpt of the Spectra grammar shown in Fig. 1.

Production rules are enclosed in brackets and printed bold. As an example, the production rule for symbol $\langle$specElem$\rangle$ is defined in Fig. 1, l. 5 and referenced in l. 3 inside the definition of the production rule for symbol $\langle$spec$\rangle$. We use common multiplicity symbols for defining the number of repetitions of elements, where $*$ denotes zero or more repetitions, $+$ denotes at least one repetition, and $?$ denotes zero or one repetitions, i.e., the element is optional. As an example, the declaration of specification elements ($\langle$specElem$\rangle$, l. 3) is repeated at least once. Terminals of the grammar, that are also keywords of Spectra are printed in blue, e.g., the keywords spec, sys, and env. Other terminals are printed in grey, e.g., the semicolon (;, l. 7) after a variable declaration.

Grammar extensions

For readability and modular language definition, we introduce two extensions to the grammar notation. First, we introduce internal names for produced symbols, e.g., the name $elems$ for the list of $\langle$specElem$\rangle$ in Fig. 1, l. 3. We refer to these internal names when we describe well-formedness rules of Spectra documents. Second, we introduce the grammar-level keyword extends to denote the extension of production rules. As an example, the production $\langle$monitor$\rangle$ extends $\langle$specElem$\rangle$ in Fig. 1, l. 9. As a result of the extension, the symbol $\langle$monitor$\rangle$ can replace any occurrence of the symbol $\langle$specElem$\rangle$. Note the difference between $\langle$varDec$\rangle$ and $\langle$monitor$\rangle$ which are both alternatives for $\langle$specElem$\rangle$. The difference is that production rule $\langle$varDec$\rangle$ was included in the definition of $\langle$specElem$\rangle$ while the production rule $\langle$monitor$\rangle$ was added later. We use this extension mechanism when we add new language features. Finally, we introduce the grammar-level keyword replaces to denote that a new production rule replaces an existing production rule. As an example, the production $\langle$specWithImports$\rangle$ replaces $\langle$spec$\rangle$ in Sect. 5.8, Fig. 12, l. 1. As a result of the replacement, the symbol $\langle$specWithImports$\rangle$ can replace any occurrence of the symbol $\langle$spec$\rangle$.

Special productions

We make use of three standard, primitive productions that we do not define in any production rule. These are $\langle$file$\rangle$ for file names, $\langle$name$\rangle$ for names of elements, and $\langle$int$\rangle$ for integers.

Simplification

The parts of the Spectra grammar we show in Sect. 4 and Sect. 5 present a simplified version of the grammar we use in the implementation of Spectra tools described in Sect. 6. For the purpose of presentation we have simplified the production rules. As an example, it is common to encode operator precedence directly into production rules to simplify parsing of specifications. This implementation related formulation blows up the grammar of expressions as every operator might require a separate production rule. We present a simplified version of the grammar and define operator precedence when we describe each language element.

3 Example

We will introduce Spectra on the example of a specification for a Lego forklift robot shown on the left side of Fig. 2. The forklift is an actual Lego robot222Robot based on these building instructions: http://www.nxtprograms.com/NXT2/forklift/steps.html we have constructed and experimented with in our lab. We first reported on this case study in [23].

3.1 Forklift Overview and Architecture

The forklift shown in Fig. 2 has a sensor to determine whether it is at a station, two distance sensors to detect obstacles and cargo, and an emergency button to stop it. It has two motors to turn the left and right wheels and one motor to lift the fork. Consider an initial set of informal requirements for the behavior of the forklift:

Do not run into obstacles. 2. 2.

Only pick up or drop cargo at stations. 3. 3.

Always keep on delivering cargo. 4. 4.

Never drop cargo at the station where it was picked up. 5. 5.

Stop moving if emergency off switch is pressed.

The logical software architecture of the forklift is depicted as a component and connector model in Fig. 2 (b). The components on the left side are hardware wrappers that read sensor values and publish them as messages on their output ports. The output ports of these sensor components are connected to input ports of component Controller. The output ports of component Controller are connected to three components on the right that receive commands and encapsulate access to the motors of the forklift. The datatypes of input and output ports as well as their names are written on the ports of component Controller. Datatypes other than boolean are defined as enumerations in Fig. 3.

The execution of the software components of the robot is performed in a cycle: read sensor data, execute controller, perform actions. All components are executed without any delay. This execution variant uses a technique inspired by Raman et al. [31] to synthesize a reactive controller for continuous control. The setting requires the synthesized controller to become aware whether actions have completed or not. In our case driving actions get feedback from distance sensors and a feedback signal from the lift motor acknowledges completion of the motor’s actions (see Fig. 2).

3.2 Forklift Specification in Spectra

A specification for the reactive behavior of the forklift controller is shown in Lst. 1 and Lst. 2. This specification is a subset of the complete specification from [23].333We have slightly adapted the specification to use new language elements of Spectra, which where not available yet for [23].

Lst. 1 shows the declaration of environment controlled input variables (ll. 1-5) and system controlled output variables (ll. 7-9). The names of environment variables in Lst. 1 correspond to the names of input ports and the names of system variables correspond to the names of output ports of component Controller from Fig. 2. Similarly, the enumeration types in Lst. 1, ll. 11-13 correspond to the enumeration types shown in Fig. 3. Finally, the remainder of Lst. 1 introduces some useful defines, e.g., backing is defined as an abbreviation of the expression mLeft = BWD & mRight = BWD, which states that both motors receive the BWD command.

Lst. 2 shows a selection of assumptions, a monitor, and guarantees of the forklift specification. As an example, the first assumption named stationsDontMove, expresses that on all transitions between states (operator trans) if the motors are stopping then the sensor input for detecting a station does not change in the next state (ll. 2-3). The monitor waitingForLifting keeps track whether the forklift has recently issued a lifting command LIFT or DROP and has not yet received an acknowledgment through input liftAck. The monitor is referenced inside a response pattern assumption in Lst. 2, l. 18. This assumption expresses that waitingForLifting is always followed by a an acknowledgment liftAck after a finite time444In LTL this would be expressed as G (waitingForLifting -> F liftAck). Note however, that this formula is syntactically not part of the GR(1) fragment..

Next, Lst. 2 contains guarantees expressing the five high-level requirements for the controller of the forklift. As an example, the first requirement to not hit obstacles is formulated as the guarantee dontHitObstacles in Lst. 2, ll. 21-22. It states that all transitions from sensing an obstacle or a low obstacle are required to go to states where the forklift does not go forward. The third requirement to always keep on delivering cargo is formulated in Lst. 2, ll. 29-30. The guarantee states that always eventually (keyword alwEv) the forklift drops its cargo unless it is blocked by obstacles (note that blocking the forklift infinitely many times could prevent it from delivering cargo and we thus had to weaken requirement (3)).

Finally, the specification in Lst. 2 shows the monitor loaded and the guarantee restrictLifting. These were added during experimenting with synthesized controllers. What happened was that the synthesized controller decided to lift cargo when it had already lifted cargo. This physically destroyed the lifting mechanism of the robot. We realized that additional restrictions are necessary and the guarantee restrictLifting thus encodes that the forklift should never lift cargo when it already has cargo loaded and it should never drop cargo when it does not have cargo loaded.

4 Spectra Kernel

Spectra is based on a small kernel language for writing specifications. The Spectra kernel contains only the essential elements to formulate GR(1) synthesis problems. Specifically, these language elements are Boolean environment variable declarations, Boolean system variable declarations, assumptions, and guarantees. We now introduce the syntax of the Spectra kernel and then give the semantics of specifications as GR(1) synthesis problems.

4.1 Syntax

A grammar of the Spectra kernel is shown in Fig. 4. Every valid specification can be produced from the production rule $\langle$spec$\rangle$ of the kernel grammar (and its extensions we present in Sect. 5).

Every specification starts with the keyword spec and a name. The name of a specification is only informative and has no technical meaning. A specification contains one or more specification elements $\langle$specElem$\rangle$. Specification elements of the Spectra kernel are variable declarations (Fig. 4, l. 7), assumptions (Fig. 4, l. 11), and guarantees (Fig. 4, l. 16).

Variable declarations introduce variables controlled by the environment (keyword env) or by the system (keyword sys). Variables have a type and a name. The only type available in the kernel is boolean (Fig. 4, l. 9).

Assumptions have an optional name and can be of three kinds. They are either initial assumptions (keyword ini), safety assumptions (keyword trans), or justice assumptions (keyword alwEv).555Other GR(1)-based specification languages use the LTL operator G for trans and GF for alwEv. This leads to confusion as their semantics usually does not match the LTL semantics. All assumption kinds are formulated by expressions $\langle$exp$\rangle$ (Fig. 4, l. 21). Expressions follow standard definitions of propositional expressions. The unary operators of expressions are negation and next, the binary operators are standard Boolean operators and equality, and the primary expressions are true, false, and references to variables (Fig. 4, l. 30). The precedence of operators in expressions from strongest binding to weakest is !, next, =, &, —, ¡-¿, -¿. As usual, binary operators associate from left to right.

Guarantees are defined analogously to assumptions with the exceptions of the keyword gar instead of asm and differences in well-formedness rules.

Well-formedness rules

The names of variables, assumptions, and guarantees have to be unique. An initial assumption cannot reference system variables. A safety assumption cannot nest references to system variables in the scope of the next operator. A next operator cannot be (transitively) nested inside a next operator.

Scopes

The Spectra kernel contains three kinds of named elements: variables, assumptions, and guarantees. The scope of variable names is global, i.e., the names of variables have to be unique and variables can be referenced from anywhere in the specification. The scope of names of assumptions and guarantees is also global but they cannot be referenced from anywhere inside the specification.

4.2 Semantics

The semantic domain of the Spectra kernel language are GR(1) synthesis problems. We define the semantics of the Spectra kernel by translating every well-formed specification to a GR(1) synthesis problem.

Given a Spectra specification $m$ its semantics is defined by the following GR(1) synthesis problem:

• •

$\mathcal{X}$ is the set of all variables declared in $m$ with the keyword env;

• •

$\mathcal{Y}$ is the set of all variables declared in $m$ with the keyword sys;

• •

$\theta^{e}$ is the conjunction of the semantics of all initial assumptions;

• •

$\theta^{s}$ is the conjunction of the semantics of all initial guarantees;

• •

$\rho^{e}(\mathcal{X}\cup\mathcal{Y},\mathcal{X})$ is the conjunction of the semantics of all safety assumptions;

• •

$\rho^{s}(\mathcal{X}\cup\mathcal{Y},\mathcal{X}\cup\mathcal{Y})$ is the conjunction of the semantics of all safety guarantees;

• •

$J^{e}_{i\in 1..n}$ is the set of the semantics of all justice assumptions;

• •

$J^{s}_{j\in 1..m}$ is the set of the semantics of all justice guarantees.

To obtain the semantics of assumptions and guarantees we translate their expression $\langle$exp$\rangle$ to assertions in the GR(1) synthesis problem. This translation is straight forward on the structures of $\langle$exp$\rangle$. The symbols of Boolean operators of $\langle$unaryOp$\rangle$ and $\langle$binaryOp$\rangle$ are translated to their counterparts in assertions. The keywords false and true of $\langle$primExp$\rangle$ are translated to a contradiction and a tautology, respectively. A variable reference of $\langle$primExp$\rangle$ is translated to an assertion over Boolean variable from $\mathcal{X}$ and $\mathcal{Y}$ with the referenced name. Finally, the unary operator next substitutes all variables from $\mathcal{X}$ and $\mathcal{Y}$ in its scope with corresponding primed variables from $\mathcal{X}^{\prime}$ and $\mathcal{Y}^{\prime}$.

5 Spectra Language Elements

We now present the Spectra language elements beyond the kernel language. For each language element we discuss the motivation to have it in the language, present its syntax as a grammar that extends the Spectra kernel, list well-formedness rules of the extended language, discuss the scope of newly introduced named elements, and finally present the semantics of new elements.

Note that we define the semantics of Spectra language elements by a translation to Spectra without the new language element. A direct translation to the Spectra kernel would be possible but often more complicated because all combinations of language elements would have to be considered in the translation, e.g., references to defines can appear in parameters of predicates. Instead, we present modular translations that allow for the combination of any subset of Spectra language elements. The application of all semantics defining translations will result in a specification in the Spectra kernel language. This design also ensures that extensions of the Spectra kernel beyond GR(1) will directly support the new Spectra language elements. 666Examples of extensions are GR(k) specifications [28] or cooperative synthesis [4].

5.1 Enumerations and bounded Integers

5.1.1 Motivation

The Spectra kernel only contains Boolean variables. However, in many cases it is more convenient to use enumerations of values to define the type of a multi-valued variable. As an example, we define the enumeration type MotorCmd in Lst. 1, l. 12 with values FWD, STOP, and BWD. In expressions, these values can be used and compared to each other and to variables of the same type, e.g., see Lst. 1, ll. 16 for the definition of backing where both motor variables have the value BWD.

Similarly, some values are best modeled using integers. Spectra supports a bounded integer type with lower and upper bounds. An example appears in Lst. 3 where the variable speed is of integer type with values from 0 to 50. In expressions, integer variables can be compared with primitive values, e.g., see Lst. 3, l. 3 where the value of variable speed is restricted to at most 6 when close to cargo. Bounded integers can also be compared to arithmetic expressions and other integer variables even when their bounds are different.

5.1.2 Syntax

The syntax of enumerations and bounded Integers is shown in Fig. 5. Enumerations are defined by production rule $\langle$enumType$\rangle$ and consist of a list of names enclosed in curly brackets {, }. Names of enumeration values can be referenced as primary expressions (Fig. 5, ll. 5-6), e.g., they can also be used in expressions.

Bounded Integer types in Spectra start with Int followed by lower and upper bounds in parenthesis (Fig. 5, ll. 9-10). We also add arithmetic operators for addition, subtraction, multiplication, division, and modulo to Spectra, together with inequalities in Fig. 5, l. 12-13. The inequalities bind with the same priority as equality and the arithmetic operators bind stronger than all previously introduced operators. Finally, we add arithmetic negation as a unary operator and integer constants as primary expressions in Fig. 5, ll. 15-19.

Well-formedness rules

The names of enumeration values must be unique and different from variable names. Equality is the only comparison allowed for enumeration values and variables of enumeration type and Boolean type. The upper bound $upper$ of a bounded integer must be strictly greater than its lower bound $lower$. The new operators $\langle$intBinaryOp$\rangle$ and $\langle$intUnaryOp$\rangle$ can only be used in arithmetic expressions constructed from these operators, primitive values $\langle$intVal$\rangle$, and references to Integer variables $\langle$varRef$\rangle$.

5.1.3 Semantics

We define the semantics of enumerations and bounded Integers by a translation into Spectra without enumerations and bounded Integers. We translate every variable of an enumeration type with $n=|vals|$ values to $\lceil\log_{2}(n)\rceil$ Boolean variables. To every value in $vals$ we assign one combination of values of the new variables. We add initial and safety constraints to the specification that the new variables represent one of the defined values (important for $2^{\lceil\log_{2}(n)\rceil}>n$). We translate every equality expression involving enumerations to equivalent expressions over the Boolean variables that encode them.

Similarly, we translate every bounded integer variable to ${\lceil\log_{2}(upper-lower)\rceil}$ Boolean variables. For the translation of bounded arithmetic expressions, we employ an encoding inspired by [1].

5.2 Defines and type definitions

5.2.1 Motivation

Specifications often contain sub-expressions that reoccur many times. In the example of the forklift, many guarantees and assumptions refer to stopping both motors, formally mLeft = STOP & mRight = STOP. Once these reoccurring expressions get longer and more complicated, the overall specification becomes harder to read and difficult to maintain, e.g., when updating a condition. To support more concise specifications and to simplify the maintenance of reoccurring sub-expressions, Spectra introduces defines. In the forklift example a define introduces the name stopping for the expression mLeft = STOP & mRight = STOP. Assumptions and guarantees then use stopping as a reference to the define.

Similarly, several variables in a specification may be of the same type. For example, in the forklift specification the left and right motors both have the enumeration type {FWD, STOP, BWD}. Here, to support more concise specifications and to simplify the maintenance of reoccurring types, Spectra introduces type definitions. In the forklift example, the type MotorCmd is defined by a type definition in Lst. 1, l. 12 and referenced as the type of system variables mLeft and mRight in ll. 7-8.

5.2.2 Syntax

The syntax of defines and type definitions is shown in Fig. 6. Defines are specification elements and thus appear as top level elements inside specifications. Defines have a name and an expression. References to defines $\langle$defRef$\rangle$ are primary expressions (Fig. 6, l. 4).

Type definitions (Fig. 6, l. 8) are also specification elements and thus appear as top level elements inside specifications. Type definitions have a name and a type. References to type definitions $\langle$typeRef$\rangle$ are treated as types (Fig. 6, l. 12).

Well-formedness rules

The names of defines and type definitions must be unique names of elements of the specification. Defines with the operator next may not be used in expressions where next is not allowed, e.g., defines with the operator next may not be nested inside the operator next. Note that the expression of a define is not required to evaluate to a Boolean value. However, the semantics of a specification with defines and type definitions has to be a well-formed specification.

Scopes

The names of defines and type definitions have the same scope as the names of environment and system variables defined in the Spectra kernel. The names of defines are visible to other defines.

5.2.3 Semantics

We define the semantics of defines and type definitions by a translation into Spectra without defines and type definitions. Every reference to a define is replaced by the expression of the define. Every reference to a type definition is replaced by the type of the type definition.

5.3 State Invariants

5.3.1 Motivation

Some constraints should hold in all states, e.g., the guarantee that the forklift lifts and drops cargo only at stations. These assumptions and guarantees could be expressed as combinations of initial and safety constraints, however we chose to introduce a separate keyword for state invariants to make specifications easier to read and write.777Note that the common keyword G used for trans in other GR(1) specification languages is often confused for defining state invariants (as the LTL semantics would suggest) leading to problems. A discussion is outside the scope of this paper.

5.3.2 Syntax

We show the syntax of state invariants in Fig. 7. State invariants are temporal constraints by extension of $\langle$tempConstraint$\rangle$ and can be used anywhere these constraints appear, e.g., in assumptions and guarantees or in patterns (see Sect. 5.7).

Well-formedness rules

The expression $\langle$exp$\rangle$ of a state invariant may not contain the operator next. A state invariant of the environment, i.e., used in an assumption, may not contain system variables.

5.3.3 Semantics

We define the semantics of state invariants by a translation of state invariants to Spectra without state invariants. Every state invariant is translated into an initial constraint with the same expression $\langle$exp$\rangle$ and a safety constraint (with keyword trans) with the expression $\langle$exp$\rangle$ nested inside the operator next. Together the two constraints ensure that the invariants holds in the initial state and in every successor state.

5.4 PastLTL

5.4.1 Motivation

Assumptions and guarantees define constraints on reactive behavior by relating the inputs and outputs of the current state to those of the next state. However, in some situations the restriction to only current and next inputs and outputs becomes limiting. As an example, the forklift is not allowed to lift cargo when it has cargo lifted already. Yet, in our example, there is no input indicating whether cargo is currently loaded888The example introduces a monitor for this purpose. Here we discuss an alternative based on PastLTL.. Interestingly, it is easy to determine from past observations whether cargo is currently loaded: if in the previous state cargo has not been dropped since it had been lifted in the past then cargo is currently loaded. We can formalize the above using PastLTL operators supported by Spectra: PREV (lift!=DROP SINCE lift=LIFT).

5.4.2 Syntax

We show the syntax of PastLTL expressions in Fig. 8. Spectra supports three unary PastLTL operators and one binary PastLTL operator. For all operators Spectra also provides a one letter abbreviation (preceding the operator name in Fig. 8).

Well-formedness rules

All operands of PastLTL operators must evaluate to Boolean values (all PastLTL expressions evaluate to Boolean values).

5.4.3 Semantics

We define the semantics of PastLTL by a translation of PastLTL to Spectra without PastLTL. Recall from the preliminaries that the two operators PREV and SINCE provide full expressiveness of PastLTL; all other PastLTL operators can be defined in terms of these two. We will show the translation for the operators PREV and SINCE.

Given the PastLTL expression PREV $\varphi$, we create a Boolean system variable aux with a fresh name. We then add the initial guarantee ini !aux and the safety guarantee trans next(aux) <=> $\varphi$. Technically, the variable aux stores the previous valuation of $\varphi$. Finally, we replace all occurrences of PREV $\varphi$ with a reference to the new variable aux.

Given a PastLTL expression $\varphi$ SINCE $\psi$, we create a Boolean system variable aux with a fresh name. We then add the initial guarantee ini aux <=> $\psi$ and the safety guarantee trans next(aux) <=> (aux & next($\varphi$) | next($\psi$)). The variable aux is true if $\psi$ holds or if aux was true before and $\varphi$ holds, i.e., if $\varphi$ holds since $\psi$ was true in the past. Finally, we replace all occurrences of $\varphi$ SINCE $\psi$ with a reference to the new variable aux.

5.5 Predicates

5.5.1 Motivation

Sometimes repeating parts appearing in specifications differ in sub-expressions. In these cases defines from Sect. 5.2 cannot be used to avoid repetition. For these cases we introduce predicates, which can instantiate sub-expressions with their parameters.

As an example, consider an extension of the forklift to load items in the front and in the back, as shown in Lst. 4. To know whether an item is loaded we express that it is loaded in the front or loaded in the back. To avoid repetition we can extract the expression whether an item is loaded into a predicate with a parameter of the item as shown in Lst. 4, ll. 5-7. The predicate can then be instantiated, e.g, in a guarantee as shown in l. 10, for different items.

5.5.2 Syntax

We show the syntax of predicate definitions and predicate instantiations in Fig. 9. The grammar starts with the syntax for predicate definitions $\langle$predicate$\rangle$, which are specification elements and thus appear as top level elements inside specifications. Predicate definitions have a name followed by a list of typed parameters $\langle$typedParam$\rangle$. The body of a predicate definition is an expression.

Predicate instances $\langle$predInst$\rangle$ (Fig. 9, ll. 11-12) are primary expressions. Instances reference the name of a predicate and provide expressions for each parameter of the predicate.

Well-formedness rules

All parameters of predicate instances must be expressions that evaluate to the type declared in the predicate definition. The body of the predicate must be an expression that evaluates to Boolean. The body of a predicate cannot (also not transitively, e.g., through predicate instances or defines) contain an instance of the predicate itself.

Scopes

The names of predicates have the same scope as the names of environment and system variables defined in the Spectra kernel. As a result, the names of predicates are visible to other predicates. The names of parameters of the predicate are only visible inside the body of the predicate.

5.5.3 Semantics

We define the semantics of predicate instantiations and predicates by a translation into Spectra without predicates. Every predicate instance is translated into a Boolean expression. Technically, we replace a predicate instance by a copy of the body of the predicate. In the copy, we replace references to predicate parameters by the expressions provided for each parameter.

5.6 Monitors

5.6.1 Motivation

Assumptions and guarantees define constraints on reactive behavior by relating the inputs and outputs of the current state to those of the next state. In some situations the restriction of referencing only inputs and outputs becomes limiting. As an example, the forklift is not allowed to lift cargo when it has cargo lifted already. However, in our example, there is no input variable indicating whether cargo has been lifted. As a solution, Spectra introduces monitors which come with a definition of how their value is updated at every execution step. As an example, the monitor loaded (Lst. 2, l. 41-46) is of type boolean and its value is updated on receiving acknowledgments of lift actions. This monitor is used in a guarantee (Lst. 2, l. 50) to prevent lifting cargo when cargo is already lifted and to prevent dropping cargo when no cargo was lifted.

5.6.2 Syntax

The syntax of monitors is shown in Fig. 10. Monitors are specification elements and thus appear as top level elements inside specifications. Monitors have a type and a name. The body of a monitor consists of initial and safety constraints.

References to monitors $\langle$monRef$\rangle$ are primary expressions (Fig. 10, l. 8).

Well-formedness rules

The names of monitors must be unique names of elements of the specification. The body of a monitor may not contain justice constraints. The expression $\langle$exp$\rangle$ of an initial constraint may not include the unary operator next. The semantics of the constraints in the body of the monitor must assign a unique value to the monitor in any step and it must not restrict any other variable (when seen as an automaton with the monitor variable as states and all other variables as input, the defined automaton has to be deterministic and complete).999This property is difficult to check or ensure syntactically.

Scopes

The names of monitors have the same scope as the names of environment and system variables defined in the Spectra kernel. Importantly, the name of a monitor is visible in the constraints of the monitor.

5.6.3 Semantics

We define the semantics of monitors by a translation of monitors to Spectra without monitors. For every monitor definition we create a system variable with the name and type of the monitor. All monitor constraints become guarantees. All references to the monitor become references to the new system variable with the same name and type.

5.7 Patterns

5.7.1 Motivation

Specifications of reactive systems require engineers to express complex temporal relations between environment and system states. LTL provides great expressiveness for temporal relations. However, some basic relations lead to long formulas, which might be complicated to read and challenging to write correctly. As an example, consider the guarantee that the forklift should leave the station (!atStation) between lifting cargo (lifting) and dropping cargo (dropping). This guarantee can be expressed in LTL as follows101010LTL formula taken from the patterns catalog of Dwyer et al. [8]. There might be multiple ways to express an equivalent guarantee.:

[TABLE]

Note that assertions on relevant states, e.g., lifting or dropping, are repeated and that LTL operators are nested, e.g., the operator until (U) is nested inside the scope of the first globally operator (G).

Dwyer et al. [8] have identified 55 LTL specification patterns which are common in industrial specifications. They have suggested a classification and natural language descriptions for the identified patterns. The example above is one of their patterns and would be transcribed as:

[TABLE]

We have investigated patterns for GR(1) synthesis in [22]. We have shown that 52 of these 55 LTL specification patterns can be supported as assumptions and guarantees for GR(1) synthesis. In Spectra, the example guarantee is formulated as a pattern definition (Spectra comes with a catalog of pattern definitions for all 52 supported LTL specification patterns) and the pattern instantiation shown in Lst. 2, l. 18-19.

Note that Spectra patterns are not limited to the 52 patterns defined in the catalog. Spectra provides engineers with means to define and reference their own patterns.

5.7.2 Syntax

The syntax of patterns is shown in Fig. 11. The grammar starts with the syntax for pattern definitions $\langle$pattern$\rangle$, which are specification elements and thus appear as top level elements inside specifications. Pattern definitions have a name followed by a list of parameter names. The body of a pattern definition can declare variables local to the pattern and temporal constraints. A pattern may contain any number of initial and safety constraints, but it must contain exactly one justice constraint.

Pattern instances $\langle$patInst$\rangle$ (Fig. 11, ll. 12-13) are primary expressions. Instances reference the name of a pattern and provide expressions for each parameter of the pattern.

Well-formedness rules

The body of a pattern contains exactly one justice constraint. The expression $\langle$exp$\rangle$ of an initial or justice constraint may not include the unary operator next. The expression $\langle$exp$\rangle$ of a safety constraint may only include references to pattern variables $vars$ in the scope of the operator next. The semantics of the initial and the safety constraints must assign a unique value to all pattern variables in any step and it must not restrict any other variable (when seen as an automaton with the pattern variables as states and all other variables as input, the defined automaton has to be deterministic and complete).111111This property is difficult to check syntactically.

The production $\langle$patInst$\rangle$ may only appear exclusively as a primary expression of assumptions or guarantees, i.e., it cannot appear inside another expression and not in any other place in a specification.

Scopes

The names of pattern parameters $params$ are only visible inside the body of the pattern delimited by {, }. The names of pattern variables $vars$ are only visible inside the body of the pattern delimited by {, }. The names of patterns are visible beyond specification files and thus can be imported, see 5.8.

5.7.3 Semantics

We define the semantics of patterns by a translation of pattern instances and patterns to Spectra without patterns. For every pattern instance we create a copy of all pattern variables as system variables with a fresh name and the same type. We instantiate pattern constraints by replacing references to pattern variables with references to the fresh names and by replacing references to variable names with copies of the corresponding expression of the parameter values from $pVals$.

Instantiated initial pattern constraints become initial guarantees; instantiated safety pattern constraints become safety guarantees; the instantiated justice constraint becomes a justice assumption if the pattern instance is contained inside an assumption; and the instantiated justice constraint becomes a justice guarantee if the pattern instance is contained inside a guarantee (see also [22]).

5.8 Imports

5.8.1 Motivation

We have motivated many language features of Spectra based on reuse. In all cases a reuse within a single specification makes sense. In some cases, a reuse across specifications is also desirable. As an example, patterns, e.g., from the catalog of Dwyer et al. [8] or domain specific pattern collections for mobile robots, are general and should be useful for other specifications as well. Thus, to support reuse across specifications, we have added an import mechanism to Spectra. A specification can import other specifications to use their patterns and predicate definitions (see Sect. 5.5 and Sect. 5.7).

5.8.2 Syntax

The syntax of imports is shown in Fig. 12. We extend specifications with import statements that each start with the keyword import, contain a filename in quotation marks, and end with a semicolon.

Well-formedness rules

The names of patterns and predicates in all imported and in the current Spectra files must be unique. The bodies of all (transitively) imported predicates may only contain references to other predicates and their parameters (e.g., they may not reference system or environment variables or defines from other specifications121212Note that these references from predicates are allowed in general (see Sect. 5.5) and are very convenient to use.).

5.8.3 Semantics

We define the semantics of imports by a translation of imports to Spectra without imports. Given a Spectra file with imports, we copy all (transitively) referenced patterns of the imported files into the current file. We also copy all (transitively) referenced predicates into the current file and remove the import statements.

6 Spectra Tools

Spectra comes with Spectra Tools, a set of analyses and tools packaged as an extensible set of Eclipse plug-ins. An eclipse editor for Spectra is implemented using XText [35]. All symbolic representations and operations are carried out using a BDD library (several libraries can be used, including e.g., CUDD [32]).

Spectra Tools is available from [33], together with a user guide and many example specifications. We encourage the interested reader to try it out.

We now give an overview of the different analyses and tools.

6.1 Synthesis of Concrete and Symbolic Controllers

First and foremost, Spectra Tools includes two synthesis features, which take the specification as input and output a correct-by-construction controller, if one exists. After a series of basic checks and translations, synthesis is performed symbolically following the algorithms described in [5], with performance heuristics adapted from [12].

The engineer can choose the form of the synthesis output. First, the output may be a concrete controller, which is further presented in the console or used for application-specific code generation. As the concrete controller is complete for the environment and deterministic for the system, i.e., in every state it accepts all inputs from the environment and deterministically responds with an assignment to the system variables, it allows for straightforward application-specific code generation.

Second, the output may be a symbolic controller, following ideas from [5]. Roughly, the symbolic controller consists of two functions, represented using BDDs. The first BDD describes the set of allowed initial states, while the second describes the controller’s allowed transitions. The engineer can save it and execute it, see below in Sect. 6.2.

One advantage of the concrete controller output is that it enables direct code generation. When it is very small, it is also simple to read and inspect. However, it does not scale. Its generation is slow, due to the need to enumerate all states, and its size is beyond what any engineer can manually inspect. Moreover, sometimes the size of straightforward generated code prohibits compilation. All these disadvantages motivated us to design and implement the symbolic controller.

6.2 Controller Execution

Spectra Tools provides several different means to execute and simulate the synthesized controller, concrete or symbolic.

First, code generation from concrete controllers. The concrete controller is directly translated to a simple implementation of a state machine. We currently have application-specific Java code generation tailored to run on Lego NXT robots.

Second, an execution API for symbolic controllers. The symbolic controller is loaded and iteratively called, at runtime, with the current inputs from the environment, to provide the next outputs (assignment to system variables). This runtime environment requires a BDD library, however its use is limited to single calls to extract a satisfying assignment. Our students have used it to execute their Lego robots (where the actual execution runs on a Raspberry Pi) and developed some small example standalone Java applications.

Third, a simulation environment, inside Eclipse, we call Controller Walker. The Walker uses the execution API for symbolic controllers. It shows the engineer the current state of the controller (values of environment and system variables) and allows her to ‘walk’, step by step, forward and backward, on its transition system. It serves as the main tool for closely inspecting the behavior of the synthesized controller.

6.3 Analyses of Unrealizability

One of the challenges of writing specifications for synthesis is unrealizability. Spectra Tools provides several means to deal with unrealizable specifications.

First, identifying unrealizability and computing an unreazlizable core. When synthesis fails due to unrealizability, the engineer receives an appropriate message. Then, she can ask to compute an unrealizable core, i.e., a locally minimal subset of the specification’s guarantees, which already makes it unrealizable. Spectra Tools computes the core using DDmin [36], following ideas described in [14] and heuristics investigated in [12]. The core guarantees are highlighted on the specification (using Eclipse standard editor markers). The user guide in [33] includes example screenshots.

Second, computing a concrete counter strategy. Given an unrealizable specification, the engineer can generate a concrete counter-strategy, which specifies one strategy for the environment to force any system to violate the specification. The counter-strategy is computed by playing a Rabin game, following the algorithm from [14, 27]. The counter-strategy can be presented in simple textual format on the console. It can also be interactively simulated, together with the JVTS, see next.

Third, computing a JVTS. As concrete counter-strategies may be very large and difficult to understand, in recent work [18] we have presented the Justice Violations Transition System (JVTS), a symbolic representation of a counter-strategy. The JVTS is much smaller and simpler than its corresponding concrete counter-strategy. Moreover, it is annotated with invariants that explain how the counter-strategy forces the system to violate the specification. We compute the JVTS symbolically, and thus more efficiently, without the expensive enumeration of concrete states. Finally, we provide the JVTS with an on-demand interactive concrete and symbolic play. See [18].

6.4 Analyses of Non-Well-Separation

One way a controller may satisfy a specification is by preventing the environment from satisfying the assumptions, without satisfying the guarantees. Although valid, this solution is usually undesired. Specifications that allow it are called non-well-separated [13]. In [24] we have shown that non-well-separation is a common problem in specifications.

Spectra Tools provides means to identify and investigate non-well-separation. The engineer can check her specification for well-separation. If the specification is not well-separated, information about the specific type of non-well-separation found is displayed. Furthermore, the engineer can ask to compute a strategy that shows how the environment can be forced to violate its assumptions. Finally, a non-well-separation core, a minimal set of assumptions that lead to non-well-separation, can be computed and highlighted on the specification (using Eclipse standard editor markers). See [24].

6.5 Additional Analyses

Spectra Tools provides several additional analyses that aim at helping engineers write higher quality specifications. We give some examples below.

First, some assumptions and guarantees may be trivially false or trivially true. Clearly, such assumptions or guarantees point to a problem in the quality of the specification, even when they are just redundant. We provide a basic analysis that looks for such trivial assumptions and guarantees and highlights them to the engineer.

Second, some Spectra language elements are not easy to write correctly. For example, monitors contain constraints inside their body that should only restrict the monitor variable itself. However, it is easy to write constraints that are contradicting or constraining other variables. These malformed monitors might lead to unrealizability of the whole specification. Spectra Tools implements checks and highlighting for monitors to rule out this reason for unrealizability.

Third, as one would expect from an engineer-friendly editor for writing and reading specifications, Spectra Tools editor provides an outline, syntax coloring, type checks, and specification completion. These are implemented by taking advantage of the rich XText [35] APIs.

7 Conclusion

The definition and development of Spectra and Spectra Tools are part of the SYNTECH project 131313SYNTECH: http://smlab.cs.tau.ac.il/syntech/, which aims at bridging the gap between the theory and algorithms of reactive synthesis on the one hand and software engineering practice on the other. We use the language and tool set to learn about the challenges in bridging this gap and to develop and evaluate possible means to address them.

In this paper we presented the Spectra language. Spectra provides means to specify assumptions and guarantees for a reactive system, using high-level constructs such as patterns and monitors. We further presented an overview of Spectra Tools, a set of analyses and tools providing synthesis into correct-by-construction controllers, means to execute and simulate the synthesized controllers, and additional analysis aimed at helping engineers write higher-quality specifications.

Acknowledgements

We thank Elizabeth Firman, Aviv Kuvent, Or Pistiner, Rafi Shalom, Ilia Shevrin, and Yoni Wolbe for their contribution to the implementation of Spectra Tools.

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 638049, SYNTECH).

Appendix A Spectra Grammar

We show a combination of the grammars of the Spectra kernel from Fig. 4 and of all extensions from Sect. 5 in Fig. 2. As mentioned in Sect. 2.3 this grammar includes simplifications for readability and in order to fit it on a single page.

Spectra provides more verbose alternative to most keywords shown in Tbl. 1. We have decided to use the shorter keywords in Sect. 4 and Sect. 5 as they seem to be preferred when writing specifications.