- Improved graph output for printing purposes.

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);

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;

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");
 }

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)
 {

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);