Changeset: Changeset [b692420844370837a19641f3b29f71bad483b21a] by Douglas Creager - hst

List changesets

Changeset [b692420844370837a19641f3b29f71bad483b21a] by Douglas Creager

April 28th, 2008 @ 12:32 PM

Adding acceptance sets for LTSs

This patch adds support for acceptance sets in an LTS. Each stable

node in an LTS (i.e., those with no outgoing τ edges) now has an

acceptance set, which is the complement of the refusal set more often

seen in the literature. If a state has some acceptance set that does

not contain event ‘a’, then there is some situation in which the state

can refuse to perform ‘a’. These acceptance sets are needed to

implement the failures and failures-divergences semantic models in

CSP.

In this patch, LTSs can now store acceptance information. As with LTS

edges, acceptances can only be added to a state that has not yet been

finalized. The CSP operators add acceptances to the underlying LTS.

However, the normalization and refinement checking code does not yet

do anything with this information.

Lighthouse: [#3]

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

Committed by Douglas Creager

A tests/csp/00-hide4.normal-output
A tests/csp/00-hide4.output
A tests/csp/00-hide4.prenormal-output
M include/hst/csp.hh
M include/hst/lts.hh
M include/hst/types.hh
M src/csp-basic.cc
M src/lts.cc
M src/normalization/normalized-lts.cc
M src/operators/extchoice.cc
M src/operators/hide.cc
M src/operators/intchoice.cc
M src/operators/interface-parallel.cc
M src/operators/interleave.cc
M src/operators/prefix.cc
M src/operators/rename.cc
M src/operators/seqcomp.cc
M src/operators/timeout.cc
M tests/csp/00-aparallel1.normal-output
M tests/csp/00-aparallel1.output
M tests/csp/00-aparallel1.prenormal-output
M tests/csp/00-aparallel2.normal-output
M tests/csp/00-aparallel2.output
M tests/csp/00-aparallel2.prenormal-output
M tests/csp/00-aparallel3.normal-output
M tests/csp/00-aparallel3.output
M tests/csp/00-aparallel3.prenormal-output
M tests/csp/00-extchoice1.normal-output
M tests/csp/00-extchoice1.output
M tests/csp/00-extchoice1.prenormal-output
M tests/csp/00-extchoice2.normal-output
M tests/csp/00-extchoice2.output
M tests/csp/00-extchoice2.prenormal-output
M tests/csp/00-extchoice3.normal-output
M tests/csp/00-extchoice3.output
M tests/csp/00-extchoice3.prenormal-output
M tests/csp/00-extchoice4.normal-output
M tests/csp/00-extchoice4.output
M tests/csp/00-extchoice4.prenormal-output
M tests/csp/00-hide1.normal-output
M tests/csp/00-hide1.output
M tests/csp/00-hide1.prenormal-output
M tests/csp/00-hide2.normal-output
M tests/csp/00-hide2.output
M tests/csp/00-hide2.prenormal-output
M tests/csp/00-hide3.normal-output
M tests/csp/00-hide3.output
M tests/csp/00-hide3.prenormal-output
M tests/csp/00-intchoice1.normal-output
M tests/csp/00-intchoice1.output
M tests/csp/00-intchoice1.prenormal-output
M tests/csp/00-intchoice2.normal-output
M tests/csp/00-intchoice2.output
M tests/csp/00-intchoice2.prenormal-output
M tests/csp/00-interleave1.normal-output
M tests/csp/00-interleave1.output
M tests/csp/00-interleave1.prenormal-output
M tests/csp/00-interleave2.normal-output
M tests/csp/00-interleave2.output
M tests/csp/00-interleave2.prenormal-output
M tests/csp/00-interleave3.normal-output
M tests/csp/00-interleave3.output
M tests/csp/00-interleave3.prenormal-output
M tests/csp/00-interleave4.normal-output
M tests/csp/00-interleave4.output
M tests/csp/00-interleave4.prenormal-output
M tests/csp/00-interleave5.normal-output
M tests/csp/00-interleave5.output
M tests/csp/00-interleave5.prenormal-output
M tests/csp/00-iparallel1.normal-output
M tests/csp/00-iparallel1.output
M tests/csp/00-iparallel1.prenormal-output
M tests/csp/00-iparallel2.normal-output
M tests/csp/00-iparallel2.output
M tests/csp/00-iparallel2.prenormal-output
M tests/csp/00-iparallel3.normal-output
M tests/csp/00-iparallel3.output
M tests/csp/00-iparallel3.prenormal-output
M tests/csp/00-iparallel4.normal-output
M tests/csp/00-iparallel4.output
M tests/csp/00-iparallel4.prenormal-output
M tests/csp/00-prefix.normal-output
M tests/csp/00-prefix.output
M tests/csp/00-prefix.prenormal-output
M tests/csp/00-rename1.normal-output
M tests/csp/00-rename1.output
M tests/csp/00-rename1.prenormal-output
M tests/csp/00-rename2.normal-output
M tests/csp/00-rename2.output
M tests/csp/00-rename2.prenormal-output
M tests/csp/00-rename3.normal-output
M tests/csp/00-rename3.output
M tests/csp/00-rename3.prenormal-output
M tests/csp/00-seqcomp1.normal-output
M tests/csp/00-seqcomp1.output
M tests/csp/00-seqcomp1.prenormal-output
M tests/csp/00-seqcomp2.normal-output
M tests/csp/00-seqcomp2.output
M tests/csp/00-seqcomp2.prenormal-output
M tests/csp/00-timeout1.normal-output
M tests/csp/00-timeout1.output
M tests/csp/00-timeout1.prenormal-output
M tests/csp/00-timeout2.normal-output
M tests/csp/00-timeout2.output
M tests/csp/00-timeout2.prenormal-output
M tests/csp/02-mem-aparallel1.normal-output
M tests/csp/02-mem-aparallel1.output
M tests/csp/02-mem-aparallel1.prenormal-output
M tests/csp/02-mem-extchoice1.normal-output
M tests/csp/02-mem-extchoice1.output
M tests/csp/02-mem-extchoice1.prenormal-output
M tests/csp/02-mem-hide1.normal-output
M tests/csp/02-mem-hide1.output
M tests/csp/02-mem-hide1.prenormal-output
M tests/csp/02-mem-intchoice1.normal-output
M tests/csp/02-mem-intchoice1.output
M tests/csp/02-mem-intchoice1.prenormal-output
M tests/csp/02-mem-interleave1.normal-output
M tests/csp/02-mem-interleave1.output
M tests/csp/02-mem-interleave1.prenormal-output
M tests/csp/02-mem-iparallel1.normal-output
M tests/csp/02-mem-iparallel1.output
M tests/csp/02-mem-iparallel1.prenormal-output
M tests/csp/02-mem-prefix1.normal-output
M tests/csp/02-mem-prefix1.output
M tests/csp/02-mem-prefix1.prenormal-output
M tests/csp/02-mem-rename1.normal-output
M tests/csp/02-mem-rename1.output
M tests/csp/02-mem-rename1.prenormal-output
M tests/csp/02-mem-seqcomp1.normal-output
M tests/csp/02-mem-seqcomp1.output
M tests/csp/02-mem-seqcomp1.prenormal-output
M tests/csp/02-mem-timeout1.normal-output
M tests/csp/02-mem-timeout1.output
M tests/csp/02-mem-timeout1.prenormal-output
M tests/csp/05-rec-aparallel1.normal-output
M tests/csp/05-rec-aparallel1.output
M tests/csp/05-rec-aparallel1.prenormal-output
M tests/csp/05-rec-extchoice1.normal-output
M tests/csp/05-rec-extchoice1.output
M tests/csp/05-rec-extchoice1.prenormal-output
M tests/csp/05-rec-extchoice2.normal-output
M tests/csp/05-rec-extchoice2.output
M tests/csp/05-rec-extchoice2.prenormal-output
M tests/csp/05-rec-hide1.normal-output
M tests/csp/05-rec-hide1.output
M tests/csp/05-rec-hide1.prenormal-output
M tests/csp/05-rec-intchoice1.normal-output
M tests/csp/05-rec-intchoice1.output
M tests/csp/05-rec-intchoice1.prenormal-output
M tests/csp/05-rec-interleave1.normal-output
M tests/csp/05-rec-interleave1.output
M tests/csp/05-rec-interleave1.prenormal-output
M tests/csp/05-rec-iparallel1.normal-output
M tests/csp/05-rec-iparallel1.output
M tests/csp/05-rec-iparallel1.prenormal-output
M tests/csp/05-rec-prefix1.normal-output
M tests/csp/05-rec-prefix1.output
M tests/csp/05-rec-prefix1.prenormal-output
M tests/csp/05-rec-rename1.normal-output
M tests/csp/05-rec-rename1.output
M tests/csp/05-rec-rename1.prenormal-output
M tests/csp/05-rec-seqcomp1.normal-output
M tests/csp/05-rec-seqcomp1.output
M tests/csp/05-rec-seqcomp1.prenormal-output
M tests/csp/05-rec-timeout1.normal-output
M tests/csp/05-rec-timeout1.output
M tests/csp/05-rec-timeout1.prenormal-output
M tests/csp/10-extchoice-intchoice.normal-output
M tests/csp/10-extchoice-intchoice.output
M tests/csp/10-extchoice-intchoice.prenormal-output
M tests/csp/10-intchoice-extchoice.normal-output
M tests/csp/10-intchoice-extchoice.output
M tests/csp/10-intchoice-extchoice.prenormal-output
M tests/csp/80-roscoe-02.normal-output
M tests/csp/80-roscoe-02.output
M tests/csp/80-roscoe-02.prenormal-output
M tests/csp/CMakeLists.txt
M tests/lts/cycle.output
M tests/lts/empty-graph.output
M tests/lts/one-edge.output
M tests/lts/test-lts.cc
M tests/prenormalize/normalize-01.output
M tests/prenormalize/roscoe-01.output
M tests/prenormalize/roscoe-02.output

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.