andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Modelchecker now avoids some redundant traces. This should yield a

Browse Source 
25-30 percent decrease of states for most cases tested sofar.
This commit is contained in:
ccremers 2004-07-13 12:36:50 +00:00
parent 72be9a6441
commit 6d9c47a029
2 changed files with 20 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/modelchecker.c
View File

@ -187,11 +187,9 @@ executeStep (const System sys, const int run)
return 1; return 1;
} }
/* //! Explores the system state given by the next step of a run.
* explorify /**
*
* grandiose naming scheme (c) sjors dubya. * grandiose naming scheme (c) sjors dubya.
* explores the system state given by the next step of a run.
*/ */
int int
@ -207,19 +205,27 @@ explorify (const System sys, const int run)
exit (1); exit (1);
} }
if (executeStep (sys, run)) flag = 0;
{
/* traverse the system after the step */
flag = traverse (sys); /* special check: internal read
* Efficiency of the next check heavily relies on lazy L-R evaluation
*/
if (rd->internal && rd->type == READ && inTermlist (sys->untrusted, agentOfRun (sys, run)))
{
/* this run is executed by an untrusted agent, do not explore */
} }
else else
{ {
flag = 0; if (executeStep (sys, run))
{
/* traverse the system after the step */
flag = traverse (sys);
runPointerSet (sys, run, rd);
sys->step--;
indentSet (sys->step);
}
} }
runPointerSet (sys, run, rd);
sys->step--;
indentSet (sys->step);
return flag; return flag;
} }

6
src/todo.txt
View File

@ -1,20 +1,18 @@
- Constraint logic now also has no checks for when a run is done by the
intruder (which should be excluded).
- Fix constants in intruder knowledge. Auto add single one of each type, - Fix constants in intruder knowledge. Auto add single one of each type,
when typed expl. Add single constant when untyped. Fix this also in when typed expl. Add single constant when untyped. Fix this also in
semantics, and add proof to establish sufficiency. semantics, and add proof to establish sufficiency.
- Fix function handling (signatures). - Fix function handling (signatures).
- Make state space output using dot package.
- Intruder should at least have one copy of each type that an agent can - Intruder should at least have one copy of each type that an agent can
construct, I think in any case. Proof needed for single identifier need. construct, I think in any case. Proof needed for single identifier need.
Furthermore reduction if type flaw testing; only one constant needed. Furthermore reduction if type flaw testing; only one constant needed.
- Functions should have a signature.
- State counter is off by one. Should start at 1, or should add 1 at printing. - State counter is off by one. Should start at 1, or should add 1 at printing.
- Make filter switch, allowing maybe for some claims only to be evaluated. - Make filter switch, allowing maybe for some claims only to be evaluated.
--check=Secret, --check-all as default. --check=Secret, --check-all as default.
- Some compiler errors are still sent to stdout. This must be fixed - Some compiler errors are still sent to stdout. This must be fixed
ASAP! because it means people get an invisible error using the ASAP! because it means people get an invisible error using the
scripts. scripts.
- There is a possible memory leak when buffering attacks, e.g. with -p0.
Investigate.
- Make --with-argtabledir= something switch, replacing - Make --with-argtabledir= something switch, replacing
README/galious-configure.sh constructs. README/galious-configure.sh constructs.
- Move initial intruder knowledge maybe into the title of the MSC. - Move initial intruder knowledge maybe into the title of the MSC.