diff --git a/src/main.c b/src/main.c index 40637e0..1629292 100644 --- a/src/main.c +++ b/src/main.c @@ -385,7 +385,7 @@ timersPrint (const System sys) /* modern version: claim label is tuple (protocname, label) */ /* first print protocol.role */ termPrint (TermOp1 (cl_scan->label)); - eprintf ("\t"); + eprintf (","); termPrint (cl_scan->rolename); eprintf ("\t"); /* second print event_label */ @@ -404,36 +404,44 @@ timersPrint (const System sys) termPrint (cl_scan->label); eprintf (")\t"); } - /* print counts etc. */ - eprintf ("found:\t"); - statesFormat (cl_scan->count); - if (cl_scan->count > 0) + + /* now report the status */ + eprintf ("attacks: "); + 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); + } + else + { + /* no attack */ + eprintf ("no\t"); + + /* subcases */ + if (cl_scan->count == 0) { - eprintf ("\t"); - eprintf ("failed:\t"); - statesFormat (cl_scan->failed); + /* not encountered */ + eprintf ("(does not occur)"); } else { - eprintf ("\tcorrect: "); + /* does occur */ if (cl_scan->complete) { - eprintf ("complete_proof"); + /* complete proof */ + eprintf ("(proof of correctness)"); } else { - eprintf ("bounded_proof"); + /* only due to bounds */ + eprintf ("(no attack within bounds)"); if (cl_scan->timebound) eprintf ("\ttime=%i", get_time_limit ()); } } } - else - { - eprintf ("\tcorrect: does_not_occur"); - } + + /* proceed to next claim */ eprintf ("\n"); } cl_scan = cl_scan->next; diff --git a/src/switches.c b/src/switches.c index b9858f9..258cb41 100644 --- a/src/switches.c +++ b/src/switches.c @@ -274,7 +274,7 @@ switcher (const int process, int index) /* ================== * Generic options */ - if (detect ('a', "arachne", 0)) + if (detect ('A', "arachne", 0)) { if (!process) { @@ -337,11 +337,11 @@ switcher (const int process, int index) } } - if (detect ('P', "proof", 0)) + if (detect ('p', "proof", 0)) { if (!process) { - helptext ("-P,--proof", "show explicit proof"); + helptext ("-p,--proof", "show explicit proof"); } 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 */ @@ -426,11 +453,11 @@ switcher (const int process, int index) } } - if (detect ('A', "all-attacks", 0)) + if (detect ('a', "all-attacks", 0)) { if (!process) { - helptext ("-A,--all-attacks", + helptext ("-a,--all-attacks", "generate all attacks instead of just one"); } else @@ -455,12 +482,12 @@ switcher (const int process, int index) } } - if (detect ('p', "prune", 1)) + if (detect ('P', "prune", 1)) { if (!process) { /* not very important - helptext ("-p,--prune=", "pruning method when an attack is found [2]"); + helptext ("-P,--prune=", "pruning method when an attack is found [2]"); */ } 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 /* ================== * Experimental options