Changeset [272fa182e899bc777bf57e13e9c53257c549f608] by Douglas Creager

May 24th, 2008 @ 06:05 PM

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...

Committed by Douglas Creager

  • A src/operators/replicated-extchoice.cc
  • A tests/csp/00-repl-extchoice0.csp0
  • A tests/csp/00-repl-extchoice0.f-normal-output
  • A tests/csp/00-repl-extchoice0.f-prenormal-output
  • A tests/csp/00-repl-extchoice0.output
  • A tests/csp/00-repl-extchoice0.t-normal-output
  • A tests/csp/00-repl-extchoice0.t-prenormal-output
  • A tests/csp/00-repl-extchoice1.csp0
  • A tests/csp/00-repl-extchoice1.f-normal-output
  • A tests/csp/00-repl-extchoice1.f-prenormal-output
  • A tests/csp/00-repl-extchoice1.output
  • A tests/csp/00-repl-extchoice1.t-normal-output
  • A tests/csp/00-repl-extchoice1.t-prenormal-output
  • A tests/csp/00-repl-extchoice2.csp0
  • A tests/csp/00-repl-extchoice2.f-normal-output
  • A tests/csp/00-repl-extchoice2.f-prenormal-output
  • A tests/csp/00-repl-extchoice2.output
  • A tests/csp/00-repl-extchoice2.t-normal-output
  • A tests/csp/00-repl-extchoice2.t-prenormal-output
  • A tests/csp/00-repl-extchoice3.csp0
  • A tests/csp/00-repl-extchoice3.f-normal-output
  • A tests/csp/00-repl-extchoice3.f-prenormal-output
  • A tests/csp/00-repl-extchoice3.output
  • A tests/csp/00-repl-extchoice3.t-normal-output
  • A tests/csp/00-repl-extchoice3.t-prenormal-output
  • A tests/csp/00-repl-extchoice4.csp0
  • A tests/csp/00-repl-extchoice4.f-normal-output
  • A tests/csp/00-repl-extchoice4.f-prenormal-output
  • A tests/csp/00-repl-extchoice4.output
  • A tests/csp/00-repl-extchoice4.t-normal-output
  • A tests/csp/00-repl-extchoice4.t-prenormal-output
  • M doc/csp0.txt
  • M include/hst/csp.hh
  • M include/hst/lts.hh
  • M include/hst/parser/scanner.hh
  • M src/CMakeLists.txt
  • M src/operators/extchoice.cc
  • M src/parser/csp0.yy
  • M src/parser/eventmap.yy
  • M src/parser/intset.yy
  • M src/parser/intsetset.yy
  • M src/parser/lts.yy
  • M src/parser/scanner.cc
  • M tests/csp/CMakeLists.txt
New-ticket 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.