diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 73e5ea839..65fdbcdb7 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -71,13 +71,13 @@ static const argp_option options[] = " propositions", 0}, /**************************************************/ { nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, - { "algo", OPT_ALGO, "ds|sd", 0, + { "algo", OPT_ALGO, "ds|sd|large", 0, "choose the algorithm for synthesis:\n" " - sd: split then determinize with Safra (default)\n" " - ds: determinize (Safra) then split\n" " - lar: translate to a deterministic automaton with arbitrary" - " acceptance condition, then use LAR to turn to parity," - " then split", 0 }, + " acceptance condition, then use LAR to turn to parity," + " then split", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output options:", 20 }, { "print-pg", OPT_PRINT, nullptr, 0, diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index 825d6d2f4..d1385ca77 100644 --- a/doc/org/ltlsynt.org +++ b/doc/org/ltlsynt.org @@ -85,13 +85,13 @@ Fortunately, the SYNTCOMP organizers also provide a tool called [[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula. -The following four steps show you how a TLSF specification called spec.tlsf can +The following four steps show you how a TLSF specification called =FILE= can be synthesized using =syfco= and =ltlsynt=: #+BEGIN_SRC sh :export code LTL=$(syfco FILE -f ltlxba -m fully) -IN=$(syfco FILE -f ltlxba -m fully) -OUT=$(syfco FILE -f ltlxba -m fully) +IN=$(syfco FILE --print-input-signals) +OUT=$(syfco FILE --print-output-signals) ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT" #+END_SRC