
NAME
DESCRIPTION
Consider, for instance, the verification problem for a sequential C procedure that computes square roots. Exhaustive statebased verification would clearly be the wrong approach here. For a Promela verification model it often suffices to model such a procedure as a simple twostate process that nondeterministically decides to give either the correct or an incorrect answer. For instance: mtype = { number, correct, incorrect }; chan sqrt = [0] of { mtype, chan }; active proctype sqrt_server() { do :: sqrt?number,answer > /* abstract from local computations */ if :: answer!correct :: answer!incorrect fi od } active proctype user() { chan me = [0] of { mtype }; again: sqrt!number,me; if :: me?correct :: me?incorrect > goto again fi; ... }The data types available in Promela are a compromise between notational convenience and modest constraints that can facilitate the construction of tractable verification models. The largest numeric quantity that can be manipulated is, for instance, a 32bit integer number. The number of different ``states'' that even one single integer variable could obtain, e.g., when used as a simple counter, is well beyond the search space of statebased model checkers. Even integer quantities, therefore, are to be treated with some suspicion in verification models, and can very often advantageously be replaced with byte or bit variables. SEE ALSO
