Homepage: http://www.daxc.de/eth

PSL Translator: psl2ba

Description

The psl2ba tool translates formulas of the linear-time temporal logic PSL into Büchi automata. The prominent linear-time logic LTL and the linear-time cores of the IEEE standardized logics SVA, and PSL are fragments of PSL. The output of psl2ba can be used in the symblic model checker NuSMV. For further information see the README.TXT file in the package.

You find some performance tests for this prototype at ./performance.

Download

The current version is beta release and distributed under the BSD license. You will need OCaml (http://caml.inria.fr) to compile the source code.

Download the newest version of the psl2ba tool at http://code.google.com/p/psl2ba/

Examples

~/psl2ba > ./psl2ba --help usage: ./psl2ba [options] options: -phi <PSL> : outputs the formula -smv <PSL> : outputs a NuSMV module -aba <PSL> : outputs the ABA -aba+ <PSL> : outputs the optimized ABA -nfa <SERE> : outputs the NFA -mnfa <SERE> : outputs the mirrored NFA -vars <PSL> : outputs the variable declarations in NuSMV -subeq <PSL> <LTL> : outputs a NuSMV module for L(PSL) <= L(LTL) -supeq <PSL> <LTL> : outputs a NuSMV module for L(PSL) >= L(LTL) -nos : disables simplification of transitions -old : old version of translation is used -prefix <prefix> : to distinguish the output -help Display this list of options --help Display this list of options

~/psl2ba > ./psl2ba -aba+ 'G(grant -> ({{{start; tt*; end} && {!cancel}*}; tt*} <->-> tt))' -- Formula: G (!grant | ({((((start; (TRUE)*); end) && (!cancel)*); (TRUE)*)} <->-> TRUE)) -- NNF: G (!grant | ({((((start; (TRUE)*); end) && (!cancel)*); (TRUE)*)} <->-> TRUE)) 2-way ABA: sf 0 -> ((! grant | (((((<1,-1> | <5,-1>) | <1,-1>) | ((end & ! cancel) & <4,-1>)) | <3,-1>) | ((end & ! cancel) & <2,-1>))) & <0,1>) 1 -> FALSE 2 -> (start & ! cancel) 3 -> (((end & ! cancel) & <4,-1>) | ((end & ! cancel) & <2,-1>)) 4 -> ((! cancel & <4,-1>) | (! cancel & <2,-1>)) 5 -> (((<1,-1> | <5,-1>) | <1,-1>) | <3,-1>)

~/psl2ba > ./psl2ba -smv 'G(grant -> ({{{start; tt*; end} && {!cancel}*}; tt*} <->-> tt))' -- Formula: G (!grant | ({((((start; (TRUE)*); end) && (!cancel)*); (TRUE)*)} <->-> TRUE)) -- NNF: G (!grant | ({((((start; (TRUE)*); end) && (!cancel)*); (TRUE)*)} <->-> TRUE)) MODULE ltl_spec_0 -- begin of automaton VAR r0 : boolean; r1 : boolean; r2 : boolean; r3 : boolean; r4 : boolean; r5 : boolean; s1 : boolean; s2 : boolean; s3 : boolean; s4 : boolean; s5 : boolean; INIT r0 & !s1 & !s2 & !s3 & !s4 & !s5 & (r0 -> ((! (grant) | (((((FALSE | FALSE) | FALSE) | ((end & ! (cancel)) & FALSE)) | FALSE) | ((end & ! (cancel)) & FALSE))) & TRUE)) & (r1 -> FALSE) & (r2 -> (start & ! (cancel))) & (r3 -> (((end & ! (cancel)) & FALSE) | ((end & ! (cancel)) & FALSE))) & (r4 -> ((! (cancel) & FALSE) | (! (cancel) & FALSE))) & (r5 -> (((FALSE | FALSE) | FALSE) | FALSE)) TRANS TRUE & (r0 -> ((! (grant) | (((((TRUE | TRUE) | TRUE) | ((end & ! (cancel)) & TRUE)) | TRUE) | ((end & ! (cancel)) & TRUE))) & next(r0))) & (r1 -> FALSE) & (r2 -> (start & ! (cancel))) & (r3 -> (((end & ! (cancel)) & TRUE) | ((end & ! (cancel)) & TRUE))) & (r4 -> ((! (cancel) & TRUE) | (! (cancel) & TRUE))) & (r5 -> (((TRUE | TRUE) | TRUE) | TRUE)) & (next(r0) -> ((next(! (grant)) | (((((r1 | r5) | r1) | ((next(end) & next(! (cancel))) & r4)) | r3) | ((next(end) & next(! (cancel))) & r2))) & (next(r1) -> FALSE) & (next(r2) -> (next(start) & next(! (cancel)))) & (next(r3) -> (((next(end) & next(! (cancel))) & r4) | ((next(end) & next(! (cancel))) & r2))) & (next(r4) -> ((next(! (cancel)) & r4) | (next(! (cancel)) & r2))) & (next(r5) -> (((r1 | r5) | r1) | r3)) & ((TRUE & !s1 & !s2 & !s3 & !s4 & !s5) -> (TRUE & (next(r1) <-> next(s1)) & (next(r2) <-> next(s2)) & (next(r3) <-> next(s3)) & (next(r4) <-> next(s4)) & (next(r5) <-> next(s5)) ) ) & ((FALSE | s1 | s2 | s3 | s4 | s5) -> (TRUE & (s1 -> FALSE) & (s2 -> (start & ! (cancel))) & (s3 -> (((end & ! (cancel)) & TRUE) | ((end & ! (cancel)) & TRUE))) & (s4 -> ((! (cancel) & TRUE) | (! (cancel) & TRUE))) & (s5 -> (((TRUE | TRUE) | TRUE) | TRUE)) & (next(s1) -> FALSE) & (next(s2) -> (next(start) & next(! (cancel)))) & (next(s3) -> (((next(end) & next(! (cancel))) & s4) | ((next(end) & next(! (cancel))) & s2))) & (next(s4) -> ((next(! (cancel)) & s4) | (next(! (cancel)) & s2))) & (next(s5) -> (((s1 | s5) | s1) | s3)) ) ) JUSTICE TRUE & !s1 & !s2 & !s3 & !s4 & !s5 -- end of automaton