* src/tgbatest/ltl2tgba.cc: Fix some typos, and factor the second
call to scc_filter when simulations are used.

* wrap/python/spot.i (cosimulation, iterated_simulations): Declare.
* wrap/python/ajax/spot.in, wrap/python/ajax/protocol.txt,
wrap/python/ajax/ltl2tgba.html: Add options to trigger these two
optimizations.

Thomas Badie authored Aug 20, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbatest/ltl2tgba.cc: Change the order of the call to the
simulation and the cosimulation.
Call scc_filter when cosimulation is called with -R3.
Call scc_filter when simulation is called with -R3.

Thomas Badie authored Aug 18, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbaalgos/simulation.cc: Create the iterated_simulations.
(direct_simulation) Add an attribute "stat" that represents the
number of states and transitions of the resulting automaton.
* src/tgbaalgos/simulation.hh: Declare the iterated_simulations.
* src/tgbatest/spotlbtt.test: Test the iterated_simulations.
* src/tgbatest/ltl2tgba.cc: Associate the option -RIS to the
iterated_simulations.

Thomas Badie authored Aug 18, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* bench/ltl2tgba/Makefile.am (run): Remove wfair.txt.
(small.txt, big.txt, known.txt) Add a dependency to ltl2tgba.

Thomas Badie authored Aug 06, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbaalgos/simulation.cc: Add the cosimulation:
(acc_compl_automaton) Add a template parameter.
(acc_compl_automaton::process_link) Add a swap source destination.
(direct_simulation) Add a template parameter.
(direct_simulation::compute_sig) Add a flag in the signature to
know if the state is initial.
(direct_simulation::build_result) Remove the flag before reading
the signature.
Swap source and destination when building the new automaton.
* src/tgbaalgos/simulation.hh: Declare and document the
Cosimulation.
* src/tgbatest/ltl2tgba.cc: Associate the cosimulation with the -RRS
option.
* src/tgbatest/spotlbtt.test: Add a test on the cosimulation.

* src/ltlvisit/apcollect.hh, src/taalgos/minimize.cc,
src/taalgos/tgba2ta.cc, src/tgbatest/ltl2tgba.cc: Here.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: Here.

* wrap/python/ajax/spot.in: Warn about formulae that don't look
stuttering insensitive.

Ala-Eddine Ben-Salem authored Jul 13, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/taalgos/tgba2ta.cc: Set is_accepting_state to false in GTA.
* src/tgbatest/ltl2tgba.cc: Call tgta_explicit.get_ta() to avoid
segfault.

* 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.

* src/taalgos/dotty.cc: Clean up output of TAs.
* src/tgbatest/ltl2tgba.cc: Fix memory management, and use the TA
printer for TGTA.
* wrap/python/spot.i (as_ta): New function to convert a tgta_explicit
into a TA.
* wrap/python/ajax/spot.in: Use this new function to display automata.

* wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/protocol.txt,
wrap/python/ajax/spot.in: Here.

* wrap/python/spot.i: Add wrapper the new TA algorithms.
* wrap/python/ajax/ltl2tgba.html: Add a testing automaton tab.
* wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Support it.

* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: Add a version
that builds a BDD.
* src/tgbatest/ltl2tgba.cc: Use it.

* 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.

* src/ta/Makefile.am, src/taalgos/Makefile.am: Add -I..

* src/tgbatest/ltl2tgba.cc: Introduce -RT to turn on bisimulation on
TA instead of hijacking -Rm.
* src/tgbatest/ltl2ta.test: Adjust.

* src/tgbatest/ltl2ta.test: Adjust expected values.
* src/tgbatest/Makefile.am (TESTS): Add ltl2ta.test.

* src/taalgos/tgba2ta.cc: Adjust to use the sba base class.

* 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().

* src/ltltest/randltl.cc: Document the -wf option.  Declare formula*
as const.  Simplify GF_n().
* src/tgbatest/ltl2tgba.cc: Suppress unused variable.

Ala-Eddine Ben-Salem authored Apr 17, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbatest/ltl2tgba.cc: update the description of the options for
the different kinds of Testing Automata: TA, STA, GTA, SGTA and TGTA.

Ala-Eddine Ben-Salem authored Apr 11, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* src/tgbatest/ltl2tgba.cc, src/ta/Makefile.am, README: code style

Ala-Eddine Ben-Salem authored Apr 11, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* 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

Ala-Eddine Ben-Salem authored Apr 10, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* 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

Ala-Eddine Ben-Salem authored Jan 26, 2012 and Alexandre Duret-Lutz committed Aug 21, 2012

* 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.

Ala-Eddine Ben-Salem authored Dec 22, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* src/taalgos/tgba2ta.cc: BUG FIX in TA construction
* src/taalgos/minimize.cc: BUG FIX in TA minimization (did_split Flag)

Ala-Eddine Ben-Salem authored Dec 14, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* src/taalgos/tgba2ta.cc: the transformations of TGBA

Ala-Eddine Ben-Salem authored Dec 08, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* src/taalgos/tgba2ta.hh, src/taalgos/tgba2ta.cc:
optimization of the TGTA automaton obtained from a TGBA.

Ala-Eddine Ben-Salem authored Dec 06, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* src/ta/taproduct.cc, src/taalgos/emptinessta.cc:
remove unused (commented) code.

Ala-Eddine Ben-Salem authored Nov 27, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* src/taalgos/tgba2ta.cc: improves the STA (Single-pass TA) by adding
the  artificial livelock state as the first successor.

Ala-Eddine Ben-Salem authored Nov 25, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* 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.

Ala-Eddine Ben-Salem authored Nov 23, 2011 and Alexandre Duret-Lutz committed Jul 15, 2012

* 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.

* src/taalgos/emptinessta.cc (ta_check::check): Remove statement
with no effect, to please GCC 4.6.