1. 15 Jul, 2012 6 commits
    • 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
      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'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
  2. 19 Jun, 2012 2 commits
  3. 20 May, 2012 4 commits
  4. 10 May, 2012 1 commit
  5. 03 May, 2012 1 commit
  6. 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
  7. 30 Apr, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Make it possible to output UTF-8 for dotty(). · e93ceeba
      Alexandre Duret-Lutz authored
      * src/tgba/tgbaexplicit.hh: Rerganize a bit to
      allow different functions to be used to format
      states.  Add an enabled_utf8() method to
      tgba_explicit_formula.
      * src/tgbaalgos/dotty.hh, src/tgbaalgos/dotty.cc:
      Simplify the interface by not depending on
      dotty_decorator explicitely.
      * src/tgba/bddprint.hh (enable_utf8): New function.
      * src/tgba/bddprint.cc (enable_utf8): Implement it
      and use the global utf8 flag in other functions.
      * src/tgbatest/ltl2tgba.cc: Add an -8 option for
      UTF-8 outpout.
      * wrap/python/spot.i: Adjust for tgbexplicit.hh
      changes.
      e93ceeba
  8. 28 Apr, 2012 4 commits
    • Alexandre Duret-Lutz's avatar
      Make sure PSL formulae are translated with the FM translation. · 3dfde9e8
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc: Diagnose attempt to use -l and -taa
      on PSL formulae.  Switch back to -f for these formulae.
      3dfde9e8
    • Alexandre Duret-Lutz's avatar
      Translate Boolean formulae as BDD using the ltl_simplifier cache. · 07e40e70
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.hh, src/ltlvisit/simplify.cc
      (ltl_simplifier::ltl_simplifier, ltl_simplifier::get_dict): Make
      it possible to supply and retrieve the dictionary used.
      (ltl_simplifier::as_bdd): New function, exported from the cache.
      * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Store the
      ltl_simplifier object.
      (translate_dict::boolean_to_bdd): Call ltl_simplifier::as_bdd.
      (translate_ratexp): New wrapper around the ratexp_trad_visitor,
      calling boolean_to_bdd whenever possible.
      (ratexp_trad_visitor): Do not deal with negated formulae, there
      are necessarily Boolean and handled by translate_ratexp().
      (ltl_visitor): Adjust to call translate_ratexp.
      (ltl_to_tgba_fm): Adjust passing of the ltl_simplifier to the
      translate_dict, and make sure everybody is using the same
      dictionary.
      * src/tgbatest/ltl2tgba.cc: Pass the dictionary to the
      ltl_simplifier.
      07e40e70
    • Alexandre Duret-Lutz's avatar
      Mark reduce_tau03() as deprecated. · b89f86ed
      Alexandre Duret-Lutz authored
      * src/ltlvisit/contain.hh (reduce_tau03): Mark as deprecated.
      * src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/ltl2tgba.cc,
      src/ltltest/equals.cc: Do not include ltlvisit/contain.hh, since
      it's not used.
      b89f86ed
    • Alexandre Duret-Lutz's avatar
      Deprecate reduce() in favor of ltl_simplifier. · 67f4e8b5
      Alexandre Duret-Lutz authored
      * src/ltlvisit/reduce.hh: Mark the file as obsolete.
      (reduce): Declare this function as obsolete.
      * src/ltlvisit/reduce.cc: Define SKIP_DEPRECATED_WARNING
      so we can include reduce.hh.
      * src/sanity/includes.test: Also use SKIP_DEPRECATED_WARNING
      when compiling headers.
      * iface/dve2/dve2check.cc,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/randtgba.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i: Adjust
      to use ltl_simplifier.
      * src/tgbatest/ltl2tgba.cc: Adjust to use ltl_simplifier,
      and replace -fr1...-fr7 options by a single -fr option.
      * src/tgbatest/spotlbtt.test: Adjust -fr flags accordingly.
      * src/tgbatest/reductgba.cc: Do not include reduce.hh.
      67f4e8b5
  9. 27 Apr, 2012 2 commits
    • Alexandre Duret-Lutz's avatar
      Change the simulation option from -RSD to -RDS and document it. · 324802c0
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc: Here.
      * src/tgbatest/spotlbtt.test: Adjust.
      324802c0
    • Alexandre Duret-Lutz's avatar
      Remove the old broken game-theory-based simulation reductions. · 7e587584
      Alexandre Duret-Lutz authored
      This implementation of direct simulation was only working on
      degeneralized automata, and produce automata that are inferiors to
      those output by the new direct simulation implementation (in
      tgba/simulation.hh) which can also work on TGBA.  The delayed
      simulation has never been reliable.  It's time for some spring
      cleaning.
      
      * src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Delete.
      * src/tgba/Makefile.am: Adjust.
      * src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh:
      Remove all code, and keep only a deprecated replacement
      from reduc_tgba_sim().
      * src/tgbaalgos/reductgba_sim_del.cc: Delete.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/tgbatest/reduccmp.test, src/tgbatest/reductgba.cc,
      src/tgbatest/reductgba.test: Delete.
      * src/tgbatest/Makefile.am: Adjust.
      * src/tgbatest/ltl2tgba.cc: Undocument options -R1s, -R1t,
      -R2s, -R2t, and implement them using the new direct simulation.
      Remove options -Rd and -RD.
      * src/tgbatest/spotlbtt.test: Remove entry using these old options.
      * wrap/python/spot.i: Do not process tgbaalgos/reductgba_sim.cc.
      7e587584
  10. 18 Apr, 2012 1 commit
    • Thomas Badie's avatar
      Create the direct simulation. · 876f8c90
      Thomas Badie authored
      * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: New files.
      * src/tgbaalgos/Makefile.am: Add the new files to the compilation.
      * src/tgbatest/spotlbtt.test: Add the simulation.
      * src/tgbatest/ltl2tgba.cc: Add direct simulation (-RSD).
      876f8c90
  11. 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
  12. 16 Dec, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Perform WDBA minimization before degeneralization. · e531da8d
      Alexandre Duret-Lutz authored
      There is no point in degeneralizing an automaton if it can be WDBA
      minimized.  Doing so will only augment the number of states and
      slow down the powerset construction used by the WDBA minimization.
      
      * src/tgbatest/babiak.test: New file.  It includes 5 formulae
      which Tomáš Babiak reported Spot 0.7.1 would take over one hour to
      translate if degeneralization and WDBA minimization were both
      requested.
      * src/tgbatest/Makefile.am (TESTS): Add it.
      * src/tgbatest/ltl2tgba.cc: Do WDBA minimization before
      degeneralization.  The above formulae are now all translated in a
      few seconds.
      e531da8d
  13. 28 Nov, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Add an ltl2tgba option to read Kripke structure. · ba3108f9
      Alexandre Duret-Lutz authored
      Also offers two ways to output Kripke structures.
      
      * src/kripketest/parse_print_test.cc, src/kripke/kripkeexplicit.cc
      : Simplify includes.
      * src/kripke/kripkeprint.hh (kripke_save_reachable,
      kripke_save_reachable_renumbered): New declarations.
      (KripkePrinter): Move and rename...
      * src/kripke/kripkeprint.cc (kripke_printer): ... here.
      (kripke_printer_renumbered): New class.
      (kripke_save_reachable, kripke_save_reachable_renumbered): New
      function.
      * src/tgbatest/ltl2tgba.cc: Add an option to read Kripke
      structures.
      * iface/dve2/dve2check.cc: Use kripke_save_reachable_renumbered.
      * iface/dve2/defs.in (run2): Remove.
      * iface/dve2/kripke.test: Adjust tests.
      ba3108f9
  14. 25 Aug, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Running `ltl2tgba -R1q -R1t -N` would degeneralize before and · d8ba172e
      Alexandre Duret-Lutz authored
      after the simulation-reduction.
      
      Report from Tomáš Babiak <xbabiak@fi.muni.cz>.
      
      * src/tgbaalgos/neverclaim.hh (never_claim_reachable): Take
      a tgba as input.
      * src/tgbaalgos/neverclaim.cc (never_claim_bfs): Call
      state_is_accepting() only if this tgba turns out to be
      a tgba_sba_proxy.  Otherwise check the acceptance of one
      outgoing transition as we do in dotty_bfs since 2011-03-05.
      * src/tgbatest/ltl2tgba.cc: Do not redegeneralize before
      calling never_claim_reachable() if we know the automaton is
      degeneralized already.
      * src/tgbatest/ltl2tgba.test: Add a test case.
      d8ba172e
  15. 17 Aug, 2011 1 commit
  16. 05 Mar, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Using double borders for acceptance states in SBAs. · e1ef47d9
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
      assume_sba argument.
      * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
      mark_accepting_states arguments.
      (dotty_bfs::process_state): Check if a state is accepting using
      the state_is_accepting() method for tgba_sba_proxies, or by
      looking at the first outgoing transition of the state.  Pass
      the result to the dectorator.
      (dotty_reachable): Adjust function.
      * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
      (state_decl): Add an "accepting" argument, and use it to
      decorate accepting states with a double border.
      * src/tgbatest/ltl2tgba.cc: Keep track of whether the output
      is an SBA or not, so that we can tell it to dotty().
      * wrap/python/ajax/spot.in: Likewise.
      * wrap/python/cgi-bin/ltl2tgba.in: Likewise.
      e1ef47d9
  17. 04 Feb, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Add a way to count the number of sub-transitions. · 30727074
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/stats.hh (tgba_sub_statistics): New class.
      (sub_stats_reachable): New function.
      * src/tgbaalgos/stats.cc (sub_stats_bfs): New class.
      (tgba_sub_statistics::dump, sub_stats_reachable): New function.
      * src/tgbatest/ltl2tgba.cc (-kt): New option.
      * src/tgbatest/ltl2tgba.test: Use -kt.
      30727074
  18. 27 Jan, 2011 2 commits
    • Alexandre Duret-Lutz's avatar
      Report formulas that are both safety and guarantee. · c8140de9
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (-O): Report formulas that are both
      safety and guarantee.
      * src/tgbatest/obligation.test: Add cases.
      c8140de9
    • 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
  19. 05 Jan, 2011 8 commits
    • Alexandre Duret-Lutz's avatar
      Cleanup the minimize.hh interface. · 8c972ad3
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
      (minimize): Split into ...
      (minimize_wdba, minimize_monitor): ... these two functions.
      * src/tgbatest/ltl2tgba.cc (main): Adjust the call to
      minimize_monitor.
      * wrap/python/cgi-bin/ltl2tgba.in: Adjust the calls to
      minimize_monitor and minimize_obligation.
      * wrap/python/spot.i: Declare minimize_monitor, minimize_wdba,
      minimize_obligations.
      * src/tgba/tgbaexplicit.hh (tgba_explicit_string)
      (tgba_explicit_formula, tgba_explicit_number): Add fake
      declarations so that SWIG can see they inherits from tgba.
      8c972ad3
    • Alexandre Duret-Lutz's avatar
      Move the logic for detecting when the minimize() algorithm is · 907d173d
      Alexandre Duret-Lutz authored
      correct from ltl2tgba to the library.
      
      * src/tgbaalgos/minimize.hh,
      src/tgbaalgos/minimize.cc (minimize_obligation): New function.
      * src/tgbatests/ltl2tgba.cc (main): Fix constness of automata,
      and call minimize_obligation() for -R3b.
      907d173d
    • Alexandre Duret-Lutz's avatar
      * src/tgbatest/ltl2tgba.cc (syntax): Regroup -M, -s, and -S option · 0392058e
      Alexandre Duret-Lutz authored
      under the same heading "automaton conversion".
      0392058e
    • Alexandre Duret-Lutz's avatar
      Preliminary support for monitors. · cc8dd49d
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (-M): New option for building
      deterministic monitors.
      * src/tgbaalgos/minimize.cc (minimize): Take a monitor
      argument and adjust the code.
      * src/tgbaalgos/minimize.hh (minimize): Document it.
      cc8dd49d
    • Alexandre Duret-Lutz's avatar
      "ltl2tgba -Rm -X foo.tgba" would fail. · a962bb6d
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Warn if -Rm is used without
      knowing the formula whose automaton is minimized.
      a962bb6d
    • Alexandre Duret-Lutz's avatar
      "ltl2tgba -Rm" will apply WDBA-minimization only if correct. · 54e10c25
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Use WDBA-minimization only when
      it is correct. Either we can quickly determine that a formula or
      its negation is a safety formula, or we can slowly check the
      equivalence of the WDBA-minimized automaton and the original
      automaton.
      * src/tgbatest/wdba.test: New test.
      * src/tgbatest/safety.test: Adjust comment.
      * src/tgbatest/spotlbtt.test: Use -Rm.
      * src/tgbatest/Makefile.am (TESTS): Add wdba.test.
      54e10c25
    • Alexandre Duret-Lutz's avatar
      Better resource handling in minimization. · f9e84ac2
      Alexandre Duret-Lutz authored
      * src/tgbatest/ltl2tgba.cc (main): Delete the minimized automaton.
      * src/tgbaalgos/minimize.cc (minimize): Remove the call to
      unregister_variable() at the end.  It was both
      wrong (unregistering only the first variable) and useless ("delete
      del_a" will unregister all these variables).  Use a map and a set
      to keep track of free BDD variable and reuse them, otherwise the
      algorithm would sometimes use more variables than allocated.
      f9e84ac2
    • Alexandre Duret-Lutz's avatar
      Implement is_safety_automaton(). · 0af8d032
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/safety.hh, src/tgbaalgos/safety.cc: New
      files.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgbatests/ltl2tgba.cc: Add option "-O".
      * src/tgbaalgos/scc.hh: Update documentation.
      * src/tgbatest/Makefile.am (TESTS): Add safety.test.
      * src/tgbatest/safety.test: New file.
      0af8d032