Re: handling infinite state systems
Douglas Creager
> Hi Doug, I'm still far from fully understanding HST, but the LTS of
> the infinite state process P comes as a surprise to me. I'd expect
> that there'd be either some magic that could fold P's LTS to a finite
> one or that HST would either abort building the LTS or run forever. I
> stumbled upon this example because I implemented a naive deadlock
> checking command (derived from your failures-refinement code) that
> searched for empty acceptance sets. I think that P isn't deadlock
> free, but the command claimed that P is deadlock free. Is there
> something wrong in building the LTS or am I missing something?
> I don't know how to create a single patch for the deadlock testing
> code, so this patch contains the tau priority code as well.
Hi Moritz
The recursion model I use deals with "finalized" and "non-finalized"
processes. There's a bit of a description here:
http://hst.github.com/doc/csp0.html
The doc says "limited" support for recursion, but I think that this
setup actually supports any recursive process that FDR supports. I'd
love to hear a contradiction or a proof, though.
Basically, the code does detect the infinite LTS, but doesn't yet error
out when it detects this. If you turn on the HST_CSP_DEBUG macro in
csp.hh, you'll see the error messages. (I've attached the debug output
for your infinite_state CSP script.)
You'll see a couple of "NOT FINALIZED" messages. These should really
throw an error. What it means is that it's encountered a CSP operator
that requires its input to be finalized -- you have to know the full set
of outgoing events in order to create the LTS for the operator. Prefix
is the main operator that *doesn't* require finalized inputs. But while
building up the LTS for your interleave statement, it loops back around
to P (state 2), which hasn't been declared yet. (It can't be until the
interleave has been declared.)
--doug
Philip Armstrong
> [CCing the Google group]
>
Am I supposed to be on the mailing list? Or just the Google group. Anyway...
>> Hi Doug, I'm still far from fully understanding HST, but the LTS of
>> the infinite state process P comes as a surprise to me. I'd expect
>> that there'd be either some magic that could fold P's LTS to a finite
>> one or that HST would either abort building the LTS or run forever. I
>> stumbled upon this example because I implemented a naive deadlock
>> checking command (derived from your failures-refinement code) that
>> searched for empty acceptance sets. I think that P isn't deadlock
>> free, but the command claimed that P is deadlock free. Is there
>> something wrong in building the LTS or am I missing something?
>> I don't know how to create a single patch for the deadlock testing
>> code, so this patch contains the tau priority code as well.
>>
>
NB. If you're going to compare your tau priority code to that in FDR,
then please use the latest pre-release (real release next week assuming
everything beds in): there are some nasty bugs in the (never officially
annouced) tau priority implentation in FDR version 2.83.
> Hi Moritz
>
> The recursion model I use deals with "finalized" and "non-finalized"
> processes. There's a bit of a description here:
>
> http://hst.github.com/doc/csp0.html
>
Sounds a little like a model for a 'symbolic FDR' that I played around
with a while back: never did get an implementation up and running though.
> The doc says "limited" support for recursion, but I think that this
> setup actually supports any recursive process that FDR supports. I'd
> love to hear a contradiction or a proof, though.
>
Certainly FDR falls over on this kind of immediate recursion through |||
The semantics of processes which can offer an infinite number of events
(even if they're all taus) is different to the finite input semantics
IIRC: I can't rember offhand how many of Bill's refinement proofs carry
over into a model which allows such processes. There's probably
something in his book about it somewhere.
> Basically, the code does detect the infinite LTS, but doesn't yet error
> out when it detects this. If you turn on the HST_CSP_DEBUG macro in
> csp.hh, you'll see the error messages. (I've attached the debug output
> for your infinite_state CSP script.)
>
> You'll see a couple of "NOT FINALIZED" messages. These should really
> throw an error. What it means is that it's encountered a CSP operator
> that requires its input to be finalized -- you have to know the full set
> of outgoing events in order to create the LTS for the operator. Prefix
> is the main operator that *doesn't* require finalized inputs. But while
> building up the LTS for your interleave statement, it loops back around
> to P (state 2), which hasn't been declared yet. (It can't be until the
> interleave has been declared.)
>
This is much the same problem that FDR has: it loops around trying to
nail down the implementation of P because the bits it has constructed so
far still depend on P...
Phil
--
Philip Armstrong <philip.a...@comlab.ox.ac.uk>
Research Assistant, Oxford University Computing Laboratory