ccremers
fd3769d683
- Agreement test for Archne implemented (untested).
2004-08-27 14:41:06 +00:00
ccremers
4009ca86ed
- Added some sanity checks for read/send/claim role parameters.
...
- The cl->roles are now distance-ordered. This, the first role is at
distance 0, etc. This is useful for checking e.g. synchronisation.
2004-08-27 13:40:46 +00:00
ccremers
dfeaf83327
- Added 'termlistFind' function, which is more generic than inTermlist
2004-08-27 13:10:46 +00:00
ccremers
d8e0e93bcf
- Fixed a condition check in termlistAddNew.
...
- Roles are now computed from prec for each claim.
2004-08-27 12:36:23 +00:00
ccremers
542044e36f
- Added preliminary labellist support to the system.
2004-08-27 11:52:43 +00:00
ccremers
275743c1a3
- Fixed a bug where labels where not generated nicely if the symbols
...
already had been declared in another role.
2004-08-27 10:24:19 +00:00
ccremers
d58fc5ab43
- Made the label naming unique, by adding tuple info with the protocol
...
name. Now, we can simply test multiple protocol names by
concatenation.
- Removed the pointer equality leaf hypothesis, as it didn't hold
anymore.
2004-08-27 10:08:03 +00:00
ccremers
959c8d2c8b
- Added termlist_to_tuple function.
2004-08-26 12:36:01 +00:00
ccremers
6c38253559
- Turned the exit codes into enum types, making it more generic.
2004-08-24 13:09:39 +00:00
ccremers
7d0be35658
- Bugfix: term output now correctly displays local constants of a run
...
before it is bound.
2004-08-23 13:46:48 +00:00
ccremers
0fc008fe33
- Added keylevels to symbols. This is to help pruning the proofs, for
...
terms and patterns that do not originate on regular nodes.
2004-08-20 19:16:56 +00:00
ccremers
98bff1e5e2
- Solved the TERM_Hidden issue for the keys in termMguSubTerm. Yields
...
cleaner behaviour for MguSubterm.
2004-08-20 15:09:49 +00:00
ccremers
d7e49028c1
- Added pruning of functions the intruder does not know (e.g. SK)
2004-08-20 14:55:34 +00:00
ccremers
851044ecd0
- Improved the SK lemma, but it is NOT correct yet.
2004-08-20 11:47:00 +00:00
ccremers
72d52a6e12
- Key goals now have priority. This strategy yields complete proofs for
...
e.g. bke, and reduces states for NSL.
2004-08-20 10:52:40 +00:00
ccremers
baae7ef94a
- The proofs now also show a list of open goals at each step.
2004-08-20 09:53:44 +00:00
ccremers
bf2cbb5540
- Updated the todo list.
2004-08-20 09:26:34 +00:00
ccremers
be44ed047a
- Fixed some goal selection issues.
...
- Added note about mirroring model checker semantics.
2004-08-20 09:21:39 +00:00
ccremers
7308791c83
- More todos.
2004-08-20 08:01:35 +00:00
ccremers
bd84625ae4
- Fixed some more problems. Seems to be stable, although pruning is not
...
sufficient. Investigate bke-broken.
2004-08-19 15:30:31 +00:00
ccremers
f2bc78cc1f
- Improved proof output.
2004-08-19 14:55:21 +00:00
ccremers
8fa7c4e839
- Fixed bug in printing.
...
- Algorithm should work again.
2004-08-19 14:52:17 +00:00
ccremers
f25f0abd4e
- Fixed a memory error.
2004-08-19 14:49:03 +00:00
ccremers
35c55c9483
- Fixed a bug for NULL case in interm/subterm.
...
- Fixed a bug where the mgu termlist was never deleted in
interm/subterm.
2004-08-19 13:55:16 +00:00
ccremers
5c15c21832
- Reports on completeness of proofs.
2004-08-19 13:09:35 +00:00
ccremers
15580c6ec9
- Added subrun counters.
2004-08-19 12:47:53 +00:00
ccremers
be2df84f91
- Much improvements to the proof output.
2004-08-19 12:35:51 +00:00
ccremers
c993e17597
- Improving proof output.
2004-08-19 11:37:41 +00:00
ccremers
1180d3cf6f
- Added --proof switch for Arachne engine, which outputs the (partial)
...
proof of correctness.
2004-08-19 10:46:27 +00:00
ccremers
d73351ace7
- Added a good idea for the output.
2004-08-18 21:44:30 +00:00
ccremers
c929fa6ea3
- Debug info should be encapsulated.
2004-08-18 20:22:55 +00:00
ccremers
85ac32fbd1
- Claim counting now works.
2004-08-18 20:22:33 +00:00
ccremers
b1259e4b03
- Updated todo list.
2004-08-18 20:13:13 +00:00
ccremers
046eb67e78
- Some stuff has been fixed, so can be removed from the todo list.
2004-08-18 19:46:25 +00:00
ccremers
c95630f93b
- Improved pruning.
2004-08-18 19:43:58 +00:00
ccremers
0f75efc787
- Fixed bug in interm relation.
...
- Commented flag for normal version.
2004-08-18 18:41:49 +00:00
ccremers
8583b4ef5c
BROKEN
...
- Improved algorithm.
2004-08-18 18:22:59 +00:00
ccremers
341f519bbb
BROKEN
...
- Works better all the time. Huge shift of main logic. Much better.
2004-08-18 15:46:33 +00:00
ccremers
b2d21f0a8a
BROKEN
...
- Working on new algorithm. Some memory error can occur.
2004-08-18 14:06:14 +00:00
ccremers
c5695d6fe8
- Added more generic term iterators.
2004-08-18 12:12:29 +00:00
ccremers
eb5a39522b
- Compilation again. Now we have the sufficient components, and can
...
start to reconnect.
2004-08-18 09:57:01 +00:00
ccremers
b2838ed1e4
- Made a start with the new version.
2004-08-17 15:52:52 +00:00
ccremers
bb78c71c90
- Introduced termInTerm (bigterm, smallterm)
2004-08-17 14:11:25 +00:00
ccremers
a2cc46bb34
- Added test ns3 thing.
2004-08-17 11:30:58 +00:00
ccremers
8869477cf0
- Broken first attempt to work towards simplified method.
2004-08-17 11:30:03 +00:00
ccremers
5dd6127e4b
- Added term to binding relation.
2004-08-17 11:03:18 +00:00
ccremers
9ec1bdc8eb
- Merged with old version of warshall.c. Some minor improvements.
2004-08-17 09:48:29 +00:00
ccremers
f384042bfe
- Switched -r n behaviour for Arachne, effectively turning it into the
...
upper bound on runs.
2004-08-16 14:49:41 +00:00
ccremers
536e5bf237
- Fixed some errors in length detection.
...
- Added more bounds checking.
2004-08-16 13:18:04 +00:00
ccremers
05ee3f7f0a
- Added a new warshall. Compare with previous version at home.
...
- Rewrote the bind_to_*_run functions.
2004-08-16 09:50:37 +00:00
ccremers
c518e68881
BROKEN
...
- Added broken attempt to solve to problem, where a new instance has to
be bound, but older variables point to role terms, e.g. RV#1->RV.
What should happen, is that it becomes RV#1->RV#new. I thought of a
solution, but it is still somewhat broken. Maybe I should ignore any
mappings of variables such as RV, which might be included.
2004-08-15 19:58:26 +00:00
ccremers
91a679a129
- Made the output of the semistate include the bindings.
2004-08-15 17:50:41 +00:00
ccremers
071b9bd735
- Improved semistate printing.
2004-08-15 17:16:13 +00:00
ccremers
1f99b16ee8
- Much better implementation of M_0.
2004-08-15 17:07:38 +00:00
ccremers
ca2eeb7235
- Implemented better matching.
...
- Pruning for untrusted agent lists in the claim run as well.
- Sloppy M_0 implementation; needs to be fixed.
2004-08-15 16:44:54 +00:00
ccremers
c3d5123ab0
- Matching is now typed.
2004-08-15 16:08:53 +00:00
ccremers
c7e290197c
- Cycle detection seems to be working.
2004-08-15 14:57:50 +00:00
ccremers
28782548b0
- Implemented cycle detection. Untested.
2004-08-15 14:07:34 +00:00
ccremers
ffe20fb168
- Integrated new binding relation. No closure as yet.
2004-08-15 12:24:27 +00:00
ccremers
ef2586236c
- Added bindings module.
2004-08-15 11:55:22 +00:00
ccremers
0fee6b5797
- Secrecy claims are now handled fairly okayish, as long as only one
...
term is in the claim. This should be tupling-or, really, for
convenience.
2004-08-14 19:19:23 +00:00
ccremers
18415c95a2
- Fixed bug in run forcing.
2004-08-14 18:38:43 +00:00
ccremers
68d3bab305
- Improved indenting.
2004-08-14 18:11:30 +00:00
ccremers
b6598ea8f4
- Fixed a bug in subst reporting, when substitutions are compund terms.
2004-08-14 18:08:59 +00:00
ccremers
911e9e4e94
- Updated todo list.
2004-08-14 18:08:23 +00:00
ccremers
bf75e93f4c
- Substitutions from roles have to be reset to compare existing runs.
2004-08-14 16:26:57 +00:00
ccremers
1b3ef9e4ac
- Improved debugging output by adhering to the level setup.
2004-08-14 16:12:32 +00:00
ccremers
53cb869426
- Claim iteration works nicely now.
2004-08-14 15:59:14 +00:00
ccremers
68b2aa16e7
- Improved semistate printing.
2004-08-14 14:38:30 +00:00
ccremers
74851e0393
- Consistency improvements.
2004-08-14 14:27:46 +00:00
ccremers
f219461c8d
- After some trouble, nonce binding is working nicely.
2004-08-14 14:23:21 +00:00
ccremers
e3d16947ee
- Output cleanup.
2004-08-14 13:17:37 +00:00
ccremers
afda4f355e
- Added much debug info, so we can see send iteration is going wrong.
...
But why?
2004-08-13 20:56:51 +00:00
ccremers
fe16785982
- Fixed error in error reporting :-\
...
- Added intruder construction nodes.
- Several cleanups.
2004-08-13 20:09:12 +00:00
ccremers
a3828a028f
- Fixed the very annoying bug! The problem was in roleInstance for
...
Arachne. When a subst was carried out by an Rolename->compoundTerm
substitution, the compound term was not duplicated, and this caused
problems at roledef destruction.
2004-08-13 14:35:22 +00:00
ccremers
ff224fee8a
- Some cleanup.
...
- Added iteration limit, just enough to show the error.
2004-08-13 13:25:25 +00:00
ccremers
eb55dbe35d
- Fixed another '&' error.
2004-08-13 12:14:58 +00:00
ccremers
887b2f3a80
- Made indentDepth availabe in non-debug modes.
2004-08-13 11:11:59 +00:00
ccremers
43caf1707e
- Stupid layout fix.
2004-08-13 10:52:20 +00:00
ccremers
54d857ca3c
- Fixed a bug in mgu.c (& instead of &&)
...
- scons shared=yes is now okay for Valgrind.
2004-08-13 10:50:56 +00:00
ccremers
758cb88c8c
- Some POR optimizations in roleInstance were disabled for Arachne.
2004-08-13 10:28:20 +00:00
ccremers
70e5b98d37
- Added more intruder constructs.
2004-08-13 10:25:23 +00:00
ccremers
9153b06012
- Cleanup, improvements across the board.
2004-08-13 08:29:11 +00:00
ccremers
8fcdc9384e
- Removed crappy debug effort.
2004-08-12 13:23:21 +00:00
ccremers
b9f4d11d0a
- Some cleanup writes, e.g. making initalisation code order correspond
...
to struct field order.
2004-08-12 13:22:49 +00:00
ccremers
032d322952
- Fixed a bug with role destruction: the intruder goal term was not
...
duplicated, but destroyed nevertheless.
2004-08-12 12:37:30 +00:00
ccremers
0862ce20da
- Added more detailed debug output for Arachne.
...
- Fixed a header problem for compiler.c.
2004-08-12 12:28:57 +00:00
ccremers
2005aa929e
- Removed some obsolete commenting.
2004-08-12 12:03:20 +00:00
ccremers
7df10cf568
- Added role/protocol adding constructs for the intruder with Arachne.
2004-08-12 11:55:03 +00:00
ccremers
293c29b88e
- Added generic indent for Arachne.
...
- Some more error reporting.
2004-08-12 11:35:13 +00:00
ccremers
1791699c01
- Moved roledef_shift to role.c
2004-08-12 11:22:49 +00:00
ccremers
fe960cfb6a
- Added termlist iterator.
...
- Fixed role instance resetting role var substitutions.
2004-08-12 09:28:50 +00:00
ccremers
0f470cf6a2
- Rewrote roleInstance to cope with Arachne needs.
...
- Introduced some iterators for e.g. term leaves and roledefs. These are
not used everywhere yet.
2004-08-12 09:14:31 +00:00
ccremers
ac174b8130
- The work for the non-intruder Arachne part is now mostly done.
2004-08-11 21:04:52 +00:00
ccremers
ec8b515218
- Added more important bits.
2004-08-11 15:05:13 +00:00
ccremers
2191d80885
- Lots of stuff starts to take shape. Nice.
2004-08-11 14:09:12 +00:00
ccremers
f30207b059
- More logic.
2004-08-11 12:08:10 +00:00
ccremers
b74567b2e0
- Added more outlining for the arachne system.
2004-08-11 11:22:20 +00:00
ccremers
9cf3bf3da3
- Setup main arachne infrastructure.
2004-08-11 09:51:17 +00:00
ccremers
0008b58739
- Fixed wrong comment.
2004-08-11 08:20:22 +00:00
ccremers
742a65bac1
- Added claim symmetry reduction; this doesn't help much for lower
...
number of runs. It is on by default.
2004-08-11 08:17:49 +00:00
ccremers
1f96c9077a
- Added bind_run and bind_index for goal bindings to the roledef stuff.
2004-08-10 15:17:00 +00:00
ccremers
7fbd43986f
Preparations for Arachne.
...
- roleInstanceDestroy is very much needed.
- fixed bug in maxruns maintenance for incRuns.
- Arachne does not use run knowledge.
2004-08-10 15:02:37 +00:00
ccremers
028c3a03f2
- Bugfix.
2004-08-10 11:26:14 +00:00
ccremers
ca4c0c8869
- Added shift and length operations for generic lists.
2004-08-09 21:44:16 +00:00
ccremers
01d914314e
- Promoted sys to the global system state. Convenient for arachne
...
iterations.
2004-08-09 21:43:55 +00:00
ccremers
246c0c1c23
- Added termMguSubTerm and termMguInTerm
2004-08-09 21:22:24 +00:00
ccremers
a096aac6dd
- Added a note with inverseKey as for how to remove it.
2004-08-09 21:22:06 +00:00
ccremers
acc29656c6
- Added generic list library.
2004-08-09 20:15:05 +00:00
ccremers
8f501b1620
- Improved status output.
2004-08-09 10:41:25 +00:00
ccremers
71c658051e
- Reindented everything, so the layout is up to date again.
2004-08-09 10:05:58 +00:00
ccremers
4d1362cb1b
- Implemented --check=Secret switch, which allows checking of specific
...
properties.
- Fixed a bug in the symbol table, where symbols were never inserted
into the hash table.
2004-08-09 09:42:58 +00:00
ccremers
4d154e8126
- Added knowledgePrintShort for knowledge displays without newlines.
2004-08-06 11:59:27 +00:00
ccremers
cd0dce31f3
- Minor cleanup.
2004-07-30 12:11:05 +00:00
ccremers
15fcbf8090
- Added scen_st to the output, which lists the number of states in the
...
specific scenario.
2004-07-30 12:04:38 +00:00
ccremers
d75e3af55c
- Added the trace prefix cutter. Goody.
2004-07-29 14:47:46 +00:00
ccremers
331569c9a8
- Added '--echo' to stdout the commandline. Useful for reporting.
2004-07-29 13:15:29 +00:00
ccremers
c88c1d4461
- Removed --claims flag again.
...
- Now new reporting on stderr, with claim details.
- Added '--summary' to redirect this report to stdout.
2004-07-29 13:08:27 +00:00
ccremers
17c6fe5136
- Fixed some more printf usages, that should now be handled by eprintf.
2004-07-29 12:47:57 +00:00
ccremers
523b0ffd32
- Added --claims flag for some detailed output on claim violations.
2004-07-29 12:36:24 +00:00
ccremers
d2a639b314
- More informative claim displays.
2004-07-29 12:04:53 +00:00
ccremers
d181365e3e
- Removed some old-fashioned defines, replacing them with enum constants.
2004-07-29 11:26:59 +00:00
ccremers
b22667a791
- Fixed termlist printing.
2004-07-29 11:15:07 +00:00
ccremers
75ecbf4346
- Reordered some switches.
...
- Inverted progress bar behaviour: default is off. Enable with -b.
2004-07-29 11:02:07 +00:00
ccremers
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.
2004-07-29 10:13:13 +00:00
ccremers
d5db3ca0e2
- Current Elegast scripts are not suitable for -t9 because scenario
...
counting through the exit code is too limited. Fix.
2004-07-28 23:47:22 +00:00
ccremers
a86e44dac6
Modifications for Elegast cluster.
2004-07-28 13:40:09 +00:00
ccremers
7aaed2dc90
- Added a reporting script, intended for parallel computations.
2004-07-28 12:40:16 +00:00
ccremers
d62a8d89e1
- Of course, errors have a higher priority.
2004-07-28 12:23:42 +00:00
ccremers
42e5efedac
- When counting scenarios, the exit code reflects the number of
...
scenarios.
2004-07-28 12:22:40 +00:00
ccremers
1ba63d16d4
- Scyther now reports a 1 exit code (error) when a scenario number is
...
selected that is too large.
2004-07-28 12:03:42 +00:00
ccremers
472de3b526
- Added switch --choose-first.
...
- Added switch --scenario (-s), to enable scenario exploration only.
Use --scenario=-1 to count the number of possible scenarios.
2004-07-28 11:39:08 +00:00
ccremers
289f71846b
- Improved graph output for printing purposes.
2004-07-26 12:43:19 +00:00
ccremers
0ffa7b81ec
- Fixed a bug with --pp=100.
2004-07-26 08:32:01 +00:00
ccremers
38a3fdb320
- Moved doxyconfig to the refman directory, which makes much more sense.
...
However, it still needs an SConstruct script.
2004-07-25 20:39:49 +00:00
ccremers
3ddedb6f7f
- Totally untested. Otherwise, niagree should work ;)
2004-07-25 18:24:50 +00:00
ccremers
9723fff382
- Added termlistAddNew function to mimic set behaviour.
2004-07-25 18:14:21 +00:00
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
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
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
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
ccremers
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.
2004-07-14 12:46:11 +00:00
ccremers
32c4183315
- Added some (commented out) better reporting code.
2004-07-14 12:17:38 +00:00
ccremers
82b2603263
- Implemented the irrelevancy cutter, which immensely improves
...
performance.
2004-07-14 12:10:39 +00:00
ccremers
269b5c7646
- Introduced the 'force-choose' switch, which helps the symmetry
...
reduction algorithm along, notably.
2004-07-14 09:33:55 +00:00
ccremers
1efa77859f
- Removed choose warnings for now.
2004-07-14 08:33:28 +00:00
ccremers
81c6be826e
- Initial symmetry reduction. Gives a lot of warnings currently.
2004-07-14 08:17:49 +00:00
ccremers
a5efc6106a
- Static run symmetry detection seems to work just fine.
...
- Added 'warning' call to error.h
2004-07-14 07:31:01 +00:00
ccremers
508d49efbb
- Added local step index to runs.
2004-07-14 06:55:05 +00:00
ccremers
5bb5f610fb
- Added -t9 search, which does the chooses first. Doesn't seem to differ
...
much from -t8 though.
2004-07-13 20:20:58 +00:00
ccremers
8dee89217e
- Cleanup of todo list.
2004-07-13 15:27:38 +00:00
ccremers
39a2b4878c
- Debug of optimization.
...
- Put down skeleton of new idea, related to a lemma from Niek Palm's
work. This needs more investigating though.
2004-07-13 15:24:47 +00:00
ccremers
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.
2004-07-13 13:34:04 +00:00
ccremers
6d9c47a029
- Modelchecker now avoids some redundant traces. This should yield a
...
25-30 percent decrease of states for most cases tested sofar.
2004-07-13 12:36:50 +00:00
ccremers
72be9a6441
- Moved the attack path display logic to output.c completely.
...
- Adjusting output slightly.
2004-07-13 12:19:03 +00:00
ccremers
6fa0f3904d
- Added more coloring.
2004-07-13 11:37:55 +00:00
ccremers
df9b97e5bc
- If the --state-space switch is used, reporting is now always disabled.
2004-07-13 11:11:27 +00:00
ccremers
0c0a5021bb
- Improved the trace highlight in the state space, but it isn't as I
...
want it yet.
2004-07-13 11:10:06 +00:00
ccremers
ae6b85f290
- Improved graph coloring etc.
2004-07-13 09:56:19 +00:00