1. 25 Nov, 2014 4 commits
  2. 21 Nov, 2014 9 commits
  3. 20 Nov, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      hoa: add support for unlabeled transitions · 69678152
      Alexandre Duret-Lutz authored
      * src/hoaparse/hoaparse.yy: Here.
      * src/tgbatest/hoaparse.test: Add tests.
      69678152
    • Alexandre Duret-Lutz's avatar
      hoa: make the parser more resilient to errors · 1d962f79
      Alexandre Duret-Lutz authored
      * src/hoaparse/hoaparse.yy: Improve error recovery,
      and fix location tracking in streams.
      * src/hoaparse/public.hh: Store the last location so
      that the next parse start at the correct position.
      * src/bin/autfilt.cc: Stop parsing a stream on irrecoverable errors.
      * src/tgbatest/hoaparse.test: Adjust tests.
      1d962f79
    • Alexandre Duret-Lutz's avatar
      monitor: add a few tests · 392c527d
      Alexandre Duret-Lutz authored
      * src/tgbatest/monitor.test: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbaalgos/minimize.cc (minimize_monitor): Mark
      the output automaton as state-based.
      * src/tgba/tgbagraph.hh: Assume automata with 0 acceptance sets are also
      state-based.
      392c527d
  4. 19 Nov, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: add support for reading TGBA as HOA · 622fe08f
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Add a %H modifier.
      * src/tgbatest/ltlcross2.test: Exercise it.
      622fe08f
    • Alexandre Duret-Lutz's avatar
      hoa: preliminary implementation of a parser · e55bcd95
      Alexandre Duret-Lutz authored
      * src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
      src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
      src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
      * src/Makefile.am, configure.ac, README: Adjust.
      * src/tgbatest/ltl2tgba.cc: Add a -XH option.
      * src/tgbatest/hoaparse.test: New file.
      * src/tgbatest/Makefile.am: Adjust.
      * buddy/src/bddx.h: Add a bdd_from_int() function.
      e55bcd95
  5. 18 Nov, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      fix line number tracking in files with DOS newlines · 45e9b96b
      Alexandre Duret-Lutz authored
      * src/dstarparse/dstarscan.ll, src/kripkeparse/kripkescan.ll,
      src/neverparse/neverclaimscan.ll, src/tgbaparse/tgbascan.ll:
      Distinguish between 1-sized EOL and 2-sized EOL.
      * src/kripketest/bad_parsing.test, src/tgbatest/neverclaimread.test,
      src/tgbatest/readsave.test: Add more tests.
      * NEWS: Mention it.
      * src/kripkeparse/scankripke.ll: Remove this unused file.
      45e9b96b
  6. 14 Nov, 2014 4 commits
    • Alexandre Duret-Lutz's avatar
      Remove the stutter test from tgbatest/. · 9effca69
      Alexandre Duret-Lutz authored
      Because src/ltltest/stutter.test is stronger.
      
      * src/tgbatest/stutter_invariant.test: Remove.
      * src/tgbatest/Makefile.am: Adjust.
      9effca69
    • Thibaud Michaud's avatar
      Adding tgba-based stutter-invariance checking · 37bcb5d9
      Thibaud Michaud authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
      Add closure function.
      * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
      Add two implementations of "self-loopize" function.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
      self-loopize.
      * src/tgba/Makefile.am: Add it.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
      closure and sl.
      * src/tgbatest/Makefile.am: Adjust.
      * src/bin/ltlfilt.cc: Modify stutter-invariant option to use
      automaton-based checking rather than syntactic-based checking.
      * src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
      Remove is_stutter_insensitive function.
      * src/tgbaalgos/stutter_invariance.cc,
      src/tgbaalgos/stutter_invariance.hh: Check if a formula is
      stutter-invariant using closure and sl.
      * wrap/python/spot.i: Add closure and sl bindings.
      * bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
      given formulas.
      * bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
      from random automata.
      * bench/stutter/Makefile.am: Add them.
      * configure.ac: Add bench/stutter/Makefile.
      * bench/Makefile.am: Add stutter subdirectory.
      * README: Document bench/stutter directory.
      37bcb5d9
    • Thibaud Michaud's avatar
      random_graph: add option to generate complete deterministic automaton · c9618f91
      Thibaud Michaud authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh:
      Add option to generate a complete deterministic automaton.
      * src/tgbatest/randtgba.cc: Test it.
      c9618f91
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: fix non-deterministic output · 11aa708a
      Alexandre Duret-Lutz authored
      The ltl_to_tgba_fm() translation function was using a hash_map of
      maps (ugh!) to merge transitions on output.  However recent libstd++
      changed the implementation of hash_map (a.k.a. unordered_map) causing
      transitions to be output in a different order.  This
      implementation-dependent order caused the ltl2ta.test to fail because
      the BA->TA transformation can produce TA of different sizes if you
      simply change the order of transitions in the input BA! This does not
      sound like a nice property for the BA->TA transformation, but Ala Eddine
      isn't sure how to fix it yet.  In the meantime, this patch makes sure
      ltl_to_tgba_fm() will return the same output regardless of the
      implementation of hash_map.
      
      The ltl2ta.test failure has been observed with g++ 4.9.2 on Arch Linux,
      and with gcc-snapshot (5.0.0 20141016) on Debian.
      
      * src/tgbaalgos/ltl2tgba_fm.cc: Rewrite the transition merging
      using a std::vector and std::sort instead of nested maps tables.
      * src/tgbatest/ltl2ta.test: Adjust sizes to the new order.
      * NEWS: Mention the fix.
      11aa708a
  7. 28 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      tgba_digraph: add a copy constructor, and obsolete dupexp · 923785f7
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc: Add a copy constructor,
      and some method to purge unreachable states.
      * src/graph/graph.hh (defrag_states): Erase transition of removed
      states.
      * src/tgbaalgos/complete.cc, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/simulation.cc,
      src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2tgba.cc: Adjust to use make_tgba_digraph() instead
      of tgba_dupexp_dfs() or tgba_dupexp_bfs().
      * src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Use
      make_tgba_digraph() when possible.
      * src/tgbatest/det.test, src/tgbatest/sim.test: Adjust expected results.
      923785f7
  8. 24 Oct, 2014 1 commit
  9. 08 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Replace most uses of scc_map by scc_info. · 2fb436a1
      Alexandre Duret-Lutz authored
      This involves reimplementing some algorithms using tgba_digraph, and
      implementing an explicit product that takes two tgba_digraphs and
      produces a tgba_digraph.
      
      * src/tgbaalgos/product.cc, src/tgbaalgos/product.hh: New files.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/bin/ltlcross.cc, src/tgba/tgba.cc, src/tgba/tgba.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
      src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
      src/tgbaalgos/isweakscc.cc, src/tgbaalgos/isweakscc.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
      src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc: Update to use scc_info and/or tgba_digraph.
      2fb436a1
  10. 06 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Store membership to acceptance sets using bitsets, not BDDs. · 2c764fb3
      Alexandre Duret-Lutz authored
      This is a huge patch, that took over a month to complete.  The bit sets
      are currently restricted to what 'unsigned can store', but it should be
      easy to extend it to 'uint64_t' should we need it.
      
      * NEWS: Update.
      * src/tgba/acc.hh: New file.
      * src/tgbatest/acc.cc, src/tgbatest/acc.test: Test it.
      * src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
      src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: Delete.  The KV
      complementation is too slow to be used in practice, and I somehow broke
      it during the conversion to bitsets.  The tgba->sgba conversion was only
      used for the KV complementation, and should be better redone on
      tgba_digraph_ptr should it be needed again.
      * src/bin/ltlcross.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/nsa2tgba.cc, src/graphtest/tgbagraph.cc,
      src/graphtest/tgbagraph.test, src/kripke/fairkripke.cc,
      src/kripke/fairkripke.hh, src/kripke/kripke.cc, src/kripke/kripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/misc/hash.hh, src/neverparse/neverclaimparse.yy, src/priv/accmap.hh,
      src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
      src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgta.cc,
      src/ta/tgta.hh, src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh,
      src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
      src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
      src/taalgos/tgba2ta.cc, src/tgba/Makefile.am, src/tgba/fwd.hh,
      src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
      src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/complete.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
      src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/hoaf.cc,
      src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/reducerun.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc,
      src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
      src/tgbaalgos/stripacc.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc,
      src/tgbaalgos/weight.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/Makefile.am, src/tgbatest/complementation.cc,
      src/tgbatest/complementation.test, src/tgbatest/degenlskip.test,
      src/tgbatest/det.test, src/tgbatest/dstar.test, src/tgbatest/emptchk.cc,
      src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
      src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test,
      src/tgbatest/maskacc.cc, src/tgbatest/maskacc.test,
      src/tgbatest/neverclaimread.test, src/tgbatest/randtgba.cc,
      src/tgbatest/readsave.test, src/tgbatest/sim.test,
      src/tgbatest/sim2.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
      iface/dve2/dve2.cc: Adjust or use to the new acceptance interface.
      2c764fb3
  11. 31 Aug, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      neverparse: diagnose redefinition of state labels · d401fadc
      Alexandre Duret-Lutz authored
      Reported by Joachim Klein.
      
      * src/neverparse/neverclaimparse.yy: Store labels and the
      location of their first definition in a global map to catch
      redefinitions.
      * src/tgbatest/neverclaimread.test: Test it.
      * NEWS: Mention it.
      d401fadc
    • Alexandre Duret-Lutz's avatar
      ltlcross: fix missing check for complement of negative automata · 9a8becb8
      Alexandre Duret-Lutz authored
      * src/bin/ltlcross.cc: Fix it.
      * src/tgbatest/ltl2dstar.test: Test it.
      * NEWS: Mention it.
      9a8becb8
    • Alexandre Duret-Lutz's avatar
      Remove futurecondcol and tgbascc. · c8b399c0
      Alexandre Duret-Lutz authored
      They are not used in Spot, and their interface is really horrible.  They
      are used in SOG-ITS to implement the SLAP product from TACAS'11, so we
      should support the functionality eventually, but maybe using the new
      kind of properties that can be attached to automata.  In the meantime,
      these classes are making refactoring harder.
      
      * src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
      src/tgba/tgbascc.cc, src/tgba/tgbascc.hh: Delete.
      * src/tgba/Makefile.am, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/checkpsl.cc, src/tgbatest/emptchk.cc: Adjust.
      c8b399c0
  12. 23 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Use shared_ptr for the emptiness check interfaces. · 6d7c258f
      Alexandre Duret-Lutz authored
      At the same time, this adds a is_empty() method to the tgba class,
      simplifying many places that ran emptiness checks.
      
      * iface/dve2/dve2check.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/ltlvisit/contain.cc, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/ce.cc,
      src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/magic.cc,
      src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/word.cc, src/tgbaalgos/word.hh,
      src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc, wrap/python/ajax/spot.in,
      wrap/python/spot.i: Use shared_ptr.
      6d7c258f
  13. 21 Aug, 2014 3 commits
  14. 20 Aug, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      hoaf: first implementation of the HOA Format output. · 310a98c1
      Alexandre Duret-Lutz authored
      The specifications are at http://adl.github.io/hoaf/
      
      * src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
      src/tgbatest/ltl2tgba.cc: Add option to output HOA.
      * NEWS: Mention it.
      310a98c1
    • Alexandre Duret-Lutz's avatar
      ltl2tgba_fm: Fix incorrect simplification of promises for M · 795c2f17
      Alexandre Duret-Lutz authored
      The bug was reported by Joachim Klein.
      
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::register_a_variable):
      Reduce P(a M b) to P(a & b), not to P(a).
      * src/tgbatest/ltlcross.test: Test Joachim's formula.
      * src/tgbatest/ltl2ta.test: Adjust some expected values.
      * NEWS: Mention the bug.
      795c2f17
    • Alexandre Duret-Lutz's avatar
      dtbasat,dtgbasat: rewrite using the tgba_digraph interface · edb220af
      Alexandre Duret-Lutz authored
      This gets rid of many state*/int conversions.  We now use scc_info
      instead of scc_map.  Finally the loops are now all 0-based.
      
      * src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh (weak_sccs): New
      method.
      * src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtbasat.hh,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/dtgbasat.hh: Use the
      tgba_digraph interface.
      * src/tgbatest/ltl2tgba.cc: Adjust calls.
      edb220af
  15. 18 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgbatest: rewrite emptchk.test in C++ · bc2e68f8
      Alexandre Duret-Lutz authored
      So that its run time goes from 10min+ to ~5s.
      
      * src/tgbatest/emptchk.cc: New file.
      * src/tgbatest/Makefile.am: Add it.
      * src/tgbatest/emptchk.test: Use it.
      bc2e68f8
    • Alexandre Duret-Lutz's avatar
      tgbatest: speed ltl2ta.test up! · b360b022
      Alexandre Duret-Lutz authored
      Again instead of calling ltl2tgba dozen of times with different options
      for various formulas, this implements a single executable that reads
      formulas from a file, translate them using the different setups, and
      dump statistics for comparison.  Valgrind now only has to be started
      once.
      
      * src/tgbatest/checkta.cc: New file.
      * src/tgbatest/Makefile.am: Use it.
      * src/tgbatest/ltl2ta.test: Rewrite using checkta.
      * src/tgbatest/ltl2tgba.cc: Remove a unused variable.
      b360b022
  16. 17 Aug, 2014 1 commit