From cb315aafc8270f4386214311856b4d6ed33bbb29 Mon Sep 17 00:00:00 2001 From: ccremers Date: Fri, 12 Aug 2005 12:13:50 +0000 Subject: [PATCH] - 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 | 112 +++++++++++++++++++++++++++++++++++++++++++++++++ src/arachne.h | 4 ++ src/binding.c | 11 +++++ src/binding.h | 4 ++ src/switches.c | 15 +++++++ src/switches.h | 1 + src/xmlout.c | 40 +++++++++++++++++- 7 files changed, 186 insertions(+), 1 deletion(-) diff --git a/src/arachne.c b/src/arachne.c index 662b397..c8e7c4c 100644 --- a/src/arachne.c +++ b/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; +} diff --git a/src/arachne.h b/src/arachne.h index 3783a69..e45e2c3 100644 --- a/src/arachne.h +++ b/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 diff --git a/src/binding.c b/src/binding.c index 5f4ca74..b46da54 100644 --- a/src/binding.c +++ b/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 diff --git a/src/binding.h b/src/binding.h index f1e1a25..d031c9e 100644 --- a/src/binding.h +++ b/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 (); diff --git a/src/switches.c b/src/switches.c index d9dfb0a..7cfdd34 100644 --- a/src/switches.c +++ b/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 */ diff --git a/src/switches.h b/src/switches.h index 774626a..00d8e9c 100644 --- a/src/switches.h +++ b/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. /** diff --git a/src/xmlout.c b/src/xmlout.c index 2614902..7f3d62f 100644 --- a/src/xmlout.c +++ b/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; + } + } + } + } } } }