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

Commit graph

  • c48b9bcfb5 Cosmetic changes in doc for bunop and multop. Alexandre Duret-Lutz 2011-02-16 10:24:56 +01:00
  • c8801935bf Fix handling of PSL operators in reductions rules. Alexandre Duret-Lutz 2011-02-15 14:34:57 +01:00
  • b8b4aa72c5 Plug a memory leak in randltl. Alexandre Duret-Lutz 2011-02-15 14:06:54 +01:00
  • 87acb15174 Translate 50 random PSL formulae until we get a better test. Alexandre Duret-Lutz 2011-02-14 11:29:07 +01:00
  • a29c87b2ed Fix infinite recursion when translating E* and E accepts [*0]. Alexandre Duret-Lutz 2011-02-14 10:09:17 +01:00
  • cce6dd34f8 Add random generators of Boolean, SERE, and PSL formula. Alexandre Duret-Lutz 2011-02-13 22:38:29 +01:00
  • cc889a7f66 Make it possible to format SERE. Alexandre Duret-Lutz 2011-02-13 22:35:11 +01:00
  • fe7d7473ed * src/ltlvisit/tostring.cc: Fix parentheses for [*] operator. Alexandre Duret-Lutz 2011-02-13 22:34:24 +01:00
  • eab91aab68 Relax usage of ->, <->, and xor in SERE. Alexandre Duret-Lutz 2011-02-13 22:29:35 +01:00
  • 8cafa200a5 Equal and Goto should only apply to Boolean expressions. Alexandre Duret-Lutz 2011-02-13 22:21:31 +01:00
  • 7c7704f92e Prepare the introduction of random_sere() and random_psl(). Alexandre Duret-Lutz 2011-02-13 15:57:54 +01:00
  • 4ef7805e73 Speedup syntactic_implication() by using a cache. Alexandre Duret-Lutz 2010-12-09 18:53:31 +01:00
  • 20c088a45a Speedup some rewriting by detecting cases where they do nothing. Alexandre Duret-Lutz 2010-12-09 18:49:33 +01:00
  • 6380968f32 Remove the has_mark() function in favor of the is_marked() method. Alexandre Duret-Lutz 2010-12-09 14:10:05 +01:00
  • 957ba664b7 Get rid of all dynamic_cast<>s while working on LTL formulae. Alexandre Duret-Lutz 2010-12-09 13:19:44 +01:00
  • 48cde88b9b Replace the constant_term visitor by a flag in the formulae. Alexandre Duret-Lutz 2010-12-09 10:15:19 +01:00
  • 546260e7a0 Maintain basic LTL properties using a bitfield inside formula objects. Alexandre Duret-Lutz 2010-12-08 18:22:35 +01:00
  • 1671aa5da1 Simplify fUf, fRf, fWf, and fRF as f. Alexandre Duret-Lutz 2010-10-25 17:46:26 +02:00
  • 5bb171c8f6 Do not simplify F([*0]) and G([*0]). Make sure it does not happen. Alexandre Duret-Lutz 2010-10-25 17:00:53 +02:00
  • 473cf77144 Fix trivial identity (0 => Exp) == 1, and add rewritings for =>. Alexandre Duret-Lutz 2010-10-16 17:24:50 +02:00
  • f2732dd8cc Read p=0Wq=1 and p=0Mq=1 correctly. Alexandre Duret-Lutz 2010-10-15 17:46:47 +02:00
  • 754ff36b01 Accept more syntaxes as range specifications for [*], [=], and [->]. Alexandre Duret-Lutz 2010-10-15 16:38:30 +02:00
  • 4fd4f83ed6 Fix rewriting of Negated constants and atomic propositions Alexandre Duret-Lutz 2010-10-15 12:32:51 +02:00
  • c6a751b9d4 Speed up computation of constant term on [->] and [=] operators. Alexandre Duret-Lutz 2010-10-15 12:30:11 +02:00
  • bfa827c774 * src/ltlast/multop.hh: Fix documentation of some trivial identity. Alexandre Duret-Lutz 2010-10-15 12:28:15 +02:00
  • da74b4f180 Introduce [->min..max] operator. Alexandre Duret-Lutz 2010-10-15 11:41:18 +02:00
  • 2c31e541b5 Rewrite Exp[=0..] as [*]. Alexandre Duret-Lutz 2010-10-14 19:14:42 +02:00
  • 8d4a413a37 Introduce [=min..max] operator. Alexandre Duret-Lutz 2010-10-14 18:51:34 +02:00
  • d7781bc4d6 Simplify ![*0] as [+]. Alexandre Duret-Lutz 2010-10-14 18:38:28 +02:00
  • 437128b55b Add functions to compute the kind of a formula (LTL, PSL, Boolean...) Alexandre Duret-Lutz 2010-05-19 18:56:57 +02:00
  • 567b460738 Add support for [+]. Alexandre Duret-Lutz 2010-05-19 17:01:11 +02:00
  • 126b724a98 Add support the bounded star operator [*i..j]. Alexandre Duret-Lutz 2010-05-12 19:09:20 +02:00
  • 47b2bea865 Print '{!a}*' rather than '!a*'. Alexandre Duret-Lutz 2010-03-13 00:32:06 +01:00
  • aef6c1a06b Fix deterministic translation of []->. Alexandre Duret-Lutz 2010-03-10 17:38:31 +01:00
  • 93c042d0fa Recognize and use "*" (or "[*]") as an abbreviation for 1*. Alexandre Duret-Lutz 2010-03-10 16:01:27 +01:00
  • 4bde130d38 Support non-overlapping concatenations operators []=> and <>=>. Alexandre Duret-Lutz 2010-03-10 15:47:04 +01:00
  • 4aa82ec762 Allow boolean atoms to be negated in rational expressions. Alexandre Duret-Lutz 2010-03-10 14:38:17 +01:00
  • bbb645e1fc Add support for PSL's non-length-matching And. Alexandre Duret-Lutz 2010-03-10 11:05:41 +01:00
  • 1ecc6984d3 Accept "{E}|->ltl" and "{E}(ltl)" as synonym for "{E}[]->ltl". Alexandre Duret-Lutz 2010-03-09 16:26:27 +01:00
  • 8b8633de8c Use [*0] instead of #e, and support [*] in addition to *. Alexandre Duret-Lutz 2010-03-09 16:08:38 +01:00
  • 4e7233d9fa Support braces in addition to parentheses in rational expressions. Alexandre Duret-Lutz 2010-03-09 15:23:42 +01:00
  • 2f8c4ac8b7 Add support for {SERE} and !{SERE} closure operators. Alexandre Duret-Lutz 2010-03-09 09:48:08 +01:00
  • f618e6bc1a Build deterministic automata for []-> operators. Alexandre Duret-Lutz 2010-03-03 16:30:52 +01:00
  • 916c154291 Adjust Python tests to the new simplification rules. Alexandre Duret-Lutz 2010-03-03 12:24:02 +01:00
  • dbdd37010c Build deterministic automata for <>-> operators. Alexandre Duret-Lutz 2010-03-02 18:19:36 +01:00
  • c2b3dac7aa Parse the fusion operator (":") and translate it in ltl2tgba_fm(). Alexandre Duret-Lutz 2010-03-02 16:25:08 +01:00
  • ad519b8568 Do not assume that concatenation cannot accept the empty word. Alexandre Duret-Lutz 2010-03-02 12:44:46 +01:00
  • bd9136a98e Update the FM translation to handle <>->, []->, *, ;, #e. Alexandre Duret-Lutz 2010-02-24 16:20:02 +01:00
  • 21e89f400a Visitors to transform <>-> into <>+> or to detect the latter. Alexandre Duret-Lutz 2010-02-24 16:16:14 +01:00
  • 171ca678b8 Introduce EConcatMarked "<>+>" as operator. Alexandre Duret-Lutz 2010-02-24 16:15:17 +01:00
  • 66317db45c Simplify #e in conjunctions. Alexandre Duret-Lutz 2010-02-08 18:01:10 +01:00
  • 76528ee2fb Simplify {#e}[]->Exp and {#e}<>->Exp. Alexandre Duret-Lutz 2010-02-08 18:00:24 +01:00
  • fc7c2943de more tests for rational operator simplifications. Alexandre Duret-Lutz 2010-02-08 12:48:15 +01:00
  • 9aebb80e08 Enable parsing stand-alone rational expressions with the LTL parser. Alexandre Duret-Lutz 2010-02-08 11:36:55 +01:00
  • c6dd811b08 Add []-> and <>->. Alexandre Duret-Lutz 2010-01-29 14:29:17 +01:00
  • 97b7211bb7 Add a constant_term() visitor to decide whether #e is accepted. Alexandre Duret-Lutz 2010-01-11 16:01:38 +01:00
  • 2d1aa0a5a0 more files to ignore Alexandre Duret-Lutz 2010-01-11 14:52:05 +01:00
  • 546559b8c3 Introduce rational operators and trivial simplification rules. Alexandre Duret-Lutz 2010-01-11 14:29:46 +01:00
  • 4fcc4f829c Apply ACI rules to multop formulae. Alexandre Duret-Lutz 2009-12-24 17:46:46 +01:00
  • 4e1a68e676 Summarize recent changes. Alexandre Duret-Lutz 2012-04-28 09:16:55 +02:00
  • 03aca91648 Don't compare memory consumption between 2 runs of dve2check Alexandre Duret-Lutz 2012-04-27 20:31:40 +02:00
  • 8aa653e010 [lbtt] Fix make pdf. Alexandre Duret-Lutz 2012-04-27 17:58:35 +02:00
  • 324802c04f Change the simulation option from -RSD to -RDS and document it. Alexandre Duret-Lutz 2012-04-27 17:26:59 +02:00
  • 7e5875845a Remove the old broken game-theory-based simulation reductions. Alexandre Duret-Lutz 2012-04-27 17:11:53 +02:00
  • 7ba4ab7931 slights documentation changes around direct simulation Alexandre Duret-Lutz 2012-04-27 15:51:20 +02:00
  • cdd576458c Document --without-included-lbtt. Alexandre Duret-Lutz 2012-04-27 14:02:54 +02:00
  • 9ea0e00ae7 Define WEXITSTATUS if not available (e.g. on MinGW) Alexandre Duret-Lutz 2012-04-27 12:57:50 +02:00
  • 2c8e5297e7 Use clock() when times() is not available. Alexandre Duret-Lutz 2012-04-27 12:51:32 +02:00
  • 8620138069 memusage: drop two useless includes. Alexandre Duret-Lutz 2012-04-27 12:26:14 +02:00
  • 907ba16bfa [lbtt] Remove a useless configure check. Alexandre Duret-Lutz 2012-04-27 11:44:33 +02:00
  • dfcaed034e Add the simulation in the Spot web interface. Thomas Badie 2012-04-15 13:12:29 +02:00
  • 085ea52bf5 Fix two VPath-related bugs in bench. Thomas Badie 2012-04-14 21:56:47 +02:00
  • 876f8c90a2 Create the direct simulation. Thomas Badie 2012-03-05 16:55:08 +01:00
  • e75ad57446 Add a class to convert a bdd into its complement. Thomas Badie 2012-03-08 21:55:36 +01:00
  • d3be530410 tgbatba: fix destroying of cache variables. Alexandre Duret-Lutz 2012-04-13 12:21:57 +02:00
  • 8269ae9cee tgbaexplicit: execute the test Alexandre Duret-Lutz 2012-04-12 17:54:20 +02:00
  • 37a6b601c1 Declare the sba class in its own header. Alexandre Duret-Lutz 2012-04-12 17:22:08 +02:00
  • 937248e561 Correct a bug in tgba_explicit_succ_iterator class Pierre PARUTTO 2012-04-06 15:55:03 +02:00
  • 9cfc408262 Modify is_accepting sba's method to run in constant time. Pierre PARUTTO 2012-04-05 17:47:38 +02:00
  • eec3a12f80 Implement sba_explicit class, add tests Pierre PARUTTO 2012-04-05 16:20:28 +02:00
  • 603c5d603b tgba_explicit: make the new class work with Swig. Alexandre Duret-Lutz 2012-03-31 17:25:53 +02:00
  • a15aac2845 Revamp tgbaexplicit.hh Pierre PARUTTO 2012-03-06 00:13:15 +01:00
  • 9e2b932fe6 maint: add .checklog Alexandre Duret-Lutz 2012-04-11 12:27:09 +02:00
  • e9ea9fd3fe maint: set umask 022 in lrde-upload.sh Alexandre Duret-Lutz 2012-03-19 07:59:15 +01:00
  • 862c248a41 ltl2tgba.html: Scroll to result. (Suggested by Thomas Badie.) Alexandre Duret-Lutz 2012-03-18 22:35:34 +01:00
  • 3fb29ce1be Typo: rename automata_ as aut_. Alexandre Duret-Lutz 2012-03-17 12:02:19 +01:00
  • 4749d77e4f Generate ChangeLog from git log during "make dist". Alexandre Duret-Lutz 2012-03-12 17:41:12 +01:00
  • 915115d9e2 Rename ChangeLog as ChangeLog.1 and leave an empty ChangeLog. Alexandre Duret-Lutz 2012-03-12 16:41:32 +01:00
  • a0a22c4f7d * configure.ac, NEWS: Bump version to 0.8.3a. Alexandre Duret-Lutz 2012-03-09 19:09:42 +01:00
  • 91b59bfe66 Release Spot 0.8.3. Alexandre Duret-Lutz 2012-03-09 18:41:11 +01:00
  • a01034e5f9 Fix a segfault in the CGI script, reported by Denis. Alexandre Duret-Lutz 2012-03-09 08:38:55 +01:00
  • 187997fe5d ltl2tgba.html: Fix initialization of unset options on reload. Alexandre Duret-Lutz 2012-03-08 22:02:16 +01:00
  • 802319ddbb * wrap/python/ajax/spot.in: Fix emulation of execfile. Alexandre Duret-Lutz 2012-03-08 21:30:09 +01:00
  • 9114305995 ltl2tgba.html: save state in URL to preserve history Alexandre Duret-Lutz 2012-03-04 17:34:13 +01:00
  • 88044453fc python: fix return value of emptiness_check_instantiator Alexandre Duret-Lutz 2012-03-04 17:23:46 +01:00
  • 503a57cad2 * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2012-02-25 14:12:28 +01:00
  • 61127a3fd5 Make all python code compatible with Python 2.x and Python 3.x. Alexandre Duret-Lutz 2012-02-25 13:36:29 +01:00
  • 5e77b2498a Fix computation of PYTHONINC for Python 3. Alexandre Duret-Lutz 2012-02-25 13:22:43 +01:00
  • 84c2eed13f * HACKING: Minor updates and corrections. Alexandre Duret-Lutz 2012-02-04 11:10:25 +01:00
  • eeda782f7f Adjust lrde-upload.sh to handle branchnames with a slash. Alexandre Duret-Lutz 2012-02-15 17:06:07 +01:00