[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re design & checking tools
>* This leads us to the point that Bryan made about state-space
> explosion. A single input of an INT32 variable in an Occam process
> would give rise to at least 2^32 states in the equivalent state
> transition system, so we need to apply some sort abstraction
> to reduce the number of states in each constitutent process.
>* This abstraction is difficult to automate - how do we decide how
> much information may be safely thrown away? Some very important work
> in this area has been done by Ranko Lazic (see Bill Roscoe's book:
> The Theory and Practice of Concurrency - Prentice Hall).
>* Much work has also been done regarding state-space compression. I
> wonder if there might not be some kind of higher-level state machine,
> that could be used, where the input of an INT32 variable would only
> require one new state to be added?
Surely this has to do just with degree of abstraction. The only reason
for considering a single state for each state value (eg with an INT32) is
if the process behaves differently with regard to others according to
every distinct case (0, 1 , 2 etc). This is rarely true.
What we can do (as suggested in the last chapter of my little book) is
_partition_ the domain of that INT32 according to process behaviour, and
define a distinct shared event for each sub-domain. This could also be
used in software testing. (Just test using a single input value from each
Am I missing something here?
Dr. Ian Robert East
Room T408, Tongue Building
School of Computing and Mathematical Sciences
Oxford Brookes University