diff --git a/src/arachne.c b/src/arachne.c
index 0eed07b..e0ed4c3 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2364,6 +2364,10 @@ arachneClaim (Claimlist cl)
}
}
claimStatusReport (sys, cl);
+ if (switches.xml)
+ {
+ xmlOutClaim (sys, cl);
+ }
return true;
}
else
diff --git a/src/claim.c b/src/claim.c
index bc9dd88..e511a7a 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -1064,6 +1064,7 @@ claimStatusReport (const System sys, Claimlist cl)
{
globalError--;
}
+
return true;
}
}
diff --git a/src/switches.c b/src/switches.c
index 7ade2ea..2a3613c 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -70,7 +70,8 @@ switchesInit (int argc, char **argv)
switches.output = SUMMARY; // default is to show a summary
switches.report = 0;
switches.reportClaims = 0; // default don't report on claims
- switches.xml = 0; // default no xml output (dot)
+ switches.xml = false; // default no xml output
+ switches.dot = false; // default no dot output
switches.human = false; // not human friendly by default
switches.reportMemory = 0;
switches.reportTime = 0;
@@ -435,7 +436,7 @@ switcher (const int process, int index, int commandline)
else
{
switches.output = ATTACK;
- switches.xml = 0;
+ switches.dot = true;
return index;
}
}
@@ -449,7 +450,7 @@ switcher (const int process, int index, int commandline)
else
{
switches.output = ATTACK;
- switches.xml = 1;
+ switches.xml = true;
return index;
}
}
diff --git a/src/switches.h b/src/switches.h
index 4f280df..9c8f600 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -49,6 +49,7 @@ struct switchdata
int report;
int reportClaims; //!< Enable claims report
int xml; //!< xml output
+ int dot; //!< dot output
int human; //!< human readable
int reportMemory; //!< Memory display switch.
int reportTime; //!< Time display switch.
diff --git a/src/xmlout.c b/src/xmlout.c
index 78ecade..414cb7b 100644
--- a/src/xmlout.c
+++ b/src/xmlout.c
@@ -19,6 +19,8 @@
#include "arachne.h" // for get_semitrace_length
#include "switches.h"
#include "specialterm.h"
+#include "claim.h"
+#include "dotout.h"
#include "xmlout.h"
@@ -98,6 +100,16 @@ xmlOutInteger (const char *tag, const int value)
xmlPrint ("<%s>%i%s>", tag, value, tag);
}
+//! Print a state counter element
+void
+xmlOutStates (const char *tag, states_t value)
+{
+ xmlIndentPrint ();
+ eprintf ("<%s>", tag);
+ statesFormat (value);
+ eprintf ("%s>\n", tag);
+}
+
//! Print a string
void
xmlOutString (const char *tag, const char *s)
@@ -960,9 +972,55 @@ xmlOutSemitrace (const System sys)
xmlOutRuns (sys);
xmlindent--;
xmlPrint ("");
+
+ if (switches.dot)
+ {
+ // dot encapsulated in XML
+ xmlPrint ("");
+ dotSemiState (sys);
+ xmlPrint ("");
+ }
+
xmlindent--;
xmlPrint ("");
/* restore only claim buffer */
only_claim_label = buffer_only_claim_label;
}
+
+//! Output for a claim
+void
+xmlOutClaim (const System sys, Claimlist cl)
+{
+ Protocol p;
+
+ p = (Protocol) cl->protocol;
+
+ xmlPrint ("");
+ xmlindent++;
+ xmlOutTerm ("claim", cl->type);
+ xmlOutTerm ("label", cl->label);
+ xmlOutTerm ("protocol", p->nameterm);
+ xmlOutTerm ("role", cl->rolename);
+ xmlOutTerm ("parameter", cl->parameter);
+
+ if (!isTermEqual (cl->type, CLAIM_Empty))
+ {
+
+ // something to say about it
+ xmlOutStates ("failed", cl->failed);
+ xmlOutStates ("count", cl->count);
+ xmlOutStates ("states", cl->states);
+ if (cl->complete)
+ {
+ xmlPrint ("");
+ }
+ if (cl->timebound)
+ {
+ xmlPrint ("");
+ }
+ }
+
+ xmlindent--;
+ xmlPrint ("");
+}
diff --git a/src/xmlout.h b/src/xmlout.h
index 3595237..e20cfac 100644
--- a/src/xmlout.h
+++ b/src/xmlout.h
@@ -2,11 +2,13 @@
#define XMLOUT
#include "system.h"
+#include "claim.h"
void xmlOutInit (void);
void xmlOutDone (void);
void xmlOutSemitrace (const System sys);
void xmlOutTrace (const System sys);
+void xmlOutClaim (const System sys, Claimlist cl);
#endif