1. 12 Feb, 2014 3 commits
    • Alexandre Duret-Lutz's avatar
      c++11: work around Swig 2.0 · c88e22d0
      Alexandre Duret-Lutz authored
      * src/misc/common.hh: Conditionally define SPOT_DELETED to = delete.
      * src/ltlvisit/simplify.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh,
      src/tgba/bdddict.hh, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbasgba.hh,
      src/tgba/tgbatba.hh, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc: Use
      SPOT_DELETED.
      * wrap/python/spot.i: Include common.hh.
      * wrap/python/Makefile.am: Remove useless definition of SPOT_API
      and BUDDY_API.
      c88e22d0
    • Alexandre Duret-Lutz's avatar
      c++11: explicitly delete copy constructors and operator=. · 9cfc9f0f
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh,
      src/tgba/bdddict.hh, src/tgba/taatgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbasgba.hh,
      src/tgba/tgbatba.hh, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc: Here.
      9cfc9f0f
    • 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
  2. 29 Jul, 2013 2 commits
    • Alexandre Duret-Lutz's avatar
      Use -fvisibility=hidden globally. · 43b3df0e
      Alexandre Duret-Lutz authored
      * configure.ac: Check for flags and fill CXXFLAGS and CFLAGS.
      * iface/dve2/dve2.hh: Mark load_dve2 for export.
      * src/eltlparse/Makefile.am, src/kripke/Makefile.am,
      src/kripkeparse/Makefile.am, src/ltlast/Makefile.am,
      src/ltlenv/Makefile.am, src/ltlparse/Makefile.am,
      src/ltlvisit/Makefile.am, src/misc/Makefile.am,
      src/neverparse/Makefile.am, src/priv/Makefile.am, src/saba/Makefile.am,
      src/sabaalgos/Makefile.am, src/ta/Makefile.am, src/taalgos/Makefile.am,
      src/tgba/Makefile.am, src/tgbaalgos/Makefile.am,
      src/tgbaalgos/gtec/Makefile.am, src/tgbaparse/Makefile.am:
      Remove $(VISIBILITY_CXXFLAGS) now that it is set globally.
      43b3df0e
    • Alexandre Duret-Lutz's avatar
      Use -fvisibility=hidden in src/ta/ and src/taalgos/. · cfbd3138
      Alexandre Duret-Lutz authored
      * src/ta/Makefile.am, src/taalgos/Makefile.am: Use
      $(VISIBILITY_CXXFLAGS).
      * src/ta/ta.hh, src/ta/taexplicit.hh, src/ta/taproduct.hh,
      src/ta/tgta.hh, src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh,
      src/taalgos/dotty.hh, src/taalgos/emptinessta.hh,
      src/taalgos/minimize.hh, src/taalgos/reachiter.hh,
      src/taalgos/statessetbuilder.hh, src/taalgos/stats.hh,
      src/taalgos/tgba2ta.hh: Add SPOT_API in front
      of all public symbols.
      cfbd3138
  3. 09 Jun, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Improve documentation here and there. · 178ba876
      Alexandre Duret-Lutz authored
      * doc/Doxyfile.in: Update to Doxygen 1.8.4
      * doc/footer.html: Point to the mailing list.
      * doc/mainpage.dox: Point to spot::translator,
      and spot::kripke.
      * src/ta/tgta.hh: Do not use \emph.
      * src/tgba/succiter.hh: Fix rendering of example.
      * src/tgba/tgba.hh: Correct documentation.
      * src/tgbaalgos/cycles.hh: Improve rendering of
      documentation.
      * src/tgbaalgos/lbtt.hh, src/tgbaalgos/minimize.hh:
      Document missing arguments.
      178ba876
  4. 08 Jun, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Move \ingroup before \brief in all Doxygen comments. · 1ec9cebe
      Alexandre Duret-Lutz authored
      Using \ingroup between \brief and the rest of the documentation causes
      Doxygen to concatenate the brief with the rest of the doc.
      
      * src/sanity/style.test: Warn when \ingroup is found
      on the line after \brief.
      * src/kripke/fairkripke.hh, src/kripke/kripke.hh,
      src/kripke/kripkeprint.hh, src/ltlast/atomic_prop.hh,
      src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh,
      src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh,
      src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
      src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh,
      src/ltlenv/environment.hh, src/ltlparse/ltlfile.hh,
      src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
      src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/mark.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh,
      src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
      src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.hh,
      src/ltlvisit/simplify.hh, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
      src/misc/freelist.hh, src/misc/hash.hh, src/misc/ltstr.hh,
      src/misc/minato.hh, src/misc/modgray.hh, src/misc/optionmap.hh,
      src/misc/version.hh, src/saba/explicitstateconjunction.hh,
      src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
      src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh,
      src/sabaalgos/sabareachiter.hh, src/ta/ta.hh, src/ta/taproduct.hh,
      src/ta/tgta.hh, src/taalgos/reachiter.hh, src/taalgos/tgba2ta.hh,
      src/tgba/futurecondcol.hh, src/tgba/sba.hh, src/tgba/state.hh,
      src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
      src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbakvcomplement.hh,
      src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
      src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
      src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh, src/tgbaalgos/bfssteps.hh,
      src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
      src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/lbtt.hh,
      src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh,
      src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh,
      src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh,
      src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/save.hh,
      src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh: Move \ingroup
      before \brief.
      1ec9cebe
  5. 17 Jan, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix documentation errors reported by clang++ 3.2. · d580cce6
      Alexandre Duret-Lutz authored
      * m4/gccwarn.m4: Use -Wdocumentation if supported.
      * src/ltlast/binop.hh, src/ltlparse/public.hh, src/ta/taproduct.hh,
      src/taalgos/emptinessta.hh, src/taalgos/reachiter.hh,
      src/tgba/state.hh, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/ltl2tgba_fm.hh: Fix Doxygen documentations errors signaled
      by clang++ 3.2.
      d580cce6
  6. 16 Jan, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix several warnings reported by clang++ 3.2. · aa7b43ea
      Alexandre Duret-Lutz authored
      * src/tgba/tgbakvcomplement.cc
      (tgba_kv_complement_succ_iterator::current_state_),
      src/ta/taexplicit.hh (state_ta_explicit::source_):
      Remove useless private member.
      * src/ta/taexplicit.cc: Adjust constructors.
      * src/ta/tgta.cc, src/ta/taexplicit.hh: Also fix
      copyright banner.
      * src/bin/ltlcross.cc (exec_with_timeout): Work
      around warning about status not being set in the
      error path.
      aa7b43ea
  7. 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/tgbabddcoredata.hh,
      src/tgba/tgbasafracomplement.cc (operator=): Do not return a const
      reference.
      * 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
      variables.
      * 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.
      a577850e
  8. 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
  9. 04 Sep, 2012 1 commit
  10. 21 Aug, 2012 8 commits
    • Alexandre Duret-Lutz's avatar
      Fix tgta_explicit not to inherit from ta_explicit to please clang++. · 941cb0b5
      Alexandre Duret-Lutz authored
      * src/ta/tgtaexplicit.cc, src/ta/tgtaexplicit.hh: Use a ta_explicit
      attribute instead of inheriting from it.
      (get_ta): New method.
      * src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/tgba2ta.cc, src/tgbatest/ltl2tgba.cc: Adjust usage.
      * wrap/python/spot.i (as_ta): Remove, now that we have get_ta.
      * wrap/python/ajax/spot.in: Use get_ta instead of as_ta.
      941cb0b5
    • Alexandre Duret-Lutz's avatar
      Don't always delete the tgba used in ta_explicit. · 8e1438c9
      Alexandre Duret-Lutz authored
      * src/ta/taexplicit.hh (ta_explicit): Take a boolean to tell whether
      the tgba is owned.
      * src/ta/taexplicit.cc, src/ta/tgtaexplicit.cc,
      src/ta/tgtaexplicit.hh: Likewise.
      * src/ta/taexplicit.cc (~ta_explicit): Adjust destruction.
      * src/tgbatest/ltl2tgba.cc: Adjust usage.
      * src/taalgos/minimize.cc: Likewise.
      8e1438c9
    • Alexandre Duret-Lutz's avatar
      Fix ta/ and taalgos/ include path for VPATH builds. · be607118
      Alexandre Duret-Lutz authored
      * src/ta/Makefile.am, src/taalgos/Makefile.am: Add -I..
      be607118
    • Alexandre Duret-Lutz's avatar
      Fixes to pass sanity checks. · 67bbe6a6
      Alexandre Duret-Lutz authored
      * src/ta/taproduct.cc, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
      src/taalgos/emptinessta.cc, src/tgbatest/ltl2ta.test: 80 columns.
      * src/ta/tgta.hh, src/ta/tgtaproduct.hh, src/taalgos/emptinessta.hh,
      src/taalgos/tgba2ta.hh: Fix include gards.
      * src/taalgos/tgba2ta.hh: Remove superfluous includes.
      * src/taalgos/tgba2ta.cc: Add missing include.
      * src/tgbatest/ltl2tgba.cc: Fix use of bdd_true().
      67bbe6a6
    • Ala-Eddine Ben-Salem's avatar
      Changes in order to pass sanity tests · 9319b0ca
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbatest/ltl2tgba.cc, src/ta/Makefile.am, README: code style
      9319b0ca
    • Ala-Eddine Ben-Salem's avatar
      Changes to pass sanity tests · 618146c1
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taexplicit.hh, src/ta/taexplicit.cc, src/taalgos/minimize.cc,
      src/taalgos/tgba2ta.cc, src/tgbatest/ltl2tgba.cc: correct the code style
      in order to respect the sanity rules
      618146c1
    • Ala-Eddine Ben-Salem's avatar
      Stable version of TGTA approach implementation (automaton + product) · 5a706300
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/tgta.hh, src/ta/tgta.cc, src/ta/tgtaexplicit.hh,
      src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.hh, src/ta/tgtaproduct.cc,
      src/taalgos/minimize.cc, src/taalgos/minimize.hh,
      src/taalgos/emptinessta.hh, src/taalgos/emptinessta.hh,
      src/taalgos/emptinessta.cc, src/taalgos/tgba2ta.hh,
      src/taalgos/tgba2ta.cc: rename tgbta to tgta
      in this source files.
      * src/ta/tgbtaexplicit.hh, src/ta/tgbtaproduct.hh,  src/ta/tgbta.cc,
      src/ta/tgbtaproduct.cc, src/ta/tgbta.hh, src/ta/tgbtaexplicit.cc:
      Rename as...
      * src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
      src/ta/taproduct.hh, src/ta/tgtaexplicit.cc: ... these.
      * src/taalgos/sba2ta.hh, src/taalgos/sba2ta.cc: deleted because
      the implementation of all the transformations beteween TGBA and
      the different forms of TA are new implemented in src/taalgos/tgba2ta.hh
       and src/taalgos/tgba2ta.cc.
      * src/tgbatest/ltl2tgba.cc: rename the options of commands that build
      the different forms of TA.
      * src/ta/ta.hh: BUG Fix
      * src/ta/Makefile.am, src/tgbatest/ltl2ta.test: impacts of this renaming
      5a706300
    • Ala-Eddine Ben-Salem's avatar
      Doxygen comments. · c76e651b
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.hh,
      src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgbtaexplicit.cc,
      src/ta/taexplicit.cc, src/ta/tgbtaproduct.cc,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
      src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Add Doxygen
      comments.
      c76e651b
  11. 15 Jul, 2012 12 commits
    • Ala-Eddine Ben-Salem's avatar
      Cleaning code of TA Product and Emptiness-check · db2fcfa9
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taproduct.cc, src/taalgos/emptinessta.cc:
      remove unused (commented) code.
      db2fcfa9
    • Ala-Eddine Ben-Salem's avatar
      Add an implementation of TGTA minimization · ed27dab3
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taexplicit.cc, src/ta/taexplicit.hh: Bug fix TGTA
      * src/taalgos/minimize.cc,src/taalgos/minimize.hh: TGTA minimization
      * src/taalgos/tgba2ta.cc: add a TGTA minimization command (uses -Rm)
      * src/taalgos/minimize.cc, src/taalgos/minimize.hh
      (minimize_tgbta): New function.
      * src/taalgos/tgba2ta.cc: Set livelock-accepting flag of TGTA states
      to false so they can be merged with other states.
      * src/ta/taexplicit.cc (hash): Use id.
      * src/ta/taexplicit.hh: Cosmetics.
      ed27dab3
    • Ala-Eddine Ben-Salem's avatar
      New Automata: TGTA (Transition-based Generalized TA) · c882eadd
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/Makefile.am, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
      src/ta/taproduct.cc, src/ta/tgbta.cc, src/ta/tgbta.hh,
      src/ta/tgbtaexplicit.cc, src/ta/tgbtaexplicit.hh,
      src/ta/tgbtaproduct.cc, src/ta/tgbtaproduct.hh,
      src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
      src/taalgos/sba2ta.cc, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
      src/tgbatest/ltl2tgba.cc: Implementation of TGTA, a new kind of automata
      combining ideas from TGBA and TA.
      c882eadd
    • Alexandre Duret-Lutz's avatar
      Remove unused argument in constructor. · 29ee11cf
      Alexandre Duret-Lutz authored
      * src/taalgos/tgba2ta.cc, src/ta/taexplicit.hh (state_ta_explicit):
      Remove unused argument in constructor.
      29ee11cf
    • Ala-Eddine Ben-Salem's avatar
      GTA (Generalized Testing Automata) implementation · 83e7f0fa
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * 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/taalgos/Makefile.am, src/taalgos/dotty.cc,
      src/taalgos/emptinessta.cc, src/taalgos/minimize.cc,
      src/taalgos/minimize.hh, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh,
      src/tgbatest/ltl2tgba.cc: changes introduced to add a new form of TA
      called GTA (Generalized Testing Automata). GTA is a TA with acceptance-
      conditions added on transitions.
      83e7f0fa
    • Ala-Eddine Ben-Salem's avatar
      Add a new form of TA with a Single-pass emptiness check (STA) · 782ba001
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * 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/taalgos/dotty.cc, src/taalgos/emptinessta.cc,
      src/taalgos/emptinessta.hh, src/taalgos/minimize.cc,
      src/taalgos/reachiter.cc, src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh,
      src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc: Impacts of the
      implementation of a new variant of TA, called STA, which involve a
      Single-pass emptiness check. The new options (-in and -lv) added to
      build the new variants of TA allow to add two artificial states:
      1- an initial artificial state to have an unique initial state (-in)
      2- a livelock artificial state which has no successors in order to
      obtain the new form of TA which requires only a Single-pass emptiness-
      check: STA (-lv).
      782ba001
    • Ala-Eddine Ben-Salem's avatar
      Improvement of TA Product/Minimisation and of WFair generation · 310973f8
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taproduct.hh, src/ta/taproduct.cc: improvement of TA Product
      * src/ltltest/randltl.cc: improvement of WFair Formulas generation
      * src/taalgos/minimize.cc: improvement of TA minimization
      310973f8
    • Ala-Eddine Ben-Salem's avatar
      TA Product optimization and WFair Formulas generation · 2aad5b10
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taproduct.cc: TA Product optimization
      * src/ltltest/randltl.cc: WFair Formulas generation
      2aad5b10
    • Alexandre Duret-Lutz's avatar
      Use downcast when appropriate. · c774ba14
      Alexandre Duret-Lutz authored
      * src/taalgos/sba2ta.cc, src/ta/ta.cc, src/ta/taexplicit.cc,
      src/ta/taproduct.cc, src/taalgos/emptinessta.cc: Use downcast
      and cleanup whitespace.
      c774ba14
    • Ala Eddine's avatar
      Impacts of the new method state.destroy() · bf01501e
      Ala Eddine authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/ta/taexplicit.cc, src/ta/taproduct.cc,
      src/taalgos/minimize.cc, src/taalgos/sba2ta.cc:
      changes to use the new method destroy() added to state.hh
      bf01501e
    • Ala Eddine's avatar
      Add Testing Automata Product & Emptiness Check · 81e80e60
      Ala Eddine authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/stats.hh, src/taalgos/stats.cc: Compute statistics for a
      automaton.
      * src/ta/ta.hh, src/ta/ta.cc: Abstract representation of a Testing
      Automata(TA)
      * src/ta/taexplicit.hh, src/ta/taexplicit.cc: Explicit representation of
      a Testing Automata (TA)
      * src/taalgos/dotty.cc: Print a TA in dot format.
      * src/taalgos/reachiter.hh, src/taalgos/reachiter.cc: Iterate over all
      reachable states of a TA
      * src/taalgos/sba2ta.cc: implements the construction of a TA from a BA
      (Buchi Automata)
      * src/tgbatest/ltl2tgba.cc: add commands to test the TA implementation
      * src/taalgos/emptinessta.hh, src/taalgos/emptinessta.cc: implementation
       of the TA emptiness-check algorithm
      * src/ta/taproduct.hh, src/ta/taproduct.cc: representation of the
      product (automaton) between a TA and a Kripke structure.
      * src/ta/Makefile.am, src/taalgos/Makefile.am: add them
      81e80e60
    • Ala Eddine's avatar
      Preliminary implementation of Testing Automata. · ba47b821
      Ala Eddine authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * configure.ac: Generate src/ta/Makefile and src/taalgos/Makefile.
      * src/Makefile.am (SUBDIRS): Add them.
      * src/tgbatest/ltl2tgba.cc (main): Add option -TA.
      * src/ta/Makefile.am, src/ta/ta.hh, src/ta/taexplicit.cc,
      src/ta/taexplicit.hh, src/taalgos/Makefile.am,
      src/taalgos/dotty.cc, src/taalgos/dotty.hh,
      src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
      src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh: New files.
      ba47b821