1. 12 Feb, 2014 4 commits
    • Alexandre Duret-Lutz's avatar
      Introduce tgba::release_iter(). · 06c69f88
      Alexandre Duret-Lutz authored
      Instead of "delete iter;" we now do "aut->release_iter(iter);" to
      give the iterator back to the automaton.  The TGBA classes now
      reuse a previously returned tgba_succ_iterator to answer a succ_iter()
      call, therefore avoiding (1) memory allocation, as well as (2) vtable
      and other constant member initialization.
      * src/tgba/tgba.hh, src/tgba/tgba.cc (release_iter, iter_cache_):
      Implement a release_iter() that stores the released iterator
      in iter_cache_.
      * src/tgba/succiter.hh (internal::succ_iterable): Move...
      * src/tgba/tgba.hh (tgba::succ_iterable): ... here. And use
      * iface/dve2/dve2.cc, src/kripke/kripke.cc, src/kripke/kripke.hh,
      src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
      src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.cc,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbamask.cc, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproxy.cc, src/tgba/tgbascc.cc, src/tgba/tgbatba.cc,
      src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/cycles.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gv04.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/reachiter.cc,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03opt.cc: Use release_iter() instead of deleting
      iterators, and used recycle iter_cache_ in implementations of
    • Alexandre Duret-Lutz's avatar
      c++11: introduce tgba::succ(s) to replace tgba::succ_iter(s). · 487cd01d
      Alexandre Duret-Lutz authored
      | tgba_succ_iterator* i = aut->succ_iter(s);
      | for (i->begin(); !i->done(); i->next())
      |   {
      |      // ...
      |   }
      | delete i;
      | for (auto i: aut->succ(s))
      |   {
      |      // ...
      |   }
      hiding the begin()/done()/next() interface, taking care of the delete,
      and allowing more optimization to come.
      * src/tgba/succiter.hh, src/tgba/tgba.hh: Implement the above
      new interface.
      * iface/gspn/ssp.cc, src/dstarparse/nsa2tgba.cc,
      src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc,
      src/tgba/tgbamask.cc, src/tgba/tgbasafracomplement.cc,
      src/tgba/tgbatba.cc, src/tgbaalgos/compsusp.cc, src/tgbaalgos/cutscc.cc,
      src/tgbaalgos/degen.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/tau03.cc, src/tgbatest/explicit2.cc: Update for
    • Alexandre Duret-Lutz's avatar
      c++11: get rid of spot::unique_ptr · 67b9e8d8
      Alexandre Duret-Lutz authored
      But do not replace it by std::unique_ptr, because this was not
      really equivalent.
      * src/misc/unique_ptr.hh: Delete.
      * src/misc/Makefile.am: Adjust.
      * src/tgbaalgos/simulation.cc, src/tgbatest/ltl2tgba.cc: Call
      delete explicitly.
    • Alexandre Duret-Lutz's avatar
      c++11: replace Sgi::hash_* by Sgi::unordered_*. · 34e91b76
      Alexandre Duret-Lutz authored
      * bench/scc-stats/stats.cc, bench/split-product/cutscc.cc,
      iface/gspn/ssp.cc, src/bin/ltlcross.cc, src/bin/ltlfilt.cc,
      src/bin/randltl.cc, src/dstarparse/nsa2tgba.cc, src/ltlast/formula.hh,
      src/ltlast/nfa.hh, src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/mark.hh, src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/snf.hh, src/misc/hash.hh,
      src/misc/mspool.hh, src/priv/acccompl.hh, src/priv/accconv.hh,
      src/saba/explicitstateconjunction.hh, src/saba/sabastate.hh,
      src/sabaalgos/sabareachiter.hh, src/sanity/style.test,
      src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/taalgos/emptinessta.cc,
      src/taalgos/minimize.cc, src/taalgos/reachiter.hh, src/tgba/state.hh,
      src/tgba/taatgba.hh, src/tgba/tgbabddconcretefactory.hh,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbakvcomplement.cc,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbatba.cc,
      src/tgba/tgbatba.hh, src/tgbaalgos/cutscc.cc, src/tgbaalgos/cycles.hh,
      src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/explscc.hh,
      src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03opt.cc: Adjust code.
      * src/sanity/style.test: Remove check.
  2. 29 Jul, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Create a new src/priv/ directory for private algorithms. · f2078ac3
      Alexandre Duret-Lutz authored
      * README: Document it.
      * configure.ac: Generate src/priv/Makefile.
      * src/Makefile.am: Recurse into priv/.
      * src/priv/Makefile.am: New file.
      * src/misc/acccompl.cc, src/misc/acccompl.hh,
      src/misc/accconv.cc, src/misc/accconv.hh: Move to...
      * src/priv/acccompl.cc, src/priv/acccompl.hh,
      src/priv/accconv.cc, src/priv/accconv.hh: ... here.
      * src/misc/Makefile.am: Adjust.
      * src/tgbaalgos/scc.cc, src/tgbaalgos/simulation.cc: Adjust
      * src/sanity/style.test: Make sure no public header
      file include a private one.
  3. 22 May, 2013 1 commit
  4. 12 May, 2013 1 commit
    • 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.
  5. 09 Apr, 2013 3 commits
    • Alexandre Duret-Lutz's avatar
      simulation: many fixes. · 1337c9c3
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/simulation.cc: Attempt to fix several cases.
      * src/tgbatest/sim.test: Add more tests.
      * src/tgbatest/sim2.test: New file.
      * src/tgbatest/Makefile.am: Add it.
    • Alexandre Duret-Lutz's avatar
    • Thomas Badie's avatar
      Add the "don't care" simulation · 08c77318
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgba/bddprint.cc, src/tgba/bddprint.hh: Add bdd_print_isop
      that prints the bdd into a Irreductible Sum Of Product.
      * src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Add a way to
      know which states (in the input) is which (in the result).
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Add
      the Don't Care Simulation and the Don't Care Iterated Simulation.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/spotlbtt.test,
      src/tgbatest/Makefile.am, src/tgbatest/sim.test: Test them.
      * bench/ltl2tgba/algorithms, bench/ltl2tgba/README,
      bench/ltl2tgba/algorithms: Add a way to bench the don't care
  6. 24 Dec, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Address several issues reported by cppcheck all over the place. · a577850e
      Alexandre Duret-Lutz authored
      * src/bin/common_finput.cc, src/tgbaalgos/lbtt.cc: Use !empty() instead
      of size() > 0.
      * src/bin/ltl2tgta.cc, src/kripke/kripkeexplicit.cc,
      src/tgbatest/complementation.cc: Avoid useless assignments.
      * src/bin/ltlcross.cc: Correct mistaken assignment inside assert().
      * src/evtgba/symbol.hh, src/tgba/tgbabddcoredata.cc,
      src/tgba/tgbasafracomplement.cc (operator=): Do not return a const
      * src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/product.cc,
      src/evtgbatest/product.cc: Check indices before using them, not after.
      * src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/tgbatest/randtgba.cc: Pass constant strings by reference.
      * src/kripke/kripkeprint.cc, src/tgbaalgos/simulation.cc:
      Remove a useless operation.
      * src/ltlvisit/simplify.cc: Remove a duplicate condition.
      * src/misc/formater.hh: Remove unused attribute.
      * src/misc/modgray.cc: Initialize done_ in the constructor.
      * src/saba/explicitstateconjunction.cc,
      src/saba/explicitstateconjunction.hh (operator=): Fix prototype.
      * src/saba/sabacomplementtgba.cc: Remove unused default constructor.
      * src/ta/taexplicit.cc, src/ta/taproduct.cc, src/ta/tgtaproduct.cc,
      src/ta/tgtaproduct.hh, src/taalgos/emptinessta.cc,
      src/taalgos/minimize.cc, src/taalgos/reachiter.cc,
      src/taalgos/tgba2ta.cc, src/tgbaalgos/cutscc.cc: Use C++ casts, and
      ++it instead of it++.
      * src/taalgos/dotty.cc, src/tgbatest/ltl2tgba.cc: Refine the scope of
      * src/tgba/tgbakvcomplement.hh (bdd_order): Always initialize bdd_.
      * src/tgba/tgbasgba.cc, src/tgba/wdbacomp.cc: Use the initialization
      line to initialize all members.
  7. 19 Dec, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Cosmetics. · aa2374c5
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Catch extra space around operator declarations.
      * src/ltlast/automatop.hh, src/ltlast/multop.hh,
      src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh,
      src/tgbaalgos/simulation.cc: Fix them.
  8. 14 Nov, 2012 1 commit
  9. 12 Oct, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Upgrade GPL v2+ to GPL v3+. · 1551c5d9
      Alexandre Duret-Lutz authored
      * NEWS: Mention this.
      * COPYING: Replace by GPL v3.
      * src/sanity/style.test: Check files with the wrong license,
      in case we forgot to update it during a merge.
      * Makefile.am, bench/Makefile.am, bench/emptchk/Makefile.am,
      bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
      bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh,
      bench/emptchk/pml-eeaean.sh, bench/emptchk/pml2tgba.pl,
      bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known,
      bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
      bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small,
      bench/ltlclasses/Makefile.am, bench/ltlclasses/defs.in,
      bench/ltlclasses/run, bench/ltlcounter/Makefile.am,
      bench/ltlcounter/defs.in, bench/ltlcounter/run,
      bench/scc-stats/Makefile.am, bench/scc-stats/stats.cc,
      bench/split-product/Makefile.am, bench/split-product/cutscc.cc,
      bench/split-product/pml2tgba.pl, bench/wdba/Makefile.am,
      bench/wdba/defs.in, bench/wdba/run, configure.ac, doc/Makefile.am,
      doc/dot.in, doc/tl/Makefile.am, ifac...
  10. 27 Sep, 2012 1 commit
  11. 26 Sep, 2012 1 commit
    • Thomas Badie's avatar
      Create unique_ptr for Spot. · f01d30eb
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/misc/unique_ptr.hh: Create unique_ptr for Spot.
      * src/misc/Makefile.am: Register this new file.
      * src/tgbatest/ltl2tgba.cc: Replace two calls to delete by the
      utilisation of unique_ptr.
      * src/tgbaalgos/simulation.cc: Replace two calls to delete by the
      utilisation of unique_ptr.
  12. 21 Aug, 2012 3 commits
    • Thomas Badie's avatar
      * src/tgbaalgos/simulation.cc: Fix a bug in the simulation. · 0b74f549
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
    • Thomas Badie's avatar
      Create the iterated simulations. · a0cce105
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbaalgos/simulation.cc: Create the iterated_simulations.
      (direct_simulation) Add an attribute "stat" that represents the
      number of states and transitions of the resulting automaton.
      * src/tgbaalgos/simulation.hh: Declare the iterated_simulations.
      * src/tgbatest/spotlbtt.test: Test the iterated_simulations.
      * src/tgbatest/ltl2tgba.cc: Associate the option -RIS to the
    • Thomas Badie's avatar
      Create the cosimulation. · 387bace9
      Thomas Badie authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbaalgos/simulation.cc: Add the cosimulation:
      (acc_compl_automaton) Add a template parameter.
      (acc_compl_automaton::process_link) Add a swap source destination.
      (direct_simulation) Add a template parameter.
      (direct_simulation::compute_sig) Add a flag in the signature to
      know if the state is initial.
      (direct_simulation::build_result) Remove the flag before reading
      the signature.
      Swap source and destination when building the new automaton.
      * src/tgbaalgos/simulation.hh: Declare and document the
      * src/tgbatest/ltl2tgba.cc: Associate the cosimulation with the -RRS
      * src/tgbatest/spotlbtt.test: Add a test on the cosimulation.
  13. 02 Jul, 2012 1 commit
  14. 19 Jun, 2012 1 commit
  15. 11 May, 2012 1 commit
  16. 02 May, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Downcase a couple of misnamed class names. · db4693b3
      Alexandre Duret-Lutz authored
      * src/misc/acccompl.hh, src/misc/acccompl.cc (AccCompl): Rename to
      * src/tgbaalgos/simulation.cc (AccComplAutomaton, Simulation): Rename
      to acc_compl_automaton and direct_simulation.  At the same time,
      reindent the whole file.
      * src/sanity/style.test: Detect capitalized class names.
      * src/kripke/kripkeexplicit.hh (KripkePrint): Remove useless
      * src/tgbaalgos/simulation.hh: Typo in comment.
  17. 18 Apr, 2012 1 commit
    • Thomas Badie's avatar
      Create the direct simulation. · 876f8c90
      Thomas Badie authored
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: New files.
      * src/tgbaalgos/Makefile.am: Add the new files to the compilation.
      * src/tgbatest/spotlbtt.test: Add the simulation.
      * src/tgbatest/ltl2tgba.cc: Add direct simulation (-RSD).