-
A Trace of a process is a log/record of the events/actions it has
undertaken (tape recording).
-
A Specification is a predicate (some expression in terms of variables
in the trace) that we would like to be true about a process.
-
A trace can go on for ever (e.g. trace of the GAME process).
-
Traces are written #tex2html_wrap_inline4080#
-
;SPM_lt;;SPM_gt; is the empty trace.
-
A trace of CLEVERGAME might be:
;SPM_lt;InCoin,OutCome, InCoinLarge,OutCome,OutCome;SPM_gt;
Operations on traces include:
-
Catenation: s #tex2html_wrap_inline4086# t
Simply appends trace t to trace s.
-
Note: f(s #tex2html_wrap_inline4088# t) is f(s) #tex2html_wrap_inline4090# f(t)
(for classes of
functions which map sequences of events to sequences of events).
-
Restriction:
s A
All the symbols not in alphabet A are removed from the trace s.
-
Most important is Ordering:
If s is a copy of an initial subsequence of t, it is possible to find
an extension u of s, s.t. s #tex2html_wrap_inline4092# u = t. Thus we can define an ordering,
in some sense #tex2html_wrap_inline4094#.
-
Other useful operations include
#tex2html_wrap_inline4096# , the head of a trace,
#tex2html_wrap_inline4098# , the tail of a trace, and
#tex2html_wrap_inline4100#, the length of a trace.