a76db666456ad02eca2c961df5bf914c78aed135 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/2eec147cd10c6bf1904b667391dca69bfee96c00 2eec147cd10c6bf1904b667391dca69bfee96c00 2008-02-23T14:31:55-08:00 2008-02-23T13:52:08-08:00 Saving changelog for 1.0-α1 e860ac6ade92a4466c41c796fb0a3f61a8f4c7e0 Douglas Creager dcreager@alum.mit.edu dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/a76db666456ad02eca2c961df5bf914c78aed135 a76db666456ad02eca2c961df5bf914c78aed135 2008-02-23T14:11:52-08:00 2008-02-23T13:47:46-08:00 Updated copyright notices I've updated all of the copyright notices to contain 2008 as an additional copyright year. f0dd640464d258608a1b9c1ada691300103fba58 Douglas Creager dcreager@alum.mit.edu 4107273a02d97eae36825e9b5674454f1d1c8a22 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c dfb1e4759e2f4a652a78c8cec1d0879cfe3a8b4c 2008-02-23T14:11:47-08:00 2008-02-23T13:44:35-08:00 Fixes to basic documentation set I've made some final changes to the README, INSTALL, and TODO files in preparation for the 1.0-α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. fa7cde5a7b9d3aa47f14a0059558c89965f16ccb Douglas Creager dcreager@alum.mit.edu 7d2338e7489d617f5c14dd196d63f6fc236c64b2 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/4107273a02d97eae36825e9b5674454f1d1c8a22 4107273a02d97eae36825e9b5674454f1d1c8a22 2008-02-23T13:11:54-08:00 2008-02-23T13:11:54-08:00 Adding description of $ identifiers to CSP₀ reference This patch describes the intention of $ identifiers as temporary processes needed while compiling high-level languages into CSP₀. f9a757a5fa4b2b476ed552ca9212b07716ceba98 Douglas Creager dcreager@alum.mit.edu f98fba8374d44174f5a03cb851b63bf95dcd16c2 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/7d2338e7489d617f5c14dd196d63f6fc236c64b2 7d2338e7489d617f5c14dd196d63f6fc236c64b2 2008-02-23T13:10:38-08:00 2008-02-23T12:34:17-08:00 Adding technical overview article This patch adds an article giving an overview of the design and implementation of the library. 0100b5f82e32c987570f769665c0e56e9dbf4d95 Douglas Creager dcreager@alum.mit.edu a8391d97b67980a173eaab4c6ef6b3bdb081f726 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/f98fba8374d44174f5a03cb851b63bf95dcd16c2 f98fba8374d44174f5a03cb851b63bf95dcd16c2 2008-02-23T09:25:37-08:00 2008-02-23T09:24:41-08:00 Renaming TAU and TICK so that they are hidden Previously, the τ and ✓ methods were given the names “TAU” and “TICK” when created during the initialization of a csp_t object. However, these names mean that the events were unintentionally visible to a CSP₀ script. This made it possible to, for instance, use a prefix statement to explicitly add a τ or ✓ to a CSP LTS, instead of only being able to introduce them using the CSP operators. I've renamed them to “%TAU” and “%TICK”; since the percent character isn't a valid identifier character in CSP₀, they are now correctly hidden in the script. It's now possible to define your own events called “TAU” and “TICK”; however, these user-defined events won't actually have the semantics of τ and ✓, so you shouldn't do that. 7d36479da8d3eb758c89913239d51e68e682cf25 Douglas Creager dcreager@alum.mit.edu 47bd1e6212e510df940dc701455a60e9e000ee7f Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/a8391d97b67980a173eaab4c6ef6b3bdb081f726 a8391d97b67980a173eaab4c6ef6b3bdb081f726 2008-02-20T16:50:29-08:00 2008-02-20T16:43:21-08:00 Initial documentation This patch adds a simple manpage for the csp0 utility that simply redirects the user to “csp0 help”, and an article describing the CSP₀ file format. We use asciidoc for all of the documentation (both articles and manpages), and the documentation targets are installed during “make install”. 346dd001fd9a3b786d2fe3e6919cd2036683cd3f Douglas Creager dcreager@alum.mit.edu 66280415c9dfea5e2c32bc817fdafd7ee0be92fe Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/47bd1e6212e510df940dc701455a60e9e000ee7f 47bd1e6212e510df940dc701455a60e9e000ee7f 2008-02-20T16:41:13-08:00 2008-02-18T20:38:59-08:00 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. 340266dc551cdbe3a4c616f6e739bdd2e78fd9dd Douglas Creager dcreager@alum.mit.edu 513004b8f7ea870d8932d46cf7f5123b26ff220b Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/66280415c9dfea5e2c32bc817fdafd7ee0be92fe 66280415c9dfea5e2c32bc817fdafd7ee0be92fe 2008-02-18T21:03:20-08:00 2008-02-18T19:15:00-08:00 CSP₀ command-line utility Added an installed command-line utility for processing CSP₀ scripts. Initially it has “help”, “lts”, and “assert” commands. If many more commands are added it might be worth refactoring it a bit, but for now it's fine as it is. dd3f26569342c94db326516a46a1554051e1989e Douglas Creager dcreager@alum.mit.edu f91b2f590b4a6445b4e04bae5e36a075aab2cc27 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/513004b8f7ea870d8932d46cf7f5123b26ff220b 513004b8f7ea870d8932d46cf7f5123b26ff220b 2008-02-17T11:59:41-08:00 2008-02-17T11:59:41-08:00 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 “least common denominator” 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. 4572ff737d44b72ef6fab5823e42820906bdd739 Douglas Creager dcreager@alum.mit.edu c8a839d8a0dd0c55e8f58073f070596447578b10 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/f91b2f590b4a6445b4e04bae5e36a075aab2cc27 f91b2f590b4a6445b4e04bae5e36a075aab2cc27 2008-02-17T11:56:35-08:00 2008-02-17T11:56:35-08:00 Traces refinement This patch adds support for checking traces refinement. The algorithm used is described in [Roscoe94, §2.2]. As with previous patches, this algorithm currently only works with the traces model. [Roscoe94] A. W. Roscoe. “Model-checking CSP”. In A. W. Roscoe, editor, /A classical mind: Essays in honour of C. A. R. Hoare/, pages 353–378. Prentice-Hall, 1994. 920ecdd560e1700d63af39ec68a1f8439ba7387e Douglas Creager dcreager@alum.mit.edu 638887f81d6ab79b0bd8132293210cca063b3d28 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/c8a839d8a0dd0c55e8f58073f070596447578b10 c8a839d8a0dd0c55e8f58073f070596447578b10 2008-02-16T15:08:28-08:00 2008-02-16T12:48:31-08:00 Fixed recursion and memoization support The CSP operator implementations were broken when it came to recursion. This was easiest to see with interleaving (see the tests/csp/05-rec-interleave1 test case), which would go into an infinite loop when you tried to compile it. I've fixed this for all of the operators (with test cases). As a result, I also fixed the memoization code, so that both versions of each operator are memoized. (In the case where a process has already been allocated for the operation, I've implemented this a single τ transition to the memoized version.) a6b5cec51886379e3b6562b97520890834e5847a Douglas Creager dcreager@alum.mit.edu ad5974e8e3e58028b47ccb0ceac88127049328df Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/638887f81d6ab79b0bd8132293210cca063b3d28 638887f81d6ab79b0bd8132293210cca063b3d28 2008-02-16T10:18:23-08:00 2008-02-15T16:41:41-08:00 Traces normalization This patch adds support for normalizing LTS. The algorithm used is described in [Roscoe94, §2.1], and combines the prenormalization and bisimulation code from previous patches. Normalized LTSs are now constructed in stages; you can prenormalize as many initial source states as you wish, but once you finalize the normalization, no more prenormalizations are allowed. As with previous patches, this algorithm currently only works with the traces model. [Roscoe94] A. W. Roscoe. “Model-checking CSP”. In A. W. Roscoe, editor, /A classical mind: Essays in honour of C. A. R. Hoare/, pages 353–378. Prentice-Hall, 1994. 071bd9105e3c5a1c62744c01ab06d7ba423c6f32 Douglas Creager dcreager@alum.mit.edu 18ad4b130b033df4865322d44df880d76133cc08 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/ad5974e8e3e58028b47ccb0ceac88127049328df ad5974e8e3e58028b47ccb0ceac88127049328df 2008-02-16T10:18:23-08:00 2008-02-13T17:00:31-08:00 Compilation warnings are now errors I've added the -Wall and -Werror GCC flags to catch all compilation warnings as fatal errors. Several files needed modifications to remove lingering warnings. 264bf2cea25db5ad63132a537c2a66512ef3a82c Douglas Creager dcreager@alum.mit.edu 8e7d848843e553530a1b1575fa0e312605f9edf2 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/18ad4b130b033df4865322d44df880d76133cc08 18ad4b130b033df4865322d44df880d76133cc08 2008-02-16T10:17:15-08:00 2008-02-11T20:22:48-08:00 Traces bisimulation This patch adds support for bisimulating an LTS. The algorithm used is described in [Roscoe94, §2.1, Stage 2]. We'll use this bisimulation algorithm against a prenormalized LTS to generate the final normalized LTS; however, the algorithm is generic, and can be applied to any LTS. As with previous patches, this algorithm currently only works with the traces model. [Roscoe94] A. W. Roscoe. “Model-checking CSP”. In A. W. Roscoe, editor, /A classical mind: Essays in honour of C. A. R. Hoare/, pages 353–378. Prentice-Hall, 1994. 792eadabbc11ddd963f0c429e723e14d0e08cb03 Douglas Creager dcreager@alum.mit.edu 923f82ed36e08cde4229ba3d221ab76baa51ab89 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/8e7d848843e553530a1b1575fa0e312605f9edf2 8e7d848843e553530a1b1575fa0e312605f9edf2 2008-02-13T16:49:10-08:00 2008-02-11T16:14:01-08:00 Equivalence classes This patch adds support for equivalence classes. An equivalence class is a set of sets, where each member of an inner set are thought to be “equal” in some way. Methods are available for adding states to an equivalence class and for merging existing equivalence classes. Test cases are provided. 5f93c73e56c9113a3613d43682d0429c5e02d4bd Douglas Creager dcreager@alum.mit.edu 4b411f413fb3a2791d0d99554540ded1bb754682 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/923f82ed36e08cde4229ba3d221ab76baa51ab89 923f82ed36e08cde4229ba3d221ab76baa51ab89 2008-02-12T15:34:58-08:00 2008-02-08T19:00:11-08:00 Adding “alias” CSP0 statement This patch adds an “alias” statement to the CSP0 language, which allows you to provide a new name for an existing process. 2ee8de2b66074c5d179c7e6802f3cdaf6d0a112d Douglas Creager dcreager@alum.mit.edu a79c975b4a3cf1222f8440eb97ae6d272e255de5 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/4b411f413fb3a2791d0d99554540ded1bb754682 4b411f413fb3a2791d0d99554540ded1bb754682 2008-02-12T15:28:45-08:00 2008-02-08T18:36:36-08:00 Prenormalization of CSP scripts This patch adds support for prenormalizing CSP scripts. This is basically just a thin wrapper that uses the existing LTS prenormalization routines; however, this required some minor changes to how a normalized LTS refers to its source LTS. 4a4872f41042956267403803a9b92eaa1d2264b8 Douglas Creager dcreager@alum.mit.edu 4a003b433e0becb6bbfb522eb858cd13543b5fc7 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/a79c975b4a3cf1222f8440eb97ae6d272e255de5 a79c975b4a3cf1222f8440eb97ae6d272e255de5 2008-02-11T17:53:35-08:00 2008-02-08T18:32:25-08:00 Normalized LTS output now includes STOP states The output routine for normalized LTSs was looping through the LTS graph to decide which states to include in the “mapping” section. Since STOP-equivalent states have no outgoing edges, they don't appear in the LTS graph, and therefore didn't appear in the output. This patch fixes this behavior. c34badcea4e4a7b9c2e94069f699cc970428b61a Douglas Creager dcreager@alum.mit.edu 196017897368a6e7b2c1774cd71c338cf58264c0 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/4a003b433e0becb6bbfb522eb858cd13543b5fc7 4a003b433e0becb6bbfb522eb858cd13543b5fc7 2008-02-11T17:53:35-08:00 2008-02-06T17:05:49-08:00 Initial support for LTS prenormalization This patch adds support for prenormalizing an LTS. The algorithm used is described in [Roscoe94, §2.1, Stage 1]. The nodes in a prenormalized LTS each represent a set of states from the original LTS, and each node is guaranteed to have at most one outgoing transition for each event. The prenormalization algorithm isn't complete yet, however, since it only supports the traces model. [Roscoe94] A. W. Roscoe. “Model-checking CSP”. In A. W. Roscoe, editor, /A classical mind: Essays in honour of C. A. R. Hoare/, pages 353–378. Prentice-Hall, 1994. 35b691f2560304dea3f089e68f4d9d7ea399af51 Douglas Creager dcreager@alum.mit.edu 6b64051bfe84fde8e561bd87b9457a12a2b4c28e Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/196017897368a6e7b2c1774cd71c338cf58264c0 196017897368a6e7b2c1774cd71c338cf58264c0 2008-02-11T17:52:36-08:00 2008-02-05T18:45:24-08:00 Refactoring LTS graph into separate class This patch extracts the LTS's inner event→stateset map into a separate class. This will allow us to use this map class on its own when we prenormalize an LTS. As part of this, I've also gone through and made sure that every time we declare a shared_ptr to a class, we also declare a shared_ptr to a const version of the class. a00925bda81a1e1c287e7760df8b6957d52d92f5 Douglas Creager dcreager@alum.mit.edu 1bf996a90932af6e843b277539c635a9d4ac5fbd Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/6b64051bfe84fde8e561bd87b9457a12a2b4c28e 6b64051bfe84fde8e561bd87b9457a12a2b4c28e 2008-02-11T17:52:18-08:00 2008-02-02T08:29:26-08:00 Divergent nodes in an LTS This patch provides a function for finding the divergent nodes in an LTS. A node is divergent if it is possible to execute an infinite sequence of a particular event from it; this is encoded in an LTS by a cycle that is reachable from the node. We use an algorithm based on depth-first search to find the divergent nodes in an LTS; this algorithm was devised by Michael Goldsmith and is described in [Roscoe94, §2.2]. [Roscoe94] A. W. Roscoe. “Model-checking CSP”. In A. W. Roscoe, editor, /A classical mind: Essays in honour of C. A. R. Hoare/, pages 353–378. Prentice-Hall, 1994. cf937d1551577809b1d3c0ea0530f6a3336a48d3 Douglas Creager dcreager@alum.mit.edu 9f2acf07ad2a3115a264a8c017156ee5f867cb6d Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/1bf996a90932af6e843b277539c635a9d4ac5fbd 1bf996a90932af6e843b277539c635a9d4ac5fbd 2008-02-11T17:50:46-08:00 2008-01-31T15:04:37-08:00 Event closure As the first part of implementating the normalization algorithm for LTSs, I've written the code to find the closure of a set of states for a particular event. The closure is the set of nodes that can be reached from any of the initial nodes by following any sequence of that event. When we get to CSP normalization, we'll be looking specifically for τ closures. The pseudo-code algorithm is: CLOSURE(initial_nodes, event): closure_nodes seen = ∅ closure_nodes = ∅ queue = initial_nodes for x ∈ queue: seen ∪= {x} closure_nodes ∪= {x} queue ∖= {x} for y ∈ afters(x, event): if y ∉ seen: queue ∪= {y} 5f8027f1335b9b674c3286c8726ee684447e3f73 Douglas Creager dcreager@alum.mit.edu 5c6448a46d8aa1f64f886ebfccad1bb63e6c026c Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/9f2acf07ad2a3115a264a8c017156ee5f867cb6d 9f2acf07ad2a3115a264a8c017156ee5f867cb6d 2008-01-31T14:18:09-08:00 2008-01-31T14:18:09-08:00 Moving CSP operator definitions into a subdirectory This patch refactors the code base, making things a bit cleaner by placing the CSP operator definitions into their own subdirectory. c4e78d0a52e90b65e20eba0a0f5c35690f78d977 Douglas Creager dcreager@alum.mit.edu 95ffa7136f93564ad191871eb46b57ecb753bdf9 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/5c6448a46d8aa1f64f886ebfccad1bb63e6c026c 5c6448a46d8aa1f64f886ebfccad1bb63e6c026c 2008-01-31T13:20:25-08:00 2008-01-31T13:20:25-08:00 Operational semantics for renaming This patch adds support for the rename operator, including a corresponding CSP0 statement and test cases. ac141b57eb511ba93a6a8ba6d4f946a357c5a8bc Douglas Creager dcreager@alum.mit.edu 8915ce3c263e539adcd1a8b3d7b558a26659c4ca Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/95ffa7136f93564ad191871eb46b57ecb753bdf9 95ffa7136f93564ad191871eb46b57ecb753bdf9 2008-01-31T12:19:00-08:00 2008-01-31T11:59:01-08:00 Operational semantics for hiding This patch adds support for the hide operator, including a corresponding CSP0 statement and test cases. b95486bb6436881cf66ea5f64390c163f2ab2739 Douglas Creager dcreager@alum.mit.edu 8a3eada2da7389d04ef2f9049055d2a8f85badf2 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/8915ce3c263e539adcd1a8b3d7b558a26659c4ca 8915ce3c263e539adcd1a8b3d7b558a26659c4ca 2008-01-31T12:18:50-08:00 2008-01-29T14:25:44-08:00 Using Bison for all parsing routines Bison is now used to implement all of the parsing routines. We don't use Flex for the scanner, since the Flex buffering routines made it difficult to scan only part of an input stream. Since our grammar is relatively simple, it was easier to write a custom lexer that uses the underlying buffering of the istream classes. As a result of this change, the alphabets in a CSP0 script should now contain event names instead of event numbers, which was the originally desired behavior. f71f51046bbe31aab84933c7daeb2b55caeaa36b Douglas Creager dcreager@alum.mit.edu a14cde9a5d048d72a676f2c9094da909b79fe22d Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/8a3eada2da7389d04ef2f9049055d2a8f85badf2 8a3eada2da7389d04ef2f9049055d2a8f85badf2 2008-01-29T14:40:55-08:00 2008-01-26T15:37:00-08:00 Refactoring test cases to use ctest The test cases all used shell scripts to execute the test executable for many different inputs. This logic has been moved into the cmake descriptions to consolidate things. It also makes the output of “make tests” more useful, since the different input files are visible as separate test cases. c8fbaf593de4240f9b66d3b0457e6ffc15cc7358 Douglas Creager dcreager@alum.mit.edu c01308e703de3654ae1ae3c8ac46634899b0ff88 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/a14cde9a5d048d72a676f2c9094da909b79fe22d a14cde9a5d048d72a676f2c9094da909b79fe22d 2008-01-29T14:40:54-08:00 2008-01-26T15:00:54-08:00 Using cmake for the build system This patch replaces the autotools with a cmake-based build system. Instructions for building the source can be found in the README and INSTALL files. I had to rename the test directory (to “tests”) so that it doesn't conflict with cmake's default test Makefile target. d45992d53665e01b562085cc5209078a628b8922 Douglas Creager dcreager@alum.mit.edu d1d79a6ea5443bf5a1f0bd3dd4c4359278468712 Douglas Creager dcreager@alum.mit.edu http://github.com/dcreager/hst/commit/c01308e703de3654ae1ae3c8ac46634899b0ff88 c01308e703de3654ae1ae3c8ac46634899b0ff88 2008-01-29T14:40:54-08:00 2008-01-20T10:42:44-08:00 Operational semantics for alphabetized parallel This patch adds support for the alphabetized parallel operator, including a corresponding CSP0 statement and test cases. Like with interface parallel, the CSP0 statement currently requires the alphabets to be specified using numbers, rather than their symbolic names, which needs to be fixed. 2d4a4dcb1e4de1757ffd05a7d9b7e6d9b28212f6 Douglas Creager dcreager@alum.mit.edu