prioritise operator takes a process and prunes low priority arcs from each state where a higher priority arc also exists.
always takes priority over everything. Events not defined to be part
of the priority ordering are never pruned.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
FDR implements some transformations on CSP processes which do not
preserve the semantics of the original process. These are brought into
scope by the external declaration.
| 5.2.1 Chase | ||
| 5.2.2 Prioritise |
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The external operator chase produces a determinised version of
a process by arbitrarily choosing a single tau arc in every unstable
state of the process. This can be very useful in eliminating unwanted
spurious non-determinism but, since the resultant process differs
semantically from the input, it must be used with care.
More details can be found in [Roscoe97].
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The prioritise operator takes a process and prunes low priority arcs from each state where a higher priority arc also exists.
always takes priority over everything. Events not defined to be part
of the priority ordering are never pruned.
The arguments to the operator consist of the process to be
prioritised, followed by a series of sets of events, with the events
in each set taking priority over all subsequent ones but being
equivalent to each other. The first set implicitly includes
.
Given the example
P = a -> STOP [] b -> STOP
Q = prioritise(P, {}, {a}, {b})
|
Q will be equivalent to a -> STOP because the event a will
take priority over b.
Only sbsism and wbsisim will preserve the semantics of
prioritise(P) when used inside P. The prioritise
operator will either produce potentially incorrect results or fail
altogether if any of the other compressions are used.
The prioritise operator can also be invoked with two arguments:
the process to be transformed and a sequence of sets of events:
Q = prioritise(P, <{}, {a}, {b}>)
|
This permits the arguments to be constructed programmatically within a CSPMscript.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] |
This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.