Commit graph

alarsyo/spot

Fork 0

db1e842a67 ltsmin: add accessors for variable names and types Alexandre Duret-Lutz 2016-01-25 18:00:08 +01:00
907b72fbfb ltsmin: implement a two-step loading Alexandre Duret-Lutz 2016-01-25 17:04:09 +01:00
84031d2ae1 more files to ignore Alexandre Duret-Lutz 2016-01-24 19:52:11 +01:00
0c2997990d * tests/run.in: Honor PREFIXCMD even without argument. Alexandre Duret-Lutz 2016-01-24 19:47:31 +01:00
5a9b0aa1c1 python: add bindings for ltsmin Alexandre Duret-Lutz 2016-01-24 19:45:59 +01:00
215fcb799a Make spot.py a python package instead of a module Alexandre Duret-Lutz 2016-01-24 16:45:10 +01:00
727d4cc678 * doc/org/concepts.org: Fix a few typos. Alexandre Duret-Lutz 2016-01-23 22:11:18 +01:00
c4e9083f4e product: raise an exception if the dict are different Alexandre Duret-Lutz 2016-01-23 21:24:53 +01:00
78fd7beaaf org: Add a Concepts page. Alexandre Duret-Lutz 2016-01-21 18:58:46 +01:00
2364ff8148 typos Alexandre Duret-Lutz 2016-01-21 19:08:26 +01:00
73b1a0901e * doc/org/.gitignore: Add sitemap.org. Alexandre Duret-Lutz 2016-01-21 18:57:02 +01:00
7673b4b535 * python/spot.py: Make it possible to call str('dot') on formula. Alexandre Duret-Lutz 2016-01-21 18:55:44 +01:00
ad8b964520 org: generate a sitemap Alexandre Duret-Lutz 2016-01-18 16:57:26 +01:00
5b82978449 * doc/org/setup.org: Disable html postamble. Alexandre Duret-Lutz 2016-01-18 16:57:06 +01:00
dc93e13490 * NEWS, configure.ac: Bump version number. Alexandre Duret-Lutz 2016-01-15 16:29:09 +01:00
f466320b4a Release Spot 1.99.7 Alexandre Duret-Lutz 2016-01-15 11:30:16 +01:00
c22ef61037 * python/ajax/spotcgi.in: Rename acc.is_tt() to acc.is_t(). Alexandre Duret-Lutz 2016-01-15 08:50:48 +01:00
f5d156abf2 * NEWS: Minor cleanup. Alexandre Duret-Lutz 2016-01-15 08:49:08 +01:00
0f39da9ed6 * doc/org/compile.org: Typos. Alexandre Duret-Lutz 2016-01-15 08:39:08 +01:00
66d8f3ce09 work around core dump created by running ipython4 Alexandre Duret-Lutz 2016-01-14 18:37:48 +01:00
51483b9b7f fix complete Alexandre Duret-Lutz 2016-01-14 17:14:01 +01:00
6c62362fe9 parseaut: add support for negated properties Alexandre Duret-Lutz 2016-01-14 11:12:30 +01:00
da391492f3 twa: store property bits as trivals Alexandre Duret-Lutz 2016-01-12 19:37:18 +01:00
1aeb260adf trival: new class for tri-valued logic Alexandre Duret-Lutz 2016-01-08 16:49:18 +01:00
e764cf6f3b Preserve named-states during defrag Etienne Renault 2016-01-12 17:02:50 +01:00
d22ecba9b6 twa: call unregister_all_my_variables() Alexandre Duret-Lutz 2016-01-10 21:02:31 +01:00
d0b38156f3 bin: make HOA the default output Alexandre Duret-Lutz 2016-01-08 12:07:30 +01:00
9d6727da5c bin: add support for SPOT_DEFAULT_FORMAT Alexandre Duret-Lutz 2016-01-06 18:17:06 +01:00
cca2022e90 bin: add -d as a shorthand for --dot Alexandre Duret-Lutz 2016-01-06 16:25:58 +01:00
ea5f52ddbb randaut: rename -d as -e Alexandre Duret-Lutz 2016-01-06 15:54:11 +01:00
8c04e31a35 org: fix definition of PATH Alexandre Duret-Lutz 2016-01-06 15:43:36 +01:00
5232e6a2fb * tests/core/randaut.test: Simplify calls to randaut/autfilt. Alexandre Duret-Lutz 2016-01-06 15:17:59 +01:00
d5c8574650 * bin/README: Typo. Alexandre Duret-Lutz 2016-01-06 15:08:28 +01:00
3b115f0105 * HACKING: Minor updates to a few sections. Alexandre Duret-Lutz 2016-01-06 14:25:37 +01:00
f470edc6c4 Do not run the Python tests when --disable-python. Alexandre Duret-Lutz 2016-01-06 14:24:51 +01:00
bf7df62032 * tools/test-driver-teamcity: Do not add tests/ in the output. Alexandre Duret-Lutz 2016-01-05 15:50:16 +01:00
f08dbe7000 * NEWS: Mention recent directory moves. Alexandre Duret-Lutz 2016-01-05 15:21:42 +01:00
82a718a0f2 * bin/common_setup.cc: Bump copyright year. Alexandre Duret-Lutz 2016-01-05 14:49:19 +01:00
d68db6ad44 use find to clean to test suite temporary directories Alexandre Duret-Lutz 2016-01-05 14:46:06 +01:00
6e854b6d83 move the sanity tests in tests/sanity/ Alexandre Duret-Lutz 2016-01-05 11:39:01 +01:00
6b881a2e38 * tests/python/ipnbdoctest.py: 80 columns. Alexandre Duret-Lutz 2016-01-05 11:33:34 +01:00
ddc424f5a3 move ltsmin tests to tests/ltsmin/ Alexandre Duret-Lutz 2016-01-05 10:26:32 +01:00
7e6bfd0e8f * debian/rules: Fix html conversion of notebooks. Alexandre Duret-Lutz 2016-01-05 09:08:06 +01:00
5cb94a1a3f Merge the core and python tests in the tests/ directory Alexandre Duret-Lutz 2015-12-30 09:50:52 +01:00
18572db39f * spot/sanity/ipynb.test: Fix notebook detection. Alexandre Duret-Lutz 2015-12-28 18:04:08 +01:00
8483f7fc50 * doc/org/tut.org: Minor fixes. Alexandre Duret-Lutz 2015-12-27 20:20:42 +01:00
134dfc73de move spot/bin/ and spot/tests/ up by one level Alexandre Duret-Lutz 2015-12-27 12:16:06 +01:00
ff4837f4f2 python: more robust handling of %timeit in notebooks Alexandre Duret-Lutz 2015-12-26 20:16:53 +01:00
6fb4df4359 Move spot-if/ltsmin/ to spot/ltsmin/ Alexandre Duret-Lutz 2015-12-25 13:45:42 +01:00
34c3c1cedc rename wrap/python/ to python/ Alexandre Duret-Lutz 2015-12-25 11:55:31 +01:00
74ec9c54c4 show how to implement product in Python Alexandre Duret-Lutz 2015-12-24 13:15:10 +01:00
ad37cacbc0 twa: fix duplicate propositions in ap() Alexandre Duret-Lutz 2015-12-24 11:02:27 +01:00
fbf5ac0ea7 acc_cond: get rid of generalized_buchi() Alexandre Duret-Lutz 2015-12-18 18:14:25 +01:00
df1ef302e8 acc_code: parse from the constructor Alexandre Duret-Lutz 2015-12-18 17:47:16 +01:00
d0b29051b2 acc_cond: allow ctor from acc_code only + bind unsat_mark() Alexandre Duret-Lutz 2015-12-18 17:04:03 +01:00
b893b55973 python: better swig options Alexandre Duret-Lutz 2015-12-18 16:03:50 +01:00
15131e74f2 python: better binding for is_parity() Alexandre Duret-Lutz 2015-12-17 11:46:46 +01:00
fd6ad9913f acc: get rid of join() Alexandre Duret-Lutz 2015-12-17 11:45:51 +01:00
94cca9de3d acc_cond: rename is_tt/is_ff as is_t/is_f and add printer Alexandre Duret-Lutz 2015-12-17 08:42:34 +01:00
2927cf38ac python: add some doc & tests for the acceptance bindings Alexandre Duret-Lutz 2015-12-16 18:55:42 +01:00
4993e80706 acc: simplify interface using operators Alexandre Duret-Lutz 2015-12-16 18:49:11 +01:00
c39d35d068 python: port the tut22.org example to Python Alexandre Duret-Lutz 2015-12-15 19:01:33 +01:00
9313222e95 python: allow iterating over the successors of a state Alexandre Duret-Lutz 2015-12-14 11:51:57 +01:00
4b853865b9 python: initial work on wrapping twa_graph::out(n) Alexandre Duret-Lutz 2015-12-11 11:54:27 +01:00
4e040fd9f7 * wrap/python/spot_impl.i: We do not use False/True anymore in Spot. Alexandre Duret-Lutz 2015-12-11 10:14:48 +01:00
3467a719bb python: kill some Swig warnings Alexandre Duret-Lutz 2015-12-10 18:25:35 +01:00
679be1d727 speed up equivalence check for LTL formulas Alexandre Duret-Lutz 2015-12-09 17:57:34 +01:00
2e15ed959d decompose_strength: work with inherently weak SCCs Alexandre Duret-Lutz 2015-12-09 15:50:13 +01:00
9bbcf85b3a acc: move unsat_mark in acc_cond Alexandre Duret-Lutz 2015-12-09 11:21:41 +01:00
2d3e7cecf5 org: update Spot description on index page Alexandre Duret-Lutz 2015-12-08 22:42:50 +01:00
1f2260f971 introduce is_inherently_weak_automaton() Alexandre Duret-Lutz 2015-12-08 18:09:44 +01:00
0edb2ad066 man: more bibliographic references Alexandre Duret-Lutz 2015-12-07 22:23:10 +01:00
b519c7d3dc rename iface/ as spot-if/ Alexandre Duret-Lutz 2015-12-07 21:53:09 +01:00
690b8f51c7 org: some documentation about compiling C++ Alexandre Duret-Lutz 2015-12-05 11:26:26 +01:00
f120dd3206 rename src/ as spot/ and use include <spot/...> Alexandre Duret-Lutz 2015-12-04 19:42:23 +01:00
1fddfe60ec * NEWS: Typo. Alexandre Duret-Lutz 2015-12-04 16:03:35 +01:00
47da953c74 * NEWS, configure.ac: Bump version number. Alexandre Duret-Lutz 2015-12-04 11:13:41 +01:00
af96afac82 Release Spot 1.99.6 Alexandre Duret-Lutz 2015-12-04 08:12:34 +01:00
871965c7fb * wrap/python/ajax/spotcgi.in: Adjust for recent renamings. Alexandre Duret-Lutz 2015-12-04 08:09:10 +01:00
5f45642a24 * NEWS: Cleanup. Alexandre Duret-Lutz 2015-12-03 18:06:07 +01:00
9d8fd50821 * elisp/hoa-mode.el: Update from its master. Alexandre Duret-Lutz 2015-12-03 17:59:01 +01:00
6a64b0804c * debian/control: Fix some dependencdies. Alexandre Duret-Lutz 2015-12-02 19:48:20 +01:00
e357c0c5bc hoa: allow dots in identifiers Alexandre Duret-Lutz 2015-12-02 15:28:05 +01:00
c60c117714 python: do not use -no-undefined Alexandre Duret-Lutz 2015-12-02 14:26:21 +01:00
2052e73af8 word: store the bdd dict for easier printing Alexandre Duret-Lutz 2015-12-01 00:12:45 +01:00
cff79b063b * doc/org/hoa.org: Simplify wording in property table. Alexandre Duret-Lutz 2015-11-29 02:51:32 +01:00
06b176991e fix constness of twa::get_init_state() and twa_succ_iterator::dst() Alexandre Duret-Lutz 2015-11-28 21:47:04 +01:00
afbaa54d92 rewrite explicit Kripke structures and their parser Alexandre Duret-Lutz 2015-11-28 02:15:36 +01:00
073d154540 Only use -Bsymbolic-functions, not -Bsymbolic. Alexandre Duret-Lutz 2015-11-28 02:00:25 +01:00
745fda1a4f print_hoa: add option "k" Alexandre Duret-Lutz 2015-11-27 23:26:17 +01:00
a825fa91e5 dtwa_sat_minimize: better selection of the reference automaton Alexandre Duret-Lutz 2015-11-24 06:18:18 +01:00
a5ca9dbc43 sat: rename dtgbasat as dtwasat Alexandre Duret-Lutz 2015-11-24 05:27:03 +01:00
6237bf4cd6 org: more language tooltips in HTML output Alexandre Duret-Lutz 2015-11-20 14:50:25 +01:00
5aba246ff0 org: syntax-highlight the HOA outputs Alexandre Duret-Lutz 2015-11-20 14:28:51 +01:00
d46da963d5 python: better interface for sat_minimize() Alexandre Duret-Lutz 2015-11-17 18:37:23 +01:00
c1bfc5d59b doc: two typos Alexandre Duret-Lutz 2015-11-17 18:18:50 +01:00
b3ff5655fb dot: add support for option +N Alexandre Duret-Lutz 2015-11-14 14:49:31 +01:00
f86beb3c68 workaround bad interactions between magit and whitespace-mode Alexandre Duret-Lutz 2015-11-14 14:12:38 +01:00
6b516df34a dot: display pairs of states for products Alexandre Duret-Lutz 2015-11-13 23:16:39 +01:00
e3b8ed7bb5 python: add a show_default option to setup() Alexandre Duret-Lutz 2015-11-13 18:18:13 +01:00