SENSEI – What is this about?

This web-page contains an online version of the tool “SENSEI” that allows you to wrangle with linear temporal logic (LTL) specifications. The purpose of the tool is to help you write specifications that actually encode what you want to encode and not what you thought you were encoding. It addresses the observation that LTL specifications are notorously difficult to write.

The tool, in a sense, pokes you to think about whether you really wrote the right specification. Whenever you write a specification (in SENSEI), you also write some positive examples (traces on which the LTL property is expected to hold) and some negative examples (traces on which the LTL property is expected to not hold). SENSEI checks the traces against the specification and lets you know if any discrepancies have been found.

The core feature of SENSEI, however, comes into play once specification and examples have been written. The tool computes several mutations of the specification and checks if for any of them, all of the positive and negative examples still apply. In this case, you as the specifier need to have a look – is perhaps the mutated specification the one that you are interested in? If yes, great! Just use that henceforth. Either way, the idea when working with SENSEI is that that you compare the mutated and original specification, define a trace that is a model of one and not the other, and then state if you want this trace to be a model of the formula or not.

After you added distinguishing traces for all mutations found by SENSEI, you as the specifying have documented that you really meant the LTL specification that you wrote. By sparring with the tool, you are forced to constantly rethink if you really wrote the correct specification and also document the decisions that you made along the way, i.e., your choices of which trace should satisfy the specification and which trace should not.

Note that in the process of checking the traces against mutations of the specification, mutations that result in LTL formulas that are semantically equivalent to the original specification are ignored.

Note that SENSEI is a research project and the concrete LTL formula mutations employed by SENSEI are subject to change.

Specifying using SENSEI

First of all, note that the web version of SENSEI doesn't store your specification. You can edit it in a web browser, but you will need to copy it to a text file on your computer regularly in order not to lose your data when you close the browser. The specifications that you are writing are not stored on the server!

Then, the input to SENSEI consist of blocks. Each block has a name in squared brackets, contains one or more specification parts, and contains one or more positive and negative examples. So the overall structure of an input file is:

[Some Block]
....


[Yet Another Block]
...

There can be arbitrarily many blocks. Lines starting with a # sign are ignored and treated as comments.

In order to add an LTL property, start a line with Spec: and let the LTL property follow. The syntax is as usual, so you can use || and | for logical or, && and & for logical and, ! for logical not, -> for logical implation, and the temporal operators G, X, F, R, and W and U as usual in LTL. You can also use braces. As far as operator precedence is concerned, the unary operators bind strongest, and logical and bind stronger than logical or. It is advisable to use braces for everything else.

As an example, a classical response temporal logic formula could be expressed as follows (within a block):

Spec: G(a -> F b)

To allow you to check if the LTL property really expresses what you wish to express, negative and positive examples can be supplied. These start with Pos: or Neg:*, followed by a descrption of the trace. A trace is always of the form (x1,…,xn)=…, where in the first braces, the atomic propositions that occur in the trace are listed. Note that in order for a trace to be usable for an LTL property, at least the propositions occuring in the LTL property must also occur along the trace, but there can be superfluous prositions used in a trace. The rest of the trace consists of the values of the propositions along a run. These are 0s and 1+s, comma-separated, and the proposition values for a trace character are again grouped in braces.

Since LTL is a property over infinite traces, words need to be infinite, and this is implemented by the word having a lasso at the end, so they end with a part that is repeated forever. This part is given with the syntax (….)^omega, where inside the braces, there can be one or more characters.

As an example, the following word is a example satisfying the LTL property above, i.e., G(a -> F b):

Pos: (a,b) = (1,0) (0,0) ( (0,0),(0,1) )^omega

The spaces are optional in this case.

Note that finite words are also supported, but the prefix shown needs to be informative for the satisfaction or violation of an LTL property over the finite trace already, so quite often the user will get an error when using them. The LTL properties are not interpreted as properties of LTL over finite traces in this case!

Sparring using SENSEI

As an example for how SENSEI is a useful sparring partner for writing LTL specification, let's consider the example from above again. So the initial specification file is:

[A Response Property Example]
Spec: G(a -> F b)
Pos: (a,b) = (1,0) (0,0) ( (0,0) )^omega

When running the tool with this specification, we may obtain an output such as:

SENSEI v.1.0 - Report
======================
Step: Checking positive and negative examples.
Step: Checking if a slightly modified specification makes a difference.
Processing spec:  G (!a|F b)
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant Fb | G!a
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant !a | GFb
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant FG(!a | b)
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant GF(!a | b)
Done!

Note that with depending on the version of SENSEI used, different mutations to the LTL property are used, so the output that you are getting with the most current version may be different. Also, the output may be colored.

SENSEI's output tells us that there are similar LTL properties that are consistent with the positive and negative examples! So…perhaps we mean those? Let's assume that the property G(a -> F b) is used in the scope of a development process of an arbiter system that should grant every request. The proposition for the requests is a, and let the proposition for the grant be b. In such a case, if can be seen that the first mutant, namely F b | G ! a is clearly the wrong specification, because it is trivially satisfied if b holds in the first step, regardless of what happens afterwards. So we add as new example one in which b is initially true, but afterwards G(a -> F b) does not hold:

Neg: (a,b) = (0,1) ( (1,0) )^omega

This is a negative example because it does not satisfy G(a -> F b).

We can now rerun the tool to check if any mutants died due to the additional example. Indeed, we get:

SENSEI v.1.0 - Report
======================
Step: Checking positive and negative examples.
Step: Checking if a slightly modified specification makes a difference.
Processing spec:  G (!a|F b)
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant Fb | G!a
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant FG(!a | b)
* Improvement needed: The specification in line 2 does not have a positive or negative example that distinguishes it from the mutant GF(!a | b)
Done!

Great, so only two cases left to look at! Let's consider FG(!a | b). In English, it means: “At some point in future, from there onwards, either a does not hold, or b holds”. But that doesn't need to be true. There can infinitely often be steps in which a request comes in, but no grant is given. We build a new positive example to rule this case out:

Pos: (a,b) = ( (1,0) (0,1) )^omega

In this example, the system gives grant in every second step. After running SENSEI again, we still get GF(!a | b) as a mutant. So what does it say. Infinitely often, there is a step, in which no request comes or no grant is given. Surely, every run of the arbiter should satisfy this property. But it's not strict enough to capture exactly the property that we want. So we come up with a negative example. That can for instance be one where an initial request is ignored for eternity (a bit or creativity in coming up with example traces is useful):

Neg: (a,b) = (1,0) ( (0,0) )^omega

Running SENSEI again yields that there are no mutants left. Awesome! So what have we gained? We have gained a few examples that highlight what we really wanted to express with an LTL property. If at some point we had a mutant for which we don't find an example distinguishing it from what the LTL property we wrote, this would have a highlighted that there is a gap in the understanding of what we wanted to express, which could have been further analyzed to figure out what we really wanted to express. In some (rare) cases, the mutant could have even be the property that we wanted, and then we could have changed the Spec to the computed mutant.

Note that SENSEI only exploys very few mutation rules, and hence will typically not help you find all problems with your specification. This is why whenever you think about the negative or positive example to add, you need to keep an open mind regarding if you already wrote the right specification.