Commit Graph

79 Commits

Author SHA1 Message Date
ccremers
7309bb5550 - Fixed debug comment. 2004-12-29 14:18:13 +00:00
ccremers
5e695097f2 - Reimplemented the weight functions for goal selection.
- Added --goal-select function, defaults to 3.
2004-12-29 14:17:49 +00:00
ccremers
635470d976 - Added -d switch. 2004-12-09 15:27:50 +00:00
ccremers
b56c01c422 - Added '--max-depth=X' switch (which is equal to the old '-l X -a')
- Modified semantics of -l with -a : this corresponds more to the
  intuition and introduces the new option to prune proofs based on trace
  length.
2004-12-09 15:11:45 +00:00
ccremers
506e42f841 - Re-indented the files. 2004-11-16 12:07:55 +00:00
ccremers
a38925c9c2 - Added some useful macros to term.h to address subparts (e.g.
TermOp1(t)). Renamed all uses.
2004-11-16 12:06:36 +00:00
ccremers
343314896b - Added version info to compilation process. 2004-11-01 14:52:52 +00:00
ccremers
67673cb608 - No more warning for output in standard debug mode. 2004-10-18 13:49:20 +00:00
ccremers
d33ec486ce - Modified -l switch to also serve as proof depth limit. 2004-10-14 15:25:28 +00:00
ccremers
87a75106d1 - Printing the protocol tab-separated from the role is more useful for
script-based parsing.
2004-10-14 13:29:28 +00:00
ccremers
2bc1df6135 - Improved readability of printed claims.
- Fixed comment.
2004-10-14 13:19:36 +00:00
ccremers
6c38253559 - Turned the exit codes into enum types, making it more generic. 2004-08-24 13:09:39 +00:00
ccremers
5c15c21832 - Reports on completeness of proofs. 2004-08-19 13:09:35 +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
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
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
ef2586236c - Added bindings module. 2004-08-15 11:55:22 +00:00
ccremers
2191d80885 - Lots of stuff starts to take shape. Nice. 2004-08-11 14:09:12 +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
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
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
01d914314e - Promoted sys to the global system state. Convenient for arachne
iterations.
2004-08-09 21:43:55 +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
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
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
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
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
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
ace16a896f - Renamed runs.[c|h] to system.[c|h], which makes much more sense. 2004-07-24 15:08:35 +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
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
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
7ad99f977c - Fixed weird behaviour of executeStep restoration. 2004-07-19 09:32:12 +00:00
ccremers
570933612f - Fixed the yywrap dependency warning in scanner.l 2004-07-17 19:35:54 +00:00