A translator for temporal formulas.
To translate a temporal formula to ASP and solve with clingo call
tel translate 4 < example.tel | clingo -Wnone 0
For further information run
tel --help
The tel
program reads a set of formulas as input. Each formula has to be
terminated with a .
. Formulas of the following format are supported:
- Atoms
p(t1,...,tn)
- similar to what is supported in the input language of gringo
- the parenthesis are optional if
n
is zero
- Boolean connectives
~ F
F & G
F | G
F -> G
- Basic temporal connectives
- for the past
#previous F
F #since G
F #trigger G
- for the future
#next F
F #until G
F #release G
- for the past
- Derived temporal connectives (and formulas)
- for the past
#always- F
#eventually- F
#initial
#previous^ F
- for the future
#always+ F
#eventually+ F
#final
#next^ F
- for the past
- Disambiguation
- The grammar uses the following precedences (strongest first)
~
,#previous
,#previous^
,#next
,#next^
,#always+
,#always-
,#eventually+
,#eventually-
#since
,#until
,#release
,#trigger
&
|
->
(F)
(parenthesis have to be used when chaining unary connectives)
- The grammar uses the following precedences (strongest first)
- Comments
- strings starting with '%' are ignored until the end of the line
The package can be build using stack. To install stack go to https://docs.haskellstack.org and follow the instructions how to install.
Then you can install tel
by calling
stack setup
stack build
stack install
Note that this will take some time and requires quite some space on your hard
disk. On unix systems the installed executable will be in ~/.local/bin/tel
,
which you might have to add to your PATH environment variable.
An alternative is to build the program using packages shipping with your
distribution. Development happens on a Debian 9 machine, which ships all the
necessary packages. The required packages are listed in the tel.cabal
file.
After installing those run
cabal build