Changeset [b692420844370837a19641f3b29f71bad483b21a] by Douglas Creager

Revision b692420844370837a19641f3b29f71bad483b21a, committed 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...

185 changed files

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