- Improved output significantly.
This commit is contained in:
parent
5ff71fa661
commit
397298290b
42
src/main.c
42
src/main.c
@ -385,7 +385,7 @@ timersPrint (const System sys)
|
|||||||
/* modern version: claim label is tuple (protocname, label) */
|
/* modern version: claim label is tuple (protocname, label) */
|
||||||
/* first print protocol.role */
|
/* first print protocol.role */
|
||||||
termPrint (TermOp1 (cl_scan->label));
|
termPrint (TermOp1 (cl_scan->label));
|
||||||
eprintf ("\t");
|
eprintf (",");
|
||||||
termPrint (cl_scan->rolename);
|
termPrint (cl_scan->rolename);
|
||||||
eprintf ("\t");
|
eprintf ("\t");
|
||||||
/* second print event_label */
|
/* second print event_label */
|
||||||
@ -404,36 +404,44 @@ timersPrint (const System sys)
|
|||||||
termPrint (cl_scan->label);
|
termPrint (cl_scan->label);
|
||||||
eprintf (")\t");
|
eprintf (")\t");
|
||||||
}
|
}
|
||||||
/* print counts etc. */
|
|
||||||
eprintf ("found:\t");
|
/* now report the status */
|
||||||
statesFormat (cl_scan->count);
|
eprintf ("attacks: ");
|
||||||
if (cl_scan->count > 0)
|
if (cl_scan->count > 0 && cl_scan->failed > 0)
|
||||||
{
|
{
|
||||||
if (cl_scan->failed > 0)
|
/* there is an attack */
|
||||||
{
|
eprintf ("yes\t(at least %i)", cl_scan->failed);
|
||||||
eprintf ("\t");
|
|
||||||
eprintf ("failed:\t");
|
|
||||||
statesFormat (cl_scan->failed);
|
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
eprintf ("\tcorrect: ");
|
/* no attack */
|
||||||
|
eprintf ("no\t");
|
||||||
|
|
||||||
|
/* subcases */
|
||||||
|
if (cl_scan->count == 0)
|
||||||
|
{
|
||||||
|
/* not encountered */
|
||||||
|
eprintf ("(does not occur)");
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
/* does occur */
|
||||||
if (cl_scan->complete)
|
if (cl_scan->complete)
|
||||||
{
|
{
|
||||||
eprintf ("complete_proof");
|
/* complete proof */
|
||||||
|
eprintf ("(proof of correctness)");
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
eprintf ("bounded_proof");
|
/* only due to bounds */
|
||||||
|
eprintf ("(no attack within bounds)");
|
||||||
if (cl_scan->timebound)
|
if (cl_scan->timebound)
|
||||||
eprintf ("\ttime=%i", get_time_limit ());
|
eprintf ("\ttime=%i", get_time_limit ());
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else
|
|
||||||
{
|
/* proceed to next claim */
|
||||||
eprintf ("\tcorrect: does_not_occur");
|
|
||||||
}
|
|
||||||
eprintf ("\n");
|
eprintf ("\n");
|
||||||
}
|
}
|
||||||
cl_scan = cl_scan->next;
|
cl_scan = cl_scan->next;
|
||||||
|
@ -274,7 +274,7 @@ switcher (const int process, int index)
|
|||||||
/* ==================
|
/* ==================
|
||||||
* Generic options
|
* Generic options
|
||||||
*/
|
*/
|
||||||
if (detect ('a', "arachne", 0))
|
if (detect ('A', "arachne", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
@ -337,11 +337,11 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('P', "proof", 0))
|
if (detect ('p', "proof", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
helptext ("-P,--proof", "show explicit proof");
|
helptext ("-p,--proof", "show explicit proof");
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
@ -351,6 +351,33 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
if (detect ('c', "class", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
helptext ("-c,--class",
|
||||||
|
"generate full class (show uninstantiated variables)");
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.concrete = false;
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if (detect (' ', "concrete", 0))
|
||||||
|
{
|
||||||
|
if (!process)
|
||||||
|
{
|
||||||
|
/* this is now the default */
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
switches.concrete = true;
|
||||||
|
return index;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/* ==================
|
/* ==================
|
||||||
* Bounding options
|
* Bounding options
|
||||||
*/
|
*/
|
||||||
@ -426,11 +453,11 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('A', "all-attacks", 0))
|
if (detect ('a', "all-attacks", 0))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
helptext ("-A,--all-attacks",
|
helptext ("-a,--all-attacks",
|
||||||
"generate all attacks instead of just one");
|
"generate all attacks instead of just one");
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
@ -455,12 +482,12 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('p', "prune", 1))
|
if (detect ('P', "prune", 1))
|
||||||
{
|
{
|
||||||
if (!process)
|
if (!process)
|
||||||
{
|
{
|
||||||
/* not very important
|
/* not very important
|
||||||
helptext ("-p,--prune=<int>", "pruning method when an attack is found [2]");
|
helptext ("-P,--prune=<int>", "pruning method when an attack is found [2]");
|
||||||
*/
|
*/
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
@ -692,33 +719,6 @@ switcher (const int process, int index)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
if (detect ('C', "class", 0))
|
|
||||||
{
|
|
||||||
if (!process)
|
|
||||||
{
|
|
||||||
helptext ("-C,--class",
|
|
||||||
"generate full class (show uninstantiated variables)");
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
switches.concrete = false;
|
|
||||||
return index;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (detect (' ', "concrete", 0))
|
|
||||||
{
|
|
||||||
if (!process)
|
|
||||||
{
|
|
||||||
/* this is now the default */
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
switches.concrete = true;
|
|
||||||
return index;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#ifdef DEBUG
|
#ifdef DEBUG
|
||||||
/* ==================
|
/* ==================
|
||||||
* Experimental options
|
* Experimental options
|
||||||
|
Loading…
Reference in New Issue
Block a user