% This file describes the modal formulas for property 5 used in section
% 5.3 of Designing and understanding the behaviour of systems
% by J.F. Groote and M.A. Reniers.

nu X(b1:Bool=false, b2:Bool=true,b3:Bool=true,b4:Bool=true).
   ([isDocked]X(true,b2,b3,b4) &&
    [unlockDock]X(false,b2,b3,b4)&&
    [pressResume]X(b1,true,b3,b4)&&
    [pressStop]X(b1,false,b3,b4)&&
    [atOutermost]X(b1,b2,true,b4)&&
    [motorLeft]X(b1,b2,false,b4)&&
    [motorOff+motorLeft]X(b1,b2,b3,true)&&
    [motorRight]X(b1,b2,b3,false)&&
        (val(b1 && b2 && b3 && b4) => [pressRight]
              mu Y.[!motorRight &&
                    !unlockDock &&
                    !pressStop &&
                    !atOutermost]Y))


