Re design & checking tools

[p0072370 <ireast@xxxxxxxxxxxxx>]

>* 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 
sub-domain.)

Am I missing something here?

Ian


Dr. Ian Robert East
01865 483635
Room T408, Tongue Building
School of Computing and Mathematical Sciences
Oxford Brookes University