%
% specification for simple graphics interaction
%

specification((
    +(((stop->
              keep(not(move))),
       ((start ->
              keep((green,move;not(green),not(move))))),
       next(halt((stop;start;quit)))
    )),
    proj(
        (  length(10),
           ((stable(red),stable(green))&skip)
        ),(
        st(s0),halt(quit)
        )
    )
)).

st_variables([stop,start,quit],[red,green,move]).


st(s0,(green,not(red)),s1).
st(s1,(not(green),red),s0).
st(s0,empty,empty).
st(s1,empty,empty).