Need replicated version of several operators
Reported by Douglas Creager | May 27th, 2008 @ 09:49 PM
CSPM includes replicated versions of several operators. For instance, instead of
P □ Q □ R □ S
you can do
□ {P,Q,R,S}
It would be nice for CSP₀ to have these operators as well. This is partly for convenience, but also partly for efficiency; the resulting LTS will be identical, but we should not need to create temporary processes (which just take up space and are never used) when constructing the LTS for the replicated version. This will (hopefully) be especially apparent with replicated versions of the parallel composition operators.
Comments and changes to this ticket
-
Douglas Creager May 24th, 2008 @ 06:09 PM
(from [272fa182e899bc777bf57e13e9c53257c549f608]) Replicated external choice
This patch introduces the “replicated external choice” operator. This
has the same semantics as the standard external choice, but it works
on a set containing any number of processes. (The standard external
choice operator takes exactly two operands.) The replicated version
is well-defined since the binary version is associative; this means
that it doesn't matter which order we apply the binary version to the
elements of the set. Since the unit of binary external choice is
STOP, we also get STOP if we apply the replicated version to the empty
set.
Lighthouse: [#8]
-
Douglas Creager May 24th, 2008 @ 06:10 PM
- State changed from “new” to “open”
-
Douglas Creager February 11th, 2009 @ 12:37 AM
- Tag set to “csp0, operators”
(from [81b1e221f6c39660782d9d2d785e477829371297]) Replicated internal choice
This patch introduces the “replicated internal choice” operator. This has the same semantics as the standard internal choice, but it works on a set containing any number of processes. (The standard internal choice operator takes exactly two operands.) The replicated version is well-defined since the binary version is associative. Unlike replicated external choice, the replicated internal choice of the empty set is not well-defined. Thus, the following is treated as a syntax error in CSP₀:
rintchoice P = |~| {};
Lighthouse: [#8] http://github.com/hst/hst/commit...
Please Sign in or create a free account to add a new ticket.
With your very own profile, you can contribute to projects, track your activity, watch tickets, receive and update tickets through your email and much more.
Create new ticket
Create your profile
Help contribute to this project by taking a few moments to create your personal profile. Create your profile »
An open-source refinement checker for the CSP process algebra.
People watching this ticket
Douglas Creager
Referenced by
-
8
Need replicated version of several operators
Lighthouse: [#8]
http://github.com/hst/hst/commit...