Lighthouse has a new layout. Prefer the old one? Return to the old layout, and switch back any time from the link at the top of each page.

Need replicated version of several operators

#8

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.

Reported by Douglas Creager · May 27th, 2008 @ 09:49 PM

State: open
Milestone: none
Assigned to: Douglas Creager Douglas Creager

Activity

  1. Douglas Creager
    Douglas Creager

    (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]

    http://github.com/dcreager/hst/c...

    May 24th, 2008 @ 06:09 PM

  2. Douglas Creager
    Douglas Creager
    • State changed from new to open

    May 24th, 2008 @ 06:10 PM

  3. Douglas Creager
    Douglas Creager
    • 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 Need replicated version of several operators] http://github.com/hst/hst/commit...

    February 11th, 2009 @ 12:37 AM

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.