-- Model generated by BIOCHAM MODULE main VAR R : 0..5; a : boolean; b : boolean; c : boolean; d : boolean; ASSIGN init(R) := 0; next(R) := 1..5; ASSIGN init(a) :=FALSE; next(a) := case R = 0 : TRUE; -- R1. R = 1 : case (a) : {FALSE, TRUE}; 1 : a; esac; -- R2. R = 2 : case (a) : {FALSE, TRUE}; 1 : a; esac; -- R5. R = 5 : case (d) : TRUE; 1 : a; esac; 1 : a; esac; ASSIGN init(b) :=FALSE; next(b) := case R = 0 : FALSE; -- R1. R = 1 : case (a) : TRUE; 1 : b; esac; -- R3. R = 3 : case (b) : {FALSE, TRUE}; 1 : b; esac; 1 : b; esac; ASSIGN init(c) :=FALSE; next(c) := case R = 0 : FALSE; -- R2. R = 2 : case (a) : TRUE; 1 : c; esac; -- R4. R = 4 : case (c) : {FALSE, TRUE}; 1 : c; esac; 1 : c; esac; ASSIGN init(d) :=FALSE; next(d) := case R = 0 : FALSE; -- R3. R = 3 : case (b) : TRUE; 1 : d; esac; -- R4. R = 4 : case (c) : TRUE; 1 : d; esac; -- R5. R = 5 : case (d) : {FALSE, TRUE}; 1 : d; esac; 1 : d; esac;