init { /* file: stexamp1.promela */
byte i = 0;
do
:: (i< 255) -> i = i+1
:: (i>=255) -> break
od
}