HST
Philip Armstrong
I've just been having a chat with Charlie about doing a "new CSP". You
might like to know that even Bill is on-side with getting rid of
".", or at least making "." only able to make a fully constructed
object. Will Bill on-side, we stand a strong chance of getting
anything extra we need into the unicode standard as well, although
I'd imagine that the available character set should suffice.
From your HST code I can see that you're re-creating the existing CSPm
parser. Personally, I'd really like to see the full power of
Haskell applied to the job of building CSP processes, but I've never
worked out a good way to express that.
Something else which is on the backburner is a protocol buffers (or
swig possibly) interface to the FDR2 refinement engine. Unfortunately
due to sad contractural limitations such an interface could only be
made available for academic use, but it could serve as a generic
"here's an interface for data exchange". Defining an XML<->protocol
buffers conversion would be straightforward for instance.
NB. Something I *can* do is make the CSPm lex / bison code
available. Some aspects are a bit crufty (there's some massaging of
the output of the lexer and parser by a couple of sed & awk scripts:
icky I know, but it was before my time...) but they might be useful as
reference points.
cheers, Phil
--
Philip Armstrong <philip.a...@comlab.ox.ac.uk>
Research Assistant, Oxford University Computing Laboratory
Douglas Creager
Thanks!
> I've just been having a chat with Charlie about doing a "new CSP". You
> might like to know that even Bill is on-side with getting rid of
> ".", or at least making "." only able to make a fully constructed
> object. Will Bill on-side, we stand a strong chance of getting
> anything extra we need into the unicode standard as well, although
> I'd imagine that the available character set should suffice.
No arguments from me about the "." issue! I also like the idea of using
Unicode for the operators, where possible. How would you envision handling
backwards-compatibility with older versions of the CSPM syntax? Would you
try to ensure that every valid old CSPM script is also a valid new one?
> From your HST code I can see that you're re-creating the existing CSPm
> parser. Personally, I'd really like to see the full power of
> Haskell applied to the job of building CSP processes, but I've never
> worked out a good way to express that.
I agree. I'd mentioned in passing to Charlie over IM an idea for a CSPH.
This, in fact, was one of the reasons I separated the CSPM code from the
CSP0 code. I had assumed that CSPH scripts would really just be Haskell
files, that had access to an easy-to-use library or DSL for creating CSP0
output — and then it would use the same refinement-checking code as the
CSPM compiler. I haven't had enough time to flesh this idea out, though.
I think a good starting point would be to decide what we'd want a CSPH
script to look like, and then figure out the best way to implement the
library or DSL.
> Something else which is on the backburner is a protocol buffers (or
> swig possibly) interface to the FDR2 refinement engine. Unfortunately
> due to sad contractural limitations such an interface could only be
> made available for academic use, but it could serve as a generic
> "here's an interface for data exchange". Defining an XML<->protocol
> buffers conversion would be straightforward for instance.
I hear you on the contractual part! I was very careful to make sure I've
never seen the FDR code, for exactly that reason. My goal with HST is
certainly not to replace FDR — rather that a truly open-source
alternative might help to promote CSP. I think an interchange format would
be brilliant for this.
What do you envision the protocol buffers interface looking like? Would
this be a programmatic interface, or more a data format for describing
LTSes? I can definitely see the benefit in making the latter not be tied
to either of our implementations — though maybe that's what you mean when
you mention XML. CSP0 might also serve as a higher-level interchange
format, in case we want to consider non-LTS implementations. (That last
point is a hunch, I don't know if it's sufficiently divorced from the LTS
idea to work in that way.)
> NB. Something I *can* do is make the CSPm lex / bison code
> available. Some aspects are a bit crufty (there's some massaging of
> the output of the lexer and parser by a couple of sed & awk scripts:
> icky I know, but it was before my time...) but they might be useful as
> reference points.
I saw references that the parser was available, but wasn't sure how current
it was. :-) But yeah, it couldn't hurt to look! I wrote the HST parser
using Happy, which should use the same kind of grammar as lex/bison —
though I've been thinking about rewriting it using Parsec, so that it
doesn't require a preprocessing step. Anyway, I used Scattergood's thesis
as a starting point — it contains an older version of the lex/bison code,
too. And then I just used black-box testing — if the latest FDR2 accepts
a script, I'd make sure that HST's does, too.
Incidentally, I created a Google group for HST awhile back, which has seen
exactly 0 traffic so far, since I'm the only member. :-) But if we want,
we can migrate some of this discussion over there if we want it to be
archived for posterity. http://groups.google.com/group/hst-project
cheers
–doug