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
dfdea5b0bf
- Finished the protocol.
2004-08-23 11:59:42 +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