Pastello is a tool for the pastification of LTL[X,F] formulas into the equivalent ones in F(pLTL). Pastello refers to the following paper: “A singly exponential transformation of LTL[X, F] into pure past LTL” - Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari.
Download the ZIP file of the source code from here.
The installation requires to have BLACK installed. Download the source code from the branch development of BLACK’s repository (the link is already directing to the development branch), and follow the istructions to compile it.
To install Pastello, first create a build directory and cd into it.
mkdir build && cd $_
Then compile Pastello with:
cmake ..
make
If the compilation has been successful, you can test Pastello with:
./pastello -h
./pastello -f "p & F q"
Input formula f: p & F q
Normal Form nf(f): p & F q
Output formula g: F O(q & O(p & True & Z False))
Checking equivalence...
Valid Equivalence!