Changeset [81b1e221f6c39660782d9d2d785e477829371297] by Douglas Creager
February 10th, 2009 @ 07:31 PM
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...
Committed by Douglas Creager
- M cspm/src/HST/CSP0/Processes.lhs
- M cspm/src/HST/CSPM/Bind.hs
- M cspm/src/HST/CSPM/Evaluate.hs
- M cspm/src/HST/CSPM/Parser.hs
- M cspm/src/HST/CSPM/Parser.ly
- M cspm/src/HST/CSPM/Types.hs
- M cspm/tests/processes/test-rintchoice.sh
- M cspm/tests/run-tests.sh
- M doc/csp0.md
- M include/hst/csp.hh
- M include/hst/parser/scanner.hh
- M src/CMakeLists.txt
- M src/operators/extchoice.cc
- M src/operators/intchoice.cc
- M src/operators/replicated-intchoice.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/00-repl-intchoice0.csp0
- M tests/csp/00-repl-intchoice0.f-normal-output
- M tests/csp/00-repl-intchoice0.f-prenormal-output
- M tests/csp/00-repl-intchoice0.output
- M tests/csp/00-repl-intchoice0.t-normal-output
- M tests/csp/00-repl-intchoice0.t-prenormal-output
- M tests/csp/00-repl-intchoice1.csp0
- M tests/csp/00-repl-intchoice1.f-normal-output
- M tests/csp/00-repl-intchoice1.f-prenormal-output
- M tests/csp/00-repl-intchoice1.output
- M tests/csp/00-repl-intchoice1.t-normal-output
- M tests/csp/00-repl-intchoice1.t-prenormal-output
- M tests/csp/00-repl-intchoice2.csp0
- M tests/csp/00-repl-intchoice2.f-normal-output
- M tests/csp/00-repl-intchoice2.f-prenormal-output
- M tests/csp/00-repl-intchoice2.output
- M tests/csp/00-repl-intchoice2.t-normal-output
- M tests/csp/00-repl-intchoice2.t-prenormal-output
- M tests/csp/CMakeLists.txt
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.