1. 23 Jul, 2013 1 commit
  2. 20 Jul, 2013 3 commits
  3. 09 Jul, 2013 6 commits
  4. 25 Jun, 2013 1 commit
  5. 19 Jun, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix "BDD Error" in scc_filter(). · fc5d4e1a
      Alexandre Duret-Lutz authored
      If all the acceptance set of an SCC but the first one were useless, the
      scc_filter() algorithm could abort with a BDD error because of a bug in
      the logic.
      
      * src/tgbaalgos/sccfilter.cc (scc_filter): Fix.
      * src/tgbatest/sccsimpl.test: Add a test case supplied by Étienne
      Renault.
      fc5d4e1a
  6. 09 Jun, 2013 6 commits
    • Alexandre Duret-Lutz's avatar
      Improve ltlfilt.org · 372a086c
      Alexandre Duret-Lutz authored
      * doc/org/ltlfilt.org: Mention that the --stutter-invariant check
      use automata.  Fix a typo.
      372a086c
    • Alexandre Duret-Lutz's avatar
      644b5f01
    • Alexandre Duret-Lutz's avatar
      Release Spot 1.1.2. · 424f04ca
      Alexandre Duret-Lutz authored
      * configure.ac, NEWS, doc/org/tools.org: Bump version to 1.1.2.
      424f04ca
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · ecc8b8c7
      Alexandre Duret-Lutz authored
      ecc8b8c7
    • Alexandre Duret-Lutz's avatar
      Improve documentation here and there. · 178ba876
      Alexandre Duret-Lutz authored
      * doc/Doxyfile.in: Update to Doxygen 1.8.4
      * doc/footer.html: Point to the mailing list.
      * doc/mainpage.dox: Point to spot::translator,
      and spot::kripke.
      * src/ta/tgta.hh: Do not use \emph.
      * src/tgba/succiter.hh: Fix rendering of example.
      * src/tgba/tgba.hh: Correct documentation.
      * src/tgbaalgos/cycles.hh: Improve rendering of
      documentation.
      * src/tgbaalgos/lbtt.hh, src/tgbaalgos/minimize.hh:
      Document missing arguments.
      178ba876
    • Alexandre Duret-Lutz's avatar
      Fix verbatim blocks of Doxygen comments. · 1cd9b204
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh, src/ltlvisit/contain.hh,
      src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
      src/ltlvisit/remove_x.hh, src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh,
      src/misc/minato.hh, src/misc/optionmap.hh,
      src/saba/sabacomplementtgba.hh, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.hh, src/taalgos/tgba2ta.hh,
      src/tgba/tgbakvcomplement.hh, src/tgbaalgos/cycles.hh,
      src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
      src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/se05.hh,
      src/tgbaalgos/simulation.hh, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.hh: Surround verbatim blocks with /** ... */
      instead of using /// on each line.  Otherwise Doxygen will output the
      leading "///" tokens -- apparently this is a feature.
      * src/sanity/style.test: Strip multi-line comments before checking
      code style.
      1cd9b204
  7. 08 Jun, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Move \ingroup before \brief in all Doxygen comments. · 1ec9cebe
      Alexandre Duret-Lutz authored
      Using \ingroup between \brief and the rest of the documentation causes
      Doxygen to concatenate the brief with the rest of the doc.
      
      * src/sanity/style.test: Warn when \ingroup is found
      on the line after \brief.
      * src/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeprint.hh, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh,
      src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh,
      src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
      src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/ltlfile.hh,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
      src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/mark.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh,
      src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
      src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.hh,
      src/ltlvisit/simplify.hh, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
      src/misc/freelist.hh, src/misc/hash.hh, src/misc/ltstr.hh,
      src/misc/minato.hh, src/misc/modgray.hh, src/misc/optionmap.hh,
      src/misc/version.hh, src/saba/explicitstateconjunction.hh,
      src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.hh, src/ta/ta.hh, src/ta/taproduct.hh,
      src/ta/tgta.hh, src/taalgos/reachiter.hh, src/taalgos/tgba2ta.hh,
      src/tgba/futurecondcol.hh, src/tgba/sba.hh, src/tgba/state.hh,
      src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbakvcomplement.hh,
      src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
      src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
      src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh,
      src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/save.hh,
      src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh: Move \ingroup
      before \brief.
      1ec9cebe
  8. 22 May, 2013 1 commit
  9. 17 May, 2013 2 commits
  10. 13 May, 2013 5 commits
  11. 12 May, 2013 6 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: add a --products=N option · 9b82d755
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Implement the new option.  Average the product
      statistics on all products.
      * src/tgbatest/basimul.test, src/tgbatest/ltlcross.test,
      src/tgbatest/ltlcross2.test, bench/ltl2tgba/tools: Use the new option.
      * NEWS: Mention it.
      9b82d755
    • Alexandre Duret-Lutz's avatar
      bdddict: add an unregister_all_typed_variables() method · b4670f85
      Alexandre Duret-Lutz authored
      * src/tgba/bdddict.cc, src/tgba/bdddict.hh
      (unregister_all_typed_variables): New method.
      * src/tgbaalgos/degen.cc (degeneralize): Use it.
      * NEWS: Mention it.
      b4670f85
    • Alexandre Duret-Lutz's avatar
      simulation: Fix co-simulation and iterated simulations of BA automata · 0c7c9338
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/simulation.hh, src/tgbaalgos/simulation.cc
      (simulation_sba, cosimulation_sba, iterated_simulations_sba): New
      function.  Also speedup the existing functions by avoiding
      add_acceptince_conditions() and add_conditions().  Finally, use
      scc_filter_states() when dealing with degeneralized automata.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh (do_ba_simul):
      New method.  Use it after degeneralization.
      * src/tgba/tgbaexplicit.hh (get_transition, get_state): New methods.
      * src/tgbatest/basimul.test: New file.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      * NEWS: Introduce the new function and summarize the bug.
      0c7c9338
    • Alexandre Duret-Lutz's avatar
      bin: Ignore empty lines on input. · 372790a4
      Alexandre Duret-Lutz authored
      * src/bin/common_finput.cc: Here.
      * src/ltltest/ltlfilt.test: Test it.
      * NEWS: Mention it.
      372790a4
    • Alexandre Duret-Lutz's avatar
      ltlcross: Add a --seed option. · 9e589422
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Here.
      * NEWS: Mention it.
      9e589422
    • Alexandre Duret-Lutz's avatar
      Introduce scc_filter_states(). · 6b5b002f
      Alexandre Duret-Lutz authored
      The main motivation is the upcoming patch that introduces
      simulation_sba() and requires this function.
      
      * src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccfilter.cc: Implement it.
      * src/tgbaalgos/postproc.cc: Use it for monitors, because we do not
      care about acceptance conditions.
      * NEWS: Mention it.
      6b5b002f
  12. 11 May, 2013 1 commit
  13. 09 May, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      lbtt: improve the LBTT output · eed7e2df
      Alexandre Duret-Lutz authored
      Provide a way to output automata with state-based acceptance.  Also
      print the guards using to_lbt_string() for consistency: as a
      consequence, atomic proposition that do not match p[0-9]+ are now
      double-quoted.
      
      * src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
      * src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
      * src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
      * src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
      Add an option --lbtt=t to get the old behavior.
      * src/bin/man/ltl2tgba.x: Document the LBTT format we use with
      some links and examples.
      * src/tgbatest/lbttparse.test: More tests.
      * src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
      * NEWS: Update.
      eed7e2df
  14. 30 Apr, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix genltl --gh-r · e2378b49
      Alexandre Duret-Lutz authored
      Reported by František Blahoudek.
      
      * src/bin/genltl.cc (R_n): Really generate (GFp1 || FGp2), not
      (GFp1 || GFp2).
      * NEWS: Mention the bug.
      * THANKS: Update.
      e2378b49
  15. 28 Apr, 2013 4 commits