Changeset: Changeset [35472266389a85d5aef424ec8e4b804d7dce659f] by Douglas Creager - hst

List changesets

Changeset [35472266389a85d5aef424ec8e4b804d7dce659f] by Douglas Creager

April 28th, 2008 @ 04:02 PM

Failures normalization

With this patch, the normalization code now works in the failures

model as well as the traces model. The normalization code now takes

as a parameter which semantic model to use. Currently, failures and

failures-divergences are treated the same, and do not consider

divergence information. The tests/csp/80-roscoe-02 test case is one

example where the normalization is different in the two models.

The interface to this code could probably use some cleaning up, but

it's also probably not worth doing this until the failures-divergences

code is added.

Lighthouse: [#3]

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

Committed by Douglas Creager

A tests/csp/00-aparallel1.f-normal-output
A tests/csp/00-aparallel1.f-prenormal-output
A tests/csp/00-aparallel1.t-normal-output
A tests/csp/00-aparallel1.t-prenormal-output
A tests/csp/00-aparallel2.f-normal-output
A tests/csp/00-aparallel2.f-prenormal-output
A tests/csp/00-aparallel2.t-normal-output
A tests/csp/00-aparallel2.t-prenormal-output
A tests/csp/00-aparallel3.f-normal-output
A tests/csp/00-aparallel3.f-prenormal-output
A tests/csp/00-aparallel3.t-normal-output
A tests/csp/00-aparallel3.t-prenormal-output
A tests/csp/00-extchoice1.f-normal-output
A tests/csp/00-extchoice1.f-prenormal-output
A tests/csp/00-extchoice1.t-normal-output
A tests/csp/00-extchoice1.t-prenormal-output
A tests/csp/00-extchoice2.f-normal-output
A tests/csp/00-extchoice2.f-prenormal-output
A tests/csp/00-extchoice2.t-normal-output
A tests/csp/00-extchoice2.t-prenormal-output
A tests/csp/00-extchoice3.f-normal-output
A tests/csp/00-extchoice3.f-prenormal-output
A tests/csp/00-extchoice3.t-normal-output
A tests/csp/00-extchoice3.t-prenormal-output
A tests/csp/00-extchoice4.f-normal-output
A tests/csp/00-extchoice4.f-prenormal-output
A tests/csp/00-extchoice4.t-normal-output
A tests/csp/00-extchoice4.t-prenormal-output
A tests/csp/00-hide1.f-normal-output
A tests/csp/00-hide1.f-prenormal-output
A tests/csp/00-hide1.t-normal-output
A tests/csp/00-hide1.t-prenormal-output
A tests/csp/00-hide2.f-normal-output
A tests/csp/00-hide2.f-prenormal-output
A tests/csp/00-hide2.t-normal-output
A tests/csp/00-hide2.t-prenormal-output
A tests/csp/00-hide3.f-normal-output
A tests/csp/00-hide3.f-prenormal-output
A tests/csp/00-hide3.t-normal-output
A tests/csp/00-hide3.t-prenormal-output
A tests/csp/00-hide4.f-normal-output
A tests/csp/00-hide4.f-prenormal-output
A tests/csp/00-hide4.t-normal-output
A tests/csp/00-hide4.t-prenormal-output
A tests/csp/00-intchoice1.f-normal-output
A tests/csp/00-intchoice1.f-prenormal-output
A tests/csp/00-intchoice1.t-normal-output
A tests/csp/00-intchoice1.t-prenormal-output
A tests/csp/00-intchoice2.f-normal-output
A tests/csp/00-intchoice2.f-prenormal-output
A tests/csp/00-intchoice2.t-normal-output
A tests/csp/00-intchoice2.t-prenormal-output
A tests/csp/00-interleave1.f-normal-output
A tests/csp/00-interleave1.f-prenormal-output
A tests/csp/00-interleave1.t-normal-output
A tests/csp/00-interleave1.t-prenormal-output
A tests/csp/00-interleave2.f-normal-output
A tests/csp/00-interleave2.f-prenormal-output
A tests/csp/00-interleave2.t-normal-output
A tests/csp/00-interleave2.t-prenormal-output
A tests/csp/00-interleave3.f-normal-output
A tests/csp/00-interleave3.f-prenormal-output
A tests/csp/00-interleave3.t-normal-output
A tests/csp/00-interleave3.t-prenormal-output
A tests/csp/00-interleave4.f-normal-output
A tests/csp/00-interleave4.f-prenormal-output
A tests/csp/00-interleave4.t-normal-output
A tests/csp/00-interleave4.t-prenormal-output
A tests/csp/00-interleave5.f-normal-output
A tests/csp/00-interleave5.f-prenormal-output
A tests/csp/00-interleave5.t-normal-output
A tests/csp/00-interleave5.t-prenormal-output
A tests/csp/00-interleave6.f-normal-output
A tests/csp/00-interleave6.f-prenormal-output
A tests/csp/00-interleave6.t-normal-output
A tests/csp/00-interleave6.t-prenormal-output
A tests/csp/00-iparallel1.f-normal-output
A tests/csp/00-iparallel1.f-prenormal-output
A tests/csp/00-iparallel1.t-normal-output
A tests/csp/00-iparallel1.t-prenormal-output
A tests/csp/00-iparallel2.f-normal-output
A tests/csp/00-iparallel2.f-prenormal-output
A tests/csp/00-iparallel2.t-normal-output
A tests/csp/00-iparallel2.t-prenormal-output
A tests/csp/00-iparallel3.f-normal-output
A tests/csp/00-iparallel3.f-prenormal-output
A tests/csp/00-iparallel3.t-normal-output
A tests/csp/00-iparallel3.t-prenormal-output
A tests/csp/00-iparallel4.f-normal-output
A tests/csp/00-iparallel4.f-prenormal-output
A tests/csp/00-iparallel4.t-normal-output
A tests/csp/00-iparallel4.t-prenormal-output
A tests/csp/00-prefix.f-normal-output
A tests/csp/00-prefix.f-prenormal-output
A tests/csp/00-prefix.t-normal-output
A tests/csp/00-prefix.t-prenormal-output
A tests/csp/00-rename1.f-normal-output
A tests/csp/00-rename1.f-prenormal-output
A tests/csp/00-rename1.t-normal-output
A tests/csp/00-rename1.t-prenormal-output
A tests/csp/00-rename2.f-normal-output
A tests/csp/00-rename2.f-prenormal-output
A tests/csp/00-rename2.t-normal-output
A tests/csp/00-rename2.t-prenormal-output
A tests/csp/00-rename3.f-normal-output
A tests/csp/00-rename3.f-prenormal-output
A tests/csp/00-rename3.t-normal-output
A tests/csp/00-rename3.t-prenormal-output
A tests/csp/00-seqcomp1.f-normal-output
A tests/csp/00-seqcomp1.f-prenormal-output
A tests/csp/00-seqcomp1.t-normal-output
A tests/csp/00-seqcomp1.t-prenormal-output
A tests/csp/00-seqcomp2.f-normal-output
A tests/csp/00-seqcomp2.f-prenormal-output
A tests/csp/00-seqcomp2.t-normal-output
A tests/csp/00-seqcomp2.t-prenormal-output
A tests/csp/00-timeout1.f-normal-output
A tests/csp/00-timeout1.f-prenormal-output
A tests/csp/00-timeout1.t-normal-output
A tests/csp/00-timeout1.t-prenormal-output
A tests/csp/00-timeout2.f-normal-output
A tests/csp/00-timeout2.f-prenormal-output
A tests/csp/00-timeout2.t-normal-output
A tests/csp/00-timeout2.t-prenormal-output
A tests/csp/02-mem-aparallel1.f-normal-output
A tests/csp/02-mem-aparallel1.f-prenormal-output
A tests/csp/02-mem-aparallel1.t-normal-output
A tests/csp/02-mem-aparallel1.t-prenormal-output
A tests/csp/02-mem-extchoice1.f-normal-output
A tests/csp/02-mem-extchoice1.f-prenormal-output
A tests/csp/02-mem-extchoice1.t-normal-output
A tests/csp/02-mem-extchoice1.t-prenormal-output
A tests/csp/02-mem-hide1.f-normal-output
A tests/csp/02-mem-hide1.f-prenormal-output
A tests/csp/02-mem-hide1.t-normal-output
A tests/csp/02-mem-hide1.t-prenormal-output
A tests/csp/02-mem-intchoice1.f-normal-output
A tests/csp/02-mem-intchoice1.f-prenormal-output
A tests/csp/02-mem-intchoice1.t-normal-output
A tests/csp/02-mem-intchoice1.t-prenormal-output
A tests/csp/02-mem-interleave1.f-normal-output
A tests/csp/02-mem-interleave1.f-prenormal-output
A tests/csp/02-mem-interleave1.t-normal-output
A tests/csp/02-mem-interleave1.t-prenormal-output
A tests/csp/02-mem-iparallel1.f-normal-output
A tests/csp/02-mem-iparallel1.f-prenormal-output
A tests/csp/02-mem-iparallel1.t-normal-output
A tests/csp/02-mem-iparallel1.t-prenormal-output
A tests/csp/02-mem-prefix1.f-normal-output
A tests/csp/02-mem-prefix1.f-prenormal-output
A tests/csp/02-mem-prefix1.t-normal-output
A tests/csp/02-mem-prefix1.t-prenormal-output
A tests/csp/02-mem-rename1.f-normal-output
A tests/csp/02-mem-rename1.f-prenormal-output
A tests/csp/02-mem-rename1.t-normal-output
A tests/csp/02-mem-rename1.t-prenormal-output
A tests/csp/02-mem-seqcomp1.f-normal-output
A tests/csp/02-mem-seqcomp1.f-prenormal-output
A tests/csp/02-mem-seqcomp1.t-normal-output
A tests/csp/02-mem-seqcomp1.t-prenormal-output
A tests/csp/02-mem-timeout1.f-normal-output
A tests/csp/02-mem-timeout1.f-prenormal-output
A tests/csp/02-mem-timeout1.t-normal-output
A tests/csp/02-mem-timeout1.t-prenormal-output
A tests/csp/05-rec-aparallel1.f-normal-output
A tests/csp/05-rec-aparallel1.f-prenormal-output
A tests/csp/05-rec-aparallel1.t-normal-output
A tests/csp/05-rec-aparallel1.t-prenormal-output
A tests/csp/05-rec-extchoice1.f-normal-output
A tests/csp/05-rec-extchoice1.f-prenormal-output
A tests/csp/05-rec-extchoice1.t-normal-output
A tests/csp/05-rec-extchoice1.t-prenormal-output
A tests/csp/05-rec-extchoice2.f-normal-output
A tests/csp/05-rec-extchoice2.f-prenormal-output
A tests/csp/05-rec-extchoice2.t-normal-output
A tests/csp/05-rec-extchoice2.t-prenormal-output
A tests/csp/05-rec-hide1.f-normal-output
A tests/csp/05-rec-hide1.f-prenormal-output
A tests/csp/05-rec-hide1.t-normal-output
A tests/csp/05-rec-hide1.t-prenormal-output
A tests/csp/05-rec-intchoice1.f-normal-output
A tests/csp/05-rec-intchoice1.f-prenormal-output
A tests/csp/05-rec-intchoice1.t-normal-output
A tests/csp/05-rec-intchoice1.t-prenormal-output
A tests/csp/05-rec-interleave1.f-normal-output
A tests/csp/05-rec-interleave1.f-prenormal-output
A tests/csp/05-rec-interleave1.t-normal-output
A tests/csp/05-rec-interleave1.t-prenormal-output
A tests/csp/05-rec-iparallel1.f-normal-output
A tests/csp/05-rec-iparallel1.f-prenormal-output
A tests/csp/05-rec-iparallel1.t-normal-output
A tests/csp/05-rec-iparallel1.t-prenormal-output
A tests/csp/05-rec-prefix1.f-normal-output
A tests/csp/05-rec-prefix1.f-prenormal-output
A tests/csp/05-rec-prefix1.t-normal-output
A tests/csp/05-rec-prefix1.t-prenormal-output
A tests/csp/05-rec-rename1.f-normal-output
A tests/csp/05-rec-rename1.f-prenormal-output
A tests/csp/05-rec-rename1.t-normal-output
A tests/csp/05-rec-rename1.t-prenormal-output
A tests/csp/05-rec-seqcomp1.f-normal-output
A tests/csp/05-rec-seqcomp1.f-prenormal-output
A tests/csp/05-rec-seqcomp1.t-normal-output
A tests/csp/05-rec-seqcomp1.t-prenormal-output
A tests/csp/05-rec-timeout1.f-normal-output
A tests/csp/05-rec-timeout1.f-prenormal-output
A tests/csp/05-rec-timeout1.t-normal-output
A tests/csp/05-rec-timeout1.t-prenormal-output
A tests/csp/10-extchoice-intchoice.f-normal-output
A tests/csp/10-extchoice-intchoice.f-prenormal-output
A tests/csp/10-extchoice-intchoice.t-normal-output
A tests/csp/10-extchoice-intchoice.t-prenormal-output
A tests/csp/10-intchoice-extchoice.f-normal-output
A tests/csp/10-intchoice-extchoice.f-prenormal-output
A tests/csp/10-intchoice-extchoice.t-normal-output
A tests/csp/10-intchoice-extchoice.t-prenormal-output
A tests/csp/80-roscoe-02.f-normal-output
A tests/csp/80-roscoe-02.f-prenormal-output
A tests/csp/80-roscoe-02.t-normal-output
A tests/csp/80-roscoe-02.t-prenormal-output
R tests/csp/00-aparallel1.normal-output
R tests/csp/00-aparallel1.prenormal-output
R tests/csp/00-aparallel2.normal-output
R tests/csp/00-aparallel2.prenormal-output
R tests/csp/00-aparallel3.normal-output
R tests/csp/00-aparallel3.prenormal-output
R tests/csp/00-extchoice1.normal-output
R tests/csp/00-extchoice1.prenormal-output
R tests/csp/00-extchoice2.normal-output
R tests/csp/00-extchoice2.prenormal-output
R tests/csp/00-extchoice3.normal-output
R tests/csp/00-extchoice3.prenormal-output
R tests/csp/00-extchoice4.normal-output
R tests/csp/00-extchoice4.prenormal-output
R tests/csp/00-hide1.normal-output
R tests/csp/00-hide1.prenormal-output
R tests/csp/00-hide2.normal-output
R tests/csp/00-hide2.prenormal-output
R tests/csp/00-hide3.normal-output
R tests/csp/00-hide3.prenormal-output
R tests/csp/00-hide4.normal-output
R tests/csp/00-hide4.prenormal-output
R tests/csp/00-intchoice1.normal-output
R tests/csp/00-intchoice1.prenormal-output
R tests/csp/00-intchoice2.normal-output
R tests/csp/00-intchoice2.prenormal-output
R tests/csp/00-interleave1.normal-output
R tests/csp/00-interleave1.prenormal-output
R tests/csp/00-interleave2.normal-output
R tests/csp/00-interleave2.prenormal-output
R tests/csp/00-interleave3.normal-output
R tests/csp/00-interleave3.prenormal-output
R tests/csp/00-interleave4.normal-output
R tests/csp/00-interleave4.prenormal-output
R tests/csp/00-interleave5.normal-output
R tests/csp/00-interleave5.prenormal-output
R tests/csp/00-interleave6.normal-output
R tests/csp/00-interleave6.prenormal-output
R tests/csp/00-iparallel1.normal-output
R tests/csp/00-iparallel1.prenormal-output
R tests/csp/00-iparallel2.normal-output
R tests/csp/00-iparallel2.prenormal-output
R tests/csp/00-iparallel3.normal-output
R tests/csp/00-iparallel3.prenormal-output
R tests/csp/00-iparallel4.normal-output
R tests/csp/00-iparallel4.prenormal-output
R tests/csp/00-prefix.normal-output
R tests/csp/00-prefix.prenormal-output
R tests/csp/00-rename1.normal-output
R tests/csp/00-rename1.prenormal-output
R tests/csp/00-rename2.normal-output
R tests/csp/00-rename2.prenormal-output
R tests/csp/00-rename3.normal-output
R tests/csp/00-rename3.prenormal-output
R tests/csp/00-seqcomp1.normal-output
R tests/csp/00-seqcomp1.prenormal-output
R tests/csp/00-seqcomp2.normal-output
R tests/csp/00-seqcomp2.prenormal-output
R tests/csp/00-timeout1.normal-output
R tests/csp/00-timeout1.prenormal-output
R tests/csp/00-timeout2.normal-output
R tests/csp/00-timeout2.prenormal-output
R tests/csp/02-mem-aparallel1.normal-output
R tests/csp/02-mem-aparallel1.prenormal-output
R tests/csp/02-mem-extchoice1.normal-output
R tests/csp/02-mem-extchoice1.prenormal-output
R tests/csp/02-mem-hide1.normal-output
R tests/csp/02-mem-hide1.prenormal-output
R tests/csp/02-mem-intchoice1.normal-output
R tests/csp/02-mem-intchoice1.prenormal-output
R tests/csp/02-mem-interleave1.normal-output
R tests/csp/02-mem-interleave1.prenormal-output
R tests/csp/02-mem-iparallel1.normal-output
R tests/csp/02-mem-iparallel1.prenormal-output
R tests/csp/02-mem-prefix1.normal-output
R tests/csp/02-mem-prefix1.prenormal-output
R tests/csp/02-mem-rename1.normal-output
R tests/csp/02-mem-rename1.prenormal-output
R tests/csp/02-mem-seqcomp1.normal-output
R tests/csp/02-mem-seqcomp1.prenormal-output
R tests/csp/02-mem-timeout1.normal-output
R tests/csp/02-mem-timeout1.prenormal-output
R tests/csp/05-rec-aparallel1.normal-output
R tests/csp/05-rec-aparallel1.prenormal-output
R tests/csp/05-rec-extchoice1.normal-output
R tests/csp/05-rec-extchoice1.prenormal-output
R tests/csp/05-rec-extchoice2.normal-output
R tests/csp/05-rec-extchoice2.prenormal-output
R tests/csp/05-rec-hide1.normal-output
R tests/csp/05-rec-hide1.prenormal-output
R tests/csp/05-rec-intchoice1.normal-output
R tests/csp/05-rec-intchoice1.prenormal-output
R tests/csp/05-rec-interleave1.normal-output
R tests/csp/05-rec-interleave1.prenormal-output
R tests/csp/05-rec-iparallel1.normal-output
R tests/csp/05-rec-iparallel1.prenormal-output
R tests/csp/05-rec-prefix1.normal-output
R tests/csp/05-rec-prefix1.prenormal-output
R tests/csp/05-rec-rename1.normal-output
R tests/csp/05-rec-rename1.prenormal-output
R tests/csp/05-rec-seqcomp1.normal-output
R tests/csp/05-rec-seqcomp1.prenormal-output
R tests/csp/05-rec-timeout1.normal-output
R tests/csp/05-rec-timeout1.prenormal-output
R tests/csp/10-extchoice-intchoice.normal-output
R tests/csp/10-extchoice-intchoice.prenormal-output
R tests/csp/10-intchoice-extchoice.normal-output
R tests/csp/10-intchoice-extchoice.prenormal-output
R tests/csp/80-roscoe-02.normal-output
R tests/csp/80-roscoe-02.prenormal-output
M build-scripts/save-csp-test
M include/hst/csp.hh
M include/hst/lts.hh
M include/hst/normalized-lts.hh
M include/hst/types.hh
M src/bin/csp0.cc
M src/normalization/bisimulate.cc
M src/normalization/normalize.cc
M src/normalization/prenormalize.cc
M tests/bisimulate/test-bisimulate.cc
M tests/csp/CMakeLists.txt
M tests/csp/test-normalize.cc
M tests/csp/test-prenormalize.cc
M tests/prenormalize/test-prenormalize.cc

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.