diff --git a/src/claim.c b/src/claim.c index 29fc5f9..0932199 100644 --- a/src/claim.c +++ b/src/claim.c @@ -347,19 +347,19 @@ check_claim_nisynch (const System sys, const int i) { cl->failed = statesIncrease (cl->failed); -//#ifdef DEBUG +#ifdef DEBUG warning ("Claim has failed!"); - printf ("To be exact, claim label "); + printf ("// To be exact, claim label "); termPrint (cl->label); printf (" with prec set "); termlistPrint (cl->prec); printf ("\n"); - printf ("i: %i\nf: ",i); + printf ("// i: %i\n// f: ",i); termmapPrint (f); - printf ("\ng: "); + printf ("\n// g: "); termmapPrint (g); printf ("\n"); -//#endif +#endif } termmapDelete (f); diff --git a/src/main.c b/src/main.c index a5d58b9..daae65f 100644 --- a/src/main.c +++ b/src/main.c @@ -258,15 +258,6 @@ main (int argc, char **argv) /* handle debug level */ #ifdef DEBUG debugSet (switch_debug_level->ival[0]); - if (DEBUGL (1)) - { - /* print command line */ - int i; - printf ("$"); - for (i = 0; i < argc; i++) - printf (" %s", argv[i]); - printf ("\n"); - } #else debugSet (0); #endif @@ -283,6 +274,18 @@ main (int argc, char **argv) /* generate system */ sys = systemInit (); + + /* transfer command line */ + sys->argc = argc; + sys->argv = argv; +#ifdef DEBUG + /* print command line */ + commandlinePrint (stderr, sys); + fprintf (stderr, "\n"); +#endif + + /* handle switches */ + if (switch_implicit_choose->count > 0) /* allow implicit chooses */ sys->switchForceChoose = 0; diff --git a/src/output.c b/src/output.c index 324d263..869b499 100644 --- a/src/output.c +++ b/src/output.c @@ -507,15 +507,32 @@ void graphInit (const System sys) /* drawing state space. */ printf ("digraph Statespace {\n"); + /* label */ + printf ("\tcomment = \""); + commandlinePrint (stdout, sys); + printf ("\";\n"); + /* fit stuff onto the page */ printf ("\trankdir=LR;\n"); - printf ("\tsize=\"11,17\";\n"); + printf ("\tpage=\"8.5,11\";\n"); + printf ("\tfontsize=\"6\";\n"); + printf ("\tfontname=\"Helvetica\";\n"); + printf ("\tmargin=0.5;\n"); + printf ("\tnodesep=0.06;\n"); + printf ("\tranksep=0.01;\n"); printf ("\torientation=landscape;\n"); + printf ("\tcenter=true;\n"); + // printf ("\tlabeljust=\"r\";\n"); + printf ("\tconcentrate=true;\n"); + + /* node/edge defaults */ + printf ("\tnode [shape=\"point\",fontsize=\"4\",fontname=\"Helvetica\"];\n"); + printf ("\tedge [fontsize=\"4\",fontname=\"Helvetica\"];\n"); /* start with initial node 0 */ printf ("\tn"); statesFormat (stdout, STATES0); - printf (" [shape=box,label=\"M0: "); + printf (" [shape=box,height=0.2,label=\"M0: "); tl = knowledgeSet (sys->know); termlistPrint (tl); termlistDelete (tl); @@ -544,13 +561,13 @@ void graphNode (const System sys) /* add node */ printf ("\tn"); statesFormat (stdout, thisNode); - printf (" [shape="); + printf (" ["); newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]); if (newtl != NULL) { /* knowledge added */ - printf ("box,label=\"M + "); + printf ("shape=box,height=0.2,label=\"M + "); termlistPrint (newtl); termlistDelete (newtl); printf ("\""); @@ -558,7 +575,7 @@ void graphNode (const System sys) else { /* no added knowledge */ - printf ("point,label=\"\""); + printf ("label=\"\""); } printf ("];\n"); @@ -626,7 +643,7 @@ void graphEdgePath (const System sys, const int length, const char* edgepar) /* color edge */ printf ("\tn"); statesFormat (stdout, prevNode); - printf (" -> "); + printf (" -> n"); statesFormat (stdout, thisNode); printf (" [%s];\n", edgepar); prevNode = thisNode; @@ -636,6 +653,6 @@ void graphEdgePath (const System sys, const int length, const char* edgepar) void graphPath (const System sys, int length) { - graphNodePath (sys,length,"shape=parallelogram,style=bold,color=red"); + graphNodePath (sys,length,"style=bold,color=red"); graphEdgePath (sys,length-1,"style=bold,color=red"); } diff --git a/src/system.c b/src/system.c index bd00c87..80bf1e7 100644 --- a/src/system.c +++ b/src/system.c @@ -823,6 +823,17 @@ int attackLength(struct tracebuf* tb) return len; } +void +commandlinePrint (FILE *stream, const System sys) +{ + /* print command line */ + int i; + + fprintf (stream, "$"); + for (i = 0; i < sys->argc; i++) + fprintf (stream, " %s", sys->argv[i]); +} + //! Get the number of roles in the system. int compute_rolecount (const System sys) { diff --git a/src/system.h b/src/system.h index 0e48989..7d87fbb 100644 --- a/src/system.h +++ b/src/system.h @@ -171,6 +171,10 @@ struct system //! Shortest attack storage. struct tracebuf* attack; + + //! Command line arguments + int argc; + char **argv; }; typedef struct system *System; @@ -203,6 +207,7 @@ int getMaxTraceLength (const System sys); void agentsOfRunPrint (const System sys, const int run); void violatedClaimPrint (const System sys, int i); int attackLength(struct tracebuf* tb); +void commandlinePrint (FILE *stream, const System sys); int compute_rolecount (const System sys); int compute_roleeventmax (const System sys);