diff --git a/src/BUILD.txt b/src/BUILD.txt new file mode 100644 index 0000000..8c83447 --- /dev/null +++ b/src/BUILD.txt @@ -0,0 +1,12 @@ +Cross-platform building: + +On linux: + + ./build-unix-both.sh + +On MAC: + + ./build-mac-universal.sh + +This copies all files into the gui bin directory, and you're done. + diff --git a/src/main.c b/src/main.c index ddfab86..e71b1f1 100644 --- a/src/main.c +++ b/src/main.c @@ -118,13 +118,10 @@ main (int argc, char **argv) /* compile */ - // Compile no runs for Arachne + // Compile no runs for Arachne and preprocess compile (spdltac, 0); scanner_cleanup (); - /* preprocess */ - preprocess (sys); - #ifdef DEBUG if (DEBUGL (1)) { @@ -254,13 +251,6 @@ modelCheck (const System sys) /* modelcheck the system */ claimcount = arachne (); - /* clean up any states display */ - if (switches.reportStates > 0) - { - // States: 1.000e+06 - printfstderr (" \r"); - } - if (claimcount == 0) { warning ("No claims in system."); diff --git a/src/switches.c b/src/switches.c index 2f10090..40b69dc 100644 --- a/src/switches.c +++ b/src/switches.c @@ -62,6 +62,9 @@ switchesInit (int argc, char **argv) switches.initUnique = false; // default allows initiator rho to contain duplicate terms switches.respUnique = false; // default allows responder rho to contain duplicate terms switches.intruder = true; // default allows an intruder + switches.agentUnfold = 0; // default not to unfold agents + switches.abstractionMethod = 0; // default no abstraction used + switches.useAttackBuffer = false; // don't use by default as it does not work properly under windows vista yet // Misc switches.switchP = 0; // multi-purpose parameter @@ -81,7 +84,6 @@ switchesInit (int argc, char **argv) switches.human = false; // not human friendly by default switches.reportMemory = 0; switches.reportTime = 0; - switches.reportStates = 0; switches.countStates = false; // default off switches.extendNonReads = 0; // default off switches.extendTrivial = 0; // default off @@ -450,7 +452,7 @@ switcher (const int process, int index, int commandline) { if (!process) { - helptext ("-d, --dot-output", "show attack output in dot format"); + helptext ("-d, --dot-output", "show patterns in dot format"); } else { @@ -464,7 +466,7 @@ switcher (const int process, int index, int commandline) { if (!process) { - helptext ("-x, --xml-output", "show attack output in XML format"); + helptext ("-x, --xml-output", "show patterns in XML format"); } else { @@ -570,7 +572,7 @@ switcher (const int process, int index, int commandline) if (switches.expert) { helptext ("-C, --class", - "generate full class (show uninstantiated variables in state output)"); + "show full class (allow uninstantiated variables in pattern output)"); } } else @@ -587,7 +589,7 @@ switcher (const int process, int index, int commandline) if (switches.expert) { helptext ("-s, --state-space", - "ignore any existing claims and add 'reachable' claims. Generate full state space classes"); + "ignore any existing claims and add 'reachable' claims. Gives complete characterization of a roles"); } } else @@ -674,7 +676,7 @@ switcher (const int process, int index, int commandline) if (!process) { helptext ("-r, --max-runs=", - "maximum number of runs in the system [5]"); + "maximum number of runs in patterns [5]"); } else { @@ -696,7 +698,7 @@ switcher (const int process, int index, int commandline) if (!process) { helptext (" --unbounded", - "Do not bound the number of runs in the state space"); + "Do not bound the number of runs in patterns"); } else { @@ -857,6 +859,25 @@ switcher (const int process, int index, int commandline) } } + if (detect (' ', "abstraction-method", 1)) + { + if (!process) + { + if (switches.expert) + { + /* Not working yet + helptext (" --abstraction-method=", + "Abstraction method used. Default: 0 (disabled)"); + */ + } + } + else + { + switches.abstractionMethod = integer_argument (); + return index; + } + } + /* ================== * Modelchecker only @@ -911,6 +932,20 @@ switcher (const int process, int index, int commandline) } } + if (detect (' ', "agent-unfold", 1)) + { + if (!process) + { + /* discourage: hide + */ + } + else + { + switches.agentUnfold = integer_argument (); + return index; + } + } + if (detect (' ', "extend-nonreads", 0)) { if (!process) @@ -1183,21 +1218,6 @@ switcher (const int process, int index, int commandline) } } - if (detect (' ', "progress-bar", 0)) - { - if (!process) - { - /* discourage: do not show in help text - helptext ("-b,--progress-bar", "show progress bar"); - */ - } - else - { - switches.reportStates = 50000; - return index; - } - } - if (detect ('e', "empty", 0)) { if (!process) diff --git a/src/switches.h b/src/switches.h index a7730a6..95c61a5 100644 --- a/src/switches.h +++ b/src/switches.h @@ -36,6 +36,9 @@ struct switchdata int initUnique; //!< Default allows duplicate terms in rho (init) int respUnique; //!< Default allows duplicate terms in rho (resp) int intruder; //!< Enable intruder actions (default) + int agentUnfold; //!< Explicitly unfold for N honest agents and 1 compromised iff > 0 + int abstractionMethod; //!< 0 means none, others are specific modes + int useAttackBuffer; //!< Use temporary file for attack storage // Misc int switchP; //!< A multi-purpose integer parameter, passed to the partial order reduction method selected. @@ -55,7 +58,6 @@ struct switchdata int human; //!< human readable int reportMemory; //!< Memory display switch. int reportTime; //!< Time display switch. - int reportStates; //!< Progress display switch. (traversed states) int countStates; //!< Count states int extendNonReads; //!< Show further events in arachne xml output. int extendTrivial; //!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)