Input Language/Syntax of Slugs and Usage

The slugs tool checks whether there exists a (finite-state) implementation for some temporal specification and can compute an implementation in case of a positive answer. It supports a slight extension of the the set of Generalized Reactivity(1) specifications. The online version supports the structuredslugs format, which allows to write specifications using infix operators and integer variables as input and output variables.

An input specification to the slugs tool is in textual format, where every line starting with a # is interpreted as a comment. Empty lines are permitted as well. The sections of a slugs specification is partitioned into sections. The following section types are available.

[INPUT]: The lines after this section header denote the atomic input propositions and integer variables.
[OUTPUT]: The lines after this section header denote the atomic output propositions and integer variables.
[ENV_TRANS]: After this section header, the environment safety assumptions are given.
[SYS_TRANS]: After this section header, the system safety guarantees are given.
[ENV_INIT]: After this section header, the environment initialization assumptions are given.
[SYS_INIT]: After this section header, the system initialization guarantees are given.
[ENV_LIVENESS]: After this section header, the environment liveness assumptions are given.
[SYS_LIVENESS]: After this section header, the system liveness guarantees are given.

The first two section types are purely declarative, while the others contain lines that define parts of the specification that we want to synthesize.

For more details on the slugs tool, you can consult its tool paper. The appendix of the paper (author-archived version only) gives an additional example for a slugs specification.

Click here to download the author-archived version of the paper. Copyright by Springer Verlag. The original publication is available at www.springerlink.com

Declaring Input and Output variables

In reactive synthesis, we synthesize finite-state machines with a finite set of input variables and a finite set of output variables. In slugs specifications, they are given in the [INPUT] and [OUTPUT] sections of the specification. The name of every input or output bit is given on a seperate line. Allowed characters in the variable names are upper- and lower-case letters as well as numbers. Every variables has to start with a letter. The words “True” and “False” cannot be used as variable names. An integer variable is declared in by an expression of the form <name>:<lower-bound>…<upper-bound>+.

As an example, the following specification fragment declares that we are interested in a finite-state machine reading two input propositions x and y in every step of their execution and writing to the Boolean variable a as well as to an integer variable v with values between 5 and 10 (so there are 6 possible variable valuations for v).

[INPUT]
x
y

[OUTPUT]
a
v:5...10

Defining Initial Conditions for the Input and Output variables

In Generalized Reactivity(1) Synthesis, we give some constraints over the initial values of all variables. Constraints are given as boolean formulas using the operators & (conjunction), | (disjunction), ! (negation), -> (implication), and <-> (biimplication). Constraints over the initial input variable valuations are given in the section [ENV_INIT], while constraints over the output variable valuations are given in the section [SYS_INIT]. In the latter case, the allowed values for the output variables may depend on the values of the input variables.

Constraints over integer variables compare their values against constants or other integer variables using the <, >, <=, >=, and =+ operators. Furthermore the addition operator + can be used.

As an example, the following specification fragment declares that initially, x and y must have different values. Additionally, a must copy the value of x and we need to have 2 cdot v < 13 if the input variable y is initially set to true by the environment in which the finite-state system to be synthesized is supposed to operate in.

[ENV_INIT]
!(x <-> y)

[OUTPUT]
a <-> x
y -> (v+v<13)

Note that even though multiplication is not supported in the slugs input language, this feature can be simulated with repeated additions.

Defining the Allowed Variable Value Changes for the Input and Output Variables

During the execution of the finite-state system that we want to synthesize, the values of the input and output variables change. In most specifications of practical use, we need to define the allowed evolutions of the values. This is done by writing constraints in the sections [ENV_TRANS] and [SYS_TRANS] of the specification file. The former represents the allowed evolution of the input (environment) variables, whereas the latter refers to the output variables. Values after a transition are represented by a variable name with an added ’ suffix. When giving constraints over the evolution of the output variables, the input variable values before and after a transition are permitted.

As an example, the following constraints require the environment to never change the value of the x variable while the value of the y variable can change arbitrarily, but at least in every second step, the variable needs to have a false value.

[ENV_TRANS]
x <-> x'
y | !y'

The following output varaible evolution constraint states that the value of the v variable must change by at least 2 along a transition if the value of y does not change along the transition.

[SYS_TRANS]
(x <-> ! y') -> (v'+2 <= v) | (v+2 >= v')

Liveness Assumptions and Guarantees

Generalized Reactivity(1) Specifications often describe systems that only need to fulfil their own goals if the environment from time to time fulfills certain environment goals. Goals are transitions and in slugs specification, we can state these in the same way as we state requirements on system transitions. Environment goals are given in the [ENV_TRANS] section whereas system goals are given in the [SYS_TRANS] section.

As an example, if we want to state that the value of v must be greater than 9 infinite often, and also smaller than 6 infinitely often, but the system can assume that y is false two times in a row infinite often when trying to achieve these goals, we can express this as:

[ENV_LIVENESS]
!x & !x'

[SYS_LIVENESS]
v>9
v<6

Checking for Realizability

To use a specification, you can type it into the text box on the main page of webslugs. After clicking on “check realizability”, you will obtain one of three results:

If the specification is realizable, then there exists a finite-state implementation satisfying it.
If the specification is unrealizable, then it is too strong, so that no finite-state implementation can satisfy it.
In case of a syntax error, no result is obtained. Carefully read the error message to observe what is going on.

Note that due to the high complexity of the problem, the web-based version of slugs will abort the computation if analyzing the specification is too resource-intensive.

If a specification is realizable, then you can run a simulator of the implementation by pressing the respective button on the results page. After starting the simulator, you can press the h key to toggle through the help pages.

If a specification is unrealizable, then the simulator can also be run, but it simulates an environment counter-strategy that shows why the specification is unrealizable instead.