331569c9a8- Added '--echo' to stdout the commandline. Useful for reporting.
ccremers
2004-07-29 13:15:29 +0000
c88c1d4461- Removed --claims flag again. - Now new reporting on stderr, with claim details. - Added '--summary' to redirect this report to stdout.
ccremers
2004-07-29 13:08:27 +0000
17c6fe5136- Fixed some more printf usages, that should now be handled by eprintf.
ccremers
2004-07-29 12:47:57 +0000
523b0ffd32- Added --claims flag for some detailed output on claim violations.
ccremers
2004-07-29 12:36:24 +0000
d2a639b314- More informative claim displays.
ccremers
2004-07-29 12:04:53 +0000
d181365e3e- Removed some old-fashioned defines, replacing them with enum constants.
ccremers
2004-07-29 11:26:59 +0000
75ecbf4346- Reordered some switches. - Inverted progress bar behaviour: default is off. Enable with -b.
ccremers
2004-07-29 11:02:07 +0000
dda2907492- Implemented output method selector, sys->output. - Changed disable-report switch into --empty. - --scenario=-1 now displays a list of scenarios. Use wc -l to count them.
ccremers
2004-07-29 10:13:13 +0000
d5db3ca0e2- Current Elegast scripts are not suitable for -t9 because scenario counting through the exit code is too limited. Fix.
ccremers
2004-07-28 23:47:22 +0000
a86e44dac6Modifications for Elegast cluster.
ccremers
2004-07-28 13:40:09 +0000
7aaed2dc90- Added a reporting script, intended for parallel computations.
ccremers
2004-07-28 12:40:16 +0000
d62a8d89e1- Of course, errors have a higher priority.
ccremers
2004-07-28 12:23:42 +0000
42e5efedac- When counting scenarios, the exit code reflects the number of scenarios.
ccremers
2004-07-28 12:22:40 +0000
1ba63d16d4- Scyther now reports a 1 exit code (error) when a scenario number is selected that is too large.
ccremers
2004-07-28 12:03:42 +0000
472de3b526- Added switch --choose-first. - Added switch --scenario (-s), to enable scenario exploration only. Use --scenario=-1 to count the number of possible scenarios.
ccremers
2004-07-28 11:39:08 +0000
0ffa7b81ec- Fixed a bug with --pp=100.
ccremers
2004-07-26 08:32:01 +0000
38a3fdb320- Moved doxyconfig to the refman directory, which makes much more sense. However, it still needs an SConstruct script.
ccremers
2004-07-25 20:39:49 +0000
3ddedb6f7f- Totally untested. Otherwise, niagree should work ;)
ccremers
2004-07-25 18:24:50 +0000
9723fff382- Added termlistAddNew function to mimic set behaviour.
ccremers
2004-07-25 18:14:21 +0000
f8aacee6ad- Improved some minor stuff regarding synchronisation checking and debugging info. - '--pp=100' switch in debug mode now allows for disabling of synchronising_labels set.
ccremers
2004-07-25 15:30:58 +0000
db52ec77e6- Distinguishing example for prec sets computation; try using --pp=100, possibly with -r2.
ccremers
2004-07-25 15:29:03 +0000
4f1c9ecb48- Amazingly, I think I implemented ni-synch partial order reduction. It still needs some careful analysis though.
ccremers
2004-07-24 20:30:00 +0000
60b02eea0e- Renamed nearly all files. Now, we try to use singular terms. Exception: states.h is the plural form.
ccremers
2004-07-24 19:07:29 +0000
ace16a896f- Renamed runs.[c|h] to system.[c|h], which makes much more sense.
ccremers
2004-07-24 15:08:35 +0000
3ac2a8d9bb- Moved some parts of runs.c into roles.c
ccremers
2004-07-24 15:05:20 +0000
1c234e3cee- Bugfixed claims.c (r722 log), although the reason for fixing and the error itself is quite irreproducable.
ccremers
2004-07-22 11:57:15 +0000
7ce5736af3- Added attack script. - Worked on ni-synch claims. Todo: weirdness with: ./scyther ../spdl/nsl3-nisynch.spdl -t1 -r2
ccremers
2004-07-21 14:26:28 +0000
7e80d048d7- Added reminder of this strange behaviour to todo.txt.
ccremers
2004-07-21 14:06:03 +0000
9a2f6c09e8- Added nisynch-rep file, which is a broken nsl3 with internal repetition.
ccremers
2004-07-21 13:14:08 +0000
0ce648cc56- Broken version (skip)
ccremers
2004-07-21 13:12:47 +0000
fb51f679a1- Added two files for nisynch testing.
ccremers
2004-07-21 13:11:36 +0000
056b5c245f- Big cleanup in modelchecker.c; threw out a lot of obsolete methods.
ccremers
2004-07-21 12:42:04 +0000
6e8dcf8598- Minor update to state progress bar cleaner.
ccremers
2004-07-21 11:03:49 +0000
45950e3e56- Lots of renaming on switches, to make it more readable.
ccremers
2004-07-21 11:01:57 +0000
de1d114f86- Much work on the new states counter abstractions.
ccremers
2004-07-21 10:35:39 +0000
1ecdd1eb5a- Made explicit chooses the default behaviour.
ccremers
2004-07-20 21:31:28 +0000
81e715d612- More cleanup and structuring in the modelchecker code.
ccremers
2004-07-20 20:58:32 +0000
4d60acf431- Rewrote all main traversal logics to use inline functions. - Added -t12. This is much faster than -t10, but yields equal states, and made it the default choice.
ccremers
2004-07-20 20:42:53 +0000
03ccf10960- More automake remnants cleanup.
ccremers
2004-07-20 14:20:22 +0000
cfda7da8d9- Remove some automake artefacts.
ccremers
2004-07-20 14:17:22 +0000
d9d94073d1- Finally solved the stupid warning.
ccremers
2004-07-20 13:01:58 +0000
b570ca2d8a- Made all references to system explicit const references. - Removed config.h reference.
ccremers
2004-07-20 12:41:56 +0000
2065c89add- Added some more macro unfolding. - More efficient term equality test.
ccremers
2004-07-20 12:21:01 +0000
837fb4d8e1- Corrected an inline definition, propagating it to the header file.
ccremers
2004-07-20 09:47:06 +0000
a588c90952- Added some code optimizations after using gprof.
ccremers
2004-07-20 08:51:23 +0000
ff0c29142e- Some modified options. Doxygen is not working currently, I don't know why.
ccremers
2004-07-19 14:01:43 +0000
ffecc1a1ac- Added some doxygen documentation.
ccremers
2004-07-19 13:31:44 +0000
03c19a4774- Improved handling of pruning in explorify. Now, when pruning is done in explorify, the signal is passed back, and match_basic etc. will signal that the event was not enabled.
ccremers
2004-07-19 12:03:29 +0000
b412e56c7b- Traversal 10 is now the default.
ccremers
2004-07-19 11:54:48 +0000
514848a10e- Implemented --no-noclaims-red and --no-endgame-red
ccremers
2004-07-19 09:44:54 +0000
73f3b4d4ad- Fixed an error, where exit was used instead of error.
ccremers
2004-07-16 14:11:56 +0000
a7a2ed2fbd- Added a preliminary SCons script.
ccremers
2004-07-16 14:11:19 +0000
1e7ef8f11d- Lots of rewrites and code cleanups.
ccremers
2004-07-16 13:09:46 +0000
5d42bf40df- State progress bar needs less updating.
ccremers
2004-07-16 09:03:37 +0000
6cf65f068f- Implemented --symm-order reduction. This clashes with --read-symm, but it actually faster.
ccremers
2004-07-15 13:32:09 +0000
62b2eca8da- Implemented read symmetries reduction as a switch '--read-symm'. Works with e.g. t8. t10 is also implemented as a test.
ccremers
2004-07-15 11:04:15 +0000
982b5e7ffd- Made some small, but very important, comments.
ccremers
2004-07-14 13:18:08 +0000
27d3bb4061- Previous entry was buggy; killing the roledef removed very extensive parts of the tree. Solved by restoring it after recursing, which is waht should have happened in the first place. - It's still a good improvement though.
ccremers
2004-07-14 12:46:11 +0000
82b2603263- Implemented the irrelevancy cutter, which immensely improves performance.
ccremers
2004-07-14 12:10:39 +0000
269b5c7646- Introduced the 'force-choose' switch, which helps the symmetry reduction algorithm along, notably.
ccremers
2004-07-14 09:33:55 +0000
1efa77859f- Removed choose warnings for now.
ccremers
2004-07-14 08:33:28 +0000
81c6be826e- Initial symmetry reduction. Gives a lot of warnings currently.
ccremers
2004-07-14 08:17:49 +0000
a5efc6106a- Static run symmetry detection seems to work just fine. - Added 'warning' call to error.h
ccremers
2004-07-14 07:31:01 +0000
508d49efbb- Added local step index to runs.
ccremers
2004-07-14 06:55:05 +0000
5bb5f610fb- Added -t9 search, which does the chooses first. Doesn't seem to differ much from -t8 though.
ccremers
2004-07-13 20:20:58 +0000
33441613e4- Added BKE versions used in secrecy reduction article.
ccremers
2004-07-13 19:36:13 +0000
8dee89217e- Cleanup of todo list.
ccremers
2004-07-13 15:27:38 +0000
39a2b4878c- Debug of optimization. - Put down skeleton of new idea, related to a lemma from Niek Palm's work. This needs more investigating though.
ccremers
2004-07-13 15:24:47 +0000
b6806f6aaf- Significantly improved state reduction by scanning for states where no claim is to be evaluated anymore. This needs some reporting, and significantly alters comparisons with previous versions.
ccremers
2004-07-13 13:34:04 +0000
6d9c47a029- Modelchecker now avoids some redundant traces. This should yield a 25-30 percent decrease of states for most cases tested sofar.
ccremers
2004-07-13 12:36:50 +0000
72be9a6441- Moved the attack path display logic to output.c completely. - Adjusting output slightly.
ccremers
2004-07-13 12:19:03 +0000
6fa0f3904d- Added more coloring.
ccremers
2004-07-13 11:37:55 +0000
46da382950- Fixed some old notation.
ccremers
2004-07-13 11:37:45 +0000
df9b97e5bc- If the --state-space switch is used, reporting is now always disabled.
ccremers
2004-07-13 11:11:27 +0000
0c0a5021bb- Improved the trace highlight in the state space, but it isn't as I want it yet.
ccremers
2004-07-13 11:10:06 +0000
ae6b85f290- Improved graph coloring etc.
ccremers
2004-07-13 09:56:19 +0000
410a35f4f4- Fixed bug in attack output. - Re-enabled the noreport switch.
ccremers
2004-07-13 09:36:30 +0000
981f0a92b4- Started working on coloring of the attack trace in the state space.
ccremers
2004-07-13 09:14:03 +0000
4b4c934b9c- Some hard-coded page sizing code.
ccremers
2004-07-12 14:47:43 +0000
cd3025e04e- Added preliminary support for state space printing using the dot package. Use the "--state-space" switch.
ccremers
2004-07-12 13:58:41 +0000
ccremers