alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • f38f9df020 * src/ltlvisit/tostring.hh: Cosmetics. Alexandre Duret-Lutz 2012-08-31 14:09:33 +02:00
  • a0e1a144ad ltlfilt: initial implementation. Alexandre Duret-Lutz 2012-08-31 13:41:22 +02:00
  • eb5de929ca ta: compatibility with Swig 1.3. Alexandre Duret-Lutz 2012-09-04 14:04:28 +02:00
  • 5939d6f493 Add back the '*' syntax for And. Alexandre Duret-Lutz 2012-08-29 18:05:31 +02:00
  • 60ec3acea0 Add an option to use WDBA only if it reduces the size of the automaton. Alexandre Duret-Lutz 2012-08-28 10:25:02 +02:00
  • f7af4e65f6 CGI: Do not call any simulation on WDBA's success. Alexandre Duret-Lutz 2012-08-24 13:34:39 +02:00
  • 70306d184e CGI: Better call of scc_filter. Alexandre Duret-Lutz 2012-08-23 09:24:30 +02:00
  • dce79ffed5 * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2012-08-22 15:16:46 +02:00
  • 8cb68d76b5 * NEWS, buddy/src/bddop.c, m4/valgrind.m4: s/wether/whether/. Alexandre Duret-Lutz 2012-08-22 13:53:59 +02:00
  • 2ea652d32c Cleanup ltl2tgba.cc. Alexandre Duret-Lutz 2012-08-21 16:38:49 +02:00
  • 74bd671350 Add cosimulation and iterated_simulations to the web interface. Alexandre Duret-Lutz 2012-08-21 16:26:28 +02:00
  • 84b6240aa9 * src/tgbaalgos/simulation.hh: Improve documentation. Alexandre Duret-Lutz 2012-08-21 15:26:42 +02:00
  • 25b8d50cf0 Optimize the use of -RRS with -R3. Thomas Badie 2012-08-20 17:34:20 +02:00
  • 0b74f54912 * src/tgbaalgos/simulation.cc: Fix a bug in the simulation. Thomas Badie 2012-08-20 17:01:47 +02:00
  • bd9e42dd68 * bench/ltl2tgba/lbtt2csv.pl: Fix a bug when using big.log. Thomas Badie 2012-08-20 16:19:47 +02:00
  • a0cce10512 Create the iterated simulations. Thomas Badie 2012-08-18 15:30:43 +02:00
  • 242386b19a Add missing dependencies to the ltl2tgba benchmark Makefile. Thomas Badie 2012-08-18 11:46:01 +02:00
  • 387bace98b Create the cosimulation. Thomas Badie 2012-08-06 18:57:26 +02:00
  • aa230d1f8b 80 columns. Alexandre Duret-Lutz 2012-08-21 14:18:13 +02:00
  • 173e100a41 ltl2tgba.html: Draw a run by default, don't print it. Alexandre Duret-Lutz 2012-07-18 15:28:36 +02:00
  • ebf48d4fa4 * wrap/python/ajax/ltl2tgba.html: Remember killed blocks. Alexandre Duret-Lutz 2012-07-17 17:42:00 +02:00
  • 8d2d9be39c ltl2tgba.html: Add a warning. Alexandre Duret-Lutz 2012-07-15 18:30:45 +02:00
  • e30b92327a Set is_accepting_state to false in GTA Ala-Eddine Ben-Salem 2012-07-13 17:59:39 +02:00
  • 941cb0b57b Fix tgta_explicit not to inherit from ta_explicit to please clang++. Alexandre Duret-Lutz 2012-06-28 16:55:36 +02:00
  • d4130f15bf Clean up dotty output of TAs. Alexandre Duret-Lutz 2012-06-27 17:20:53 +02:00
  • 852cd0d553 ltl2tgba.html: Add testing automata options. Alexandre Duret-Lutz 2012-06-26 19:37:07 +02:00
  • 27a2de331f ltl2tgba.html: Preliminary support for TA Alexandre Duret-Lutz 2012-06-24 21:57:50 +02:00
  • 20c3f9f8ba Simplify the construction of TA. Alexandre Duret-Lutz 2012-06-24 21:56:47 +02:00
  • 8e1438c98f Don't always delete the tgba used in ta_explicit. Alexandre Duret-Lutz 2012-06-24 21:54:52 +02:00
  • be6071184e Fix ta/ and taalgos/ include path for VPATH builds. Alexandre Duret-Lutz 2012-06-24 17:07:22 +02:00
  • 20c7f1e8cf Don't use -Rm for two different things. Alexandre Duret-Lutz 2012-06-24 13:35:12 +02:00
  • 6bd905c63e Fix, run, and distribute ltl2ta.test. Alexandre Duret-Lutz 2012-06-24 13:07:18 +02:00
  • 2462a3d570 Post-rebase fixup. Alexandre Duret-Lutz 2012-06-24 13:05:29 +02:00
  • 67bbe6a6c7 Fixes to pass sanity checks. Alexandre Duret-Lutz 2012-05-26 16:23:31 +02:00
  • dcc809ff4a Post rebase fixups. Alexandre Duret-Lutz 2012-05-26 12:26:20 +02:00
  • 84b1d24e8f Update the description of the commands options (-TA,-lv,-sp,-in,-TGTA) Ala-Eddine Ben-Salem 2012-04-17 15:26:14 +02:00
  • 9319b0ca25 Changes in order to pass sanity tests Ala-Eddine Ben-Salem 2012-04-11 18:52:03 +02:00
  • 618146c157 Changes to pass sanity tests Ala-Eddine Ben-Salem 2012-04-11 11:15:19 +02:00
  • 5a706300b0 Stable version of TGTA approach implementation (automaton + product) Ala-Eddine Ben-Salem 2012-04-10 23:30:03 +02:00
  • c76e651bad Doxygen comments. Ala-Eddine Ben-Salem 2012-01-26 17:34:22 +01:00
  • a13d2c8fc7 BUG FIX in TA construction and minimization Ala-Eddine Ben-Salem 2011-12-22 22:56:05 +01:00
  • 4a1d6dd67c STA and TGTA optimisations Ala-Eddine Ben-Salem 2011-12-14 15:19:32 +01:00
  • 4eaa7b24df Improving the construction of TGTA Ala-Eddine Ben-Salem 2011-12-08 20:11:06 +01:00
  • db2fcfa97a Cleaning code of TA Product and Emptiness-check Ala-Eddine Ben-Salem 2011-12-06 16:01:37 +01:00
  • d64b40452c STA: the artificial livelock state becomes the first successor Ala-Eddine Ben-Salem 2011-11-27 14:23:18 +01:00
  • ed27dab306 Add an implementation of TGTA minimization Ala-Eddine Ben-Salem 2011-11-25 10:16:49 +01:00
  • c882eadda6 New Automata: TGTA (Transition-based Generalized TA) Ala-Eddine Ben-Salem 2011-11-23 12:24:25 +01:00
  • 1f0bf0b1cf Remove statement with no effect, to please GCC 4.6. Alexandre Duret-Lutz 2011-08-31 18:39:28 +02:00
  • 29ee11cfd3 Remove unused argument in constructor. Alexandre Duret-Lutz 2011-08-31 18:32:33 +02:00
  • 422bb842bf Properly free memory and print logs Ala-Eddine Ben-Salem 2011-08-31 18:32:25 +02:00
  • 83e7f0fa18 GTA (Generalized Testing Automata) implementation Ala-Eddine Ben-Salem 2011-07-05 21:26:22 +02:00
  • c7f4b8e262 Single-pass Testing Automata (STA) optimizations Ala-Eddine Ben-Salem 2011-06-28 13:43:33 +02:00
  • 782ba0010b Add a new form of TA with a Single-pass emptiness check (STA) Ala-Eddine Ben-Salem 2011-05-17 23:41:45 +02:00
  • 310973f88c Improvement of TA Product/Minimisation and of WFair generation Ala-Eddine Ben-Salem 2011-04-12 14:22:49 +02:00
  • 2aad5b10d2 TA Product optimization and WFair Formulas generation Ala-Eddine Ben-Salem 2011-04-06 22:15:05 +02:00
  • c774ba141d Use downcast when appropriate. Alexandre Duret-Lutz 2011-04-06 11:03:29 +02:00
  • bf01501e15 Impacts of the new method state.destroy() Ala Eddine 2011-04-04 11:01:27 +02:00
  • cd04d9acf3 Add TA minimization: merge bisimulating states Ala Eddine 2011-03-08 15:06:56 +01:00
  • 81e80e6069 Add Testing Automata Product & Emptiness Check Ala Eddine 2011-02-11 11:40:21 +01:00
  • ba47b821c6 Preliminary implementation of Testing Automata. Ala Eddine 2010-12-02 12:04:29 +01:00
  • c373a2f35e * NEWS, configure.ac: Bump version to 0.9.2a. Alexandre Duret-Lutz 2012-07-02 18:02:49 +02:00
  • ddb18b4084 Relase Spot 0.9.2. Alexandre Duret-Lutz 2012-07-02 14:45:34 +02:00
  • 85391ab9fe * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add loading.gif. Alexandre Duret-Lutz 2012-07-02 17:25:51 +02:00
  • fc22fe56e4 * NEWS: Mention recent changes. Alexandre Duret-Lutz 2012-07-02 12:52:02 +02:00
  • 786499534f Please the upcoming g++ 4.8. Alexandre Duret-Lutz 2012-06-28 17:10:49 +02:00
  • 3793454864 [lbtt] Fix issues reported by Clang++ 3.1. Alexandre Duret-Lutz 2012-06-27 18:07:42 +02:00
  • 141baae57e ltl2tgba.html: Use the new degeneralization routine. Alexandre Duret-Lutz 2012-06-26 18:35:08 +02:00
  • bc5a4ba416 [buddy] Fix the recent Automake workaround for VPATH builds. Alexandre Duret-Lutz 2012-06-20 20:52:25 +02:00
  • 3acc53d55a Add a bench script for the output of `lbtt'. Thomas Badie 2012-06-19 18:35:00 +02:00
  • 0c1fec1259 LTL parser: better error recovery. Alexandre Duret-Lutz 2012-06-19 23:43:36 +02:00
  • ac41825efd * src/tgbaalgos/degen.cc (~unicity_table): Accommodate g++ 4.0.1. Alexandre Duret-Lutz 2012-06-20 08:30:11 +02:00
  • d5bb0ffe89 Fix a perl warning in `parseout.pl'. Thomas Badie 2012-06-19 18:26:11 +02:00
  • 6d047a1d6b Document recent changes. Alexandre Duret-Lutz 2012-06-19 22:13:00 +02:00
  • bb8142910e * wrap/python/ajax/ltl2tgba.html: Typos, and better WDBA doc. Alexandre Duret-Lutz 2012-06-17 14:30:55 +02:00
  • 601fbedbf6 * wrap/python/ajax/ltl2tgba.html: Add a favicon link. Alexandre Duret-Lutz 2012-06-15 09:56:35 +02:00
  • b0193e1418 Apply Jan's comments on ltl3ba's interface. Alexandre Duret-Lutz 2012-06-14 19:57:03 +02:00
  • 5c04022505 * wrap/python/ajax/ltl2tgba.html: Add tooltips for LTL, PSL, SERE. Alexandre Duret-Lutz 2012-06-13 15:48:57 +02:00
  • c4c42a37c6 ltl2tgba.html: Update tooltips with Tomáš Babiak's comments. Alexandre Duret-Lutz 2012-06-04 20:42:03 +02:00
  • 8d9d0f7b5b ltl2tgba.html: add meta description, and validate page. Alexandre Duret-Lutz 2012-06-02 11:42:07 +02:00
  • 81d3ee48f0 ltl2tgba.html: Display a loading logo for delayed results. Alexandre Duret-Lutz 2012-06-02 11:06:19 +02:00
  • bfc668246c Add more ltl3ba options. Alexandre Duret-Lutz 2012-05-30 20:15:05 +02:00
  • 689f56f480 ltl2tgba.html: Detect ltl3ba's presence and version. Alexandre Duret-Lutz 2012-05-23 19:47:17 +02:00
  • 04cc63cac2 Use tgba_explicit_numbered to create SCC-filtered automata. Alexandre Duret-Lutz 2012-05-23 17:00:28 +02:00
  • 988e7e2499 Preliminary work on integrating LTL3BA in ltl2tgba.html. Alexandre Duret-Lutz 2012-05-23 11:50:21 +02:00
  • 7ceca326ad Small speedup in sba_explicit::state_is_accepting(). Alexandre Duret-Lutz 2012-06-14 17:15:31 +02:00
  • 09864a9d3c * NEWS: Mention that Safra is faster. Alexandre Duret-Lutz 2012-06-14 16:56:29 +02:00
  • 334366a78c * src/tgba/tgbasafracomplement.cc: Use the new offline degeneralization. Alexandre Duret-Lutz 2012-06-14 16:52:49 +02:00
  • 59dc4a9822 * src/tgbaalgos/degen.cc: Use a small map instead of merge_transitions. Alexandre Duret-Lutz 2012-06-14 16:24:42 +02:00
  • 509fb7e2a8 * src/tgbaalgos/degen.cc: Use the new bdd_implies() function. Alexandre Duret-Lutz 2012-06-14 15:17:45 +02:00
  • b7c77dca31 * src/tgbatest/ltl2tgba.cc: Clock the degeneralization. Alexandre Duret-Lutz 2012-06-14 15:16:58 +02:00
  • 59a2763f41 * src/tgbaalgos/degen.cc (outgoing_acc): Fill both caches at once. Alexandre Duret-Lutz 2012-06-05 08:05:18 +02:00
  • 5dbee4faab Offline version of the degeneralization. Alexandre Duret-Lutz 2012-06-04 23:12:04 +02:00
  • b68d9d189c * NEWS: Summarize recent BDD speedups. Alexandre Duret-Lutz 2012-06-14 14:41:13 +02:00
  • 3a1a71016d * m4/buddy.m4: Check for bdd_implies. Alexandre Duret-Lutz 2012-06-14 14:26:55 +02:00
  • 484ea488c3 Use bdd_implies() to speedup various algorithms. Alexandre Duret-Lutz 2012-06-13 21:16:33 +02:00
  • 821d5e54b7 Export bdd_implies to the Python interface, and test it. Alexandre Duret-Lutz 2012-06-13 17:57:07 +02:00
  • a814b97543 [buddy] Add a function bdd_implies to decide implications between BDDs. Alexandre Duret-Lutz 2012-06-13 17:56:37 +02:00
  • e7a46e10e2 [buddy] Reduce the size of bddNode to improve cache efficiency. Alexandre Duret-Lutz 2012-06-08 11:28:48 +02:00
  • 96c436e0e2 Accomodate Automake 1.12.x. Alexandre Duret-Lutz 2012-06-19 19:03:01 +02:00
  • e9e132dd29 [lbtt] Adjust parsers to accommodate old and new versions of Automake. Alexandre Duret-Lutz 2012-06-19 17:21:28 +02:00