Translating an LTL formula into a never claim
Table of Contents
Here is how to translate an LTL (or PSL) formula into a never claim.
Shell
ltl2tgba --spin 'GFa -> GFb'
never { /* F(GFb | G!a) */ T0_init: if :: (true) -> goto T0_init :: (b) -> goto accept_S1 :: (!(a)) -> goto accept_S2 fi; accept_S1: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; accept_S2: if :: (!(a)) -> goto accept_S2 fi; T0_S3: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; }
Python
The formula
function returns a formula object (or raises a
parse-error exception). Formula objects have a translate()
method
that returns an automaton, and the automata objects have a to_str
method that can output in one of the supported syntaxes.
So the translation is actually a one-liner in Python:
import spot print(spot.formula('GFa -> GFb').translate('BA').to_str('spin'))
The above line can actually be made a bit shorter, because
translate()
can also be used as a function (as opposed to a method)
that takes a formula (possibly as a string) as first argument:
import spot print(spot.translate('GFa -> GFb', 'buchi', 'sbacc').to_str('spin'))
never { T0_init: if :: (true) -> goto T0_init :: (b) -> goto accept_S1 :: (!(a)) -> goto accept_S2 fi; accept_S1: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; accept_S2: if :: (!(a)) -> goto accept_S2 fi; T0_S3: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; }
C++
All the translation pipeline (this includes simplifying the formula,
translating the simplified formula into an automaton, and simplifying
the resulting automaton) is handled by the spot::translator
class.
An instance of this class can configured by calling set_type()
to
choose the type of automaton to output, set_level()
to set the level
of optimization (it's high by default), and set_pref()
to set
various preferences (like small or deterministic) or characteristic
(complete, unambiguous, state-based acceptance) for the resulting
automaton. Finally, the output as a never claim is done via the
print_never_claim
function.
#include <iostream> #include <spot/tl/parse.hh> #include <spot/twaalgos/translate.hh> #include <spot/twaalgos/neverclaim.hh> int main() { spot::parsed_formula pf = spot::parse_infix_psl("GFa -> GFb"); if (pf.format_errors(std::cerr)) return 1; spot::translator trans; trans.set_type(spot::postprocessor::Buchi); trans.set_pref(spot::postprocessor::SBAcc | spot::postprocessor::Small); spot::twa_graph_ptr aut = trans.run(pf.f); print_never_claim(std::cout, aut) << '\n'; return 0; }
never { T0_init: if :: (true) -> goto T0_init :: (b) -> goto accept_S1 :: (!(a)) -> goto accept_S2 fi; accept_S1: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; accept_S2: if :: (!(a)) -> goto accept_S2 fi; T0_S3: if :: (b) -> goto accept_S1 :: (!(b)) -> goto T0_S3 fi; }
Additional comments
The Python version of translate()
is documented as follows:
Help on function translate in module spot: translate(formula, *args, dict=<spot.impl.bdd_dict; proxy of <Swig Object of type 'std::shared_ptr< spot::bdd_dict > *' at 0x7fdbea105a40> >, xargs=None) Translate a formula into an automaton. Keep in mind that 'Deterministic' expresses just a preference that may not be satisfied. The optional arguments should be strings among the following: - at most one in 'GeneralizedBuchi', 'Buchi', or 'Monitor', 'generic', 'parity', 'parity min odd', 'parity min even', 'parity max odd', 'parity max even', 'coBuchi' (type of acceptance condition to build) - at most one in 'Small', 'Deterministic', 'Any' (preferred characteristics of the produced automaton) - at most one in 'Low', 'Medium', 'High' (optimization level) - any combination of 'Complete', 'Unambiguous', 'StateBasedAcceptance' (or 'SBAcc' for short), and 'Colored' (only for parity acceptance) The default corresponds to 'tgba', 'small' and 'high'. Additional options can be supplied using a `spot.option_map`, or a string (that will be converted to `spot.option_map`), as the `xargs` argument. This is similar to the `-x` option of command-line tools; so check out the spot-x(7) man page for details.