init { /* file: stexamp1.promela */

byte i = 0;

do

:: (i< 255) -> i = i+1

:: (i>=255) -> break

od

}