sylv/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Commit Graph

  • 4d154e8126 - Added knowledgePrintShort for knowledge displays without newlines. ccremers 2004-08-06 11:59:27 +00:00
  • cd0dce31f3 - Minor cleanup. ccremers 2004-07-30 12:11:05 +00:00
  • 15fcbf8090 - Added scen_st to the output, which lists the number of states in the specific scenario. ccremers 2004-07-30 12:04:38 +00:00
  • d75e3af55c - Added the trace prefix cutter. Goody. ccremers 2004-07-29 14:47:46 +00:00
  • 331569c9a8 - Added '--echo' to stdout the commandline. Useful for reporting. ccremers 2004-07-29 13:15:29 +00:00
  • 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 +00:00
  • 17c6fe5136 - Fixed some more printf usages, that should now be handled by eprintf. ccremers 2004-07-29 12:47:57 +00:00
  • 523b0ffd32 - Added --claims flag for some detailed output on claim violations. ccremers 2004-07-29 12:36:24 +00:00
  • d2a639b314 - More informative claim displays. ccremers 2004-07-29 12:04:53 +00:00
  • d181365e3e - Removed some old-fashioned defines, replacing them with enum constants. ccremers 2004-07-29 11:26:59 +00:00
  • b22667a791 - Fixed termlist printing. ccremers 2004-07-29 11:15:07 +00:00
  • 75ecbf4346 - Reordered some switches. - Inverted progress bar behaviour: default is off. Enable with -b. ccremers 2004-07-29 11:02:07 +00:00
  • 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 +00:00
  • 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 +00:00
  • a86e44dac6 Modifications for Elegast cluster. ccremers 2004-07-28 13:40:09 +00:00
  • 7aaed2dc90 - Added a reporting script, intended for parallel computations. ccremers 2004-07-28 12:40:16 +00:00
  • d62a8d89e1 - Of course, errors have a higher priority. ccremers 2004-07-28 12:23:42 +00:00
  • 42e5efedac - When counting scenarios, the exit code reflects the number of scenarios. ccremers 2004-07-28 12:22:40 +00:00
  • 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 +00:00
  • 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 +00:00
  • 289f71846b - Improved graph output for printing purposes. ccremers 2004-07-26 12:43:19 +00:00
  • 0ffa7b81ec - Fixed a bug with --pp=100. ccremers 2004-07-26 08:32:01 +00:00
  • 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 +00:00
  • 3ddedb6f7f - Totally untested. Otherwise, niagree should work ;) ccremers 2004-07-25 18:24:50 +00:00
  • 9723fff382 - Added termlistAddNew function to mimic set behaviour. ccremers 2004-07-25 18:14:21 +00:00
  • 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 +00:00
  • db52ec77e6 - Distinguishing example for prec sets computation; try using --pp=100, possibly with -r2. ccremers 2004-07-25 15:29:03 +00:00
  • 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 +00:00
  • 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 +00:00
  • bf991aa993 - Buggy: Broken intermediate version. ccremers 2004-07-24 19:00:43 +00:00
  • ace16a896f - Renamed runs.[c|h] to system.[c|h], which makes much more sense. ccremers 2004-07-24 15:08:35 +00:00
  • 3ac2a8d9bb - Moved some parts of runs.c into roles.c ccremers 2004-07-24 15:05:20 +00:00
  • 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 +00:00
  • 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 +00:00
  • 7e80d048d7 - Added reminder of this strange behaviour to todo.txt. ccremers 2004-07-21 14:06:03 +00:00
  • 9a2f6c09e8 - Added nisynch-rep file, which is a broken nsl3 with internal repetition. ccremers 2004-07-21 13:14:08 +00:00
  • 0ce648cc56 - Broken version (skip) ccremers 2004-07-21 13:12:47 +00:00
  • fb51f679a1 - Added two files for nisynch testing. ccremers 2004-07-21 13:11:36 +00:00
  • 056b5c245f - Big cleanup in modelchecker.c; threw out a lot of obsolete methods. ccremers 2004-07-21 12:42:04 +00:00
  • 6e8dcf8598 - Minor update to state progress bar cleaner. ccremers 2004-07-21 11:03:49 +00:00
  • 45950e3e56 - Lots of renaming on switches, to make it more readable. ccremers 2004-07-21 11:01:57 +00:00
  • de1d114f86 - Much work on the new states counter abstractions. ccremers 2004-07-21 10:35:39 +00:00
  • 1ecdd1eb5a - Made explicit chooses the default behaviour. ccremers 2004-07-20 21:31:28 +00:00
  • 81e715d612 - More cleanup and structuring in the modelchecker code. ccremers 2004-07-20 20:58:32 +00:00
  • 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 +00:00
  • 03ccf10960 - More automake remnants cleanup. ccremers 2004-07-20 14:20:22 +00:00
  • cfda7da8d9 - Remove some automake artefacts. ccremers 2004-07-20 14:17:22 +00:00
  • d9d94073d1 - Finally solved the stupid warning. ccremers 2004-07-20 13:01:58 +00:00
  • b570ca2d8a - Made all references to system explicit const references. - Removed config.h reference. ccremers 2004-07-20 12:41:56 +00:00
  • 2065c89add - Added some more macro unfolding. - More efficient term equality test. ccremers 2004-07-20 12:21:01 +00:00
  • 837fb4d8e1 - Corrected an inline definition, propagating it to the header file. ccremers 2004-07-20 09:47:06 +00:00
  • d74d70218f - Improved candidates throughput. ccremers 2004-07-20 09:07:43 +00:00
  • a588c90952 - Added some code optimizations after using gprof. ccremers 2004-07-20 08:51:23 +00:00
  • ff0c29142e - Some modified options. Doxygen is not working currently, I don't know why. ccremers 2004-07-19 14:01:43 +00:00
  • ffecc1a1ac - Added some doxygen documentation. ccremers 2004-07-19 13:31:44 +00:00
  • 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 +00:00
  • b412e56c7b - Traversal 10 is now the default. ccremers 2004-07-19 11:54:48 +00:00
  • 514848a10e - Implemented --no-noclaims-red and --no-endgame-red ccremers 2004-07-19 09:44:54 +00:00
  • ee0501d82d - Implemented --no-agent-symm to disable agent symmetry reductions. ccremers 2004-07-19 09:34:46 +00:00
  • 7ad99f977c - Fixed weird behaviour of executeStep restoration. ccremers 2004-07-19 09:32:12 +00:00
  • 7769fdbdf6 - Useful shortcut script for all this bke testing. ccremers 2004-07-19 09:25:40 +00:00
  • 5be15eb73b - Added state space display script. ccremers 2004-07-19 08:55:23 +00:00
  • 23b4d167c8 - Removed some warnings to the debug version only. - Added -t11. ccremers 2004-07-17 21:11:35 +00:00
  • 6a3edd06c2 - Cleaned up -t10, removed the inclination towards chooses. ccremers 2004-07-17 20:18:55 +00:00
  • ff178f46a5 - The yywrap solution was wrong; it should return 1. Fixed now. ccremers 2004-07-17 19:52:07 +00:00
  • ca975ed970 - Rollback of commit r674, because stuff was pretty broken. Work at that in phases. ccremers 2004-07-17 19:43:20 +00:00
  • 570933612f - Fixed the yywrap dependency warning in scanner.l ccremers 2004-07-17 19:35:54 +00:00
  • b70255ddbc - Fix symmetry reductions, choose might interfere with this. ccremers 2004-07-16 21:17:32 +00:00
  • 73f3b4d4ad - Fixed an error, where exit was used instead of error. ccremers 2004-07-16 14:11:56 +00:00
  • a7a2ed2fbd - Added a preliminary SCons script. ccremers 2004-07-16 14:11:19 +00:00
  • 1e7ef8f11d - Lots of rewrites and code cleanups. ccremers 2004-07-16 13:09:46 +00:00
  • 5d42bf40df - State progress bar needs less updating. ccremers 2004-07-16 09:03:37 +00:00
  • 6cf65f068f - Implemented --symm-order reduction. This clashes with --read-symm, but it actually faster. ccremers 2004-07-15 13:32:09 +00:00
  • 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 +00:00
  • 982b5e7ffd - Made some small, but very important, comments. ccremers 2004-07-14 13:18:08 +00:00
  • 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 +00:00
  • 32c4183315 - Added some (commented out) better reporting code. ccremers 2004-07-14 12:17:38 +00:00
  • 82b2603263 - Implemented the irrelevancy cutter, which immensely improves performance. ccremers 2004-07-14 12:10:39 +00:00
  • 269b5c7646 - Introduced the 'force-choose' switch, which helps the symmetry reduction algorithm along, notably. ccremers 2004-07-14 09:33:55 +00:00
  • 1efa77859f - Removed choose warnings for now. ccremers 2004-07-14 08:33:28 +00:00
  • 81c6be826e - Initial symmetry reduction. Gives a lot of warnings currently. ccremers 2004-07-14 08:17:49 +00:00
  • a5efc6106a - Static run symmetry detection seems to work just fine. - Added 'warning' call to error.h ccremers 2004-07-14 07:31:01 +00:00
  • 508d49efbb - Added local step index to runs. ccremers 2004-07-14 06:55:05 +00:00
  • 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 +00:00
  • 33441613e4 - Added BKE versions used in secrecy reduction article. ccremers 2004-07-13 19:36:13 +00:00
  • 8dee89217e - Cleanup of todo list. ccremers 2004-07-13 15:27:38 +00:00
  • 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 +00:00
  • 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 +00:00
  • 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 +00:00
  • 72be9a6441 - Moved the attack path display logic to output.c completely. - Adjusting output slightly. ccremers 2004-07-13 12:19:03 +00:00
  • 6fa0f3904d - Added more coloring. ccremers 2004-07-13 11:37:55 +00:00
  • 46da382950 - Fixed some old notation. ccremers 2004-07-13 11:37:45 +00:00
  • df9b97e5bc - If the --state-space switch is used, reporting is now always disabled. ccremers 2004-07-13 11:11:27 +00:00
  • 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 +00:00
  • ae6b85f290 - Improved graph coloring etc. ccremers 2004-07-13 09:56:19 +00:00
  • 410a35f4f4 - Fixed bug in attack output. - Re-enabled the noreport switch. ccremers 2004-07-13 09:36:30 +00:00
  • 981f0a92b4 - Started working on coloring of the attack trace in the state space. ccremers 2004-07-13 09:14:03 +00:00
  • 4b4c934b9c - Some hard-coded page sizing code. ccremers 2004-07-12 14:47:43 +00:00
  • cd3025e04e - Added preliminary support for state space printing using the dot package. Use the "--state-space" switch. ccremers 2004-07-12 13:58:41 +00:00
  • 363f95977a - Removed obsolete debugging output. ccremers 2004-07-12 13:57:59 +00:00