Commit Graph

340 Commits

Author SHA1 Message Date
ccremers
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.
2004-07-25 15:30:58 +00:00
ccremers
db52ec77e6 - Distinguishing example for prec sets computation; try using --pp=100,
possibly with -r2.
2004-07-25 15:29:03 +00:00
ccremers
4f1c9ecb48 - Amazingly, I think I implemented ni-synch partial order reduction. It
still needs some careful analysis though.
2004-07-24 20:30:00 +00:00
ccremers
60b02eea0e - Renamed nearly all files. Now, we try to use singular terms.
Exception: states.h is the plural form.
2004-07-24 19:07:29 +00:00
ccremers
bf991aa993 - Buggy: Broken intermediate version. 2004-07-24 19:00:43 +00:00
ccremers
ace16a896f - Renamed runs.[c|h] to system.[c|h], which makes much more sense. 2004-07-24 15:08:35 +00:00
ccremers
3ac2a8d9bb - Moved some parts of runs.c into roles.c 2004-07-24 15:05:20 +00:00
ccremers
1c234e3cee - Bugfixed claims.c (r722 log), although the reason for fixing and the
error itself is quite irreproducable.
2004-07-22 11:57:15 +00:00
ccremers
7ce5736af3 - Added attack script.
- Worked on ni-synch claims.
  Todo: weirdness with: ./scyther ../spdl/nsl3-nisynch.spdl -t1 -r2
2004-07-21 14:26:28 +00:00
ccremers
7e80d048d7 - Added reminder of this strange behaviour to todo.txt. 2004-07-21 14:06:03 +00:00
ccremers
9a2f6c09e8 - Added nisynch-rep file, which is a broken nsl3 with internal
repetition.
2004-07-21 13:14:08 +00:00
ccremers
0ce648cc56 - Broken version (skip) 2004-07-21 13:12:47 +00:00
ccremers
fb51f679a1 - Added two files for nisynch testing. 2004-07-21 13:11:36 +00:00
ccremers
056b5c245f - Big cleanup in modelchecker.c; threw out a lot of obsolete methods. 2004-07-21 12:42:04 +00:00
ccremers
6e8dcf8598 - Minor update to state progress bar cleaner. 2004-07-21 11:03:49 +00:00
ccremers
45950e3e56 - Lots of renaming on switches, to make it more readable. 2004-07-21 11:01:57 +00:00
ccremers
de1d114f86 - Much work on the new states counter abstractions. 2004-07-21 10:35:39 +00:00
ccremers
1ecdd1eb5a - Made explicit chooses the default behaviour. 2004-07-20 21:31:28 +00:00
ccremers
81e715d612 - More cleanup and structuring in the modelchecker code. 2004-07-20 20:58:32 +00:00
ccremers
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.
2004-07-20 20:42:53 +00:00
ccremers
03ccf10960 - More automake remnants cleanup. 2004-07-20 14:20:22 +00:00
ccremers
cfda7da8d9 - Remove some automake artefacts. 2004-07-20 14:17:22 +00:00
ccremers
d9d94073d1 - Finally solved the stupid warning. 2004-07-20 13:01:58 +00:00
ccremers
b570ca2d8a - Made all references to system explicit const references.
- Removed config.h reference.
2004-07-20 12:41:56 +00:00
ccremers
2065c89add - Added some more macro unfolding.
- More efficient term equality test.
2004-07-20 12:21:01 +00:00
ccremers
837fb4d8e1 - Corrected an inline definition, propagating it to the header file. 2004-07-20 09:47:06 +00:00
ccremers
d74d70218f - Improved candidates throughput. 2004-07-20 09:07:43 +00:00
ccremers
a588c90952 - Added some code optimizations after using gprof. 2004-07-20 08:51:23 +00:00
ccremers
ff0c29142e - Some modified options. Doxygen is not working currently, I don't know why. 2004-07-19 14:01:43 +00:00
ccremers
ffecc1a1ac - Added some doxygen documentation. 2004-07-19 13:31:44 +00:00
ccremers
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.
2004-07-19 12:03:29 +00:00
ccremers
b412e56c7b - Traversal 10 is now the default. 2004-07-19 11:54:48 +00:00
ccremers
514848a10e - Implemented --no-noclaims-red and --no-endgame-red 2004-07-19 09:44:54 +00:00
ccremers
ee0501d82d - Implemented --no-agent-symm to disable agent symmetry reductions. 2004-07-19 09:34:46 +00:00
ccremers
7ad99f977c - Fixed weird behaviour of executeStep restoration. 2004-07-19 09:32:12 +00:00
ccremers
7769fdbdf6 - Useful shortcut script for all this bke testing. 2004-07-19 09:25:40 +00:00
ccremers
5be15eb73b - Added state space display script. 2004-07-19 08:55:23 +00:00
ccremers
23b4d167c8 - Removed some warnings to the debug version only.
- Added -t11.
2004-07-17 21:11:35 +00:00
ccremers
6a3edd06c2 - Cleaned up -t10, removed the inclination towards chooses. 2004-07-17 20:18:55 +00:00
ccremers
ff178f46a5 - The yywrap solution was wrong; it should return 1. Fixed now. 2004-07-17 19:52:07 +00:00
ccremers
ca975ed970 - Rollback of commit r674, because stuff was pretty broken. Work at that
in phases.
2004-07-17 19:43:20 +00:00
ccremers
570933612f - Fixed the yywrap dependency warning in scanner.l 2004-07-17 19:35:54 +00:00
ccremers
b70255ddbc - Fix symmetry reductions, choose might interfere with this. 2004-07-16 21:17:32 +00:00
ccremers
73f3b4d4ad - Fixed an error, where exit was used instead of error. 2004-07-16 14:11:56 +00:00
ccremers
a7a2ed2fbd - Added a preliminary SCons script. 2004-07-16 14:11:19 +00:00
ccremers
1e7ef8f11d - Lots of rewrites and code cleanups. 2004-07-16 13:09:46 +00:00
ccremers
5d42bf40df - State progress bar needs less updating. 2004-07-16 09:03:37 +00:00
ccremers
6cf65f068f - Implemented --symm-order reduction. This clashes with --read-symm, but
it actually faster.
2004-07-15 13:32:09 +00:00
ccremers
62b2eca8da - Implemented read symmetries reduction as a switch '--read-symm'. Works with e.g. t8. t10 is also implemented as a test. 2004-07-15 11:04:15 +00:00
ccremers
982b5e7ffd - Made some small, but very important, comments. 2004-07-14 13:18:08 +00:00