```
#lang uclid

var red : boolean;
var green : boolean;

-- initial state
init {
    red := true;
    green := false;
}

-- transitions
next {
    red := case
             red : green;
             green : red;
           esac;
    green := !red;
}

-- safety property: red and green cannot be true at the same time
system red_exclusive {
    ! (red && green);
}
```