INIT colset INIT = int; ACTIVATED colset ACTIVATED = int; INITxACTIVATED INIT ACTIVATED colset INITxACTIVATED = product INIT * ACTIVATED; Standard declarations UNIT colset UNIT = unit; INT BOOL STRING colset STRING = string; INIT n var n : INIT; ACTIVATED x var x : ACTIVATED; BOOL b var b : BOOL; down up END MARKER END MARKER 2`(1,0) 1`(0,1) (1,0) 2`(1,0) 1`(0,1) (1,0) 2`(1,0) 1`(0,1) (1,0) b b b b n n b (n,0) b (n,0) 1`(0,1) 2`(1,0) (1,0) (1,0) (1,0) 1`(0,1) 2`(1,0) 2`(1,0) 1`(0,1) b b b b b b (1,0) (0,1) b b (0,1) (1,0) 1. Random direction choice 0. Initial value Down movement Up movement <same as model> true true false false false true true false false true false false true false true false false true true false false false false false false false false true false true false false true true false false false true false