Hst hst → 1.0-α2

Comments and changes to this ticket

• 

  Douglas Creager April 27th, 2008 @ 07:42 PM

  • Milestone set to “1.0-α2”
  • State changed from “new” to “open”
• 

  Douglas Creager April 28th, 2008 @ 12:33 PM

  (from [b692420844370837a19641f3b29f71bad483b21a]) 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...

• 

  Douglas Creager April 28th, 2008 @ 04:02 PM

  (from [35472266389a85d5aef424ec8e4b804d7dce659f]) 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...

• 

  Douglas Creager May 31st, 2008 @ 01:29 PM

  (from [fb172a05812c6f2ed5ffa44f088c5ab0f822a41a]) Refactoring refinement code to support multiple semantic models

  As another step towards implementing failures refinement, this patch

  refactors the refinement code to have better support for different

  semantic models. Part of the refinement code is identical regardless

  of semantic model. Mostly, this is the scaffolding of the

  breadth-first search, where we examine each pair of (SPEC, IMPL)

  states from the original processes. The only model-specific code is

  the part that checks whether a particular (SPEC, IMPL) pair is part of

  a valid refinement, and that constructs a counterexample object if

  it's not.

  This new design has the model-independent code as a templated

  function. There are two template parameters: Refiner and

  Counterexample. Counterexample is the type of the counterexample

  object that's created if the refinement fails. The refine function

  does not need to know any details of this type. The Refiner type

  contains the model-specific code for checking a pair of states and

  constructing a Counterexample object if needed. The API of the

  Refiner object is described in the refine.cc file.

  With this modification, we should be able to implement failures

  refinement simply by defining a new Refiner class.

  Lighthouse: [#3]

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

• 

  Douglas Creager May 31st, 2008 @ 06:48 PM

  • State changed from “open” to “resolved”

  (from [4754d168e43124cb467c6c82b6333905bd208a7c]) Failures refinement

  This patch adds support for checking failures refinement. The Refiner

  class checks that each (SPEC, IMPL) pair satisfies the following

  condition:

  ∀ α: accs(IMPL) • ∃ β: accs(SPEC) • α ⊇ β

  An acceptance is the complement of a refusal, so this is equivalent

  to:

  ∀ α: refs(IMPL) • ∃ β: refs(SPEC) • α ⊆ β

  The refs() function only represents the maximal refusals that are

  actually stored in the LTS. This corresponds to an allrefs() function

  that contains all of refusals, which are subset closed. Thus, the

  condition also ensures that

  ∀ α: allrefs(IMPL) • ∃ β: allrefs(SPEC) • α = β

  or, in other words, that

  allrefs(IMPL) ⊆ allrefs(SPEC)

  Lighthouse: [#3 state:resolved]

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

• 

  Douglas Creager July 6th, 2008 @ 01:31 PM

  • Tag cleared.

  (from [8317134761619c5c0b768c2c2d0493936913e5db]) Adding failures refinement option to csp0 script

  A previous patch added support for failures refinement, but I hadn't

  yet made this functionality available in the csp0 command-line script.

  This patch does so.

  Lighthouse: [#3 state:resolved]

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