From 982b5e7ffde547c7a0ed75afd8abd5319ce92108 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 14 Jul 2004 13:18:08 +0000 Subject: [PATCH] - Made some small, but very important, comments. --- src/modelchecker.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/modelchecker.c b/src/modelchecker.c index 823d55c..8e1c134 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -191,7 +191,9 @@ executeStep (const System sys, const int run) } /** - * remove from a roledef that is instantiated, the uninteresting ends bits + * Determine for a roledef that is instantiated, the uninteresting ends bits. + * + *@todo "What is interesting" relies on the fact that there are only secrecy, sychnr and agreement properties. */ Roledef removeIrrelevant (const System sys, const int run, Roledef rd) { @@ -273,6 +275,7 @@ explorify (const System sys, const int run) * need to be evaluated, then we can skip * further traversal. */ + //!@todo This implementation relies on the fact that there are only secrecy, sychnr and agreement properties. if (sys->secrets == NULL) { /* there are no remaining secrecy claims to be checked */ Roledef rdscan;