1. 21 Aug, 2012 9 commits
    • Alexandre Duret-Lutz's avatar
      Fix, run, and distribute ltl2ta.test. · 6bd905c6
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2ta.test: Adjust expected values.
      * src/tgbatest/Makefile.am (TESTS): Add ltl2ta.test.
      6bd905c6
    • Alexandre Duret-Lutz's avatar
      Post-rebase fixup. · 2462a3d5
      Alexandre Duret-Lutz authored
      * src/taalgos/tgba2ta.cc: Adjust to use the sba base class.
      2462a3d5
    • 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
    • Alexandre Duret-Lutz's avatar
      Post rebase fixups. · dcc809ff
      Alexandre Duret-Lutz authored
      * src/ltltest/randltl.cc: Document the -wf option.  Declare formula*
      as const.  Simplify GF_n().
      * src/tgbatest/ltl2tgba.cc: Suppress unused variable.
      dcc809ff
    • Ala-Eddine Ben-Salem's avatar
      Update the description of the commands options (-TA,-lv,-sp,-in,-TGTA) · 84b1d24e
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbatest/ltl2tgba.cc: update the description of the options for
      the different kinds of Testing Automata: TA, STA, GTA, SGTA and TGTA.
      84b1d24e
    • 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
  2. 15 Jul, 2012 20 commits
    • Ala-Eddine Ben-Salem's avatar
      BUG FIX in TA construction and minimization · a13d2c8f
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/tgba2ta.cc: BUG FIX in TA construction
      * src/taalgos/minimize.cc: BUG FIX in TA minimization (did_split Flag)
      a13d2c8f
    • Ala-Eddine Ben-Salem's avatar
      STA and TGTA optimisations · 4a1d6dd6
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/tgba2ta.cc: the transformations of TGBA
      4a1d6dd6
    • Ala-Eddine Ben-Salem's avatar
      Improving the construction of TGTA · 4eaa7b24
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/tgba2ta.hh, src/taalgos/tgba2ta.cc:
      optimization of the TGTA automaton obtained from a TGBA.
      4eaa7b24
    • 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
      STA: the artificial livelock state becomes the first successor · d64b4045
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/tgba2ta.cc: improves the STA (Single-pass TA) by adding
      the  artificial livelock state as the first successor.
      d64b4045
    • 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 statement with no effect, to please GCC 4.6. · 1f0bf0b1
      Alexandre Duret-Lutz authored
      * src/taalgos/emptinessta.cc (ta_check::check): Remove statement
      with no effect, to please GCC 4.6.
      1f0bf0b1
    • 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
      Properly free memory and print logs · 422bb842
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/tgbatest/ltl2tgba.cc: Properly free memory
      * src/taalgos/tgba2ta.cc, src/taalgos/emptinessta.cc: print logs
      422bb842
    • 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
      Single-pass Testing Automata (STA) optimizations · c7f4b8e2
      Ala-Eddine Ben-Salem authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/sba2ta.cc, src/taalgos/emptinessta.cc: STA optimizations
      c7f4b8e2
    • 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 TA minimization: merge bisimulating states · cd04d9ac
      Ala Eddine authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * src/taalgos/minimize.hh, src/taalgos/minimize.cc: implements a
      minimization of TA by merging bisimular states.
      * src/taalgos/statessetbuilder.hh, src/taalgos/statessetbuilder.cc:
      returns the set of reachable states of a TA (used in minimize.cc).
      * src/taalgos/Makefile.am: add them.
      * src/tgbatest/ltl2tgba.cc: add commands to test TA minimization
      cd04d9ac
    • 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
  3. 02 Jul, 2012 7 commits
  4. 20 Jun, 2012 4 commits