andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,208 Commits 1 Branch 0 Tags 21 MiB
4529fd4bfd
Commit Graph

110 Commits

Author SHA1 Message Date
ccremers
89c3a20acf - Many cleanups to make -Wall happy. Next up is pedantic... 2007-01-06 14:45:29 +00:00
ccremers
460c087cf2 - Some work towards moving stderror output for non-linux things out of 
the way.
 2006-08-02 10:29:40 +00:00
ccremers
4b671384af - Some fixes to compile under Cygwin 2006-08-01 09:13:55 +00:00
ccremers
9a98e66671 - Claim status is now reported after each claim. 2006-08-01 06:10:12 +00:00
ccremers
ff87bf180f - Claim reporting moved into claim.c 2006-08-01 05:58:02 +00:00
ccremers
5487d3ae90 - From this version onwards, Scyther no longer supports the modelchecker 
method. A big cleanup has been started, but is not finished yet, so
  minor artefacts might still remain. These are to be cleaned up later.
 2006-03-08 13:58:46 +00:00
ccremers
0ce88af6ac - [[[ Broken commit ]]] 
Committing partial new Warshall work because it is getting too big.
 2006-02-26 15:00:58 +00:00
ccremers
1d3d154a2f - If the timebound is hit, it should be reported anyway, because the 
results are not to be trusted anymore.
 2006-02-23 16:21:25 +00:00
ccremers
b2e40e07f3 - Some more work on hidelevel backbone. 
- Added '--count-states' switch for the Arachne engine.
 2006-02-22 08:24:29 +00:00
ccremers
da75862d82 - Huge code documentation effort. 2006-01-02 21:06:08 +00:00
ccremers
ebf50b5252 - Removed the bold for complete proof. 2005-12-29 13:36:01 +00:00
ccremers
ab75acea62 - Added colour output, with --monochrome switch to disable this. 2005-12-28 15:27:22 +00:00
ccremers
e19f8bddd1 - Improved Reachable claims output 
- Use square brackets for remark output instead of normal brackets.
 2005-12-28 14:42:46 +00:00
ccremers
0505aaacd6 - New claim: CLAIM_Reachable 
- Added new switches:
  -G,--generate-statespace
  -C,--generate-claims
- Claims are now allowed to have no label (they will be generated
  automatically)
- Output summary shows parameter of claims
- Internally, new symbols can now be generated by
  symbolNextFree(prefixsymbol)
 2005-12-28 11:50:17 +00:00
ccremers
ca4c5674ac - Added check for non-used variables. 2005-12-27 13:44:12 +00:00
ccremers
397298290b - Improved output significantly. 2005-12-27 12:24:12 +00:00
ccremers
cb2aef3915 - Old state/time info has now been removed. This was only needed for the 
POR engine anyway, so that's where it is shown now.
 2005-12-26 16:28:45 +00:00
ccremers
b6e9841c0f - Moved special terms into their own (very) special file. 2005-06-16 14:10:07 +00:00
ccremers
db18b203a9 - Added "Empty" claim type, which is ignored. 
Syntax example:   claim_x(I, Empty);
 2005-06-16 11:59:44 +00:00
ccremers
1bdaf7b5d9 - Large rewrite of switch code. Instead of having switch parameters in 
the (monstrously large) system structure, there is now a global
  'switchdata' structure originating in switches.c. This makes it much
  easier to see what's happening.
  * Note: although this code has been tested, there might be some
    hiccups, because doing multiple search&replace actions over all
    files is bound to cause some problems.
 2005-06-07 15:02:27 +00:00
ccremers
3bbaf0fc97 - Added scyther wrapper tag (cf. GH bug report) 
- Fixed binding closure (cf. GH bug report)
- Reduced indenting to two instead of three spaces.
 2005-05-03 09:45:54 +00:00
ccremers
18d523d8a4 - Fixed segfault when modelchecker was called on an empty scenario. 2005-04-22 16:03:58 +00:00
ccremers
4919cf2a2d - Some consistency fixes after removing argtable2 dependency. 2005-04-10 15:36:41 +00:00
ccremers
738a2b5859 - Rewrote complete switch code. Scyther now no longer depends on 
argtable2. Great.
 2005-04-10 15:30:47 +00:00
ccremers
560acb220d - Removed an obsolete warning about -m2 2005-03-08 13:54:13 +00:00
ccremers
e36392b1d2 - Rewrote the way the version number is imported into the source. Much 
better now.
 2005-02-01 20:05:41 +00:00
ccremers
56caa2c1e4 - Fixed the svn version number registering. Still needs some work 
though, as the -SVNVERSION thing only needs to be passed to the
  builder of main.c.
 2005-02-01 19:39:03 +00:00
ccremers
b607b1e260 - If we run into the time bound, report it. 2005-01-14 13:01:31 +00:00
ccremers
9df1bfed5b - Made the output more easily machine-parsed. 2005-01-14 12:48:26 +00:00
ccremers
bd0069886c - "correct" output for claims that are not encountered, as one would 
expect.
 2005-01-14 12:38:43 +00:00
ccremers
e0e56964d1 - Added a --timer=x switch to abort Arachne proofs after x seconds. 2005-01-05 15:29:27 +00:00
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