1. 26 Feb, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Prefix many algorithms with runtime_error for unexpected acceptance · f0b1b943
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.cc (merge_transitions): Disable acceptance
      merging if Fin acceptance is used.
      * src/tgbaalgos/degen.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/safety.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc: Throw an
      exception if an unsupported type of acceptance is received.
      f0b1b943
  2. 13 Jan, 2015 1 commit
  3. 09 Jan, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      powerset: rewrite using the tgba_digraph interface · eadcf953
      Alexandre Duret-Lutz authored
      Fixes #48.
      
      * src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: Here.
      * src/tgbaalgos/minimize.cc: Adjust usage.
      eadcf953
    • Alexandre Duret-Lutz's avatar
      product: rename the one-the-fly version as otf_product · 94577d65
      Alexandre Duret-Lutz authored
      This avoid compiler errors about ambiguous calls and make sure we are
      calling the intended algorithms everywhere (this wasn't the case).
      
      * src/tgba/tgbaproduct.hh (product, product_at): Rename as...
      (otf_product, otf_product_at): ... this.
      * iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc, src/bin/ltlfilt.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/complementation.cc, src/tgbatest/ltlprod.cc: Adjust
      callers.
      94577d65
  4. 20 Nov, 2014 1 commit
    • 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
  5. 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
  6. 31 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      remove wdbacomp.cc and wdbacomp.hh · 359e0c6f
      Alexandre Duret-Lutz authored
      The weak complementation is now implemented by dtgba_complement(), with
      dispatch based on the automaton property.
      
      * src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh: Remove.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/dtgbacomp.cc: Implement the weak version.
      * src/tgbaalgos/dtgbacomp.hh: Document it.
      * src/tgbaalgos/minimize.cc: Use dtgba_complement() instead.
      359e0c6f
  7. 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
  8. 15 Aug, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      tgba: move boolean properties from tgba_digraph to tgba · b43f75e9
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh: Remove the set_bprop/get_bprop interface.
      * src/tgba/tgba.cc, src/tgba/tgba.hh: Add a new interface for
      setting/querying/copying the following properties: single_acc_set,
      state_based_acc, inherently_weak, deterministic.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/neverparse/neverclaimparse.yy, src/saba/sabacomplementtgba.cc,
      src/tgba/tgbagraph.cc, src/tgbaalgos/degen.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/simulation.cc, src/tgbatest/degenlskip.test,
      src/tgbatest/ltl2tgba.cc: Adjust to the new interface, or use
      it to bypass some useless work.
      b43f75e9
    • Alexandre Duret-Lutz's avatar
      Handle all automata through shared_ptr. (monstro patch) · 51151ab2
      Alexandre Duret-Lutz authored
      A type such as 'const tgba_digraph*' and 'tgba_digraph*' are replaced
      by 'const_tgba_digraph_ptr' and 'tgba_digraph_ptr'.  Additionally 'new
      tgba_digraph(...)' is replaced by 'make_tgba_digraph(...)'.
      
      This convention is followed by all automata types. Those smart
      pointers should normally be passed by const reference as input of
      function to avoid the atomic increments/decrements, but I probably
      missed a few, as this huge patch took me nearly 12h.
      
      * src/kripke/fwd.hh, src/tgba/fwd.hh: New files.
      * src/kripke/Makefile.am, src/tgba/Makefile.am: Adjust.
      * iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
      src/bin/common_output.hh, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/dstar2tgba.cc, src/dstarparse/dstarparse.yy,
      src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/dstarparse/public.hh, src/graphtest/tgbagraph.cc,
      src/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
      src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/neverparse/neverclaimparse.yy,
      src/neverparse/public.hh, src/priv/accmap.hh,
      src/priv/countstates.cc, src/priv/countstates.hh, src/saba/saba.hh,
      src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
      src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
      src/sabatest/sabacomplementtgba.cc, src/ta/ta.hh,
      src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
      src/ta/taproduct.hh, 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/dotty.hh,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
      src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
      src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
      src/taalgos/tgba2ta.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
      src/tgba/formula2bdd.hh, src/tgba/futurecondcol.cc,
      src/tgba/futurecondcol.hh, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.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/tgba/tgbascc.cc,
      src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh,
      src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
      src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc,
      src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
      src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.cc,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.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/safety.cc,
      src/tgbaalgos/safety.hh, src/tgbaalgos/save.cc,
      src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh,
      src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
      src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
      src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/explprod.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/maskacc.cc, src/tgbatest/powerset.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i,
      wrap/python/tests/interdep.py: Use shared pointers for automata.
      51151ab2
  9. 13 Aug, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      Simplify copying of atomic propositions in new tgba_digraph. · 10e5c623
      Alexandre Duret-Lutz authored
      * src/tgba/bdddict.cc, src/tgba/bdddict.hh
      (register_all_propositions_of): New method.
      * src/tgba/tgbagraph.hh (copy_ap_of): New method.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/dstarparse/nsa2tgba.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stripacc.cc: Simplify using copy_ap_of.
      10e5c623
  10. 12 Aug, 2014 4 commits
    • Alexandre Duret-Lutz's avatar
      get rid of tgba_tba_proxy · 5739240c
      Alexandre Duret-Lutz authored
      Replace it by a new degeneralize_tba(), that use the same tricks as
      degeneralize().
      
      * src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: Delete.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Implement
      a degeneralize_tba() function sharing its code
      with degeneralize().
      * src/tgbatest/ltl2tgba.cc: Rename -D to -DT so that we can pass it the
      same option as -DS.
      * src/tgbatest/degenid.test, src/tgbatest/emptchk.test,
      src/tgbatest/emptchke.test, src/tgbatest/ltlcounter.test,
      src/tgbatest/ltlcross.test, src/tgbatest/spotlbtt.test,
      src/tgbatest/ltl2tgba.test: Adjust.
      * src/tgbatest/det.test, src/tgbatest/emptchk.test: Adjust numbers to
      the smaller output.
      * src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/complementation.cc,
      wrap/python/spot.i, wrap/python/tests/ltl2tgba.py,
      src/sabatest/sabacomplementtgba.cc: Adjust to the removal
      of tgba_tba_proxy, using degeneralize_tba() if needed.
      5739240c
    • Alexandre Duret-Lutz's avatar
      remove the sba interface · e9893586
      Alexandre Duret-Lutz authored
      * src/tgba/tgbagraph.hh: Automatize the setting of the SingleAccSet
      property.
      * src/tgbaalgos/minimize.cc: Do not bother setting SingleAccSet.
      * src/tgba/sba.hh: Delete.
      * src/tgba/Makefile.am, wrap/python/spot.i: Adjust.
      * src/taalgos/tgba2ta.cc: Do not include sba.hh.
      * src/neverparse/neverclaimparse.yy: Set the SBA property on the output.
      * src/tgbaalgos/lbtt.cc (lbtt_read_gba): Set the StateBasedAcc property
      on output.
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Do not rely on
      the sba interface.
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/tgbaalgos/simulation.cc, src/tgbaalgos/sccfilter.cc: Set
      tgba_digraph::StateBasedAcc as appropriate.
      * src/tgbatest/ltl2tgba.cc: Add extra assert.
      e9893586
    • Alexandre Duret-Lutz's avatar
      remove tgba_explicit variants and the old scc_filter · e6ea90e3
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh: Delete.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
      Delete these obsoleted algorithms.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
      src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
      src/tgbatest/explicit3.cc, src/tgbatest/explicit3.test:
      Delete.
      * src/tgbatest/Makefile.am: Adjust.
      * src/bin/ltl2tgba.cc, src/priv/countstates.cc,
      src/tgbaalgos/isweakscc.cc, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/simulation.cc,
      src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/powerset.cc, src/tgbatest/tgbaread.cc,
      src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
      wrap/python/spot.i: Remove all remaining references to
      tgba_explicit.
      e6ea90e3
    • Alexandre Duret-Lutz's avatar
      replace sba_explicit_* by tgba_digraph, and use tgba_digraph is postproc · 6c9d5e4b
      Alexandre Duret-Lutz authored
      This is a huge patch.  tgba_digraph are equiped with some boolean
      properties that can be used to indicate whether they represent SBA
      (and will carry more informations later).  All algorithms that produce
      or use sba_explicit_* automata are changed to use tgba_digraph.
      postproc has been rewritten using only tgba_digraph, and this required
      changing the return types of many algorithms from tgba* to
      tgba_digraph*.
      
      * src/bin/dstar2tgba.cc, src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/dstar2tgba.cc, src/dstarparse/nra2nba.cc,
      src/dstarparse/nsa2tgba.cc, src/dstarparse/public.hh,
      src/tgba/tgbagraph.hh, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
      src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/postproc.cc,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/stripacc.cc,
      src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.cc,
      src/tgbaalgos/translate.hh, src/tgbatest/ltl2tgba.cc,
      wrap/python/spot.i: Update.
      6c9d5e4b
  11. 10 Aug, 2014 1 commit
  12. 07 Jul, 2014 1 commit
  13. 12 Feb, 2014 4 commits
    • Alexandre Duret-Lutz's avatar
      Replace << "c" by << 'c', and check for it in style.sh · ba5aff24
      Alexandre Duret-Lutz authored
      * src/sanity/style.test: Add a test.
      * iface/dve2/dve2.cc, iface/dve2/dve2check.cc, src/bin/common_output.cc,
      src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/dstarparse/dra2ba.cc, src/dstarparse/fmterror.cc,
      src/dstarparse/nsa2tgba.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/fmterror.cc, src/ltlast/atomic_prop.cc,
      src/ltlast/bunop.cc, src/ltltest/ltlrel.cc, src/ltltest/reduc.cc,
      src/ltltest/syntimpl.cc, src/ltlvisit/dotty.cc, src/ltlvisit/lbt.cc,
      src/ltlvisit/randomltl.cc, src/ltlvisit/relabel.cc,
      src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc, src/misc/bitvect.cc,
      src/misc/optionmap.cc, src/misc/timer.cc, src/neverparse/fmterror.cc,
      src/priv/freelist.cc, src/saba/sabacomplementtgba.cc,
      src/sabaalgos/sabadotty.cc, src/taalgos/dotty.cc,
      src/taalgos/minimize.cc, src/tgba/bdddict.cc, src/tgba/bddprint.cc,
      src/tgba/futurecondcol.cc, src/tgba/taatgba.hh,
      src/tgba/tgbakvcomplement.cc, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/cycles.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/save.cc, src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc,
      src/tgbaalgos/weight.cc, src/tgbaalgos/word.cc,
      src/tgbaparse/fmterror.cc, src/tgbatest/bitvect.cc,
      src/tgbatest/complementation.cc, src/tgbatest/intvcmp2.cc,
      src/tgbatest/intvcomp.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc: Replace << "c" by << 'c' when
      appropriate.
      ba5aff24
    • 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;
      
      becomes
      
      | 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
      loops.
      487cd01d
    • Alexandre Duret-Lutz's avatar
      Use the degeneralization unicity_table in more places. · 2f717415
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/degen.cc (unicity_table): Move and rename as...
      * src/tgba/state.hh (state_unicity_table): ... this.
      * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cycles.cc,
      src/tgbaalgos/cycles.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/safety.cc: Use it to simplify existing code.
      2f717415
    • 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.
      34e91b76
  14. 08 Sep, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      rename dba_complement() to dtgba_complement() · 7a7ed8a6
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dbacomp.cc, src/tgbaalgos/dbacomp.hh
      (dba_complement): Rename to...
      * src/tgbaalgos/dtgbacomp.cc, src/tgbaalgos/dtgbacomp.hh
      (dtgba_complement): ... this.
      * src/tgbaalgos/minimize.cc, src/tgbaalgos/powerset.cc,
      src/tgbatest/ltl2tgba.cc, src/bin/ltlcross.cc,
      src/tgbaalgos/Makefile.am: Adjust to name change.
      7a7ed8a6
  15. 26 Aug, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      minimize_obligation: can complement the input TGBA if deterministic · 2dda2c91
      Alexandre Duret-Lutz authored
      This makes dstar2tgba able to produce a minimal WDBA when the input DRA
      represent an obligation property.
      
      * src/tgbaalgos/minimize.cc (minimize_obligation): When the
      formula is not supplied but the input automaton is deterministic,
      complement it to check the result of WDBA minimization.
      * src/tgbatest/ltl2dstar.test, src/tgbatest/ltl2dstar2.test: Improve
      tests.
      2dda2c91
  16. 23 Aug, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Introduce spot::state_set. · 68ce9980
      Alexandre Duret-Lutz authored
      * src/tgba/state.hh: Define state_set and shared_state_set.
      * src/tgba/taatgba.cc, src/tgba/taatgba.hh: Rename the existing
      state_set (that inherits from spot::state) as set_state.
      * src/tgba/tgbakvcomplement.cc: Use shared_state_set instead
      of state_set.
      * src/tgbaalgos/minimize.cc (state_set): Rename as...
      (build_state_set): ... this.
      68ce9980
  17. 29 Jul, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Use the count_state() function instead of stats_reachable(). · f00d97b4
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/postproc.cc: Move the count_state() function...
      * src/priv/countstates.cc, src/priv/countstates.hh: ... in these
      new files.
      * src/priv/Makefile.am: Add them.
      * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc,
      src/tgbaalgos/minimize.cc: Use count_states() instead of
      stats_reachable().
      f00d97b4
  18. 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...
      1551c5d9
  19. 14 Sep, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Use more sba_explicit more often. · a010ebc8
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh
      (minimize_dfa, minimize_wdba): Return a sba_explicit_number automaton
      instead of tgba_explicit_number.
      * src/tgba/tgbaexplicit.hh (declare_acceptance_condition): Fix code
      so it works on sba as well.
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/neverclaim.cc: Specialize
      for sba instead of tgba_sba_proxy.
      * src/tgbaalgos/neverclaim.hh: Point to degeneralize().
      a010ebc8
  20. 28 Aug, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Add an option to use WDBA only if it reduces the size of the automaton. · 60ec3ace
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh (num_states): New method.
      * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
      (minimize_obligation): Add a reject_bigger option.
      * src/tgbatest/ltl2tgba.cc (-RM): New option.
      * src/tgbatest/spotlbtt.test: Test -RM.
      * bench/ltl2tgba/algorithms: Include -RM in addition to -Rm, and
      replace -RDS by -RIS.
      * NEWS: Mention this.
      60ec3ace
  21. 06 Jun, 2012 1 commit
  22. 02 May, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Use 'const formula*' instead of 'formula*' everywhere. · bf62d439
      Alexandre Duret-Lutz authored
      The distinction makes no sense since Spot 0.5, where we switched from
      mutable furmulae to immutable formulae.  The difference between
      const_visitor and visitor made no sense either.  They have been merged
      into one: visitor.
      
      * iface/dve2/dve2check.cc, iface/gspn/ltlgspn.cc,
      src/eltlparse/eltlparse.yy, src/eltlparse/public.hh,
      src/evtgbatest/ltl2evtgba.cc, src/kripkeparse/kripkeparse.yy,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
      src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
      src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
      src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
      src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/visitor.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh,
      src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/ltlfile.cc,
      src/ltlparse/ltlfile.hh, src/ltlparse/ltlparse.yy,
      src/ltlparse/public.hh, src/ltltest/consterm.cc,
      src/ltltest/equals.cc, src/ltltest/genltl.cc, src/ltltest/kind.cc,
      src/ltltest/length.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc,
      src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
      src/ltltest/tostring.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
      src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
      src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
      src/ltlvisit/length.cc, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.cc, src/ltlvisit/mark.hh,
      src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
      src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
      src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
      src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh,
      src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
      src/ltlvisit/snf.cc, src/ltlvisit/snf.hh, src/ltlvisit/tostring.cc,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
      src/neverparse/neverclaimparse.yy, src/sabatest/sabacomplementtgba.cc,
      src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgbaalgos/eltl2tgba_lacim.cc,
      src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
      src/tgbatest/randtgba.cc: Massive adjustment!
      * src/tgbatest/reductgba.cc: Delete.
      bf62d439
  23. 30 Apr, 2012 1 commit
  24. 28 Apr, 2012 1 commit
  25. 12 Apr, 2012 1 commit
    • Pierre PARUTTO's avatar
      Revamp tgbaexplicit.hh · a15aac28
      Pierre PARUTTO authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: Factor most of
      the code in an explicit_graph<State, Type> that inherits from type.
      The tgba_explicit type<State> now inherits from
      explicit_graph<State,tgba>.
      * src/ltlvisit/contain.cc, src/neverparse/neverclaimparse.yy
      src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, src/tgbaalgos/cutscc.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/sccfilter.cc, src/tgbaparse/tgbaparse.yy,
      src/tgbatest/complementation.cc, src/tgbatest/explicit.cc,
      src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc,
      src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc:
      Replace tgba_explicit* by the actual type used.
      * src/tgbatest/explicit2.cc: New file.
      * src/tgbatest/Makefile.am: Add it.
      a15aac28
  26. 17 Jan, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      minimize_wdba() failed to fully minimize some automata. · a5787937
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_wdba): Fix the Löding
      algorithm to use colors.  The previous implementation was an
      incorrect approximation.
      * src/tgbatest/wdba2.test: New file showing two equivalent
      formulas that were minimized in automata with different sizes.
      * src/tgbatest/Makefile.am: Add it.
      a5787937
  27. 05 Jan, 2012 1 commit
  28. 04 Mar, 2011 1 commit
  29. 06 Feb, 2011 1 commit
  30. 28 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Fixup minimize_monitor(). · ad93f875
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.cc (minimize_monitor): Fix typo yielding
      incorrect monitor if the input tgba is not deterministic.
      * src/tgbatest/ltl2tgba.test: Add test case.
      ad93f875
  31. 27 Jan, 2011 2 commits
    • Alexandre Duret-Lutz's avatar
      Rename is_safety_automaton() as is_guarantee_automaton() and · db124d02
      Alexandre Duret-Lutz authored
      implement is_safety_mwdba().
      
      Note: I swapped the name of safety and guarantee when I
      implemented is_safety_automaton() on 2010-03-20.  Fortunately,
      is_safety_automaton() was only used where is_guarantee_automaton()
      would have been correct.
      
      * src/tgbaalgos/safety.cc (is_guarantee_automaton): Rename as ...
      (is_guarantee_automaton): ... this.
      (is_safety_mwdba): New function.
      * src/tgbaalgos/safety.hh: Adjust and add documentation.
      * src/tgbaalgos/minimize.cc: Use is_guarantee_automaton() instead
      of is_safety_automaton().
      * src/tgbatests/safety.test: Rename as ...
      * src/tgbatests/obligation.test: ... this, and augment the
      test.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc (-O): Display whether a formula
      represent a safety, guarantee, or obligation property.
      * NEWS: Adjust.
      db124d02
    • Alexandre Duret-Lutz's avatar
      Introduce a destroy() method on states, and use it instead of delete. · 574a2285
      Alexandre Duret-Lutz authored
      Right now, destroy() just executes "delete this".  But in a later
      version, we will rewrite tgba_explicit so that it does not
      allocate new states (and the destroy() method for explicit state
      will do nothing).
      
      * src/tgba/state.hh (state::destroy): New method, to replace
      state::~state() in the future.
      (shared_state_deleter): New function.
      * src/evtgba/product.cc, src/evtgbaalgos/reachiter.cc,
      src/evtgbaalgos/save.cc, src/evtgbaalgos/tgba2evtgba.cc,
      src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgba/tgbareduc.cc,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasgba.cc,
      src/tgba/tgbatba.cc, src/tgba/tgbaunion.cc, src/tgba/wdbacomp.cc,
      src/tgbaalgos/cutscc.cc, src/tgbaalgos/emptiness.cc,
      src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/explscc.cc,
      src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/nsheap.cc,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/reachiter.cc, src/tgbaalgos/reducerun.cc,
      src/tgbaalgos/reductgba_sim.cc,
      src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/safety.cc, src/tgbaalgos/save.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/se05.cc,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Adjust to call
      "s->destroy()" instead of "delete s".
      * src/saba/sabacomplementtgba.cc, src/tgba/tgbakvcomplement.cc:
      Pass shared_state_deleter to the shared_ptr constructor, so that
      it calls destroy() instead of delete.
      574a2285