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

Commit graph

  • ad93f87591 Fixup minimize_monitor(). Alexandre Duret-Lutz 2011-01-28 12:11:20 +01:00
  • dd0f01fe03 more files to ignore Alexandre Duret-Lutz 2011-01-27 21:47:47 +01:00
  • c8140de9d6 Report formulas that are both safety and guarantee. Alexandre Duret-Lutz 2011-01-27 21:41:04 +01:00
  • db124d02c0 Rename is_safety_automaton() as is_guarantee_automaton() and implement is_safety_mwdba(). Alexandre Duret-Lutz 2011-01-27 18:21:27 +01:00
  • 14b701b54d * NEWS: Minor rewritings. Alexandre Duret-Lutz 2011-01-27 15:08:57 +01:00
  • 0c9c9fc639 Replace delete by destroy in comments dealing with states. Alexandre Duret-Lutz 2011-01-27 10:47:57 +01:00
  • 95cc50da51 Update gspn interface for recent tools. Alexandre Duret-Lutz 2011-01-26 11:01:00 +01:00
  • 574a228583 Introduce a destroy() method on states, and use it instead of delete. Alexandre Duret-Lutz 2011-01-25 18:56:42 +01:00
  • 60930d7a12 * wrap/python/ajax/ltl2tgba.html: Display the Spot version in the tooltip over the Spot logo. Alexandre Duret-Lutz 2011-01-26 23:01:32 +01:00
  • 656eeeaf3b * wrap/python/ajax/Makefile.am (EXTRA_DIST): Add icons/mail.png. Alexandre Duret-Lutz 2011-01-26 22:10:57 +01:00
  • 6df06aceeb * NEWS: Mention the new on-line ltl2tgba version. Alexandre Duret-Lutz 2011-01-26 22:09:37 +01:00
  • f3c6f01e8d Updates to the ltl2tgba ajax version. Alexandre Duret-Lutz 2011-01-26 22:03:14 +01:00
  • c7f3bd5111 * wrap/python/ajax/ltl2tgba.html: Disable the browser spellcheck on the input box. Alexandre Duret-Lutz 2011-01-19 08:44:33 +01:00
  • 34f49a8692 Preliminary implementation of an ajax-based ltl2tgba translator. Alexandre Duret-Lutz 2011-01-17 23:14:22 +01:00
  • dc2a89f853 Do not output empty parse error blocks in the CGI script. Alexandre Duret-Lutz 2011-01-17 21:52:59 +01:00
  • fe535a1594 Fix "unused function" warnings reported by clang++. Alexandre Duret-Lutz 2011-01-12 18:44:29 +01:00
  • 45d7c88062 Fix segfault with g++-3.3. Alexandre Duret-Lutz 2011-01-12 16:59:12 +01:00
  • b39e68c51e Fix a compilation failure with g++-3.3. Alexandre Duret-Lutz 2011-01-12 14:01:07 +01:00
  • 74f14567d1 Fix usage of minimize_obligation in the CGI script. Alexandre Duret-Lutz 2011-01-07 23:21:04 +01:00
  • a8fb2c4b8e more files to ignore Alexandre Duret-Lutz 2011-01-06 19:32:29 +01:00
  • da571a151a * NEWS: Convert to utf-8 and fix a few typos. Alexandre Duret-Lutz 2011-01-06 19:31:18 +01:00
  • 256eb5bb15 '([]a && XXXX!a)' was not properly minimized because its translation contain useless SCCs that where not ignored for minimization. Alexandre Duret-Lutz 2011-01-06 19:23:34 +01:00
  • df2a950ed4 The neverclaim output by spin -f '([]a && XXXX!a)' was not understood by Spot. Alexandre Duret-Lutz 2011-01-06 19:03:41 +01:00
  • 6cb5df0bd7 Speed up computation of non_final states for minimize_wdba. Alexandre Duret-Lutz 2011-01-06 12:16:55 +01:00
  • 474e69565b Introduce a class to complement a WDBA on-the-fly. Alexandre Duret-Lutz 2011-01-06 11:40:57 +01:00
  • b9dd72b29b * src/tgbatest/Makefile.am: Remove the unused minimize program. * src/tgbatest/minimize.cc: Delete. Alexandre Duret-Lutz 2011-01-05 23:12:33 +01:00
  • 8c972ad3ce Cleanup the minimize.hh interface. Alexandre Duret-Lutz 2011-01-05 22:35:38 +01:00
  • 92126a6cf9 Cleanup the DFA minimization algorithm. Alexandre Duret-Lutz 2011-01-05 19:38:48 +01:00
  • ef317685c8 Speed up the obligation test. Alexandre Duret-Lutz 2011-01-05 14:15:15 +01:00
  • f06fc8ac77 * src/tgbaalgos/minimize.cc (minimize): Use the Loeding algorithm to label transient states. Alexandre Duret-Lutz 2011-01-05 12:34:37 +01:00
  • 358d4bfdf2 Rewrite the check of WDBA state acceptance in minimize(). Alexandre Duret-Lutz 2011-01-04 19:13:44 +01:00
  • 37a8d1dc92 Add trivial() and one_state_of() functions to scc_map. Alexandre Duret-Lutz 2011-01-04 19:02:06 +01:00
  • 5bc6d1d4ff * src/tgba/tgbaunion.hh: Remove one useless include. Alexandre Duret-Lutz 2011-01-04 19:00:23 +01:00
  • 3a8e1cdce0 * README: Mention bench/wdba/. Alexandre Duret-Lutz 2011-01-04 18:59:46 +01:00
  • 92756e49c8 Define tgba_product_init, a new kind of product with different initial states. Alexandre Duret-Lutz 2011-01-04 18:59:24 +01:00
  • f4e583d078 * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many failure because the minimization() algorithm is currently incorrect when applied to non-weak automata. Alexandre Duret-Lutz 2011-01-04 14:33:04 +01:00
  • 607676d701 * src/tgbaalgos/scc.hh: Typo in documentation. Alexandre Duret-Lutz 2011-01-04 14:31:38 +01:00
  • 907d173d6a Move the logic for detecting when the minimize() algorithm is correct from ltl2tgba to the library. Alexandre Duret-Lutz 2011-01-04 14:29:33 +01:00
  • 241ba112d6 Make minimization of obligation properties and deterministic monitor available in the CGI script. Alexandre Duret-Lutz 2010-12-26 19:30:36 +01:00
  • edc71b807e Add a WDBA benchmark. Alexandre Duret-Lutz 2010-12-14 11:13:49 +01:00
  • aadef1fd87 * NEWS: Update the news about minimization. Alexandre Duret-Lutz 2010-12-13 19:28:48 +01:00
  • d72a2f0a31 Speed up wdba.test, it was too slow for our buildfarm. Alexandre Duret-Lutz 2010-11-26 14:21:53 +01:00
  • 0392058e6e * src/tgbatest/ltl2tgba.cc (syntax): Regroup -M, -s, and -S option under the same heading "automaton conversion". Alexandre Duret-Lutz 2010-11-26 14:19:13 +01:00
  • cc8dd49d06 Preliminary support for monitors. Alexandre Duret-Lutz 2010-11-25 19:52:16 +01:00
  • a962bb6ddc "ltl2tgba -Rm -X foo.tgba" would fail. Alexandre Duret-Lutz 2010-11-25 13:21:34 +01:00
  • 7d8a5310e4 Fix bugs in minimize(). Alexandre Duret-Lutz 2010-11-25 12:58:33 +01:00
  • 72139fd760 Fix bugs in minimize(), caught by spotlbtt.test. Alexandre Duret-Lutz 2010-04-13 14:29:58 +02:00
  • 54e10c2501 "ltl2tgba -Rm" will apply WDBA-minimization only if correct. Alexandre Duret-Lutz 2010-04-13 10:38:08 +02:00
  • f9e84ac245 Better resource handling in minimization. Alexandre Duret-Lutz 2010-04-12 18:21:50 +02:00
  • 0af8d03261 Implement is_safety_automaton(). Alexandre Duret-Lutz 2010-03-20 12:57:36 +01:00
  • 99c1b607de * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. Felix Abecassis 2010-03-26 17:31:58 +01:00
  • 52090e4875 Small fixes. Felix Abecassis 2010-03-20 15:23:19 +01:00
  • fac30eb08e Test program for the minimization algorithm. Felix Abecassis 2010-03-20 14:51:02 +01:00
  • 03e6dc4769 * src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh: New files. Algorithm to minimize an automaton using first the powerset construction to determinize the input automaton, the automaton is then minimized using the standard algorithm, using BDDs to check if states are equivalent. Felix Abecassis 2010-03-20 14:36:29 +01:00
  • e2e138f6e6 Modify the powerset algorithm to keep track of accepting states from the initial automaton. Felix Abecassis 2010-03-20 14:01:10 +01:00
  • bd742ef6a4 Fix computation of support_conditions for bdd-based TGBA. This fixes a bug in the powerset of such TGBA on the minimize branch. Alexandre Duret-Lutz 2011-01-05 08:01:46 +01:00
  • 0f08fbc206 * wrap/python/cgi-bin/ltl2tgba.in: Remove all "new" markers. Alexandre Duret-Lutz 2010-12-26 18:42:14 +01:00
  • f1d3e999ae Define SWIG_TYPE_TABLE as suggested by the SWIG documentation. Alexandre Duret-Lutz 2010-12-23 22:29:35 +01:00
  • 8419cb6f8d Use swig2.0 if available. Alexandre Duret-Lutz 2010-12-23 22:27:07 +01:00
  • 3d61b3a3c0 Get rid of ltihooks.py. Alexandre Duret-Lutz 2010-12-23 22:25:23 +01:00
  • 2ac37ad58f * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2010-12-12 11:17:20 +01:00
  • 01843379a3 Merge transitions in tgba_tba_proxy. Alexandre Duret-Lutz 2010-12-11 20:48:53 +01:00
  • 87ee1cfe7d Augment the size of the ltlclasses benchmark. Alexandre Duret-Lutz 2010-12-10 10:12:20 +01:00
  • 1dd524ebce Introduce -ks to print only the size of the automaton (without SCC information). Alexandre Duret-Lutz 2010-12-10 10:02:53 +01:00
  • 3e7debe53e Use a cache to speed up tgba_tba_proxy. Alexandre Duret-Lutz 2010-12-09 19:37:01 +01:00
  • e713cb3b67 more files to ignore Alexandre Duret-Lutz 2010-12-07 18:34:32 +01:00
  • d9fb4d1d09 * src/ltltest/Makefile.am (genltl_SOURCES): Add missing variable. Alexandre Duret-Lutz 2010-12-07 18:32:43 +01:00
  • 48e4c13da9 * README: Mention bench/ltlclases/. Alexandre Duret-Lutz 2010-12-07 15:52:22 +01:00
  • d42deb7fa4 Preliminary benchmark using genltl, introduced earlier. Alexandre Duret-Lutz 2010-12-04 18:07:22 +01:00
  • c4a7efb9e0 * src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s. Alexandre Duret-Lutz 2010-12-04 17:10:47 +01:00
  • 437af50afe Preliminary implementation of a tool to generate some interesting families of LTL formulae. Alexandre Duret-Lutz 2010-12-03 18:53:00 +01:00
  • ac9d0a502a Add full_parent support to to_spin_string(). Alexandre Duret-Lutz 2010-12-03 18:29:59 +01:00
  • c735249873 Halve the number of application of eventual_universal_visitor in reduce_visitor::visit(binop). Alexandre Duret-Lutz 2010-12-01 08:06:49 +01:00
  • dabb7ecc97 Move the eventual-universal functions where the belong. Alexandre Duret-Lutz 2010-12-01 07:32:06 +01:00
  • f5503090b1 * src/ltlvisit/randomltl.cc (random_ltl::update_sums): Typo in string. Alexandre Duret-Lutz 2010-11-30 23:14:32 +01:00
  • 2a33bd17ec Remove a quadratic behavior in eventual_universal_visitor. Alexandre Duret-Lutz 2010-11-30 23:13:36 +01:00
  • 487c4ac48c * src/tgbatest/ltl2tgba.cc (main): Delete the accepting run even if it hasn't been printed. Alexandre Duret-Lutz 2010-12-01 08:38:47 +01:00
  • 75a24111da Rationalize options for counter-example output. Alexandre Duret-Lutz 2010-11-30 13:40:11 +01:00
  • ae03bc6704 Fix a GCC 4.6 warning. Alexandre Duret-Lutz 2010-11-30 12:19:45 +01:00
  • 3b3711286b * src/tgbatest/ltl2tgba.cc (syntax): Typo. Alexandre Duret-Lutz 2010-11-27 21:45:47 +01:00
  • 0785d729d5 [iface/nips/nips_vm] Fix compilation with Clang. Alexandre Duret-Lutz 2010-11-27 14:31:04 +01:00
  • 8156766fe3 Another Clang report. Alexandre Duret-Lutz 2010-11-27 14:29:28 +01:00
  • 019c85dff6 Fix more errors reported by Clang. Alexandre Duret-Lutz 2010-11-27 10:21:44 +01:00
  • 0d9d0b08ec Finalize Kripke interface. Alexandre Duret-Lutz 2010-11-26 17:50:12 +01:00
  • 67f46b85b3 Never claim output used to print the degeneralized automaton before some optional operations (like more optimizations, or a product). Alexandre Duret-Lutz 2010-11-25 20:29:16 +01:00
  • 7627b9673b * src/tgbatest/ltl2tgba.test: Test both -l and -f. This should have been done on 2010-01-30 when the default translation was changed from -l to -f. Alexandre Duret-Lutz 2010-11-25 19:59:46 +01:00
  • 0dca4be69d * src/tgbaalgos/scc.hh: Typos in the documentation. Alexandre Duret-Lutz 2010-11-25 19:57:10 +01:00
  • 0a2dbab413 * src/tgbaalgos/sccfilter.hh: Fix some typos in the documentation. Alexandre Duret-Lutz 2010-11-24 21:59:16 +01:00
  • 57d4df47dd Suggest using bddtrue and bddfalse instead of bdd_true() and bdd_false(). Alexandre Duret-Lutz 2010-11-24 21:03:14 +01:00
  • 2ba963200a Fix some struct/class missmatches reported by clang. Alexandre Duret-Lutz 2010-11-20 18:01:15 +01:00
  • 2b46cb4bab Add interface for and test the bdd_setxor() function added to Buddy. Alexandre Duret-Lutz 2010-11-07 11:15:56 +01:00
  • 4034b7f87f [buddy] * src/bddop.c (bdd_setxor): New function. * src/bdd.h (bdd_setxor): New function. Alexandre Duret-Lutz 2010-11-07 11:15:45 +01:00
  • 38913302dd * src/Makefile.am (libspot_la_LIBADD): Rename libneverclaimparse.la as libneverparse.la. * src/neverparse/Makefile.am: Install files in $(pkgincludedir)/neverparse, not $(pkgincludedir)/neverclaimparse. Alexandre Duret-Lutz 2010-11-06 20:44:37 +01:00
  • 1e0f99e824 Cosmetics to please sanity checks. Alexandre Duret-Lutz 2010-11-06 17:56:27 +01:00
  • 87f69eaf18 * src/tgbatest/ltl2tgba.cc: Clock the time spent reading -P file. Alexandre Duret-Lutz 2010-11-06 16:40:44 +01:00
  • b1dbfed17f * src/tgbatest/neverclaimread.test: Check that Spot can read the neverclaims it outputs. Alexandre Duret-Lutz 2010-11-06 15:56:50 +01:00
  • a6677c2984 Do not output a counterexample by default in ltl2tgba, introduce options -C and -CR for that. Alexandre Duret-Lutz 2010-11-06 15:38:00 +01:00
  • fe1f59cd30 Make sure the neverclaim parser works on the output of spin and ltl2ba. Alexandre Duret-Lutz 2010-11-06 13:39:26 +01:00
  • ac08c5abce Cleanup neverclaim support. Alexandre Duret-Lutz 2010-11-06 10:23:35 +01:00
  • ab6ec5cb63 Add never claim parser. Felix Abecassis 2010-05-25 16:19:20 +02:00