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

Commit graph

  • 2fb436a174 Replace most uses of scc_map by scc_info. Alexandre Duret-Lutz 2014-10-07 18:21:37 +02:00
  • b6745482af * src/tgba/tgbagraph.cc: Improve comment. Alexandre Duret-Lutz 2014-10-08 16:52:30 +02:00
  • 1696fac80c tgbagraph: fix detection of dead transitions Alexandre Duret-Lutz 2014-10-08 16:50:54 +02:00
  • 645ecce1c9 Some cleanup of Thibaud's patches. Alexandre Duret-Lutz 2014-10-06 19:38:36 +02:00
  • 4e1586dc54 ltlcross: adding option --grind=FILENAME Thibaud Michaud 2014-09-19 16:34:00 +02:00
  • e327f6ea11 Adding ltlgrind as a command-line tool Thibaud Michaud 2014-09-12 15:39:01 +02:00
  • 51fe5108fe Remove support for state-based alternating automata. Alexandre Duret-Lutz 2014-10-06 10:31:53 +02:00
  • 2c764fb3c7 Store membership to acceptance sets using bitsets, not BDDs. Alexandre Duret-Lutz 2014-09-29 18:17:34 +02:00
  • 37ece2b878 * src/graphtest/tgbagraph.cc: Add parentheses to please gcc-snapshot. Alexandre Duret-Lutz 2014-09-29 18:17:34 +02:00
  • 8c2efa6615 Merge branch 'master' into next Alexandre Duret-Lutz 2014-09-29 18:07:34 +02:00
  • c7f98fd7f7 hoaf: rename I(i) as Inf(i). Alexandre Duret-Lutz 2014-09-06 11:15:45 +02:00
  • d401fadc65 neverparse: diagnose redefinition of state labels Alexandre Duret-Lutz 2014-08-31 19:07:53 +02:00
  • 9a8becb8d8 ltlcross: fix missing check for complement of negative automata Alexandre Duret-Lutz 2014-08-31 18:12:28 +02:00
  • 49a0997866 ltlcross: add --verbose option Alexandre Duret-Lutz 2014-08-31 17:50:46 +02:00
  • 261b073ae7 * doc/org/ltlcross.org: Typos. Alexandre Duret-Lutz 2014-08-31 17:01:49 +02:00
  • 359e0c6fb4 remove wdbacomp.cc and wdbacomp.hh Alexandre Duret-Lutz 2014-08-31 00:54:52 +02:00
  • c8b399c02a Remove futurecondcol and tgbascc. Alexandre Duret-Lutz 2014-08-30 23:23:59 +02:00
  • baf644a93a python: add an SVG printer for automata Alexandre Duret-Lutz 2014-08-24 17:21:47 +02:00
  • ae35cc29f5 Better formula I/O for ipython. Alexandre Duret-Lutz 2014-08-24 14:00:59 +02:00
  • 6d7c258fd7 Use shared_ptr for the emptiness check interfaces. Alexandre Duret-Lutz 2014-08-23 18:34:00 +02:00
  • 803e17bb8d apcollect: Fix prototype. Alexandre Duret-Lutz 2014-08-23 18:33:10 +02:00
  • c3c02bfb44 Remove useless forward declarations of class tgba. Alexandre Duret-Lutz 2014-08-23 13:10:24 +02:00
  • 4d82ca7055 * src/tgbaalgos/hoaf.hh: Typos in comments. Alexandre Duret-Lutz 2014-08-22 17:37:58 +02:00
  • 92848f73af * src/tgbaalgos/hoaf.hh: Typos in comments. Alexandre Duret-Lutz 2014-08-22 17:37:58 +02:00
  • 700cf88b06 Merge branch master (Spot 1.2.5) into next. Alexandre Duret-Lutz 2014-08-22 16:45:41 +02:00
  • 3152c1a6cb * NEWS, configure.ac: Bump version to 1.2.5a. Alexandre Duret-Lutz 2014-08-22 00:11:00 +02:00
  • 290106b0a4 Release Spot 1.2.5. Alexandre Duret-Lutz 2014-08-21 15:46:50 +02:00
  • a72b84b0b4 * src/tgbatest/ltlcross.test: More formulas from Joachim. Alexandre Duret-Lutz 2014-08-21 23:06:33 +02:00
  • 408dc878e5 ltl2tgba_fm: fix translation of !{f} as done last year for {f} Alexandre Duret-Lutz 2014-08-21 17:36:34 +02:00
  • d3ddd724c9 * doc/org/satmin.org: Tweak so org-mode does not botch the output. Alexandre Duret-Lutz 2014-08-21 15:45:56 +02:00
  • bab579cf9d ltl2tgba.html: Separate the ltl3ba tabs from the others. Alexandre Duret-Lutz 2014-08-21 15:28:30 +02:00
  • 85beeec2e4 ltl2tgba.html: Add option to output LBT format. Alexandre Duret-Lutz 2014-08-21 15:18:43 +02:00
  • d9d9837e55 * wrap/python/ajax/ltl2tgba.html: Update tooltips. Alexandre Duret-Lutz 2014-08-21 15:04:12 +02:00
  • 829012fe43 ltlcross: implement a --save-bogus=FILENAME option Alexandre Duret-Lutz 2014-08-21 14:54:29 +02:00
  • 2227ad60cf randltl: do not reset the seed between formulas Alexandre Duret-Lutz 2014-08-21 13:23:36 +02:00
  • 44fc323e7b randltl: accept a number of atomic propositions Alexandre Duret-Lutz 2014-08-21 13:17:18 +02:00
  • 310a98c15a hoaf: first implementation of the HOA Format output. Alexandre Duret-Lutz 2014-06-01 19:44:43 +02:00
  • e997676c3e Support LBT formula in ltl2tgba.html. Alexandre Duret-Lutz 2014-08-20 21:40:51 +02:00
  • e78548ebae ltlcross: display formulas in blue instead of white Alexandre Duret-Lutz 2014-08-20 21:29:57 +02:00
  • 795c2f1720 ltl2tgba_fm: Fix incorrect simplification of promises for M Alexandre Duret-Lutz 2014-08-20 20:52:18 +02:00
  • edb220af6a dtbasat,dtgbasat: rewrite using the tgba_digraph interface Alexandre Duret-Lutz 2014-08-20 16:11:50 +02:00
  • 99d28c3cc2 * src/tgbaalgos/complete.cc: Introduce a sink state only if needed. Alexandre Duret-Lutz 2014-08-20 16:11:00 +02:00
  • d28e7f9c5c graph: Add a is_dead_transition method. Alexandre Duret-Lutz 2014-08-20 16:09:53 +02:00
  • 73e74c0ad3 * src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh: Cleanup. Alexandre Duret-Lutz 2014-08-20 10:33:10 +02:00
  • 5c9a5403fe use scc_info instead of scc_map in a couple of easy places Alexandre Duret-Lutz 2014-08-20 10:03:21 +02:00
  • 14570f62d0 bivect: workaround flexible arrays not being standard C++ Alexandre Duret-Lutz 2014-08-19 22:50:08 +02:00
  • 52ce449bbc tgba: merge succiter.hh, state.hh, and tgba.hh Alexandre Duret-Lutz 2014-08-19 21:48:32 +02:00
  • a5bc7c3ff6 * src/misc/bitvect.hh (bitvect_array): Make as SPOT_DELETED. Alexandre Duret-Lutz 2014-08-19 16:15:02 +02:00
  • e7dc62e3c8 * NEWS: Add more news. Alexandre Duret-Lutz 2014-08-19 14:57:35 +02:00
  • e5124faa13 man: more doc about TGBA and monitors Alexandre Duret-Lutz 2014-08-19 14:52:51 +02:00
  • 06a0c498a4 * src/bin/common_setup.cc: Disable sync_with_stdio to boost I/O. Alexandre Duret-Lutz 2014-08-19 10:01:29 +02:00
  • bc2e68f85c tgbatest: rewrite emptchk.test in C++ Alexandre Duret-Lutz 2014-08-18 23:58:00 +02:00
  • b360b02290 tgbatest: speed ltl2ta.test up! Alexandre Duret-Lutz 2014-08-18 19:00:31 +02:00
  • 9502266f95 tgbatest: implement a large part of ltl2tgba.test in c++ Alexandre Duret-Lutz 2014-08-17 19:43:54 +02:00
  • 6a741189bc ltltest: speedup more tests Alexandre Duret-Lutz 2014-08-17 12:22:06 +02:00
  • 7b9f695265 Speedup reduccmp.test Alexandre Duret-Lutz 2014-08-17 11:22:00 +02:00
  • b43f75e917 tgba: move boolean properties from tgba_digraph to tgba Alexandre Duret-Lutz 2014-08-15 16:10:39 +02:00
  • e3b5119f25 degen: return input if it is already degeneralized Alexandre Duret-Lutz 2014-08-15 11:24:41 +02:00
  • bf6c906772 Fix some bdd_dict_ptr not being passed by const reference. Alexandre Duret-Lutz 2014-08-15 11:04:16 +02:00
  • 51151ab271 Handle all automata through shared_ptr. (monstro patch) Alexandre Duret-Lutz 2014-08-14 20:18:04 +02:00
  • ca85d4184d tgba_union: Remove this unused class. Alexandre Duret-Lutz 2014-08-14 10:58:54 +02:00
  • dc5ad78b3e Make bdd_dict a shared pointer. Alexandre Duret-Lutz 2014-08-13 16:55:25 +02:00
  • 10e5c62386 Simplify copying of atomic propositions in new tgba_digraph. Alexandre Duret-Lutz 2014-08-13 14:21:16 +02:00
  • 917f70073f tgba_digraph: add a set_single_acceptance_set() method. Alexandre Duret-Lutz 2014-08-13 11:37:39 +02:00
  • 5739240c0f get rid of tgba_tba_proxy Alexandre Duret-Lutz 2014-08-12 13:32:32 +02:00
  • e9893586cc remove the sba interface Alexandre Duret-Lutz 2014-08-12 11:31:42 +02:00
  • cc38443ed0 get rid of tgba_sba_proxy Alexandre Duret-Lutz 2014-08-12 11:09:51 +02:00
  • a63612a515 Remove deprecated algorithms. Alexandre Duret-Lutz 2014-08-12 10:29:36 +02:00
  • e6ea90e326 remove tgba_explicit variants and the old scc_filter Alexandre Duret-Lutz 2014-08-12 09:16:07 +02:00
  • 6c9d5e4bb3 replace sba_explicit_* by tgba_digraph, and use tgba_digraph is postproc Alexandre Duret-Lutz 2014-08-11 19:08:14 +02:00
  • 637aeff2d3 compsusp: Use new implem of scc_filter to remove suspended variables Alexandre Duret-Lutz 2014-08-11 10:36:44 +02:00
  • d4e3a9521b [buddy] Fix a harmless uninitialized read. Alexandre Duret-Lutz 2014-08-11 00:18:54 +02:00
  • 1244b61710 [buddy] Fix a harmless uninitialized read. Alexandre Duret-Lutz 2014-08-11 00:18:54 +02:00
  • 55715dfb87 * src/tgbaalgos/ltl2tgba_fm.cc: Get rid of tgba_explicit_formula. Alexandre Duret-Lutz 2014-08-10 20:02:37 +02:00
  • 6dc29547fe * src/graph/ngraph.hh (names): Fix constness. Alexandre Duret-Lutz 2014-08-10 20:01:49 +02:00
  • cccb6edfdd * src/tgbaalgos/ltl2tgba_fm.hh: Fix comment. Alexandre Duret-Lutz 2014-08-10 18:34:40 +02:00
  • 70a6b70f89 * src/bin/dstar2tgba.cc: Do not try to enable utf-8 on automata. Alexandre Duret-Lutz 2014-08-10 18:32:06 +02:00
  • bbeae65031 * src/priv/countstates.hh: Disallow calls using tgba_digraph. Alexandre Duret-Lutz 2014-08-10 18:28:37 +02:00
  • cbca22d1f1 * src/taalgos/minimize.cc: Replace tgba_explicit_number by tgba_digraph. Alexandre Duret-Lutz 2014-08-10 18:17:02 +02:00
  • 57e7bbb3b1 Remove is_syntactic_weak_scc and is_syntactic_terminal_scc Alexandre Duret-Lutz 2014-08-10 18:03:59 +02:00
  • ead04cb1ac dtgbacomp: Rewrite using tgba_digraph instead of tgba_explicit_number Alexandre Duret-Lutz 2014-08-10 17:59:34 +02:00
  • 0909c2fe3d * src/tgbaalgos/minimize.cc: Get rid of tgba_explicit_number. Alexandre Duret-Lutz 2014-08-10 15:29:03 +02:00
  • 74e20a6ec4 complete: get rid of tgba_explicit_number Alexandre Duret-Lutz 2014-08-10 15:18:17 +02:00
  • df05162780 tgba_digraph: Simplify declaration of forwarded methods. Alexandre Duret-Lutz 2014-08-10 15:17:22 +02:00
  • 6ecd71c485 * src/graph/graph.hh (transitions): New method. Alexandre Duret-Lutz 2014-08-10 15:17:14 +02:00
  • 7b23691629 ltl_to_tgba_fm: Build a tgba_digraph instead of a tgba_explicit_formula Alexandre Duret-Lutz 2014-08-06 18:31:18 +02:00
  • 38887f4960 * src/tgbaalgos/compsusp.cc: Use tgba_digraph. Alexandre Duret-Lutz 2014-08-05 17:15:49 +02:00
  • 5dd731eab6 * src/ltlvisit/contain.cc: Do not mention tgba_explicit_number. Alexandre Duret-Lutz 2014-08-05 17:03:21 +02:00
  • 7299fcda2c * src/neverparse/public.hh: Typo in comment. Alexandre Duret-Lutz 2014-08-05 16:37:21 +02:00
  • f9d85d7d2e dra2ba: Use tgba_digraph. Alexandre Duret-Lutz 2014-08-05 16:33:37 +02:00
  • 9923cbaae0 nra2nba: Produce a tgba_digraph. Alexandre Duret-Lutz 2014-08-05 16:08:44 +02:00
  • 7c0ce376c5 nsa2tgba: Construct a tgba_digraph. Alexandre Duret-Lutz 2014-08-05 11:57:33 +02:00
  • ed94a35bea dstarparse: Build a tgba_digraph instead of tgba_explicit_number. Alexandre Duret-Lutz 2014-08-05 10:49:03 +02:00
  • 886d4e75a2 neverparse: build a tgba_digraph Alexandre Duret-Lutz 2014-07-31 18:55:50 +02:00
  • ff83e92db4 tgba_digraph: Fix handling of initial state. Alexandre Duret-Lutz 2014-08-05 19:43:30 +02:00
  • fd5fbda4dd Use emplace() for associative containers. Alexandre Duret-Lutz 2014-07-31 16:59:47 +02:00
  • 1eaaf8832a * NEWS: Mention recent removals. Alexandre Duret-Lutz 2014-07-31 15:47:01 +02:00
  • 401179eae7 Delete the cutscc algorithms. Alexandre Duret-Lutz 2014-07-31 11:41:10 +02:00
  • 1a93166d15 tgbadigraph: delegate useful graph methods Alexandre Duret-Lutz 2014-07-10 10:23:48 +02:00
  • 18f6fe772b bdddict: remove now/next variables. Alexandre Duret-Lutz 2014-07-09 23:32:23 +02:00