At 10:00 22/04/99 +0100, Jeremy Martin wrote: >* 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. I rather like the facility available in some languages, such as Ada, Pascal), for both specifying limited-range datatypes and for enumerating them. Things such as: integer i is (10-20) or var i is (green => 2, blue => 4, red => 6) I rather like the syntax Roger and Barry have used in their hardware compiler, and it would allow at least the first of these; it's not hard to imagine ways of including the second too. One benefit of both would be that typical programs stop using loads of int32's or int16's, and start using int3's or uint21's. Although at the level of program checking, an int21 is still an awful lot of states, it is still very many less than an int32. I believe occam should include these things, both because it allows the colpiler to check even more of the program at compile time, and because it avoids some of the need for VAL x IS y: type declarations, and because if we are (as I hope) moving towards formal checking of real programs this is a good thing from that point of view too. Regards, Ruth