- Added '--extend-trivial' switch. This is not a complete '--extend'

algorithm, as it is pretty dumb, but it works in most cases. Use with
  care.

src/arachne.c

@@ -3484,3 +3484,115 @@ arachne ()
       cl = cl->next;
     }
 }
+
+//! Construct knowledge set at some event, based on a semitrace.
+/**
+ * This is a very 'stupid' algorithm; it is just there because GijsH
+ * requested it. It does in no way guarantee that this is the actual
+ * knowledge set at the given point. It simply gives an underapproximation,
+ * that will be correct in most cases. The main reason for this is that it
+ * completely ignores any information on unbound variables, and regards them
+ * as bound constants.
+ *
+ * Because everything is supposed to be bound, we conclude that even 'read'
+ * events imply a certain knowledge.
+ *
+ * If aftercomplete is 0 or false, we actually check the ordering; otherwise we
+ * just assume the trace has finished.
+ *
+ * Use knowledgeDelete later to clean up.
+ */
+Knowledge
+knowledgeAtArachne (const System sys, const int myrun, const int myindex,
+		    const int aftercomplete)
+{
+  Knowledge know;
+  int run;
+
+  goal_graph_create ();		// ensure a valid ordering graph
+  know = knowledgeDuplicate (sys->know);	// duplicate initial knowledge
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      int index;
+      int maxstep;
+      Roledef rd;
+
+      index = 0;
+      rd = sys->runs[run].start;
+      maxstep = sys->runs[run].step;
+      if (run == myrun && myindex > maxstep)
+	{
+	  // local run index can override real step
+	  maxstep = myindex;
+	}
+
+      while (rd != NULL && index < maxstep)
+	{
+	  // Check whether this event precedes myevent
+	  if (aftercomplete || isOrderedBefore (run, index, myrun, myindex))
+	    {
+	      // If it is a send (trivial) or a read (remarkable, but true
+	      // because of bindings) we can add the message and the agents to
+	      // the knowledge.
+	      if (rd->type == SEND || rd->type == READ)
+		{
+		  knowledgeAddTerm (know, rd->message);
+		  if (rd->from != NULL)
+		    knowledgeAddTerm (know, rd->from);
+		  if (rd->to != NULL)
+		    knowledgeAddTerm (know, rd->to);
+		}
+	      index++;
+	      rd = rd->next;
+	    }
+	  else
+	    {
+	      // Not ordered before anymore, so we skip to the next run.
+	      rd = NULL;
+	    }
+	}
+      run++;
+    }
+  return know;
+}
+
+//! Determine whether a term is trivially known at some event in a partially ordered structure.
+/**
+ * Important: read disclaimer at knowledgeAtArachne()
+ *
+ * Returns true iff the term is certainly known at that point in the
+ * semitrace.
+ */
+int
+isTriviallyKnownAtArachne (const System sys, const Term t, const int run,
+			   const int index)
+{
+  int result;
+  Knowledge knowset;
+
+  knowset = knowledgeAtArachne (sys, run, index, false);
+  result = inKnowledge (knowset, t);
+  knowledgeDelete (knowset);
+  return result;
+}
+
+//! Determine whether a term is trivially known after execution of some partially ordered structure.
+/**
+ * Important: read disclaimer at knowledgeAtArachne()
+ *
+ * Returns true iff the term is certainly known after all events in the
+ * semitrace.
+ */
+int
+isTriviallyKnownAfterArachne (const System sys, const Term t, const int run,
+			      const int index)
+{
+  int result;
+  Knowledge knowset;
+
+  knowset = knowledgeAtArachne (sys, run, index, true);
+  result = inKnowledge (knowset, t);
+  knowledgeDelete (knowset);
+  return result;
+}

src/arachne.h

@@ -8,5 +8,9 @@ void arachneDone ();
 int arachne ();
 int get_semitrace_length ();
 void indentPrint ();
+int isTriviallyKnownAtArachne (const System sys, const Term t, const int run,
+			       const int index);
+int isTriviallyKnownAfterArachne (const System sys, const Term t,
+				  const int run, const int index);
 
 #endif

src/binding.c

@@ -66,6 +66,17 @@ binding_destroy (Binding b)
   memFree (b, sizeof (struct binding));
 }
 
+//! Test whether one event is ordered before another
+/**
+ * Is only guaranteed to yield trustworthy results after a new graph is created, using
+ * goal_graph_create ()
+ */
+int
+isOrderedBefore (const int run1, const int ev1, const int run2, const int ev2)
+{
+  return graph[graph_nodes (nodes, run2, ev2, run2, ev2)];
+}
+
 /*
  *
  * Main

src/binding.h

@@ -36,6 +36,10 @@ int node_count ();
 int node_number (int run, int ev);
 __inline__ int graph_nodes (const int nodes, const int run1, const int ev1,
 			    const int run2, const int ev2);
+
+int isOrderedBefore (const int run1, const int ev1, const int run2,
+		     const int ev2);
+
 void goal_graph_create ();
 
 

src/switches.c

@@ -78,6 +78,7 @@ switchesInit (int argc, char **argv)
   switches.reportTime = 0;
   switches.reportStates = 0;
   switches.extendNonReads = 0;	// default off
+  switches.extendTrivial = 0;	// default off
 
   // Obsolete
   switches.latex = 0;		// latex output?
@@ -481,6 +482,20 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "extend-trivial", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   */
+	}
+      else
+	{
+	  switches.extendTrivial = 1;
+	  return index;
+	}
+    }
+
   /* ==================
    *  External options
    */

src/switches.h

@@ -57,6 +57,7 @@ struct switchdata
   int reportTime;		//!< Time display switch.
   int reportStates;		//!< Progress display switch. (traversed states)
   int extendNonReads;		//!< Show further events in arachne xml output.
+  int extendTrivial;		//!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
 
   //! Latex output switch.
   /**

src/xmlout.c

@@ -872,12 +872,50 @@ xmlOutRuns (const System sys)
 		}
 	      else
 		{
-		  if (switches.extendNonReads)
+		  if (switches.extendTrivial || switches.extendNonReads)
 		    {
 		      if (rd->type != READ)
 			{
 			  return true;
 			}
+		      else
+			{
+			  if (switches.extendTrivial)
+			    {
+			      /* This is a read, and we don't know whether to
+			       * include it. Default behaviour would be to jump
+			       * out of the conditions, and return false.
+			       * Instead, we check whether it can be trivially
+			       * satisfied by the knowledge from the preceding
+			       * events.
+			       */
+			      if (isTriviallyKnownAtArachne (sys,
+							     rd->message,
+							     run, index))
+				{
+				  return true;
+				}
+			      else
+				{
+				  /* We cannot extend it trivially, based on
+				   * the preceding events, but maybe we can
+				   * base it on another (*all*) event. That
+				   * would in fact introduce another implicit
+				   * binding. Currently, we do not explicitly
+				   * introduce this binding, but just allow
+				   * displaying the event.
+				   *
+				   * TODO consider what it means to leave out
+				   * this binding.
+				   */
+				  if (isTriviallyKnownAfterArachne
+				      (sys, rd->message, run, index))
+				    {
+				      return true;
+				    }
+				}
+			    }
+			}
 		    }
 		}
 	    }