1. 23 Apr, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      ltsmin: do not install the library · e201c3c9
      Alexandre Duret-Lutz authored
      For some reason, we used to install the library (causing the warning
      from Lintian while building the Debian packages) and not the binary.
      Let's not install any of these: the user interface is not nice enough.
      
      * iface/ltsmin/Makefile.am: Do not install libspotltsmin.la.
      e201c3c9
    • Alexandre Duret-Lutz's avatar
      debian: fix two lintian errors · 7770572c
      Alexandre Duret-Lutz authored
      * debian/control (libspot-dev): Do not depend on an exact version of
      spot.
      (spot-doc): depend on libjs-mathjax.
      * debian/rules: Patch doc/userdoc/ to use the local version of MathJax.
      7770572c
  2. 22 Apr, 2015 14 commits
    • Alexandre Duret-Lutz's avatar
      * NEWS: Update to mention TωA. · e07c7057
      Alexandre Duret-Lutz authored
      e07c7057
    • Alexandre Duret-Lutz's avatar
      5e67d28c
    • Alexandre Duret-Lutz's avatar
      rename src/tgbaalgos/ as src/twaalgos/ · de529df5
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/tgbaalgos/: Rename as...
      * src/twaalgos/: ... this.
      * README, configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh, src/bin/common_output.hh,
      src/bin/common_post.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc,
      src/bin/ltl2tgta.cc, src/bin/ltlcross.cc, src/bin/ltldo.cc,
      src/bin/ltlfilt.cc, src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
      src/graphtest/twagraph.cc, src/kripke/kripkeprint.cc,
      src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
      src/ltlvisit/exclusive.cc, src/taalgos/emptinessta.hh,
      src/tgbatest/checkpsl.cc, src/tgbatest/checkta.cc,
      src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
      src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc, src/twa/twa.cc,
      src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
      wrap/python/spot_impl.i: Adjust.
      de529df5
    • Alexandre Duret-Lutz's avatar
      rename tgba files as twa · 703fbd0e
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/graphtest/tgbagraph.cc, src/tgba/acc.cc, src/tgba/acc.hh,
      src/tgba/bdddict.cc, src/tgba/bdddict.hh, src/tgba/bddprint.cc,
      src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
      src/tgba/formula2bdd.hh, src/tgba/fwd.hh, src/tgba/Makefile.am,
      src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
      src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh, src/tgba/tgba.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/.cvsignore: Rename as...
      * src/graphtest/twagraph.cc, src/twa/acc.cc, src/twa/acc.hh,
      src/twa/bdddict.cc, src/twa/bdddict.hh, src/twa/bddprint.cc,
      src/twa/bddprint.hh, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
      src/twa/fwd.hh, src/twa/Makefile.am, src/twa/taatgba.cc,
      src/twa/taatgba.hh, src/twa/twa.cc, src/twa/twagraph.cc,
      src/twa/twagraph.hh, src/twa/twa.hh, src/twa/twamask.cc,
      src/twa/twamask.hh, src/twa/twaproduct.cc, src/twa/twaproduct.hh,
      src/twa/twaproxy.cc, src/twa/twaproxy.hh,
      src/twa/twasafracomplement.cc, src/twa/twasafracomplement.hh,
      src/twa/.cvsignore: ... these.
      * README, bench/stutter/stutter_invariance_randomgraph.cc,
      configure.ac, iface/ltsmin/modelcheck.cc, src/Makefile.am,
      src/bin/common_aoutput.cc, src/bin/common_conv.hh,
      src/bin/common_trans.hh, src/bin/dstar2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/randaut.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/public.hh, src/graphtest/Makefile.am,
      src/graphtest/ngraph.cc, src/hoaparse/hoaparse.yy,
      src/hoaparse/public.hh, src/kripke/fairkripke.hh,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeprint.cc,
      src/kripkeparse/kripkeparse.yy, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ltlvisit/exclusive.hh,
      src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
      src/priv/accmap.hh, src/ta/ta.hh, src/ta/taexplicit.cc,
      src/ta/taexplicit.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
      src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/taalgos/dotty.cc,
      src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
      src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
      src/tgbaalgos/bfssteps.cc, src/tgbaalgos/canonicalize.cc,
      src/tgbaalgos/canonicalize.hh, src/tgbaalgos/cleanacc.hh,
      src/tgbaalgos/complete.hh, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dtbasat.cc,
      src/tgbaalgos/dtbasat.hh, 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/sccstack.hh, src/tgbaalgos/gtec/status.hh,
      src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/hoa.cc,
      src/tgbaalgos/hoa.hh, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, src/tgbaalgos/mask.hh,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/product.cc,
      src/tgbaalgos/product.hh, src/tgbaalgos/projrun.cc,
      src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/randomize.hh,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
      src/tgbaalgos/reducerun.hh, src/tgbaalgos/relabel.hh,
      src/tgbaalgos/remfin.hh, src/tgbaalgos/remprop.hh,
      src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/sbacc.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
      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.hh,
      src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
      src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
      src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
      src/tgbaalgos/weight.hh, src/tgbaalgos/word.cc, src/tgbatest/acc.cc,
      src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/taatgba.cc,
      wrap/python/spot_impl.i: Adjust.
      703fbd0e
    • Alexandre Duret-Lutz's avatar
      rename Doxygen groups · 8839f50a
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/dstarparse/public.hh, src/hoaparse/public.hh,
      src/kripke/fairkripke.hh, src/kripke/kripkeprint.hh,
      src/tgba/bdddict.hh, src/tgba/tgba.hh, src/tgba/tgbamask.cc,
      src/tgba/tgbamask.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgbaalgos/are_isomorphic.hh, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/canonicalize.hh, src/tgbaalgos/degen.hh,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/hoa.hh,
      src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.hh,
      src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.hh,
      src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/minimize.hh,
      src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.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/simulation.hh, src/tgbaalgos/stats.hh,
      src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh:
      Rename all documention group starting with tgba_ as
      group starting with twa_.
      8839f50a
    • Alexandre Duret-Lutz's avatar
      Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep · 03f78ee8
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/dstarparse/dra2ba.cc, src/tgba/tgbamask.cc, src/tgba/tgbamask.hh:
      Rename tgba_mask and tgba_mask_keep as twa_mask and twa_mask_keep.
      03f78ee8
    • Alexandre Duret-Lutz's avatar
      rename tgba_proxy into twa_proxy · 5301fce3
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/tgba/tgbamask.cc, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh:
      Rename tgba_proxy into twa_proxy.
      5301fce3
    • Alexandre Duret-Lutz's avatar
      rename tgba_graph_state and tgba_graph_trans_data as twa_... · 2648ea17
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/tgba/tgbagraph.hh, src/tgbaalgos/powerset.cc: Rename
      tgba_graph_state and tgba_graph_trans_data as twa_graph_state and
      twa_graph_trans_data.
      2648ea17
    • Alexandre Duret-Lutz's avatar
      rename tgba_ptr into twa_ptr · 8520c4c3
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * iface/ltsmin/modelcheck.cc, src/dstarparse/dra2ba.cc,
      src/dstarparse/nra2nba.cc, src/ltlvisit/apcollect.cc,
      src/ltlvisit/apcollect.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
      src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh,
      src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgba/fwd.hh,
      src/tgba/tgba.cc, src/tgba/tgba.hh, 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/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
      src/tgbaalgos/compsusp.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dotty.hh, src/tgbaalgos/dtgbasat.cc,
      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/hoa.cc,
      src/tgbaalgos/hoa.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
      src/tgbaalgos/minimize.cc, src/tgbaalgos/ndfs_result.hxx,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.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/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
      src/tgbaalgos/se05.hh, src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
      src/tgbaalgos/stutter.cc, src/tgbaalgos/tau03.cc,
      src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc,
      src/tgbaalgos/tau03opt.hh, src/tgbatest/checkta.cc,
      src/tgbatest/complementation.cc, src/tgbatest/emptchk.cc,
      src/tgbatest/ltl2tgba.cc, wrap/python/spot_impl.i: Rename tgba_ptr as
      twa_ptr.
      8520c4c3
    • Alexandre Duret-Lutz's avatar
      rename tgba_succ_iterator as twa_succ_iterator · 5d977847
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/dstarparse/dra2ba.cc, src/dstarparse/nra2nba.cc,
      src/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeprint.cc, src/ta/ta.hh, 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/emptinessta.cc, src/taalgos/reachiter.hh,
      src/taalgos/tgba2ta.cc, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
      src/tgba/tgba.cc, src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbamask.cc, 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.hh, src/tgbaalgos/compsusp.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/gtec/gtec.cc,
      src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gv04.cc,
      src/tgbaalgos/lbtt.cc, src/tgbaalgos/magic.cc,
      src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reachiter.cc,
      src/tgbaalgos/reachiter.hh, src/tgbaalgos/replayrun.cc,
      src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh, src/tgbaalgos/se05.cc,
      src/tgbaalgos/stats.cc, src/tgbaalgos/stutter.cc,
      src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Rename
      tgba_succ_iterator as twa_succ_iterator.
      5d977847
    • Alexandre Duret-Lutz's avatar
      rename tgba_product as twa_product · c8569330
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * iface/ltsmin/finite.test, src/ta/tgtaproduct.cc,
      src/ta/tgtaproduct.hh, src/tgba/fwd.hh, src/tgba/tgbaproduct.cc,
      src/tgba/tgbaproduct.hh, wrap/python/spot_impl.i: Rename tgba_product
      as twa_product.
      c8569330
    • Alexandre Duret-Lutz's avatar
      rename tgba_digraph as twa_graph · e0bd0ad4
      Alexandre Duret-Lutz authored
      Automatic mass renaming.
      
      * src/bin/autfilt.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh, src/bin/common_conv.cc,
      src/bin/common_conv.hh, src/bin/common_output.hh, src/bin/dstar2tgba.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/randaut.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/hoaparse/hoaparse.yy,
      src/hoaparse/public.hh, src/ltlvisit/contain.hh,
      src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh,
      src/priv/accmap.hh, src/taalgos/minimize.cc, src/tgba/fwd.hh,
      src/tgba/tgba.cc, src/tgba/tgbagraph.cc, src/tgba/tgbagraph.hh,
      src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/are_isomorphic.hh,
      src/tgbaalgos/canonicalize.cc, src/tgbaalgos/canonicalize.hh,
      src/tgbaalgos/cleanacc.cc, src/tgbaalgos/cleanacc.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/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/hoa.cc,
      src/tgbaalgos/isdet.cc, src/tgbaalgos/isdet.hh, src/tgbaalgos/lbtt.cc,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/mask.cc, src/tgbaalgos/mask.hh, src/tgbaalgos/minimize.cc,
      src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.cc,
      src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
      src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
      src/tgbaalgos/product.cc, src/tgbaalgos/product.hh,
      src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
      src/tgbaalgos/randomize.cc, src/tgbaalgos/randomize.hh,
      src/tgbaalgos/relabel.cc, src/tgbaalgos/relabel.hh,
      src/tgbaalgos/remfin.cc, src/tgbaalgos/remfin.hh,
      src/tgbaalgos/remprop.cc, src/tgbaalgos/remprop.hh,
      src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
      src/tgbaalgos/sbacc.cc, src/tgbaalgos/sbacc.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
      src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.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/stutter.cc, src/tgbaalgos/stutter.hh,
      src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh,
      src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
      src/tgbatest/checkpsl.cc, src/tgbatest/complementation.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      src/tgbatest/randtgba.cc, wrap/python/spot_impl.i,
      wrap/python/tests/automata-io.ipynb, wrap/python/tests/automata.ipynb,
      wrap/python/tests/piperead.ipynb, wrap/python/tests/testingaut.ipynb:
      Rename tgba_digraph as twa_graph.
      e0bd0ad4
    • Alexandre Duret-Lutz's avatar
      rename the spot::tgba class as spot::twa · c2ae99e7
      Alexandre Duret-Lutz authored
      Now that we support any type of omega-accetpance, not just "Generalized
      Büchi", it is time to move away from GB and replace it by "ω", written
      just w in ASCII.
      
      This just change the name of the tgba class.  This part has to be done
      by hand because the word "tgba" occurs in many contexts and a mass
      replacement would be wrong.
      
      This will be followed by some automatic renaming of all the derived
      types and more.
      
      * src/bin/autfilt.cc, src/bin/randaut.cc, src/kripke/fairkripke.hh,
      src/ta/tgta.cc, src/ta/tgta.hh, src/tgba/fwd.hh, src/tgba/taatgba.cc,
      src/tgba/taatgba.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
      src/tgba/tgbagraph.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/are_isomorphic.cc, src/tgbaalgos/cleanacc.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
      src/tgbaalgos/dupexp.hh, src/tgbaalgos/hoa.cc,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stutter.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc, wrap/python/spot.py,
      wrap/python/spot_impl.i: Rename the tgba class into twa.
      c2ae99e7
    • Alexandre Duret-Lutz's avatar
      ltlfilt: add a --define option · 82480720
      Alexandre Duret-Lutz authored
      * src/bin/ltlfilt.cc: Implement it.
      * src/bin/common_output.cc, src/bin/common_output.hh: export the
      stream_formula function.
      * src/ltltest/ltlfilt.test: Test it.
      * src/ltlvisit/relabel.hh: Make it possible to clear the
      relabeling map.
      * NEWS, doc/org/ltlfilt.org: Mention --define.
      82480720
  3. 21 Apr, 2015 1 commit
  4. 20 Apr, 2015 4 commits
  5. 19 Apr, 2015 2 commits
  6. 17 Apr, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      stutter: new variant of Etessami's check · 9e959cdc
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/stutter.cc: Add a new variant of Etessami's check,
      closer to his original paper in IPL.
      * src/ltltest/stutter.test: Add more tests.
      * bench/stutter/user.sh: Include this new variant in the benchmark.
      9e959cdc
  7. 16 Apr, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      dot: add option to number transitions · ecfd9b77
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.cc: Add option 'o'.
      * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document it.
      * src/taalgos/dotty.cc: Ignore this option.
      * src/tgbatest/readsave.test: Test it.
      ecfd9b77
  8. 15 Apr, 2015 1 commit
  9. 14 Apr, 2015 3 commits
    • Alexandre Duret-Lutz's avatar
      acc: more helper functions · c65bf731
      Alexandre Duret-Lutz authored
      * src/tgba/acc.hh: Make it possible to call acc_cond::mark_t({1,2,3}),
      and acc_code::fin({1,2,3}).
      c65bf731
    • Alexandre Duret-Lutz's avatar
      python: fix non-determinism in the test suite. · 39b92a6d
      Alexandre Duret-Lutz authored
      Some tests calling spot.automaton('non-existing|') where failing either
      with a "process returned 127", or, under heavier load, with "failed to
      read from...".  The latter occur if we poll() the exit status before the
      children has had the tame to finish.
      
      * wrap/python/spot.py: Make sure we wait for the child process if we
      reach EOF, so that we can report the error status.
      * wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
      Update.
      39b92a6d
    • Alexandre Duret-Lutz's avatar
      python: avoid some locking errors with the history · ebdb5b7c
      Alexandre Duret-Lutz authored
      * wrap/python/tests/ipnbdoctest.py: Store all the history
      in memory.
      ebdb5b7c
  10. 13 Apr, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      more final keywords · 98e4d99b
      Alexandre Duret-Lutz authored
      For #42.
      
      * src/graph/graph.hh, src/ltlast/multop.hh, src/ltlenv/defaultenv.hh,
      src/misc/tmpfile.hh, src/tgba/taatgba.hh, src/tgba/tgbagraph.hh,
      src/tgba/tgbaproduct.hh, src/tgbaalgos/gtec/gtec.hh: Declare more
      classes as final.
      98e4d99b
    • Alexandre Duret-Lutz's avatar
      python: fix error handling while reading automata · ab7ee2c4
      Alexandre Duret-Lutz authored
      * wrap/python/tests/run.in: Make it easier to run python with gdb.
      * wrap/python/tests/automata-io.ipynb: Add test case.
      * wrap/python/spot.py (spot.automata): Make sure p is defined in all
      cases.
      * src/hoaparse/hoascan.ll: Make sure we do not close a file that
      hasn't been opened.
      ab7ee2c4
  11. 03 Apr, 2015 2 commits
  12. 02 Apr, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      new transformation from Fin-less to TGBA · e589e208
      Alexandre Duret-Lutz authored
      Fixes #72.
      
      * src/tgbaalgos/totgba.cc, src/tgbaalgos/totgba.hh: New files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add
      a Generic output type, and call to_generalized_buchi() if
      this type is not selected.
      * src/tgbatest/remfin.test: Add some tests.
      * src/bin/autfilt.cc: Add a --generic option, and set it
      by default.
      e589e208
    • Alexandre Duret-Lutz's avatar
      python: better bindings for testing automata · 16204e8e
      Alexandre Duret-Lutz authored
      * src/taalgos/dotty.cc, src/taalgos/dotty.hh: Add an interface
      similar to that of tgba/dotty.hh, even if we have to ignore
      most options.
      * src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh: Add an option
      to display the intermediate automaton with explicit stuttering
      transitions, for the purpose of making demonstrations.
      * src/tgba/tgbagraph.hh: Tweak the file so that SWIG can
      read it.
      * wrap/python/spot.py: Add wrappers for testing automata.
      * wrap/python/spot_impl.i: Fix support for
      atomic_prop_collect_as_bdd, and include a few more files.
      * wrap/python/tests/testingaut.ipynb: New file.
      * wrap/python/tests/Makefile.am: Add it.
      16204e8e
  13. 01 Apr, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      degen: add a lowinit option · 7bb183b9
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: New argument
      to disable the "jump to the accepting level if the entering
      state as an accepting self-loop" optimization.
      * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Check
      the degen-lowinit option and pass it on to degeneralize().
      * src/bin/spot-x.cc: Document it.
      * src/tgbatest/degenlskip.test: Add some tests.
      * src/tgbatest/ltl2ta.test: Update value.  We output less
      accepting states now.
      7bb183b9
    • Alexandre Duret-Lutz's avatar
      degen: do not mark initial trivial SCCs as accepting · 6e8170e3
      Alexandre Duret-Lutz authored
      Doing so is not wrong, but it's superfluous, and the extra accepting
      state will cause additional work in emptiness checks based on NDFS.
      Report from Jan Strejček.
      
      * src/tgbaalgos/degen.cc: Here.
      * src/tgbatest/degenid.test: Add a test case.
      6e8170e3
    • Alexandre Duret-Lutz's avatar
      python: LRU cache for the dot->svg conversion · 54a8ce50
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Here.
      54a8ce50
    • Alexandre Duret-Lutz's avatar
      python 2 is no longer supported · 31b3862f
      Alexandre Duret-Lutz authored
      * m4/pypath.m4: Check for Python 3.2+.
      * README, NEWS, HACKING: Reflect this change.
      31b3862f
  14. 31 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      stutter: improve closure · a18327d4
      Alexandre Duret-Lutz authored
      if a transition with the same label already exist, reuse it
      
      * src/tgbaalgos/stutter.cc: Here.
      * src/tgbatest/stutter.test: Add a test case.
      a18327d4