<?xml version="1.0" encoding="UTF-8"?>
<commits type="array">
  <commit>
    <parents type="array">
      <parent>
        <id>2a3f31e387e7b41c1856ff79a47ad5bfebdea5cc</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/37739ef6e867fa53cb039c707bf15d4e1affd1ba</url>
    <id>37739ef6e867fa53cb039c707bf15d4e1affd1ba</id>
    <committed-date>2008-08-30T13:50:01-07:00</committed-date>
    <authored-date>2008-08-30T13:47:18-07:00</authored-date>
    <message>Flattening the Expression type

Before, we had separate datatypes for each &#8220;class&#8221; of expression; for
instance, a Number type for any expression that always evaluates to a
number.  The Expression type was then defined as a sum type across all
of these subtypes.

This patch flattens things so that there's only a single Expression
type.  This simplifies things by removing a level of indirection in
the type definitions, and also will make it easier to define &#8220;bound
expressions&#8221; as we implement static-scoped environments.

Lighthouse: [#11]</message>
    <tree>bd66e4392f5dfff3c5111189e23ac2cde766155b</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>eefa050ea24b224a956ca442752678d9a23c441c</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/2a3f31e387e7b41c1856ff79a47ad5bfebdea5cc</url>
    <id>2a3f31e387e7b41c1856ff79a47ad5bfebdea5cc</id>
    <committed-date>2008-08-30T13:42:50-07:00</committed-date>
    <authored-date>2008-08-30T13:04:21-07:00</authored-date>
    <message>CSPM environments

An environment is the symbol table that hold CSPM definitions.  They
provide a standard mapping between identifiers and the expressions
that define them.  Environments can also have an optional parent,
which allows nested scoping; if an identifier is not found in the
current environment, we then proceed to look for it in the containing
environment.

This patch introduces the basic API for creating and using
environments, but does not extend the evaluation rules to use them.

Lighthouse: [#11]</message>
    <tree>d8fb5b18d814a7e331d40eae76b846b903ee0479</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>6c92ff8cd645665253dc5604ed9aa4cd1ba43967</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/eefa050ea24b224a956ca442752678d9a23c441c</url>
    <id>eefa050ea24b224a956ca442752678d9a23c441c</id>
    <committed-date>2008-08-26T20:41:14-07:00</committed-date>
    <authored-date>2008-08-26T20:41:14-07:00</authored-date>
    <message>Adding more test cases for booleans

This patch expands the test suite with some tests for basic boolean
expressions.  Not all of them are covered yet, though.</message>
    <tree>71b0c87e94b05ff9ffe1fed229909fe474abd5fa</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>015d87c470e1e67cba3de830767d2413aa3f78a7</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/6c92ff8cd645665253dc5604ed9aa4cd1ba43967</url>
    <id>6c92ff8cd645665253dc5604ed9aa4cd1ba43967</id>
    <committed-date>2008-08-26T20:24:12-07:00</committed-date>
    <authored-date>2008-08-26T20:04:51-07:00</authored-date>
    <message>Adding more test cases for sets

This patch expands the test suite with some tests for basic set
expressions.  Not all of them are covered yet, though.</message>
    <tree>7cfedc3b67174f303a22252bd241fe9476f0e0f9</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>2b108c39f9179982b3d2447a980928aeb81e99d5</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/015d87c470e1e67cba3de830767d2413aa3f78a7</url>
    <id>015d87c470e1e67cba3de830767d2413aa3f78a7</id>
    <committed-date>2008-08-25T20:55:55-07:00</committed-date>
    <authored-date>2008-08-25T20:54:53-07:00</authored-date>
    <message>Cabal build infrastructure

This patch introduces a Cabal package description for the current HST
library.  This includes a hook to call the QuickCheck test suite.  To
build and test the Haskell code, simply run the following from the
cspm directory:

  ./Setup.lhs configure
  ./Setup.lhs build
  ./Setup.lhs test

Lighthouse: [#10 state:resolved]</message>
    <tree>3b3ba82703670aab583ea8972fa7b794efd49f85</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>8317134761619c5c0b768c2c2d0493936913e5db</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/2b108c39f9179982b3d2447a980928aeb81e99d5</url>
    <id>2b108c39f9179982b3d2447a980928aeb81e99d5</id>
    <committed-date>2008-08-25T16:09:38-07:00</committed-date>
    <authored-date>2008-08-25T16:06:46-07:00</authored-date>
    <message>Initial Haskell CSPM implementation

This is an initial patch implementing the CSPM language in Haskell.
I've chosen Haskell since, like CSPM, it's a lazy functional language.
This means we don't have to &#8220;implement&#8221; any of the functional features
of CSPM; rather, we can just call the appropriate Haskell functions.

This patch includes a basic implementation of the simple non-process
expressions in CSPM.  It does not yet include variable references,
&#8216;let&#8217; bindings, or functions, since they'll all require static-scoped
environments.  There is a basic test suite, based on QuickCheck.  I
also still need to wrap everything up in a Cabal package.

Lighthouse: [#2]</message>
    <tree>6885da7d3739eba5f1778947b5db1fc5f4bda2b5</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>d9c7dc294b48e2f3a5009e26a27a96b33f562db8</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/8317134761619c5c0b768c2c2d0493936913e5db</url>
    <id>8317134761619c5c0b768c2c2d0493936913e5db</id>
    <committed-date>2008-07-06T10:30:56-07:00</committed-date>
    <authored-date>2008-07-06T10:30:56-07:00</authored-date>
    <message>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]</message>
    <tree>9614134343319783de0fe4c885a0c7451cf291ea</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>4754d168e43124cb467c6c82b6333905bd208a7c</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/d9c7dc294b48e2f3a5009e26a27a96b33f562db8</url>
    <id>d9c7dc294b48e2f3a5009e26a27a96b33f562db8</id>
    <committed-date>2008-06-23T18:02:23-07:00</committed-date>
    <authored-date>2008-06-23T15:25:32-07:00</authored-date>
    <message>Fixed superset proof for integer sets

The is_superset_with_proof method would return incorrect proof in
certain situations.  When testing A &gt;= B, it's supposed to return an
element of B that's not in A.  Since our method works on sorted sets,
it will return the least such element, though this is not a required
part of the method's contract.  When A contained an element that was
greater than the least element of B not in A, our method would return
the A element, not the B element.  This would cause downstream errors
in the refinement code, in that the wrong counterexample could be
returned in certain situations.

Lighthouse: [#9 state:resolved]</message>
    <tree>1c2a527ad4b2f4f8c77bfa91ede011f33878f853</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>fb172a05812c6f2ed5ffa44f088c5ab0f822a41a</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/4754d168e43124cb467c6c82b6333905bd208a7c</url>
    <id>4754d168e43124cb467c6c82b6333905bd208a7c</id>
    <committed-date>2008-05-31T15:47:26-07:00</committed-date>
    <authored-date>2008-05-31T15:47:26-07:00</authored-date>
    <message>Failures refinement

This patch adds support for checking failures refinement.  The Refiner
class checks that each (SPEC, IMPL) pair satisfies the following
condition:

  &#8704; &#945;: accs(IMPL) &#8226; &#8707; &#946;: accs(SPEC) &#8226; &#945; &#8839; &#946;

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

  &#8704; &#945;: refs(IMPL) &#8226; &#8707; &#946;: refs(SPEC) &#8226; &#945; &#8838; &#946;

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

  &#8704; &#945;: allrefs(IMPL) &#8226; &#8707; &#946;: allrefs(SPEC) &#8226; &#945; = &#946;

or, in other words, that

  allrefs(IMPL) &#8838; allrefs(SPEC)

Lighthouse: [#3 state:resolved]</message>
    <tree>59642ade03c96d586c6587f019e57d5df4e671cd</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>de0feac4e64d84398444568d99918fa8d9f6cdde</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/fb172a05812c6f2ed5ffa44f088c5ab0f822a41a</url>
    <id>fb172a05812c6f2ed5ffa44f088c5ab0f822a41a</id>
    <committed-date>2008-05-31T10:28:51-07:00</committed-date>
    <authored-date>2008-05-31T10:23:54-07:00</authored-date>
    <message>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]</message>
    <tree>6d369d6072145d41e2a9abb3f6b9826e2e87d83a</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>0c111239b97698f412c09a3cbbd78ffcbba43257</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/de0feac4e64d84398444568d99918fa8d9f6cdde</url>
    <id>de0feac4e64d84398444568d99918fa8d9f6cdde</id>
    <committed-date>2008-05-31T10:28:51-07:00</committed-date>
    <authored-date>2008-05-30T21:10:07-07:00</authored-date>
    <message>Using new superset algorithm in traces refinement

This patch rewrites the traces refinement code to use the new superset
algorithm.  We'll also use this superset algorithm to check the
acceptances during a failures refinement.</message>
    <tree>eccaf64ef0e6f6014114f3cf298c01b654ed2878</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>aa82cf80491c76c99e24d03d775f73340f3f07d8</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/0c111239b97698f412c09a3cbbd78ffcbba43257</url>
    <id>0c111239b97698f412c09a3cbbd78ffcbba43257</id>
    <committed-date>2008-05-31T10:25:02-07:00</committed-date>
    <authored-date>2008-05-30T19:42:55-07:00</authored-date>
    <message>Replacing custom proxy_iterator with Boost's transform_iterator

The Boost library already has a more robust implementation of our
&#8220;proxy iterator&#8221;, so this patch changes our code to use Boost's.</message>
    <tree>7d649a05ba665473a82f86a44a45a383b8a7f763</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>272fa182e899bc777bf57e13e9c53257c549f608</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/aa82cf80491c76c99e24d03d775f73340f3f07d8</url>
    <id>aa82cf80491c76c99e24d03d775f73340f3f07d8</id>
    <committed-date>2008-05-30T20:43:36-07:00</committed-date>
    <authored-date>2008-05-29T19:18:47-07:00</authored-date>
    <message>Better equality and superset comparisons for intsets

This patch introduces a better algorithm for comparing two sets for
equality or containment.  Before, we would check S1 &#8839; S2 by looping
through all of the elements of S2, ensuring that each was in S1.
Since intset::contains isn't constant-time, this superset algorithm
isn't linear.

Now, we exploit the fact that intset's iterators return their elements
in sorted order.  We loop through the elements of S1 and S2 at the
same time.  If S1's iterator ever &#8220;passes&#8221; S2's, then we've found an
element of S2 that's not in S1, meaning that S1 &#8841; S2.  This algorithm
is linear in the maximum of #S1 and #S2.

We can use a similar algorithm for equality.  Before, we checked S1 ==
S2 by checking S1 &#8839; S2 and S2 &#8839; S1.  Now, we have a similar loop as
with the superset test, but we abort the loop if either iterator
passes the other.

Finally, the new algorithms are implemented as standalone functions
that take iterators as parameters, rather than directly taking
intsets.  This makes them more flexible.  The &gt;= and == operators in
intset have been redefined to use the new functions.</message>
    <tree>47d399b82a45c8642bd74207206b65d993ca0d18</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>61b37e197ef47a91949befb3fc773ee79ce9a31d</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/272fa182e899bc777bf57e13e9c53257c549f608</url>
    <id>272fa182e899bc777bf57e13e9c53257c549f608</id>
    <committed-date>2008-05-24T15:05:39-07:00</committed-date>
    <authored-date>2008-05-24T15:05:39-07:00</authored-date>
    <message>Replicated external choice

This patch introduces the &#8220;replicated external choice&#8221; operator.  This
has the same semantics as the standard external choice, but it works
on a set containing any number of processes.  (The standard external
choice operator takes exactly two operands.)  The replicated version
is well-defined since the binary version is associative; this means
that it doesn't matter which order we apply the binary version to the
elements of the set.  Since the unit of binary external choice is
STOP, we also get STOP if we apply the replicated version to the empty
set.

Lighthouse: [#8]</message>
    <tree>fce357544b830f8a7ce8301acf5899daa0b21686</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>35472266389a85d5aef424ec8e4b804d7dce659f</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/61b37e197ef47a91949befb3fc773ee79ce9a31d</url>
    <id>61b37e197ef47a91949befb3fc773ee79ce9a31d</id>
    <committed-date>2008-04-28T15:10:44-07:00</committed-date>
    <authored-date>2008-04-28T15:10:44-07:00</authored-date>
    <message>CSP&#8320; can now contain internal underscores

The CSP&#8320; parser was only accepting underscores in an identifier name
if they were the first character in the identifier.  This patch
corrects the parser so that underscores can occur anywhere in an
identifier.

Lighthouse: [#7 state:resolved]</message>
    <tree>e1c91f85c82441b07037cdeec8b4c83a1fdc7b55</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>c07efc77da81821cbca65c1df3aba7959bba2e1e</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/35472266389a85d5aef424ec8e4b804d7dce659f</url>
    <id>35472266389a85d5aef424ec8e4b804d7dce659f</id>
    <committed-date>2008-04-28T13:02:08-07:00</committed-date>
    <authored-date>2008-04-28T13:02:08-07:00</authored-date>
    <message>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]</message>
    <tree>b2c18508da31b55b9375dcedf0d0b920f9cf3543</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>b692420844370837a19641f3b29f71bad483b21a</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/c07efc77da81821cbca65c1df3aba7959bba2e1e</url>
    <id>c07efc77da81821cbca65c1df3aba7959bba2e1e</id>
    <committed-date>2008-04-28T10:46:02-07:00</committed-date>
    <authored-date>2008-04-28T10:46:02-07:00</authored-date>
    <message>Interleave now synchronizes on &#10003;

The &#10003; event must always be part of the synchronization alphabet for
any parallel composition, including interleaving.  The interface
parallel operator was already correctly synchronizing on &#10003;, so I've
refactored the interleaving code to simply call the interface parallel
code with an empty synchronization alphabet.  (This is similar to
alphabetized parallel, which is also implemented as a call to
interface parallel.)  This eliminates some redundant code, and ensures
that all of the parallel composition operators will now have the same
behavior.

Lighthouse: [#6 state:resolved]</message>
    <tree>d1e708f405afd0771c8be0aa2c146e469c31492e</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>58e5a3a4444fde5983b86b446359223f2ca9d598</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/b692420844370837a19641f3b29f71bad483b21a</url>
    <id>b692420844370837a19641f3b29f71bad483b21a</id>
    <committed-date>2008-04-28T09:32:45-07:00</committed-date>
    <authored-date>2008-04-28T09:32:45-07:00</authored-date>
    <message>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 &#964; 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 &#8216;a&#8217;, then there is some situation in which the state
can refuse to perform &#8216;a&#8217;.  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]</message>
    <tree>9ded79da914a93a128a75c999efb49a4b9ebe699</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>7c29484dc2c66b9afc90f23782049eacf5e1c6ec</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/58e5a3a4444fde5983b86b446359223f2ca9d598</url>
    <id>58e5a3a4444fde5983b86b446359223f2ca9d598</id>
    <committed-date>2008-04-27T16:38:47-07:00</committed-date>
    <authored-date>2008-04-27T16:38:07-07:00</authored-date>
    <message>Current &#8220;interrupt&#8221; operator is actually &#8220;timeout&#8221;

The operator that's currently called &#8220;interrupt&#8221; is actually the CSP
&#8220;timeout&#8221; operator.  All of the semantics are correct; it's just the
name of the operator that's wrong.  This patch corrects this, in the
code, test cases, and all documentation.

Lighthouse: [#4 state:resolved]</message>
    <tree>5c64cd421558b3845d96756588b1ddcdb67673fe</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>04ffccc1b5572d80415bac200d0544576e8078b9</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/7c29484dc2c66b9afc90f23782049eacf5e1c6ec</url>
    <id>7c29484dc2c66b9afc90f23782049eacf5e1c6ec</id>
    <committed-date>2008-04-25T21:00:53-07:00</committed-date>
    <authored-date>2008-04-25T20:20:39-07:00</authored-date>
    <message>Adding comments to CSP&#8320; scripts

This patch adds support for comments in CSP&#8320; scripts.  They use the
same syntax as in Perl or Python; they start with a &#8220;#&#8221; and continue
to the end of the line.  I've also added comments to many of the
existing test cases.

Lighthouse: [#1 state:resolved]</message>
    <tree>052e5bdf9ee03992760422ee1f845d4a6dedc6a9</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>a76db666456ad02eca2c961df5bf914c78aed135</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/04ffccc1b5572d80415bac200d0544576e8078b9</url>
    <id>04ffccc1b5572d80415bac200d0544576e8078b9</id>
    <committed-date>2008-04-15T19:09:33-07:00</committed-date>
    <authored-date>2008-03-21T13:10:38-07:00</authored-date>
    <message>Adding counterexamples to the traces refinement check

Instead of just giving a yes/no answer for a traces refinement, we now
provide a counterexample when the refinement fails.  The
counterexample consists of a trace of visible events, after which the
IMPL process can perform some event that SPEC cannot perform.  (This
event is provided in the counterexample, as well.)  There will often
me many possible counterexamples for a particular failed refinement;
the current implementation uses a breadth-first search, so we know
that the returned counterexample will be one with the smallest trace.
If there are many counterexamples of this length, an arbitrary one
will be returned.

The csp0 utility has also been modified to display this
counterexample, as have the traces refinement test cases.

As currently defined, the counterexample might not be especially
useful, since it only includes visible events.  If the high-level SPEC
and IMPL processes involve a lot of hiding, then you won't actually be
able to see any useful detail in the counterexample trace.  We'll need
to add some logic for drilling down into the syntax tree of a CSP
process to fix this.</message>
    <tree>afb449e6ba061168c494d9f53366dd62a9ccfead</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/a76db666456ad02eca2c961df5bf914c78aed135</url>
    <id>a76db666456ad02eca2c961df5bf914c78aed135</id>
    <committed-date>2008-02-23T14:11:52-08:00</committed-date>
    <authored-date>2008-02-23T13:47:46-08:00</authored-date>
    <message>Updated copyright notices

I've updated all of the copyright notices to contain 2008 as an
additional copyright year.</message>
    <tree>f0dd640464d258608a1b9c1ada691300103fba58</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>4107273a02d97eae36825e9b5674454f1d1c8a22</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c</url>
    <id>dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c</id>
    <committed-date>2008-02-23T14:11:47-08:00</committed-date>
    <authored-date>2008-02-23T13:44:35-08:00</authored-date>
    <message>Fixes to basic documentation set

I've made some final changes to the README, INSTALL, and TODO files in
preparation for the 1.0-&#945;1 release.  I've also fixed the COPYING file
so it contains the correct license (LGPL 2.1).  Finally, I've removed
the empty ChangeLog file, since instead I will be placing git
shortlogs into the doc/changelog directory for each release.</message>
    <tree>fa7cde5a7b9d3aa47f14a0059558c89965f16ccb</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>7d2338e7489d617f5c14dd196d63f6fc236c64b2</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/4107273a02d97eae36825e9b5674454f1d1c8a22</url>
    <id>4107273a02d97eae36825e9b5674454f1d1c8a22</id>
    <committed-date>2008-02-23T13:11:54-08:00</committed-date>
    <authored-date>2008-02-23T13:11:54-08:00</authored-date>
    <message>Adding description of $ identifiers to CSP&#8320; reference

This patch describes the intention of $ identifiers as temporary
processes needed while compiling high-level languages into CSP&#8320;.</message>
    <tree>f9a757a5fa4b2b476ed552ca9212b07716ceba98</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>f98fba8374d44174f5a03cb851b63bf95dcd16c2</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/7d2338e7489d617f5c14dd196d63f6fc236c64b2</url>
    <id>7d2338e7489d617f5c14dd196d63f6fc236c64b2</id>
    <committed-date>2008-02-23T13:10:38-08:00</committed-date>
    <authored-date>2008-02-23T12:34:17-08:00</authored-date>
    <message>Adding technical overview article

This patch adds an article giving an overview of the design and
implementation of the library.</message>
    <tree>0100b5f82e32c987570f769665c0e56e9dbf4d95</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>a8391d97b67980a173eaab4c6ef6b3bdb081f726</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/f98fba8374d44174f5a03cb851b63bf95dcd16c2</url>
    <id>f98fba8374d44174f5a03cb851b63bf95dcd16c2</id>
    <committed-date>2008-02-23T09:25:37-08:00</committed-date>
    <authored-date>2008-02-23T09:24:41-08:00</authored-date>
    <message>Renaming TAU and TICK so that they are hidden

Previously, the &#964; and &#10003; methods were given the names &#8220;TAU&#8221; and &#8220;TICK&#8221;
when created during the initialization of a csp_t object.  However,
these names mean that the events were unintentionally visible to a
CSP&#8320; script.  This made it possible to, for instance, use a prefix
statement to explicitly add a &#964; or &#10003; to a CSP LTS, instead of only
being able to introduce them using the CSP operators.  I've renamed
them to &#8220;%TAU&#8221; and &#8220;%TICK&#8221;; since the percent character isn't a valid
identifier character in CSP&#8320;, they are now correctly hidden in the
script.  It's now possible to define your own events called &#8220;TAU&#8221; and
&#8220;TICK&#8221;; however, these user-defined events won't actually have the
semantics of &#964; and &#10003;, so you shouldn't do that.</message>
    <tree>7d36479da8d3eb758c89913239d51e68e682cf25</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>47bd1e6212e510df940dc701455a60e9e000ee7f</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/a8391d97b67980a173eaab4c6ef6b3bdb081f726</url>
    <id>a8391d97b67980a173eaab4c6ef6b3bdb081f726</id>
    <committed-date>2008-02-20T16:50:29-08:00</committed-date>
    <authored-date>2008-02-20T16:43:21-08:00</authored-date>
    <message>Initial documentation

This patch adds a simple manpage for the csp0 utility that simply
redirects the user to &#8220;csp0 help&#8221;, and an article describing the CSP&#8320;
file format.  We use asciidoc for all of the documentation (both
articles and manpages), and the documentation targets are installed
during &#8220;make install&#8221;.</message>
    <tree>346dd001fd9a3b786d2fe3e6919cd2036683cd3f</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>66280415c9dfea5e2c32bc817fdafd7ee0be92fe</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/47bd1e6212e510df940dc701455a60e9e000ee7f</url>
    <id>47bd1e6212e510df940dc701455a60e9e000ee7f</id>
    <committed-date>2008-02-20T16:41:13-08:00</committed-date>
    <authored-date>2008-02-18T20:38:59-08:00</authored-date>
    <message>Improvements to build infrastructure

The build infrastructure now adds a version tag to the libhst library
(currently 0.0.0), and I've added a script that creates a source
tarball using git-archive.</message>
    <tree>340266dc551cdbe3a4c616f6e739bdd2e78fd9dd</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>513004b8f7ea870d8932d46cf7f5123b26ff220b</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/66280415c9dfea5e2c32bc817fdafd7ee0be92fe</url>
    <id>66280415c9dfea5e2c32bc817fdafd7ee0be92fe</id>
    <committed-date>2008-02-18T21:03:20-08:00</committed-date>
    <authored-date>2008-02-18T19:15:00-08:00</authored-date>
    <message>CSP&#8320; command-line utility

Added an installed command-line utility for processing CSP&#8320; scripts.
Initially it has &#8220;help&#8221;, &#8220;lts&#8221;, and &#8220;assert&#8221; commands.  If many more
commands are added it might be worth refactoring it a bit, but for now
it's fine as it is.</message>
    <tree>dd3f26569342c94db326516a46a1554051e1989e</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
  <commit>
    <parents type="array">
      <parent>
        <id>f91b2f590b4a6445b4e04bae5e36a075aab2cc27</id>
      </parent>
    </parents>
    <author>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </author>
    <url>http://github.com/dcreager/hst/commit/513004b8f7ea870d8932d46cf7f5123b26ff220b</url>
    <id>513004b8f7ea870d8932d46cf7f5123b26ff220b</id>
    <committed-date>2008-02-17T11:59:41-08:00</committed-date>
    <authored-date>2008-02-17T11:59:41-08:00</authored-date>
    <message>Fixed strict-aliasing warning in release builds

The release builds, which turn on compiler optimatizations, generate a
strict aliasing warning when compiling the parser files.  This is
because the scanner is written in terms of a &#8220;least common
denominator&#8221; Bison semantic type.  We are careful to define all of the
Bison semantic types so that they begin with the same elements as the
one used by the scanner.  However, the typecase that we use when
calling the lexer violates the strict aliasing constraints, which
don't allow you to perform type punning using pointer casts.  To get
around this, I've turned off the strict aliasing optimizations for
these compilation units.</message>
    <tree>4572ff737d44b72ef6fab5823e42820906bdd739</tree>
    <committer>
      <name>Douglas Creager</name>
      <email>dcreager@alum.mit.edu</email>
    </committer>
  </commit>
</commits>
