SEED Specification Tutorial
LTL Formulas
A first specification (tags constants union unary binary and start)
Set of Constants (tag constants_set)
Idempotent operators (tag binary_neq)
Associative operators (tag Sequence)
Idempotent and Symmetric Operators (tag binary_sym_neq)
Boolean Formulas
3-SAT Formulas (tag constants_set of fixed arity)
Presburger Formulas
General case (tag variables)
Quantifiers (tags fragment_pi and fragment_sigma)
LTL Formulas
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 |
Disjunction of symbols are
encoded using the union tag. |
The first rule is encoded by
|
Binary operator are encoded
using the binary tag. |
The rules for Until, And, OR
are encoded by |
Unary operators are encoded
similarly with unary tag. |
The rules for Next, Not are
encoded by |
Constant are encoded similarly
to unions with the constants tag. |
Here the rule for atomic
formula is encoded by |
The XML files is (Tuto1.xml):
<?xml version="1.0"?> |
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"> |
becomes |
<union id="F"> |
<constants id="G"> |
becomes |
<constants id="G"> |
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"> |
becomes |
<binary_neq id="A"> |
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"> |
becomes |
<sequence id="C"> |
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"> |
becomes |
<binary_sym_neq id="A"> |
The corresponding XML file is Tuto4.xml
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 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
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" />