SEED Specification Tutorial





LTL Formulas

  1. A first specification (tags constants union unary binary and start)

  2. Set of Constants (tag constants_set)

  3. Idempotent operators (tag binary_neq)

  4. Associative operators (tag Sequence)

  5. Idempotent and Symmetric Operators (tag binary_sym_neq)

  6. Non-Repeated Unary Symbols

Boolean Formulas

  1. Formulas in Conjunctive Normal Form

  2. 3-SAT Formulas (tag constants_set of fixed arity)

Presburger Formulas

  1. General case (tag variables)

  2. Quantifiers (tags fragment_pi and fragment_sigma)

LTL Formulas


A First Specification>

We consider here LTL formulas defined over a finite set of atomic properties {a,b,c},using classical Boolean operators and the two temporal operators Until (arity 2) and Next (arity 1). Formally, LTL formulas are defined by the grammar:

F := F Until F | Next F | F Or F | F And F | not F | a | b | c



Such grammars can't be directly translated into the specification file. Indeed, it is required to use a grammar whose right-hand sides have either to contain only constants, or only grammar symbols, or only one unary/binary operator (or only variables symbols). Therefore, the grammar has to be split into the following one:

F := A | B | C | D | E | G

A := F Until F

B := Next F

C := F Or F

D := F And F

E := Not F

G:= a | b | c




Each rule is encoded with an appropriate XML tag.

First we define the initial symbol with the start tag.

Here the initial symbol is F
<start idref="F"/>

Disjunction of symbols are encoded using the union tag.
The id field encodes the name of the class. There are as many child tags as classes in the left hand side of the rule.

The first rule is encoded by
<union id="F">
<child idref="A"/>
<child idref="B"/>
<child idref="C"/>
<child idref="D"/>
<child idref="E"/>
<child idref="G"/>
</union>

Binary operator are encoded using the binary tag.
The id field encodes the name of the class. There is first a symbol tag for the symbol name. Next there are two child tags for left and right children. Here the children are identical.

The rules for Until, And, OR are encoded by
<binary id="A">
<symbol value="U"/>
<child idref="F"/>
<child idref="F"/>
</binary>

<binary id="C">
<symbol value="OR"/>
<child idref="F"/>
<child idref="F"/>
</binary>

<binary id="D">
<symbol value="AND"/>
<child idref="F"/>
<child idref="F"/>
</binary>

Unary operators are encoded similarly with unary tag.
The id field encodes the name of the class. There is first a symbol tag for the symbol name. Next there is child tags for the son.

The rules for Next, Not are encoded by
<unary id="E">
<symbol value="X"/>
<child idref="F">
</unary>

<unary id="B">
<symbol value="Not"/>
<child idref="F">
</unary>

Constant are encoded similarly to unions with the constants tag.
The id field encodes the name of the class. There are as many child tags as constants.

Here the rule for atomic formula is encoded by
<constants id="G">
<symbol value="a"/>
<symbol value="b"/>
<symbol value="c"/>
</constants >


The XML files is (Tuto1.xml):


<?xml version="1.0"?>
<!DOCTYPE specification SYSTEM "seed.dtd" >

<specification>

<start idref="F"/>

<union id="F">
<child idref="A"/>
<child idref="B"/>
<child idref="C"/>
<child idref="D"/>
<child idref="E"/>
<child idref="G"/>
</union>

<binary id="A">
<symbol value="U"/>
<child idref="F"/>
<child idref="F"/>
</binary>

<binary id="C">
<symbol value="OR"/>
<child idref="F"/>
<child idref="F"/>
</binary>

<binary id="D">
<symbol value="AND"/>
<child idref="F"/>
<child idref="F"/>
</binary>

<unary id="E">
<symbol value="X"/>
<child idref="F"/>
</unary>

<unary id="B">
<symbol value="Not"/>
<child idref="F"/>
</unary>

<constants id="G">
<symbol value="a"/>
<symbol value="b"/>
<symbol value="c"/>
</constants >

</specification>


Set of Constants

Frequently, when dealing with Kripke Structures, LTL atomic formulas are not constants (like a,b,c) but subsets of a finite set of predicates. Of course, one can encode each subset of predicates by a different constant. However, it requires many (an exponential number) constant names and this encoding changes formula sizes. We consider the new grammar:

F := F Until F | Next F | F Or F | F And F | Not F | S

S := Set(G)

G := a | b | c



Sets of constants are encoded with the appropriate tag. The specification is changed as follows (Tuto2.xml):

<union id="F">
<child idref="A"/>
<child idref="B"/>
<child idref="C"/>
<child idref="D"/>
<child idref="E"/>
<child idref="G"/>
</union>

becomes

<union id="F">
<child idref="A"/>
<child idref="B"/>
<child idref="C"/>
<child idref="D"/>
<child idref="E"/>
<child idref="S"/>
</union>

<constants id="G">
<symbol value="a"/>
<symbol value="b"/>
<symbol value="c"/>
</constants >

becomes

<constants id="G">
<symbol value="a"/>
<symbol value="b"/>
<symbol value="c"/>
</constants >

<constants_set id="S">
<child idref="G"/>
</constants_set>



Idempotent (Non-Equal) Binary Operators

Semantically, a formula of the form E1 Until E2, with E1=E2, is equivalent to the formula E1. Thus, in order to generate nicer formulas, one can add the following requirement: in each LTL formula, each Until-sub-formula must have two distinct children (i.e. sub-formulas of the form E1 Until E2, with E1=E2, are forbidden). A specific Tag exists:

<binary id="A">
<symbol value="U"/>
<child idref="F"/>
<child idref="F"/>
</binary>

becomes

<binary_neq id="A">
<symbol value="U"/>
<child idref="F"/>
</binary_neq>

Notice that tag binary_neq has a unique child in the specification. Of course, generated trees have two children for this kind of operator, but this two children have to be expressed by the same grammar symbol.


Associative Operators, Sequences

The Or symbol is associative: formula (E1 Or (E2 Or E3)) is equivalent to the formula ((E1 Or E2) Or E3). Frequently, such a formula is simply written Or (E1,E2,E3). For random generation, it makes a big difference: using a binary operator may lead to a large number of trivially equivalent formulas. In order to generate formulas of the form Or(....), one can use the sequence tag

<binary id="C">
<symbol value="Or"/>
<child idref="F"/>
<child idref="F"/>
</binary>

becomes

<sequence id="C">
<symbol value="Or"/>
<child idref="F"/>
</sequence>

However, this specification is still imperfect since if a node is labelled by Or, one wants each child to be labelled by something else than Or. It suffices to use the following grammar:


F := A | B | C | D | E | S

A := F Until F

B := Next F

C := Seq_Or(H)

D := F And F

E := Not F

G:= a | b | c

S := Set(G)

H := A | B | D | E | S




The corresponding XML file is Tuto3.xml


Symmetric-Commutative Operators (Symmetric-nonequal)

The And Operator can be managed as the Or operator. However we choose now to focus on others properties. The And operator is symmetric (formula E1 And E2 is equivalent to the formula E2 AAnd E1). Moreover, as for the Until Operator, formulas E1 And E2, with E1=E2, is equivalent to the formula E1. The binary_sym_neq tag is dedicated to this kind of specification.

<binary_sym id="D">
<symbol value="AND"/>
<child idref="F"/>
</binary_sym>

becomes

<binary_sym_neq id="A">
<symbol value="AND"/>
<child idref="F"/>
</binary_sym_neq>

The corresponding XML file is Tuto4.xml




Non-Repeated Unary Symbols

One can do better. Indeed, it is not forbidden with the current specification to have generate formulas of the form Not Not E. In order to avoid this kind of configurations, one can use the following grammar:

F := A | B | C | D | E | S

A := F Until F

B := Next F

C := Seq_Or(H)

D := F And F

E := Not I

G:= a | b | c

S := Set(G)

H := A | B | D | E | S

I := A | B | C | D | S



The corresponding XML file is Tuto5.xml





Boolean Formulas


Formulas in Conjunctive Normal Form

Boolean formulas are defined over a set of atomic properties (in this example this finite set is {a,b,c,d,e,f,g}) and using Boolean operators. It is known that each formula is equivalent to a formula in Conjunctive Normal Form, that is a formula which is a conjunction (And) of clauses: a clause is a formula of the form Or(x1,...,xn), where the xi's are either atomic formulas or negation of atomic formulas.

We propose to encode formula in CNF with the following grammar:

F := Seq_And(Clause)

Clause := Set(Atom)

Atom := a |...| g | not_a | ... | not_g


With this specification, the size of the formula not_a is one. The corresponding XML files is Tuto6.xml

It is important to emphasise that in this formulas, we do not explicitly use the not operator: formula not_a has size 1, not size 2. If we want to introduce a unary operator Not, it would not be possible to use the constants_set tag anymore.


3-SAT formulas

3-SAT formulas are formulas in Conjunctive Normal forms where each clause contains three atoms.

We propose to encode a 3-SAT formula with the following grammar:

F := Seq_And(Clause)

Clause := Set_3(Atom)

Atom := a |...| g | not_a | ... | not_g


To specify that each set has exactly three elements, it suffices to ad the field size="3" in the tag constants_set

The correspondent XML files is Tuto7.xml



Presburger Formulas


General Case

Presburger Logic is the first order logic over positive integers, using the equality and the addition.

Atomic formulas over a set of variables (here {x,y,z}) are defined by the grammar

Atomic := Term = Term

where terms are defined by


Term := x | y | z | 0 | 1 | Term+Term

Terms and Atomic formulas are encoded by the following grammar


Term := V | I | Plus

I := 0 | 1

Atomic := Term = Term

C := V | I

Plus := Seq_+(C)

V := x | y | z




In this specification, + is encoded as an associative operator. C encodes variables or integers.

The symbol = would be declared as symmetric and commutative.


Quantifier-free Presburger formulas over a set of variables (here {x,y,z}) are defined by the grammar

Pres := Atomic | Pres Or Pres | Not Pres

In order to specify Or as Associative and to not have repeated not, we use the following additional grammar rules:


Pres := O | N | Atomic

O := Seq_Or(nO)

N := Not nN

nN := O | Atomic

nO := N | Atomic





The correspondent XML files is Tuto8.xml

Notice that the tag variables has to be at the beginning of the specification, just after the start tag.Using the above file with Seed will generate first order Presburger formulas.



Existential/Universal Formulas

Notice that tags fragment_pi and fragment_sigma require a parameter value which is a positive integer encoding the number of alternations.


For instance adding the fragment <fragment_sigma value="1" /> will generate formula where all variables are universally quantified.

The correspondent XML files is Tuto9.xml

In order to generate formulas of the form ∀*∃*, it suffices to write <fragment_pi value="2" />