Timbuk specifications
A typical Timbuk specification looks like this:
Ops plus:0 s:1 o:0 app:2
Const s o
Vars X Y
TRS R
app(app(plus,o),X) -> X
app(app(plus,s(X)),Y) -> s(app(app(plus,X),Y))
Automaton A1
States qf qp qp2 qi qnz
Final States qf
Transitions
app(qp,qi) -> qf
app(qp2,qnz) -> qp
plus -> qp2
o -> qi
s(qi) -> qi
s(qi) -> qnz
Automaton TC
States qi
Final States qi
Transitions
o -> qi
s(qi) -> qi
Patterns
o
where the Ops section defines all operators with their
arity. The Const section defines the constructor symbols
(here the symbols s and o used to represent peano natural numbers, o
is the natural 0, s(o) is 1, etc.). The TRS section
defines the Term Rewriting System (here the simple TRS defining the
addition of natural numbers). The first Automaton section
defines the initial language (here the language of terms of the form
app(app(plus,nz),i) where i is any natural and nz
is any natural number different from o. Note that, if this
automaton is not deterministic, it will be determinised by Timbuk
(see in this part). There are several
alternative for defining languages such as Regexp and SRegexp (a.k.a. Simplified Regular Expressions)
The automaton named TC gives the language of (well typed)
constructor terms (here limited to natural numbers). Finally, the
section Patterns defines the terms or the patterns that we
want to show unreachable. Here we want to show that adding a non
zero natural number to any natural number cannot result in
the number 0.
A specification may also contain some equations that are defined in
a specific section in the specification, e.g.
Ops plus:0 s:1 o:0 app:2
Const s o
Vars X Y
TRS R
app(app(plus,o),X) -> X
app(app(plus,s(X)),Y) -> s(app(app(plus,X),Y))
Automaton A1
States qf qp qp2 qi qnz
Final States qf
Transitions
app(qp,qi) -> qf
app(qp2,qnz) -> qp
plus -> qp2
o -> qi
s(qi) -> qi
s(qi) -> qnz
Automaton TC
States qi
Final States qi
Transitions
o -> qi
s(qi) -> qi
Equations Simp
Rules
s(s(X))=s(X)
Patterns
o